Adding Decision Procedures to SMT Solvers Using Axioms with Triggers

• Published in: Journal of automated reasoning 2016-04, Vol.56 (4), p.387-457
• Main Authors: Dross, Claire, Conchon, Sylvain, Kanig, Johannes, Paskevich, Andrei
• Format: Article
• Language: English
• Subjects: Annotations; Arrays; Artificial Intelligence; Axioms; Completeness; Computer Science; Decision theory; Handles; Lists; Logic; Logic in Computer Science; Mathematical analysis; Mathematical Logic and Formal Languages; Mathematical Logic and Foundations; Program verification (computers); Searching; Solvers; Stopping; Symbolic and Algebraic Manipulation; Vectors (mathematics)
• ISSN: 0168-7433; 1573-0670
• DOI: 10.1007/s10817-015-9352-2

Satisfiability modulo theories (SMT) solvers are efficient tools to decide the satisfiability of ground formulas, including a number of built-in theories such as congruence, linear arithmetic, arrays, and bit-vectors. Adding a theory to that list requires delving into the implementation details of a given SMT solver, and is done mainly by the developers of the solver itself. For many useful theories, one can alternatively provide a first-order axiomatization. However, in the presence of quantifiers, SMT solvers are incomplete and exhibit unpredictable behavior. Consequently, this approach can not provide us with a complete and terminating treatment of the theory of interest. In this paper, we propose a framework to solve this problem, based on the notion of instantiation patterns , also known as triggers . Triggers are annotations that suggest instances which are more likely to be useful in proof search. They are implemented in all SMT solvers that handle first-order logic and are included in the SMT-LIB format. In our framework, the user provides a theory axiomatization with triggers, along with a proof of completeness and termination properties of this axiomatization, and obtains a sound, complete, and terminating solver for her theory in return. We describe and prove a corresponding extension of the traditional Abstract DPLL Modulo Theory framework. Implementing this mechanism in a given SMT solver requires a one-time development effort. We have implemented the proposed extension in the Alt-Ergo prover and we discuss some implementation details in the paper. To show that our framework can handle complex theories, we prove completeness and termination of a feature-rich axiomatization of doubly-linked lists. Our tests show that our approach results in a better performance of the solver on goals that stem from the verification of programs manipulating doubly-linked lists and sets.