I am still in the process of learning the guts of Z3 (Python).
It was brought to my attention that Z3 performs incremental SAT solving by default (see SAT queries are slowing down in Z3-Python: what about incremental SAT?): specifically, every time you use the s.add command (where s is a solver), it means that it adds that clause to s, but it does not forget everything you have learned before.
First question: can non-incremental SAT solving be done in Z3? That is, somehow 'deactivate' the incremental solving. What would this mean? That we are creating a new solver for each enlarged formula?
For instance, this approach would be Z3-default-incremental:
...
phi = a_formula
s = Solver()
s.add(phi)
while s.check() == sat:
s.check()
m = s.model()
phi = add_modelNegation(m)
s.add(phi) #in order not to explore the same model again
...
That is, once we get a model, we attach the negated model to the same solver.
While this one is 'forcing' Z3 to be non-incremental:
...
phi_st = a_formula
s = Solver()
s.add(phi_st)
negatedModelsStack = []
while s.check() == sat:
m = s.model()
phi_n = add_modelNegation(m)
negatedModelsStack.append(phi_n)
original_plus_negated = And(phi_st, And(negatedModelsStack))
s = Solver()
s.add(original_plus_negated) #in order not to explore the same model again
...
That is, once we get a model, we attach the obtained models to a new solver.
Am I right?
On the other hand, in the attached link, the following is stated:
Compare this to, for instance, CVC4; which is by default not incremental. If you want to use CVC4 in incremental mode, you have to pass a specific command line argument
Does this mean in CVC4 you must create a new solver every time? Like in the second code?
Second question: how can I know exactly what techniques I am using to do incremental solving in Z3? I have been reading about incremental SAT theory and I see that one of those techniques is 'CDCL' (http://www.cril.univ-artois.fr/~audemard/slidesMontpellier2014.pdf), is this used in Z3's incremental search?
References: In order not to inundate Stack with similar questions, which readings do you recommend for incremental SAT in general and Z3's incremental SAT in particular? Also, is the incremental SAT of Z3 similar to the ones of other solvers such as MiniSAT or PySAT?
