How to estimate time spent in SAT solving part in z3 for SMT?

Question

I have profiled my problems, which are in (pseudo-nonlinear) integer real fragment using the profiler gprof (stats here including the call graph) and was trying to separate out the time taken into two classes:

I)The SAT solving part (including [purely] boolean propagation and [purely] boolean conflict clause detection, backjumping, any other propositional manipulation)

II)The theory solving part (including theory consistency checks, generation of theory conflict-clauses and theory propagation).

Do lines 3280-3346 in smt_context.cpp within bounded_search() constitute the top-level DPLL(X) loop?

I believe it is easier to sum-up the time in SAT solver functions (since they are fewer) and then the rest can be considered as theory solvers's time. I am trying to figure out which functions I should consider as falling under class I above? Are they smt::context::decide(), smt::context::bcp() within smt::context::propagate()? Any others? smt::context: resolve_conflict() seems to be mixed with calls to theory solver?

Is it correct that smt::context::propagate() seems to be mostly theory propagation (class II) except its bcp() function? Also, smt::context::final_check() seems to be purely in class II.

Any hints greatly appreciated. Thanks.

Answer 1

You are correct, bcp() and decide() are part of the "SAT solver". The function final_check() is just theory reasoning. It executes procedures that Z3 "claims" to be too "expensive". The resolve_conflict() procedure is mixed: it performs lemma learning, and backtracking. To generate new lemmas, Z3 uses Boolean resolution (which is in "SAT part"). In several cases, the most expensive part of resolve_conflict is backtracking the state of the theory solvers.