0

Q1: Is it possible to query the times Z3 spent in different sub-solvers?

Calling (get-info :all-statistics) gives the overall run time of Z3, but I would like to break it down into individual sub-solvers.

I am particularly interested in the time spent in arithmetic-related sub-solver, more precisely, in those that give rise to the statistics grobner and nonlinear-horner.


Q2: Furthermore, is it possible to put a timeout on sub-solver?

I could imagine something like defining a timeout per check-sat and sub-solver that bounds the time Z3 can spent in that sub-solver. Z3 would repeatedly call n different sub-solvers, and if the time bound of one of them is reached it continues, but only uses the remaining n-1 sub-solvers.

I read the tactics tutorial and got the impression that this might actually be possible by something along the lines of

(repeat
  (par-or
    (try-for <arithmetic-solvers> 500)
    <all-other-solvers>))

but I couldn't figure out which solvers to use.

Malte Schwerhoff
  • 12,684
  • 4
  • 41
  • 71

1 Answers1

1

For Q1: No, you'd have to add your own timers on that and I would expect this to be nontrivial as it's not clear what exactly should and shouldn't be counted.

Q2: Yes, you can build your own custom strategies/tactics. Note that par-or means parallel or, i.e., it will try to run the provided tactics in parallel. Not everything we call a "solver" has it's own tactic, so this might require some fiddling. Note that "solver" in this context is not necessarily the same as the Z3 C++ object called "solver". Some "solvers" are also integral parts of the SMT kernel.

Christoph Wintersteiger
  • 8,234
  • 1
  • 16
  • 30
  • Thanks for the clarifications! I am optimistic that I can work out from `help-tactic` which "solvers" are arithmetic-related; however, your comment about some "solvers" being integral parts of the SMT kernel makes me worry if it will be possible to essentially run "everything but arithmetic-related solvers". I assume the `smt` tactic includes arithmetic-related tactics? Is there a way of finding out which sub-tactics `smt` involves? That might allow we to remove the arithmetic-related ones and run all the others. – Malte Schwerhoff Jan 21 '15 at 15:34
  • The smt tactic doesn't have any subtactics (see https://z3.codeplex.com/SourceControl/latest#src/smt/tactic/smt_tactic.cpp), it is just a tactic wrapper around the (old) smt kernel, which includes everything (see https://z3.codeplex.com/SourceControl/latest#src/smt/smt_context.cpp). It works through theory plugins that are initially set up in https://z3.codeplex.com/SourceControl/latest#src/smt/smt_setup.cpp You could try to not install the arith plugin and then only install it when needed perhaps. – Christoph Wintersteiger Jan 21 '15 at 15:47