An Instantiation Scheme for Satisfiability Modulo Theories

State-of-the-art theory solvers generally rely on an instantiation of the axioms of the theory, and depending on the solvers, this instantiation is more or less explicit. This paper introduces a generic instantiation scheme for solving SMT problems, along with syntactic criteria to identify the classes of clauses for which it is complete. The instantiation scheme itself is simple to implement, and we have produced an implementation of the syntactic criteria that guarantee a given set of clauses can be safely instantiated. We used our implementation to test the completeness of our scheme for several theories of interest in the SMT community, some of which are listed in the last section of this paper.     

Modular instantiation schemes

Instantiation schemes are proof procedures that test the satisfiability of clause sets by instantiating the variables they contain, and testing the satisfiability of the resulting ground set of clauses. Such schemes have been devised for several theories, including fragments of linear arithmetic or theories of data-structures. In this paper we investigate under what conditions instantiation schemes can be combined to solve satisfiability problems in unions of theories.     

Rewrite-Based Satisfiability Procedures for Recursive Data Structures

If a rewrite-based inference system is guaranteed to terminate on the axioms of a theory and any set of ground literals, then any theorem-proving strategy based on that inference system is a rewrite-based decision procedure for -satisfiability. In this paper, we consider the class of theories defining recursive data structures, that might appear out of reach for this approach, because they are defined by an infinite set of axioms. We overcome this obstacle by designing a problem reduction that allows us to prove a general termination result for all these theories. We also show that the theorem-proving strategy decides satisfiability problems in any combination of these theories with other theories decided by the rewrite-based approach.     

On the Complexity of Deduction Modulo Leaf Permutative Equations

In the context of equational reasoning, J. Avenhaus and D. Plaisted proposed to deal with leaf permutative equations in a uniform, specialized way. The simplicity of these equations and the useless variations that they produce are good incentives to lift theorem proving to so-called stratified terms, in order to perform deduction modulo such equations. This requires specialized algorithms for standard problems involved in automated deduction. To analyze the computational complexity of these problems, we focus on the group theoretic properties of stratified terms. NP-completeness results are given and (slightly) relieved by restrictions on leaf permutative theories, which allow the use of techniques from computational group theory.     

Theory decision by decomposition

The topic of this article is decision procedures for satisfiability modulo theories (SMT) of arbitrary quantifier-free formulæ. We propose an approach that decomposes the formula in such a way that its definitional part, including the theory, can be compiled by a rewrite-based first-order theorem prover, and the residual problem can be decided by an SMT-solver, based on the Davis–Putnam–Logemann–Loveland procedure. The resulting decision by stages mechanism may unite the complementary strengths of first-order provers and SMT-solvers. We demonstrate its practicality by giving decision procedures for the theories of records, integer offsets and arrays, with or without extensionality, and for combinations including such theories.     

Rewrite-Based Decision Procedures

The rewrite-based approach to satisfiability modulo theories consists of using generic theorem-proving strategies for first-order logic with equality. If one can prove that an inference system generates finitely many clauses from the presentation of a theory and a finite set of ground unit clauses, then any fair strategy based on that system can be used as a -satisfiability procedure. In this paper, we introduce a set of sufficient conditions to generalize the entire framework of rewrite-based -satisfiability procedures to rewrite-based -decision procedures. These conditions, collectively termed subterm-inactivity, will allow us to obtain rewrite-based -decision procedures for several theories, namely those of equality with uninterpreted functions, arrays with or without extensionality and two of its extensions, finite sets with extensionality and recursive data structures.     

On leaf permutative theories and occurrence permutation groups

Leaf permutative theories contain variable-permuting equations, so that rewriting a term may lead to an exponential number of terms which are only permutations of it. In [1] Avenhaus and Plaisted propose to represent such sets by stratified terms, and to deduce directly with these. Our aim is to use computational group theory to analyse the complexity of the corresponding problems, and hopefully devise better algorithms than [1]. In order to express stratified sets as orbits, we adopt a representation of terms based on occurrences, which can conveniently be permuted. An algorithm solving a basic equivalence problem is presented.     

On Variable-inactivity and Polynomial Formula-Satisfiability Procedures

Verification problems require to reason in theories of datastructures and fragments of arithmetic. Thus, decision proceduresfor such theories are needed, to be embedded in, or interfacedwith, proof assistants or software model checkers. Such decisionprocedures ought to be sound and complete, to avoid false negativesand false positives, efficient, to handle large problems, andeasy to combine, because most problems involve multiple theories.The rewrite-based approach to decision procedures aims at addressingthese sometimes conflicting issues in a uniform way, by harnessingthe power of general first-order theorem proving. In this article,we generalize the rewrite-based approach from deciding the satisfiabilityof sets of ground literals to deciding that of arbitrary groundformulæ in the theory. Next, we present polynomial rewrite-basedsatisfiability procedures for the theories of records with extensionalityand integer offsets. The generalization of the rewrite-basedapproach to arbitrary ground formulæ and the polynomialsatisfiability procedure for the theory of records with extensionalityuse the same key property—termed variable-inactivity—thatallows one to combine theories in a simple way in the rewrite-basedapproach.