Using SMT-Lib Solvers

The examples presented so far have used the internal proof system provided by SAWScript, based primarily on a version of the ABC tool from UC Berkeley linked into the saw executable. However, there is internal support for other proof tools – such as Yices and Z3 as illustrated in the next example – and more general support for exporting models representing theorems as goals in the SMT-Lib language. These exported goals can then be solved using an external SMT solver.

Consider the following C file:

int double_ref(int x) {
    return x * 2;
}

int double_imp(int x) {
    return x << 1;
}

In this trivial example, an integer can be doubled either using multiplication or shifting. The following SAWScript program (in double.saw) verifies that the two are equivalent using both internal Yices and Z3 modes, and by exporting an SMT-Lib theorem to be checked later, by an external SAT solver.

l <- llvm_load_module "double.bc";
double_imp <- llvm_extract l "double_imp";
double_ref <- llvm_extract l "double_ref";
let thm = {{ \x -> double_ref x == double_imp x }};

r <- prove yices thm;
print r;

r <- prove z3 thm;
print r;

let thm_neg = {{ \x -> ~(thm x) }};
write_smtlib2 "double.smt2" thm_neg;

print "Done.";

The new primitives introduced here are the tilde operator, ~, which constructs the logical negation of a term, and write_smtlib2, which writes a term as a proof obligation in SMT-Lib version 2 format. Because SMT solvers are satisfiability solvers, their default behavior is to treat free variables as existentially quantified. By negating the input term, we can instead treat the free variables as universally quantified: a result of “unsatisfiable” from the solver indicates that the original term (before negation) is a valid theorem. The prove primitive does this automatically, but for flexibility the write_smtlib2 primitive passes the given term through unchanged, because it might be used for either satisfiability or validity checking.

The SMT-Lib export capabilities in SAWScript make use of the Haskell SBV package, and support ABC, Bitwuzla, Boolector, CVC4, CVC5, MathSAT, Yices, and Z3.