about summary refs log tree commit diff homepage
path: root/lib/Solver
diff options
context:
space:
mode:
authorDan Liew <daniel.liew@imperial.ac.uk>2017-05-24 18:45:40 +0100
committerDan Liew <delcypher@gmail.com>2017-06-01 11:36:09 +0100
commit1d9b6096e68eda51b95ae92b69b1f91c4cff0f7b (patch)
tree7b0146c003b322425607dbdcd339a3bfc9127cc4 /lib/Solver
parent2e12c5326edde78b1344cc9df1a51db902e41bd5 (diff)
downloadklee-1d9b6096e68eda51b95ae92b69b1f91c4cff0f7b.tar.gz
[Z3] Switch from `Z3_mk_simple_solver()` to `Z3_mk_solver()`.
My discussions [1] with the Z3 team have revealed that
`Z3_mk_simple_solver()` is the wrong solver to use. That solver
basically runs the `simplify` tactic and then the `smt` tactic.
This by-passes Z3's attempt to probe for different logics and
apply its own specialized tactic.

Using `Z3_mk_solver()` should be closer to the behaviour of the
Z3 binary.

This partially addresses #653. We still need to try rolling our
own custom tactic.

[1] https://github.com/Z3Prover/z3/issues/1035
Diffstat (limited to 'lib/Solver')
-rw-r--r--lib/Solver/Z3Solver.cpp12
1 files changed, 7 insertions, 5 deletions
diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp
index f32860f7..4443c246 100644
--- a/lib/Solver/Z3Solver.cpp
+++ b/lib/Solver/Z3Solver.cpp
@@ -223,11 +223,13 @@ bool Z3SolverImpl::internalRunSolver(
     std::vector<std::vector<unsigned char> > *values, bool &hasSolution) {
 
   TimerStatIncrementer t(stats::queryTime);
-  // TODO: Does making a new solver for each query have a performance
-  // impact vs making one global solver and using push and pop?
-  // TODO: is the "simple_solver" the right solver to use for
-  // best performance?
-  Z3_solver theSolver = Z3_mk_simple_solver(builder->ctx);
+  // NOTE: Z3 will switch to using a slower solver internally if push/pop are
+  // used so for now it is likely that creating a new solver each time is the
+  // right way to go until Z3 changes its behaviour.
+  //
+  // TODO: Investigate using a custom tactic as described in
+  // https://github.com/klee/klee/issues/653
+  Z3_solver theSolver = Z3_mk_solver(builder->ctx);
   Z3_solver_inc_ref(builder->ctx, theSolver);
   Z3_solver_set_params(builder->ctx, theSolver, solverParameters);