Try other SMT solvers

[philzook58]

Since we have added the capability to print the smtlib2 query, it is not so hard to evaluate other SMT solvers (in particular CVC4 and Boolector). If there is significant variation among solvers, it may be worth running them in a parallel portfolio in separate processes. We don't necessarily even have to replace our usage of Z3 for constraint construction to achieve this.

[philzook58]

Yices 2 and bitwuzla are also promising seeming https://smt-comp.github.io/2020/results/qf-aufbv-single-query

[philzook58]

On a very preliminary experiment for a particular query (addname in grammatech)

• z3 3m20s
• yices 54s
• cvc4 timeout
• boolector 15s

[philzook58]

Here is a rough outline of a relatively painless way to integrate other solvers.

You'll want to start from this branch https://github.com/draperlaboratory/cbat_tools/pull/229 which has some modifications to make more legal smtlib

Add a flag to point to a smtlib compatible binary --wp-solver=~/Downloads/boolector/bin/boolector

Fork a process calling this binary name in Precondition.check. I'm not sure exactly how to do this. core probably has this functionality. Maybe this https://ocaml.janestreet.com/ocaml-core/latest/doc/core/Core__/Core_command/index.html . Roughly you need to pipe in the following string to the process:

Printf.printf "(set-logic QF_AUFBV) \n %s \n (check-sat) \n (get-model) %!" (Z3.Solver.to_string solver) );

You may want to check that it returns "sat" before asking for the model. I think solvers can often be run interactively via pipe.

The model should look something like this http://smtlib.cs.uiowa.edu/examples.shtml

(get-model)
; ((define-fun x () Int 8)
;  (define-fun y () Int 6)
; )

Take this, parse as an SExpr and then assert these values to the z3 solver and call Z3.Solver.check if sat.

[codyroux]

@philzook58 can we close this?

[philzook58]

I suppose we can. This work has been integrated into master