CODEWITHSUNDEEP
z3
Steven
Steven

Reputation: 13

Trigger the running time of theory solver

I want to trigger the running time of theory solver to see how much time does each theory checking take. Does anyone know which file and which variable do I need to look at? I don't know if the statistics method has this option.

Upvotes: 1

Views: 57

Answers (1)

Malte Schwerhoff
Malte Schwerhoff

Reputation: 12852

According to this answer, Christoph Wintersteiger "expect[s] this to be nontrivial as it's not clear what exactly should and shouldn't be counted."

For the special case of Z3's SAT solver, this answer by Leonardo de Moura mentions several methods (such as bcp() and decide()) in a particular C++ file (smt_context.cpp) of Z3's sources that belong to this particular sub-solver.

Upvotes: 1

Related Questions