4

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.

Guy Coder
  • 24,501
  • 8
  • 71
  • 136
user1779685
  • 283
  • 2
  • 8

1 Answers1

5

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.

Leonardo de Moura
  • 21,065
  • 2
  • 47
  • 53
  • A clarification sought: `smt::conflict_resolution::resolve` is the lemma learning part you mentioned about (in the SAT part) and `smt::context::pop_scope_core()` does the expensive backtracking in the theory solvers, right? – user1779685 Jan 23 '14 at 19:55