I profiled my problems that are in a (pseudo-linear) integer real fragment using the gprof profiler (stats here , including the call graph) and tried to separate the time spent in two classes:
I) Part of the SAT solution (including [purely] Boolean distribution and [purely] definition of logical conflict, reverse bias, any other propositional manipulations)
II) The part that decides the theory (including verification of the consistency of the theory, the formation of theoretical conflict proposals and the dissemination of theory).
Do lines 3280-3346 in smt_context.cpp inside bounded_search()make up a top-level loop of DPLL (X)?
I believe that it is easiest to summarize the time in the functions of the SAT solver (since there are fewer of them) and then the rest can be considered as the time of decisive theories. I am trying to figure out what functions should I consider as falling under the class I above? Are they smt::context::decide(), smt::context::bcp()inside smt::context::propagate()? Any others?
smt::context: resolve_conflict()seems to be mixed with the challenges of solver theory?
Is it right that smt::context::propagate(), apparently, it is mainly the extension of the theory (class II), except for its function bcp()? It also smt::context::final_check()seems to be purely class II.
Any advice is highly appreciated. Thanks.
source
share