I was wondering whether it's possible to get z3 not to use Extract and Concat in the output expression when one applies simplify on an expression with bitvectors.
For example, instead of
>>> x = BitVector("x", 32)
>>> simplify(x ^ 7 ^ 6)
Concat(Extract(31, 1, x), ~Extract(0, 0, x))
I'd like to have
>>> x = BitVector("x", 32)
>>> simplify(x ^ 7 ^ 6)
x ^ 1
I had a look at help_simplify, but I couldn't find such an "option".
Not easily. z3 converts XOR with numerals to a mask fairly early in the rewriter, and there appears to be no easy way to control that behavior. See here: https://github.com/Z3Prover/z3/blob/master/src/ast/rewriter/bv_rewriter.cpp#L1817-L1823
Having said that, the advantage of the programmable API is that z3 gives you all the tools to code such transformations yourself. This does not mean it is easy to do so, but at least it exposes all the necessary bits and pieces. While doing a complete job of doing exactly the rewrites you want can be a large task, you can get away with something simple like this:
def constFold(e):
try:
if is_app(e) and all([is_bv_value(c) for c in e.children()]):
return simplify(e)
else:
return e
except:
return e
This is extremely simple-minded; and it actually doesn't even handle the problem you posed:
>>> constFold(x^6^7)
x ^ 6 ^ 7
But it does handle this:
>>> constFold(x^(6^7))
x ^ 1
But for 8 lines of code, it's not too bad! The point is that you can improve upon it as you walk down the structure of expressions, recognize associativity/commutativity etc., and do whatever transformations you want on the AST as exposed by the programmable API.
Keep in mind that if you're using this in a solver context you have to maintain a bunch of invariants and if you do an "incorrect" transformation, you can easily render the solver unsound. With great power, comes great responsibility! Nonetheless, a lot can be achieved with relatively simple programming, if you're willing to study the API and do a deep dive.
Good luck!