2

I need it for incremental solving in the context of symbolic execution (Klee). In points of branching of symbolic execution paths it is necessary to split solver context into 2 parts: with true and false conditions. Of course, there is an expensive workaround - create empty context and replay all constraints.

Is there a way to split Z3_context? Do you plan to add such functionality?

Note

splitting of context can be avoided if use depth-first symbolic exploration, that is exploring current execution path until it reaches "end" and hence this path won't be explored anymore in future. In this case it is enough to pop until branch point reached and continue to explore another condition branch. But in case of Klee many symbolic paths are explored "simultaneously" (exploration of true and false branches is interleaved), so you need solver context solver switching (there is Z3_context argument in each method) and branching (there are no methods for this, that is what I need).

Thanks!

Ayrat
  • 1,221
  • 1
  • 18
  • 36

2 Answers2

4

No, the current version of Z3 (3.2) does not support this feature. We realize this is an important capability, and an equivalent feature will be available in the next release. The idea is to separate the concepts of Context and Solver. In the next release, we will have APIs for creating (and copying) solvers. So, you will be able to use a different solver for each branch of the search. In a nutshell, the Context is used to manage/create Z3 expressions, and the Solver for checking satisfiability.

Leonardo de Moura
  • 21,065
  • 2
  • 47
  • 53
  • Hello! Just checking, since this answer is 9 years old. Has this feature been added ? And if so, could you update your answer ? Many thanks :) – ZakC Nov 09 '20 at 15:00
  • Did you find anything that would documents that feature, if it exists by now? – Benni Mar 19 '21 at 09:39
3

The approach I currently use for this sort of thing is to assert formulas like p => A instead of A, where p is a fresh Boolean literal. Then in my client I maintain the association between the list of guard literals that correspond to each branch, and use check_assumptions(). In my situation I happen to be able to get away with leaving all formulas allocated during each search, but YMMV. Even for depth-first explorations, I seem to get much more incremental reuse this way than by using push/pop.

Josh Berdine
  • 326
  • 1
  • 1