RESOLUTE – A Simple Proof Format for SMT-LIB

The SMT-LIB standard defines a command for requesting proofs from solvers, but it does not prescribe how these proofs should be represented. Different solvers therefore use different proof formats.

RESOLUTE is the proof format used by SMTInterpol. It is a low-level, resolution-based format designed to be simple, explicit, and easy to check. Proofs are represented as S-expressions and closely follow SMT-LIB syntax wherever possible.

RESOLUTE proofs use the resolution rule to derive the empty clause from the asserted formulas in the input and a fixed set of axioms for logical and theory reasoning. The format is intentionally minimal: complex reasoning is reduced to resolution steps over explicitly stated axioms.

We have a proof checker for these proofs.

Resolution proofs

A RESOLUTE proof is given as a tree of subproofs. Each subproof establishes the validity of a clause. A clause is a set of literals and semantically represents the disjunction of these literals. A literal is a positive or negative atom and an atom is a Boolean SMT-LIB term, in other words, an SMT-LIB formula.

We use + t to denote the positive literal for the term t and - t for the negative literal. A clause is denoted by an S-expression ( +/- t1 ... +/- tn ). As usual, a positive literal represents the fact that the term is true, a negative literal that the term is false, and a clause represents the fact that at least one of its literals holds.

A resolution proof is a proof of the unsatisfiability of an SMT-LIB input script. It is given as a proof tree proving the empty clause, where the internal nodes of the proof tree apply the resolution rule and the leaves of the tree are the assumptions from the SMT-LIB input script and logical or theory-specific axioms.

Resolution Rule

The only inference rule in RESOLUTE is binary resolution. If proof1 proves a clause $C_1$ and proof2 proves a clause $C_2$, then the resolution with the pivot $t$ produces a proof of the clause $(C_1\setminus \{+t\}) \cup (C_2\setminus\{-t\})$ where the complementary literals $+ t$ and $- t$ are removed from the respective clauses. The resolution step is written as (res t proof1 proof2). Clauses are treated as sets of literals; therefore, literals occurring in both $C_1$ and $C_2$ occur only once in the conclusion. Strictly speaking, the resolution rule is sound even when the clauses $C_1$ and $C_2$ do not contain the pivot literal; however, the proof checker will issue a warning in that case.

Assumptions

Each input formula denoted by (assert t) in the SMT-LIB benchmark can be used as an assumption in the proof. The assumption is denoted by the S-expression (assume t) and proves the unit clause ( + t ). Assumptions together with axioms form the leaves of the proof tree.

Axioms

In addition to assumptions, RESOLUTE uses a fixed collection of axioms that encode the semantics of logical operators and background theories.

Each axiom is represented as a clause that is universally valid. These axioms serve as the basic building blocks from which all reasoning is derived. An axiom is written as a proof term (axiom-name parameter …) that proves a tautological clause.

In particular, the core theory defines the axioms for the logical operators. As an example, the axiom (or+ 1 (or t0 t1 t2)) where t0, t1, and t2 are arbitrary terms is a proof for the valid clause ( +(or t0 t1 t2) - t1 ).

Axioms for core theory

The meaning of logical operators is expressed by a set of core axioms that are available in every SMT-LIB theory. The axioms explicitly support associative SMT-LIB operators like and, or, => with more than two arguments.

The following block is a schematic summary; the precise axioms are given in “Core Axioms” below. Axioms are written as axiom-name: (clause).

; logical operators
true+: ( + true )                      false-: ( - false )
 not+: ( +(not p0) + p0 )                not-: ( -(not p0) - p0 )
 and+: ( +(and p0 … pn) - p0 … - pn )    and-: ( -(and p0 … pn) + pi )
  or+: ( +(or p0 … pn) - pi )             or-: ( -(or p0 … pn) + p0 … + pn )
  =>+: ( +(=> p0 … pn) +/- pi )           =>-: ( -(=> p0 … pn) - p0 … + pn )
  =+1: ( +(= p0 p1) + p0 + p1 )           =-1: ( -(= p0 p1) + p0 - p1 )
  =+2: ( +(= p0 p1) - p0 - p1 )           =-2: ( -(= p0 p1) - p0 + p1 )
 xor+: ( +(xor l1) +(xor l2) -(xor l3) ) xor-: ( -(xor l1) -(xor l2) -(xor l3) )
    where each term in l1,l2,l3 occurs an even number of times.

; quantifiers
  forall+: ( +(forall (x) (F x)) -(F (choose (x) (F x))) )
  forall-: ( -(forall (x) (F x)) +(F t) )
  exists+: ( +(exists (x) (F x)) -(F t) )
  exists-: ( -(exists (x) (F x)) +(F (choose (x) (F x))) )

; equality axioms
     refl: ( +(= t t) )                  symm: ( +(= t0 t1) -(= t1 t0) )
    trans: ( +(= t0 tn) -(= t0 t1) … -(= tn-1 tn) )
     cong: ( +(= (f t0 … tn) (f t'0 … t'n)) -(= t0 t'0) … -(= tn t'n) )
       =+: ( +(= t0 … tn) -(= t0 t1) … -(= tn-1 tn) )
       =-: ( -(= t0 … tn) +(= ti tj) )
distinct+: ( +(distinct t0 … tn) +(= t0 t1) … +(= t0 tn) … +(= tn-1 tn) )
distinct-: ( -(distinct t0 … tn) -(= ti tj) )   where i != j

; ite, define-fun, annotations
  ite1: ( +(= (ite t0 t1 t2) t1) - t0 )  ite2: ( +(= (ite t0 t1 t2) t2) + t0 )
  del!: ( +(= (! t :annotation…) t) )
expand: ( +(= (f t0 … tn) (let ((x0 t0)…(xn tn)) d)) )
   where f is defined by (define-fun f ((x0 τ0)…(xn τn)) τ d)

A detailed explanation of the axioms will be given in the section “Core Axioms” below.

Syntactic extensions

Conceptually a resolution proof is just a huge proof term applying the resolution rule res to axioms and assumptions. However, there are a few important extensions to concisely express large proofs.

let terms

