SMT Solver Outputs

Satisfiable Queries

When a solver returns sat, we have already seen that one possible way to get more information is to call get-model, which returns values for all of the uninterpreted constants in the formula. A more fine-grained approach is to call get-value which takes a term as an argument and returns the value of that specific term.

Unsatisfiable Queries

When a solver returns unsat, it makes a quite strong statement: there is no interpretation of the user-declared symbols that satisfies the formula. SMT solvers can provide more information as to why a formula is unsatisfiable via an unsat(isfiable) core, a subset of the assertions that is already unsatisfiable. In SMT-LIB scripts, it can be obtained with the command get-unsat-core. The unsat core is not guaranteed to be minimal, but solvers generally make an effort to reduce its size as much as possible without having to solve additional SMT queries.

Some solvers can also produce proofs for the unsatisfiability of a formula, i.e., a structured argument showing how an inconsistency can be derived from an unsat core of the formula. A proof can serve as a certificate of the result and be used to independently validate the solver’s response [R4]. A proof (if supported) can be obtained in an SMT-LIB script with the command get-proof. The result is dependent on the proof system and format the solver uses to represent its reasoning. cvc5 has full support for proofs and unsat cores.

Consider again the Socrates example (Example 3). Below, we show how to retrieve an unsat core and a proof of its unsatisfiability.

 1from cvc5.pythonic import *
 2
 3s = SolverFor('UF')
 4
 5s.set("produce-proofs", "true")
 6s.set("proof-granularity", "theory-rewrite")
 7s.set("produce-unsat-cores", "true")
 8
 9S = DeclareSort("S")
10Human = Function("Human", S, BoolSort())
11Mortal = Function("Mortal", S, BoolSort())
12Socrates = Const("Socrates", S)
13
14x = Const("x", S)
15
16s.add(ForAll([x], Implies(Human(x), Mortal(x))))
17s.add(Human(Socrates))
18s.add(Not(Mortal(Socrates)))
19
20print(s.check())
21print("The core is: ", s.unsat_core())
22
23p = s.proof()
24
25print("The proof is:\n", p)

The first part of the output is the unsat core.

- (forall ((x S)) (=> (Human x) (Mortal x)))
- (Human Socrates)
- (not (Mortal Socrates))

The core contains all three assertions. In this case, the core is minimal, as all three are needed to derive unsat. The reasoning is shown in the proof. The result of the proof() method is a proof object which connects the input assertions to the conclusion (unsat) via a sequence of steps justified by proof rules. The proof rules used by cvc5 are documented on the cvc5 website.

The above figure shows a visualization of the proof as a tree. For readability, we use simple names to abbreviate long terms. Each node in the tree shows: \((i)\) the formula proved (the conclusion); \((ii)\) the name of the proof rule used; \((iii)\) a numeric id; and \((iv)\) the total number of descendants. Immediate children of each node represent premises required for the node’s proof rule. The root node of the tree is let9, which stands for (not (and let4 let3 let2)), where let4, let3, and let2 represent the three assertions. This node has a single child containing the conclusion false, based on a proof tree whose leaves are the three assertions. The derivation of false depends on instantiating the quantified assertion (let4) with x as Socrates. This is done in node 5, but only after (forall ((x S)) (=> (Human x) (Mortal x))) (i.e., let4) is rewritten (node 8) into (forall ((x S)) (or (not (Human x)) (Mortal x))) (i.e., let8). The instantiation (or (not (Human Socrates)) (Mortal Socrates)) is named let6. Node 9 concludes (not let6) from the other assertions. And finally, node 2 concludes false by combining the mutually inconsistent clauses derived by the solver (where let7 is (not let6), let2 is (not let1), and let5 is (not let3)).

Unknown Queries

A solver returns unknown when it is unable to solve the input problem. There could be several different reasons for this. One is that the solver’s procedure may be incomplete for the class of problems the input belongs to, which means that it is not always able to determine if the problem is satisfiable or not. Another possible reason is that some resource limit was exceeded, causing the solver to stop before it could find an answer. In SMT-LIB, the command (get-info :reason-unknown) can be used to request more information about why a solver returned unknown.