substitution in Z3Py

Question

It seems that the substitute(f,t) function in Z3Py performs simplification on f first before doing the substitution. Is there a way to disallow this?

I would like the following behavior to occur:

f = And(x,Not(x))
result = substitute(f,*[(Not(x),BoolVal(True))])  #sub Not(x) => True
#if we simplify f first then the result = False,  but if we do the substitution first then result = x

Answer 1

Unfortunately, the substitute procedure is implemented using the simplifier which can apply substitutions during the simplification. The substitute Python procedure invokes the Z3 C API Z3_substitute in the file api_ast.cpp. Internally, the simplifier is called th_rewriter (theory rewriter).

That being said, I agree this is not nice and may be very inconvenient in some cases. I will change that for the next release.