A large proof may use the same large term multiple times. These large terms can be shared between different clauses in the proof. To express proofs in a concise manner, we support the let syntax from SMT-LIB to bind terms to variables. Such let terms are seen as syntactic sugar and are equal to their expanded form, i.e., no proof rule is required to expand a let. In particular, the resolution rule will also remove the pivot literal from the proved clause if the pivot terms are only identical after let expansion.

To bind a proof to a variable, the let-proof keyword is used with the same syntax as let. This can be used to avoid repeating the same subproof multiple times. This proof variable may then be used wherever a proof is expected, e.g., as arguments of the resolution rule.

The let-proof syntax is also useful for expressing the proofs in a linear form. A solver may choose to print its proof incrementally by binding each learned clause to a variable until the empty clause is derived:

(let-proof ((C1 (assume …)))
(let-proof ((C2 (res … C1 …)))
…
 C100 ; empty clause
)…)

Function definitions

The proof format also supports custom defined functions that are only used inside the proof. This is useful for auxiliary functions that are created by Skolemization or by CNF conversion of quantified formulas. The syntax for this is ((define-fun f ((x0 τ0)…(xn τn)) d) subproof) where subproof may use the function symbol f and the cong and expand axioms for this function symbol.

Extended resolution

The proof calculus trivially supports extended resolution, where a fresh atom p is introduced that represents (and p0 p1) and the three clauses ( - p0 - p1 + p ), ( - p + p0 ), and ( - p + p1 ) are added. This is facilitated by the let syntax and the axioms for logical operators as follows:

(let ((p (and p0 p1)))
  (let-proof ((C1 (and+ p))
              (C2 (and- 0 p))
              (C3 (and- 1 p)))
    …))

Resolution proofs are usually only refutation complete, i.e., they can prove the empty clause if the conjunction of the input clauses is unsatisfiable. However, the addition of the core axioms makes the calculus complete in the sense that for every valid SMT-LIB formula t there is a proof that proves the unit clause ( + t ).

The proof calculus does not support RUP proofs directly. They need to be converted to applications of res by explicitly listing the clauses and pivot term used in the unit propagation subproof. More importantly, DRAT proofs are not supported and there is no syntax for deleting clauses. Instead they need to be converted to extended resolution (which blows up the proof quadratically). On the other hand, this simplifies the proof checker, which would otherwise need to rediscover the necessary clauses and subproofs.

Example Proof: eq-diamond2

We give an example proof of the following simple benchmark from the SMT-LIB benchmark library.

(set-option :produce-proofs true)
(set-logic QF_UF)
(declare-sort U 0)
(declare-fun x0 () U)
(declare-fun y0 () U)
(declare-fun z0 () U)
(declare-fun x1 () U)
(declare-fun y1 () U)
(declare-fun z1 () U)
(assert (and (or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1))) (not (= x0 x1))))
(check-sat)
(get-proof)

A valid output for this benchmark would be the following.

unsat
(let ((t1 (= x0 y0))
      (t2 (= y0 x1))
      (t3 (= x0 z0))
      (t4 (= z0 x1))
      (t5 (= x0 x1)))
(let ((t6 (and t1 t2))
      (t7 (and t3 t4))
      (t8 (not t5)))
(let ((t9 (or t6 t7)))
(let ((t10 (and t9 t8)))
(let-proof ((C0 (assume t10)))
(let-proof ((C1 (res t9 (res t10 C0 (and- 0 t10)) (or- t9))))
(let-proof ((C2 (res t8 (res t10 C0 (and- 1 t10)) (not- t8))))
(let-proof ((C3 (and- 0 t6)))
(let-proof ((C4 (and- 1 t6)))
(let-proof ((C5 (and- 0 t7)))
(let-proof ((C6 (and- 1 t7)))
(let-proof ((C7 (res t5 (res t1 C3 (res t2 C4 (trans x0 y0 x1))) C2)))
    (res t5 (res t6 (res t7 C1 (res t4 C6 (res t3 C5 (trans x0 z0 x1)))) C7) C2)
))))))))))))

As mentioned earlier, the proof follows mostly the syntax of SMT-LIB terms. In particular, it uses let and let-proof to bind terms and subproofs to variables. We now explain how such a proof can be constructed.

Introducing names for subterms

The first ten lines define names for the subterms of the formula from bottom-up. Note that t10 is the asserted formula in the input file (after expanding let bindings). It is not required to introduce an identifier for every subterm, but doing so helps keep the proof small.

CNF conversion

Then C0 is defined, which is an input clause. Using the assume rule, an input clause can be proved as a unit clause. As usual, a clause is a list of literals, which are atoms with positive or negative polarity. In our proof calculus, the atoms are SMT-LIB terms of type Boolean. Thus, the input formula is represented by a unit clause containing one positive atom that is the asserted term.

Every proof rule produces a proof of a clause. The assume rule produces the proof that the unit clause ( + t10 ) holds. Clauses are written by listing the literals in parentheses and the + indicates that the literal has positive polarity. This proof is then assigned to the variable C0 so it can be referenced in later proofs.

The next step is to convert the input formula into CNF. We use C1–C7 for the clauses resulting from the conversion (or more precisely, they are the proofs of the clauses of the CNF). Let us look at how this is done. The input formula t10 is

(and (or t6 t7) (not t5))

Thus, we want to split it into C1: ( + t6 + t7 ) and C2: ( - t5 ). To split the and formula, we use the and- elimination rule. In this example the axiom (and- 0 t10) is used to prove t9 from t10. Note that t10 is just an abbreviation for (and t9 t8) and that t9 is the argument at index 0. So the axiom (and- 0 t10) proves the tautology clause ( - t10 + t9 ), which states that t10 implies t9. By resolving this clause with the input formula t10, we get a proof of t9. The resolution is written as (res t10 C0 (and- 0 t10)), where t10 is the pivot literal, C0 is a proof of a clause containing it positively, and (and- 0 t10) a proof containing it negatively. The result is a proof for ( + t9 ).

The next step is to eliminate (or t6 t7), that is t9, using the or- elimination rule. The axiom (or- t9) proves the tautology clause ( - t9 + t6 + t7 ). Resolving it with the previous proof on the pivot t9, we obtain C1 which is a proof of ( + t6 + t7 ).

