Model-based Theory Combination

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.

• Type: Journal
• Year: 2008
• Where: ENTCS
• Authors: Leonardo Mendonça de Moura, Nikolaj Bjørner
• Keywords: Additional Literals, ENTCS 2008, Theory Solvers, Traditional Methods