Model-based Theory Combination
Leonardo de Moura, Nikolaj Bjørner · Electronic Notes in Theoretical Computer Science · 2008
Traditional methods for combining theory solvers rely on capabilities of the solvers to produce all implied equalities or a pre-processing step that introduces additional literals into the search space. This paper introduces a combination method that incrementally reconciles models maintained by each theory. We evaluate the practicality and efficiency of this approach.