2

I'm trying to find the c++ file for Z3 where the algorithm backtraces if it can't find a solution on the current branch. I've been looking through all the files and tried debug mode on the python files, but no luck so far. I just want to add a print statement to the method, so I can tell when it is returning to a previous node and trying a new path.

Thanks!

Guy Coder
  • 24,501
  • 8
  • 71
  • 136

1 Answers1

1

It depends on which solver Z3 uses for your problem. It typically uses smt_context.cpp in src/smt. The relevant backjump can be traced in the context::pop_scope method. Other solvers exist too: the src/sat/sat_solver is used for bit-vector and Boolean problems. It has a similar pop method. Finally, nlsat is used for non-linear polynomial arithmetic over the reals.

Nikolaj Bjorner
  • 8,229
  • 14
  • 15
  • for the example.py file, which solver would it use? Could a simple printf ("test") be inserted? –  Aug 03 '16 at 18:30