(let-proof ((C1 (res t9 (res t10 C0 (and- 0 t10)) (or- t9))))

Similarly we use the other and- elimination rule (and- 1 t10) and the not- elimination rule (not- t8) to obtain from C0 the clause C2 that proves ( - t5 ).

(let-proof ((C2 (res t8 (res t10 C0 (and- 1 t10)) (not- t8))))

Furthermore, we add the clauses of the Plaisted–Greenbaum encoding C3–C6. These clauses are simply the and- elimination clauses, but this time applied to (and t1 t2) and (and t3 t4). This gives us the full CNF of the input:

C1: ( + t6 + t7 )
C2: ( - t5 )
C3: ( - t6 + t1 )
C4: ( - t6 + t2 )
C5: ( - t7 + t3 )
C6: ( - t7 + t4 )

SMT solving

The only unit clause C2 propagates - t5. We assume the DPLL engine now decides the literal + t6 and propagates + t1 and + t2 by unit propagation. Then the theory solver finds the conflict involving transitivity:

(trans x0 y0 x1): ( - t1 - t2 + t5 )

By definition t1 is (= x0 y0), t2 is (= y0 x1) and t5 is (= x0 x1), so the transitivity axiom for x0 = y0 = x1 has exactly this form.

CDCL now explains the conflict, yielding C7: ( - t6 )

(let-proof ((C7 (res t5 (res t2 C4 (res t1 C3 (trans x0 y0 x1))) C2)))

Now unit propagation derives - t6, + t7, + t3, and + t4, and again a theory conflict is found:

(trans x0 z0 x1): ( - t3 - t4 + t5 )

The explanation of this conflict yields the empty clause:

(res t5 (res t6 (res t7 C1 (res t4 C6 (res t3 C5 (trans x0 z0 x1)))) C7) C2)

This concludes the proof.

Grammar

The grammar for proofs builds on the grammar for ⟨numeral⟩, ⟨term⟩, ⟨sort⟩, ⟨symbol⟩, ⟨sorted_var⟩, and ⟨attribute⟩ from the SMT-LIB standard, version 2.6. It is given below:

⟨term_or_proof⟩ ::= ⟨term⟩ | ⟨proof⟩
⟨polarity⟩ ::= + | -
⟨literal⟩ ::= ⟨polarity⟩ ⟨term⟩
⟨clause⟩ ::= ( ⟨literal⟩ ⃰ )
⟨proof⟩ ::= (res ⟨term⟩ ⟨proof⟩ ⟨proof⟩)
          | (let ((⟨symbol⟩ ⟨term⟩)⁺) ⟨proof⟩)
          | (let-proof ((⟨symbol⟩ ⟨proof⟩)⁺) ⟨proof⟩)
          | ⟨symbol⟩
          | ((define-fun ⟨symbol⟩ (⟨sorted_var⟩⁺) ⟨sort⟩ ⟨term⟩) ⟨proof⟩)
          | ((declare-fun ⟨symbol⟩ (⟨sort⟩⁺) ⟨sort⟩) ⟨proof⟩)
          | ((refine-fun ⟨symbol⟩ (⟨sorted_var⟩⁺) ⟨sort⟩ ⟨term⟩) ⟨proof⟩)
          | (assume ⟨term⟩)
          | (oracle ⟨clause⟩ ⟨attribute⟩ ⃰)
          | ⟨core-axiom⟩
          | ⟨arith-axiom⟩
          | ⟨datatype-axiom⟩
          | ⟨bitvector-axiom⟩

As mentioned earlier, an atom is an SMT-LIB term. A literal is a term with a polarity + or -. A clause is a set of literals, written as a sequence enclosed in parentheses.

Every proof proves a clause. The proof produced by an SMT solver should prove the empty clause. A proof may be constructed from subproofs. For this purpose, a subproof may be bound to a symbol, so that it can be reused efficiently.

The rule (res t p1 p2) is the resolution rule, the main workhorse of this proof format. Here p1 is a proof of some clause $C_1$ and p2 is a proof of $C_2$. The resulting proof term proves the clause $(C_1\setminus \{+ t\}) \cup (C_2\setminus\{- t\})$. The order of p1 and p2 is important: $C_1$ should contain the positive pivot literal, and $C_2$ the negative one. The proof checker warns if the pivot literal does not occur in the corresponding clause but still accepts the proof.

The let binder let ((x t)) p binds the value of t to a symbol x. Here t can be an arbitrary term. The symbol x can then be used in terms as a free variable. Similarly, the let binder let-proof ((x p1)) p binds a proof p1 to the variable x and x can be referenced in p using the ⟨symbol⟩ rule. The scope of x is the proof p and the resulting proof proves the same clause as p.

Proofs can also contain a define-fun declaration with the same syntax as in SMT-LIB. This defines a function symbol for the subproof, which may use the definition via the expand axiom. The defined function symbol must not be used outside the subproof. Similarly, declare-fun introduces an uninterpreted function symbol.

There is also a refine-fun declaration which adds a function definition to an already declared function. It is only allowed at the outermost level of a satisfiability proof and is used to fix the model for an uninterpreted function occurring in the benchmark.

The rule (assume t) proves the unit clause ( + t ). Its side condition (checked by the proof checker) is that t was asserted in the input problem by an SMT-LIB assert command.

The oracle rule can be used to introduce clauses that cannot be easily explained. It should be used as a last resort if a full low-level proof is too tedious or if the axioms for the theory are missing. The proof checker allows any oracle clause but will warn about these clauses.

The remaining rules correspond to the logical and theory axioms of the proof format. Each of them creates a tautological clause. They are given in the next section.

Core Axioms

The core axioms are ⟨proof⟩ objects that prove tautologies. They are usually parametrized by ⟨term⟩ objects. We distinguish the following categories.

Logical axioms – elimination and introduction

For every logical operator we have the usual elimination and introduction rules. In our calculus they take the form of a clause where the premises have negative polarity and the conclusion has positive polarity. They are also identical to the clauses produced by Tseitin encoding. The following lists the axioms and the corresponding clause proved by each axiom. In this list t, t0, … denote terms, n, i, j denote numerals. The elimination rules are indicated by - and the introduction rules by +.

⟨core-axiom⟩ ::=
 | (false-)               ;( - false )
 | (true+)                ;( + true )
 | (not+ (not t))         ;( +(not t) + t )
 | (not- (not t))         ;( -(not t) - t )
 | (and+ (and t0 … tn))   ;( +(and t0 … tn) - t0 … - tn )
 | (and- i (and t0 … tn)) ;( -(and t0 … tn) + ti )       (for 0 <= i <= n)
 | (or+ i (or t0 … tn))   ;( +(or t0 … tn) - ti )        (for 0 <= i <= n)
 | (or- (or t0 … tn))     ;( -(or t0 … tn) + t0 … + tn )
 | (=>+ i (=> t0 … tn))   ;( +(=> t0 … tn) + ti )        (for 0 <= i < n)
 | (=>+ n (=> t0 … tn))   ;( +(=> t0 … tn) - tn )
 | (=>- (=> t0 … tn))     ;( -(=> t0 … tn) - t0 … - tn-1 + tn )
 | (=+1 (= t0 t1))        ;( +(= t0 t1) + t0 + t1 )      (only for Boolean t0/t1)
 | (=+2 (= t0 t1))        ;( +(= t0 t1) - t0 - t1 )      (only for Boolean t0/t1)
 | (=-1 (= t0 t1))        ;( -(= t0 t1) + t0 - t1 )      (only for Boolean t0/t1)
 | (=-2 (= t0 t1))        ;( -(= t0 t1) - t0 + t1 )      (only for Boolean t0/t1)
 | …                      ;;; see next section

Equality rules

We support the usual axioms of reflexivity, symmetry, transitivity (with arbitrarily long chains), and congruence:

⟨core-axiom⟩ ::= …
 | (refl t):              ;( +(= t t) )
 | (symm t0 t1):          ;( +(= t0 t1) -(= t1 t0) )
 | (trans t0 … tn):       ;( +(= t0 tn) -(= t0 t1) … -(= tn-1 tn) )  (for n >= 2)
 | (cong (f t0 … tn) (f t'0 … t'n))
                       ;( +(= (f t0 … tn) (f t'0 … t'n))
                       ;  -(= t0 t'0) … -(= tn t'n))

Additionally we have elimination and introduction rules for equality chains and for distinct:

⟨core-axiom⟩ ::= …
 | (=+ (= t0 … tn)):              ;( +(= t0 … tn) -(= t0 t1) … -(= tn-1 tn))
 | (=- i j (= t0 … tn)):          ;( -(= t0 … tn) +(= ti tj))
 | (distinct+ (distinct t0 … tn)) ;( +(distinct t0 … tn)
                                  ;  +(= t0 t1) … +(= t0 tn)
                                  ;  +(= t1 t2) … +(= t2 tn)…
                                  ;  +(= tn-1 tn))
              ; Note that these are the pairwise equalities (= ti tj) for i < j.
 | (distinct- i j (distinct t0 … tn)); ( -(distinct t0 … tn) -(= ti tj))      (for i != j)

The rules containing i,j have the implicit constraint 0 <= i <= n, 0 <= j <= n. For = we have n >= 2. For distinct we have n >= 1.

ite rules

To support ite terms, we have two simple axioms (t0 is the condition).

⟨core-axiom⟩ ::= …
 | (ite1 (ite t0 t1 t2))   ;( - t0 +(= (ite t0 t1 t2) t1) )
 | (ite2 (ite t0 t1 t2))   ;( + t0 +(= (ite t0 t1 t2) t2) )

xor rules

For efficient xor reasoning we allow arbitrary splitting and reordering of the xor arguments between three xor terms. The rules are

⟨core-axiom⟩ ::= …
 | (xor+ (t̅0) (t̅1) (t̅2))   ;( +(xor t̅0) +(xor t̅1) -(xor t̅2) )
 | (xor- (t̅0) (t̅1) (t̅2))   ;( -(xor t̅0) -(xor t̅1) -(xor t̅2) )

where t̅0, t̅1, t̅2 are three non-empty sequences of terms that in total contain each term an even number of times. Furthermore, if one of the sequences t̅i consists of only a single term ti then the clause contains the atom ti instead of the corresponding xor term. For example:

(xor+ (t0 t1 t2) (t1) (t2 t0)): ( +(xor t0 t1 t2) + t1 -(xor t2 t0) )
(xor- (t t) (t t) (t t)):       ( -(xor t t) )

Note that the last rule uses the fact that a clause is a set of literals, so multiple occurrences of literals are implicitly removed.

Quantifier instantiation and Skolemization

The rules for quantifier introduction and elimination bind the quantified variables either to an arbitrary term or via the choose operator (the Hilbert epsilon operator).

⟨core-axiom⟩ ::= …
 | (forall+ (forall ((x0 X0) … (xn Xn)) F))
    ;( +(forall ((x0 X0) … (xn Xn)) F)
    ;  -(let ((x0 (choose (x0 X0) (not (forall ((x1… xn Xn)) F)))))
    ;    (let ((x1 (choose (x1 X1) (not (forall ((x2… xn Xn)) F)))))
    ;     …
    ;     (let ((xn (choose (xn Xn)) (not F))) F)..)) )
 | (forall- (t0 … tn) (forall ((x0 X0) … (xn Xn)) F)):
    ;( -(forall ((x0 X0) … (xn Xn)) F) +(let ((x0 t0) … (xn tn)) F) )
 | (exists+ (t0 … tn) (exists ((x0 X0) … (xn Xn)) F)):
    ;( +(exists ((x0 X0) … (xn Xn)) F) -(let ((x0 t0) … (xn tn)) F) )
 | (exists- (exists ((x0 X0) … (xn Xn)) F))
    ;( -(exists ((x0 X0) … (xn Xn)) F)
    ;  +(let ((x0 (choose (x0 X0) (exists ((x1… xn Xn)) F))))
    ;    (let ((x1 (choose (x1 X1) (exists ((x2… xn Xn)) F))))
    ;     …
    ;      (let ((xn (choose (xn Xn)) F)) F)…)) )

In forall- and exists+, ti has to be a term of sort Xi.

Miscellaneous rules

For every symbol defined by define-fun (either in the proof or in the benchmark), we have a rule that expands the function definition. Assume f is defined as

(define-fun f ((x0 X0) … (xn Xn)) X t)

then the expand rule for f is

⟨core-axiom⟩ ::= …
 | (expand (f t0 … tn)) ;( +(= (f t0 … tn) (let ((x0 t0) … (xn tn)) t)))

Note that the :named attribute is implicitly expanded to define-fun according to the standard and therefore the expand rule can also be used for named terms.

For some internal functions, the expand rule is also applicable. For every function with the LEFTASSOC, RIGHTASSOC, CHAINABLE, or PAIRWISE attribute and more than two arguments, expand applies the transformation given by the SMT-LIB standard, e.g.:

(expand (or t0 … tn)): ( +(= (or t0 … tn)
                              (or … (or t0 t1) … tn)))
(expand (=> t0 … tn)): ( +(= (=> t0 … tn)
                              (=> t0 … (=> tn-1 tn) … )))
(expand (< t0 … tn)):  ( +(= (< t0 … tn)
                              (and (< t0 t1) … (< tn-1 tn))))

Theories have their own expand rules for some of the theory functions, like abs or (_ divisible k). These are listed in the section describing the theory extensions.

We also have a simple rule to delete attributes from input terms:

⟨core-axiom⟩ ::= …
 | (del! t :attributes…)  ;( +(= (! t :attributes…) t) )

Equality between terms

A proof calculus needs to define which terms are intrinsically equal. This equality relation needs to be decidable, but it should also be simple for efficient implementation of proof checkers. To ensure consensus on when a proof is correct, we need to formally define this intrinsic equality.

Equality is used by the proof checker in two places. The first is for the side condition of the assume rule, which requires that the assumed term be equal to a formula asserted in the input problem. The second is for the set operations in the resolution rule, which remove the pivot literal from the clauses and eliminate duplicated elements in the resolvent.

In type theory, equality is usually defined by α-, β-, δ-, … reductions. Here we define our own reduction rules in the form of a rewrite system. Two terms are equal if they are rewritten to the same canonical term.

The rules are

x → t                where x in the current context is bound to t by a let
(let (...) t) → t    where t contains no variable bound by let
|symbol| → symbol    where symbol is a valid SMT-LIB symbol
numeral → numeral.0  only for LRA/NRA logics where numeral has sort Real

Discussion

The above rules are minimal to keep the canonicalization of terms simple. The let rules are necessary for efficient proof representation. The |symbol| rule should help solvers whose internal representation may not differentiate between quoted and unquoted terms.

The last rule for numeral is only used for matching the input formula of the benchmark with the asserted formula in the proof. It is necessary because, when bitvectors are present, a proof is parsed as a term in the logic LIRA, since our bitvector rules use integers. This means that every ⟨numeral⟩ in the input formula must be written as the corresponding ⟨decimal⟩ in the proof.

Note that any change to these rules can make existing proofs invalid. If new rules are added, this may cause resolution steps to become superfluous and produce a warning that the pivot literal was not found in the antecedent clause. This could be solved by making the resolution rule more lenient, but such a change would make debugging faulty proofs much harder, since then only the final emptiness check for the proved clause would fail.

Clashing variable names

For the rewrite system above, variable names can clash. As an example, consider the following term.

(exists ((x Int)) (let ((y x)) (exists (x Int) (not (= x y)))))

When rewriting the above term using the let rules and replacing y by its definition x, the proof validator needs to remember that x refers to the variable bound by the outer quantifier and not to the inner one. In particular, the above term is not equal (not even equivalent) to the term

(exists ((x Int)) (exists (x Int) (not (= x x))))

Instead the term could be represented by

(exists ((x₁ Int)) (exists (x₂ Int) (not (= x₂ x₁))))

Extensions for other theories

When adding more theories, we need to add more axioms to support these theories. Here we list the axioms for the theories that SMTInterpol supports.

Array Theory

We add the McCarthy axioms and an axiom for extensionality. We choose the axiom with an explicit @diff operator that returns an index witnessing a difference between two arrays.

⟨array-axiom⟩ ::=
 | (selectstore1 a i v)   ;( +(= (select (store a i v) i) v) )
 | (selectstore2 a i j v) ;( +(= (select (store a i v) j) (select a j)) +(= i j) )
 | (extdiff a b)          ;( +(= a b) -(= (select a (@diff a b)) (select b (@diff a b))) )

To support const arrays, one additional axiom is needed:

 | (const v i)            ;( +(= (select (@const v) i) v) )

Arithmetic

For arithmetic we need to manipulate polynomials. Polynomials are represented by an SMT-LIB term of the following form.

  (+ (* c1 t11 … t1m) … (* cn tn1 … tnm))

Here c1, …, cn are constants (⟨numeral⟩, ⟨decimal⟩, or integer/real numbers in canonical form). All (ti1 … tim) are different multisets, and the head symbol of tij is not + or *. All ci, tij have the same type (Real or Int). The constant ci may be omitted if it is 1, except if there are no other terms in the monomial. The operators * and + are omitted if they have only one argument. The zero polynomial is represented by 0.

When multiplying polynomials or adding them together, the usual rules of distributivity, commutativity, and associativity are applied to bring them into the above normal form again.

We have four rules that manipulate these polynomials. The first two perform polynomial addition and multiplication:

⟨arith-axiom⟩ ::=
 | (poly+ (+ a1 … an) a):  ;( +(= (+ a1 … an) a) )  where a1+…+an = a
 | (poly* (* a1 … an) a):  ;( +(= (* a1 … an) a) )  where a1*…*an = a
 | …

Here a1, …, an, a are polynomials. The side-condition a1+…+an=a states that adding the polynomial a1, …, an yields a polynomial equal to a, i.e., it has the same monomials with the same coefficients, but may differ in term order. Similarly for a1*…*an=a.

Then we have one rule for to_real:

⟨arith-axiom⟩ ::= …
 | (to_real-def a)  ;( +(= (to_real a) a') )

where a is a polynomial (+ … (* ci … tij …)) with integer coefficients and terms and a' is the polynomial (+ … (* ci' … (to_real tij) …)) where ci' is the real representation of the integer ci, i.e., an integer NUM is replaced with NUM.0 and (- NUM) is replaced with (- NUM.0). Every other term t is replaced by (to_real t).

The heart of the proof system is the following rule proving the inconsistency of a set of inequalities by using Farkas’ Lemma. (Note that this is only complete for linear arithmetic).

⟨arith-axiom⟩ ::= …
 | (farkas c1 (<=? a1 b1) … cn (<=? an bn)): ( -(<=? a1 b1) … -(<=? an bn) )

where ci are positive integers, <=? stands for <, <=, or =, ai, bi are polynomials. The weighted sum of these polynomials, c1*(a1-b1) + … + cn*(an-bn) is a (rational or integer) constant c where c >= 0. If c = 0, then at least one inequality must be strict. If some inequalities are over Int and some are over Real, all inequalities are implicitly converted to Real by converting all coefficients in ai/bi to real constants and replacing all terms t in ai/bi with (to_real t).

The remaining axioms work with arbitrary terms and do not require adding or multiplying polynomials:

⟨arith-axiom⟩ ::= …
 | (trichotomy a b)   ;( +(< a b) +(= a b) +(< b a) )
 | (total a b)        ;( +(<= a b) +(< b a) )

The only side condition is that the terms in the clause type check. For integer reasoning we use the following axiom that states that there is no number between c and c+1:

⟨arith-axiom⟩ ::= …
 | (total-int a c)    ;( +(<= a c) +(<= (c+1) a) )

where c is an integer constant (NUMERAL or negated NUMERAL) and (c+1) is the SMT-LIB representation of that constant plus one. The term a is an arbitrary term of sort Int. Note: an alternative would be to restrict the axiom to c = 0; i.e., (total-int a) proves ( +(<= a 0) +(<= 1 a) )

Also we need the following axioms for handling division and modulo. The rules are for the theories that contain the corresponding function symbols. Note that these rules are syntactic. No polynomial normalization is performed in these rules.

⟨arith-axiom⟩ ::= …
 | (/def a b1 … bn)  ;( +(= a (* b1 … bn (/ a b1 … bn))) +(= b1 0) … +(= bn 0) )
 | (div-low x d):    ;( +(<= (* d (div x d)) x) +(= d 0) )
 | (div-high x d):   ;( +(< x (+ (* d (div x d)) (abs d))) +(= d 0) )
 | (mod-def x d):    ;( +(= (mod x d) (- x (* d (div x d)))) +(= d 0) )
 | (to_int-low x):   ;( +(<= (to_real (to_int x)) x) )
 | (to_int-high x):  ;( +(< x (+ (to_real (to_int x)) 1.0)) )

In addition to the axioms above, we also add new definitions for the expand axioms. These are given in the following table:

(define-fun - ((x Int)) Int (* (- 1) x))
(define-fun - ((x Real)) Real (* (- 1) x))
(define-fun - ((x Int) (y Int)) Int (+ x (* (- 1) y)))
(define-fun - ((x Real) (y Real)) Real (+ x (* (- 1.0) y)))
(define-fun > ((x Int) (y Int)) Bool (< y x))
(define-fun > ((x Real) (y Real)) Bool (< y x))
(define-fun >= ((x Int) (y Int)) Bool (<= y x))
(define-fun >= ((x Real) (y Real)) Bool (<= y x))
(define-fun abs ((x Int)) Int (ite (< x 0) (- x) x))
(define-fun abs ((x Real)) Real (ite (< x 0) (- x) x))
(define-fun (_ divisible c) ((x Int)) Bool (= x (* c (div x c))))
(define-fun is_int ((x Real)) Bool (= x (to_real (to_int x))))

The other proof rules do not use the symbols -, /, >=, >. A solver should first rewrite them using these definitions and then only work with <=, <, *, +. Note that in (divisible-def c x) the constant c must be a positive numeral larger than zero, to make the term ((_ divisible c) x) syntactically correct.

Also for every internal binary function in LIRA that takes two reals, we define corresponding functions that take a mix of Int and Real arguments and cast all integer arguments to Real. This is supported by the expand rule and works even if the function is used with more than two arguments. As an example, for (+ i0 r1 i2 r3) where i0, i2 are terms of sort Int and r1, r3 are terms of sort Real, the expand axiom looks like:

(expand (+ i0 r1 i2 r3)): ( +(= (+ i0 r1 i2 r3)
                                (+ (to_real i0) r1 (to_real i2) r3)))

Note that the axiom farkas is the only axiom with negated literals. It can be used in a resolution proof to rewrite a positive literal into an equivalent negated literal. On the other hand, the axiom total and total-int can be used to rewrite a negated literal into the equivalent positive literal.

Data Types

For reasoning about data types, the following rules are used:

⟨datatype-axiom⟩ ::= …
 | (dt_project seli a1 … an)       ;( +(= (seli (cons a1 … an)) ai) )
 | (dt_cons cons x)                ;( -((_ is cons) x) +(= (cons (sel1 x) … (seln x)) x) )
 | (dt_test cons (cons a1 … an))   ;( +((_ is cons) (cons a1 … an)) )
 | (dt_test cons' (cons a1 … an))  ;( -((_ is cons') (cons a1 … an)) )
 | (dt_exhaust x)                  ;( +((_ is cons1) x) … +((_ is consn) x) )
 | (dt_acyclic (cons …(cons… x …)…) x) ;( -(= (cons …(cons… x …)…) x) )
   ; where (cons …(cons… x …)…) is a term containing x, and around x
   ; only constructor functions appear.
 | (dt_match (match t …))
   ;( +(= (match t ((p1 x1) c1) …) (ite ((_ is p1) t) (let ((x1 (sel1 t))) c1) …)) )

Bitvectors

The idea is to translate bitvectors into integer arithmetic. We use the new functions ubv_to_int and int_to_bv introduced in SMT-LIB version 2.7 to convert between integers and bitvectors.

We have the following correspondences:

⟨bitvector-axiom⟩ ::=
 | (int2ubv2int k t0)  ;( +(= (ubv_to_int ((_ int_to_bv k) t0)) (mod t0 2^k)) )
 | (int2sbv2int k t0)  ;( +(= (sbv_to_int ((_ int_to_bv k) t0)) (+ (mod (+ t0 2^(k-1)) 2^k) (- 2^(k-1)))) )
 | (ubv2int2bv t0)     ;( +(= ((_ int_to_bv k) (ubv_to_int t0)) t0) )
                       ; where t0 is of sort (_ BitVec k)

In these axioms 2^k, 2^(k-1) stand for the corresponding numerals, e.g., for $k=3$ the axiom (int2sbv2int 3 t0) proves the clause ( +(= (sbv_to_int ((_ int_to_bv 3) t0)) (+ (mod (+ t0 4) 8) (- 4)))). The axiom is syntactic, i.e., the term (+ t0 4) is not simplified. In (ubv2int2bv t0) the width k is implicitly determined by the sort of t0, which is (_ BitVec k). This is not possible for the other two axioms because t0 has sort Int.

The following definitions handle arithmetic:

(define-fun bvadd ((x (_ BitVec k)) (y (_ BitVec k))) (_ BitVec k)
   ((_ int_to_bv k) (+ (ubv_to_int x) (ubv_to_int y))))
(define-fun bvsub ((x (_ BitVec k)) (y (_ BitVec k))) (_ BitVec k)
   ((_ int_to_bv k) (+ (ubv_to_int x) (* (- 1) (ubv_to_int y)))))
(define-fun bvneg ((x (_ BitVec k))) (_ BitVec k)
   ((_ int_to_bv k) (* (- 1) (ubv_to_int x))))
(define-fun bvmul ((x (_ BitVec k)) (y (_ BitVec k))) (_ BitVec k)
   ((_ int_to_bv k) (* (ubv_to_int x) (ubv_to_int y))))
(define-fun bvudiv ((x (_ BitVec k)) (y (_ BitVec k))) (_ BitVec k)
   ((_ int_to_bv k) (ite (= (ubv_to_int y) 0) (- 1) (div (ubv_to_int x) (ubv_to_int y)))))
(define-fun bvurem ((x (_ BitVec k)) (y (_ BitVec k))) (_ BitVec k)
   (ite (= (ubv_to_int y) 0) x ((_ int_to_bv k) (mod (ubv_to_int x) (ubv_to_int y)))))
(define-fun bvsdiv ((x (_ BitVec k)) (y (_ BitVec k))) (_ BitVec k)
   (let ((ix (sbv_to_int x)) (iy (sbv_to_int y)))
   ((_ int_to_bv k) (ite (< ix 0)
            (ite (< iy 0) (div (- ix) (- iy)) (ite (= iy 0) 1 (- (div (- ix) iy))))
            (ite (< iy 0) (- (div ix (- iy))) (ite (= iy 0) (- 1) (div ix iy)))))))
(define-fun bvsrem ((x (_ BitVec k)) (y (_ BitVec k))) (_ BitVec k)
   (let ((ix (sbv_to_int x)) (iy (sbv_to_int y)))
   ((_ int_to_bv k) (ite (= iy 0) ix
            (ite (< ix 0) (- (mod (- ix) iy)) (mod ix iy))))))
(define-fun bvsmod ((x (_ BitVec k)) (y (_ BitVec k))) (_ BitVec k)
   (let ((ix (sbv_to_int x)) (iy (sbv_to_int y)))
   ((_ int_to_bv k) (ite (= iy 0) ix (ite (< iy 0) (+ (mod (+ ix (- 1)) (- iy)) iy 1) (mod ix iy)))))
(define-fun bvnego ((x (_ BitVec k))) Bool
   (= (ubv_to_int x) 2^(k-1)))
(define-fun bvuaddo ((x (_ BitVec k)) (y (_ BitVec k))) Bool
   (<= 2^k (+ (ubv_to_int x) (ubv_to_int y))))
(define-fun bvsaddo ((x (_ BitVec k)) (y (_ BitVec k))) Bool
   (or (< (+ (sbv_to_int x) (sbv_to_int y)) 2^(k-1)) (<= 2^(k-1) (+ (sbv_to_int x) (sbv_to_int y)))))
(define-fun bvumulo ((x (_ BitVec k)) (y (_ BitVec k))) Bool
   (<= 2^k (* (ubv_to_int x) (ubv_to_int y))))
(define-fun bvsmulo ((x (_ BitVec k)) (y (_ BitVec k))) Bool
   (or (< (* (sbv_to_int x) (sbv_to_int y)) 2^(k-1)) (<= 2^(k-1) (* (sbv_to_int x) (sbv_to_int y)))))
(define-fun bvsdivo ((x (_ BitVec k)) (y (_ BitVec k))) Bool
   (and (= (ubv_to_int x) 2^(k-1)) (= (sbv_to_int y) (- 1))))
(define-fun bvusubo ((x (_ BitVec k)) (y (_ BitVec k))) Bool
   (< (ubv_to_int x) (ubv_to_int y)))
(define-fun bvssubo ((x (_ BitVec k)) (y (_ BitVec k))) Bool
   (or (< (sbv_to_int x) (+ (sbv_to_int y)) 2^(k-1)) (<= (+ (sbv_to_int y) 2^(k-1)) (sbv_to_int x))))

For shifts, we define a function pow2 for shifts and its inverse log2. We add a few axioms.

⟨bitvector-axiom⟩ ::= …
 | (pow2const k) ;( +(= (pow2 k) 2^k) )    ; where k >= 0 is a constant
 | (pow2add n m) ;( -(<= 0 n) -(<= 0 m) +(= (pow2 (+ n m)) (* (pow2 n) (pow2 m))) )
 | (log2low a)   ;( -(<= 0 a) +(<= (pow2 (log2 a)) a) )
 | (log2high a)  ;( -(<= 0 a) +(< a (* 2 (pow2 (log2 a)))) )

(define-fun bvshl ((x (_ BitVec k)) (y (_ BitVec k))) (_ BitVec k)
   ((_ int_to_bv k) (* (pow2 (ubv_to_int y)) (ubv_to_int x))))
(define-fun bvlshr ((x (_ BitVec k)) (y (_ BitVec k))) (_ BitVec k)
   ((_ int_to_bv k) (div (ubv_to_int x) (pow2 (ubv_to_int y)))))
(define-fun bvashr ((x (_ BitVec k)) (y (_ BitVec k))) (_ BitVec k)
   ((_ int_to_bv k) (div (sbv_to_int x) (pow2 (ubv_to_int y)))))

For logical operations we use a & operator over integers that computes bitwise AND. It is left-associative, takes two integers, and returns an integer. It returns a negative number if and only if both arguments are negative and ensures that no bits are truncated before performing bitwise AND.

⟨bitvector-axiom⟩ ::= …
 | (&flat (& (& a_ij)) (& bi))
      ;( +(= (& (& a_11 …) … (& an1 …)) (& b_1 … b_m)) ) where {b_i} ∪ {-1} = { a_ij }
      ;     ( if an "&" has only one parameter, the & is omitted)
 | (&shift a b k)      ;( -(<= 0 k) +(= (* (& (div a (pow2 k)) b) (pow2 k)) (& a (* b (pow2 k)))) )
 | (&split a b)        ;( +(= (+ (& a b) (& a (+ (* (- 1) b) (- 1)))) a) )
 | (&bound a b)        ;( -(<= 0 a) +(<= (& a b) a) )
 | (&nonneg a b)       ;( -(<= 0 a) +(<= 0 (& a b)) )

Using this function we can define the logical operators:

(define-fun bvnot ((x (_ BitVec k))) (_ BitVec k)
   ((_ int_to_bv k) (+ (- 1) (* (- 1) (ubv_to_int x)))))
(define-fun bvand ((x (_ BitVec k)) (y (_ BitVec k))) (_ BitVec k)
   ((_ int_to_bv k) (& (ubv_to_int x) (ubv_to_int y))))
(define-fun bvor ((x (_ BitVec k)) (y (_ BitVec k))) (_ BitVec k)
   ((_ int_to_bv k) (+ (ubv_to_int x) (ubv_to_int y) (* (- 1) (& (ubv_to_int x) (ubv_to_int y))))))
(define-fun bvxor ((x (_ BitVec k)) (y (_ BitVec k))) (_ BitVec k)
   ((_ int_to_bv k) (+ (ubv_to_int x) (ubv_to_int y) (* (- 2) (&
   (ubv_to_int x) (ubv_to_int y))))))
(define-fun bvnand ((x (_ BitVec k)) (y (_ BitVec k))) (_ BitVec k) (bvnot (bvand x y)))
(define-fun bvnor  ((x (_ BitVec k)) (y (_ BitVec k))) (_ BitVec k) (bvnot (bvor x y)))
(define-fun bvxnor ((x (_ BitVec k)) (y (_ BitVec k))) (_ BitVec k) (bvnot (bvxor x y)))

Comparisons:

(define-fun bvule ((x (_ BitVec k)) (y (_ BitVec k))) Bool (<= (ubv_to_int x) (ubv_to_int y)))
(define-fun bvult ((x (_ BitVec k)) (y (_ BitVec k))) Bool (< (ubv_to_int x) (ubv_to_int y)))
(define-fun bvuge ((x (_ BitVec k)) (y (_ BitVec k))) Bool (<= (ubv_to_int y) (ubv_to_int x)))
(define-fun bvugt ((x (_ BitVec k)) (y (_ BitVec k))) Bool (< (ubv_to_int y) (ubv_to_int x)))
(define-fun bvsle ((x (_ BitVec k)) (y (_ BitVec k))) Bool (<= (sbv_to_int x) (sbv_to_int y)))
(define-fun bvslt ((x (_ BitVec k)) (y (_ BitVec k))) Bool (< (sbv_to_int x) (sbv_to_int y)))
(define-fun bvsge ((x (_ BitVec k)) (y (_ BitVec k))) Bool (<= (sbv_to_int y) (sbv_to_int x)))
(define-fun bvsgt ((x (_ BitVec k)) (y (_ BitVec k))) Bool (< (sbv_to_int y) (sbv_to_int x)))
(define-fun bvcomp ((x (_ BitVec k)) (y (_ BitVec k))) (_ BitVec 1)
   (ite (= x y) (_ bv1 1) (_ bv0 1)))

Miscellaneous:

(define-fun (_ zero_extend i) ((x (_ BitVec k))) (_ BitVec i+k)
   ((_ int_to_bv (i+k)) (ubv_to_int x)))
(define-fun (_ sign_extend i) ((x (_ BitVec k))) (_ BitVec i+k)
   ((_ int_to_bv (i+k)) (sbv_to_int x)))
(define-fun concat ((x (_ BitVec k1)) (y (_ BitVec k2))) (_ BitVec k1+k2)
   ((_ int_to_bv (k1+k2)) (+ (* (2^k2) (ubv_to_int x)) (ubv_to_int y))))
(define-fun (_ extract i j) ((x (_ BitVec k1))) (_ BitVec i-j+1)
   ((_ int_to_bv (i-j+1)) (div (ubv_to_int x) 2^j)))
(define-fun (_repeat i) ((x (_ BitVec k))) (_ BitVec i*k)
   ((_ int_to_bv (i*k)) (* ((2^(i*k)-1)/(2^k-1)) (ubv_to_int x))))
(define-fun (_ rotate_left i)  ((x (_ BitVec k))) (_ BitVec k)
   ((_ int_to_bv k) (+ (* 2^(i mod k) (ubv_to_int x)) (div (ubv_to_int x) 2^(-i mod k)))))
(define-fun (_ rotate_right i)  ((x (_ BitVec k))) (_ BitVec k)
   ((_ int_to_bv k) (+ (* 2^(-i mod k) (ubv_to_int x)) (div (ubv_to_int x) 2^(i mod k)))))