CODEWITHSUNDEEP
z3simplifyz3py
QLM
QLM

Reputation: 47

Z3 (z3py) "elim_and" option of the "simplify()" function always enabled for bit vectors

I would like to use the simplify() function of z3py, but without changing the bitwise and '&' to a bitwise or '|'.

There seem to exist an option called "elim_and" to the simplify function, but I cannot manage to have it to work for bitwise operations. The function help_simplify() states:

elim_and (bool) conjunctions are rewritten using negation and disjunctions (default: false)

>>> from z3 import *
>>> x = BitVec('x', 8)
>>> y = BitVec('y', 8)
>>> z = x & y
>>> z
x & y
>>> simplify(z)
~(~x | ~y)
>>> simplify(z, elim_and=False)
~(~x | ~y)

I would like the result to be "x & y". Is there a way to do it?

Upvotes: 0

Views: 183

Answers (2)

alias
alias

Reputation: 30460

This is currently not possible. Note that elim_and is targeted for booleans, not bit-vectors:

>>> from z3 import *
>>> a = Bool("a")
>>> b = Bool("b")
>>> simplify(And(a, b))
And(a, b)
>>> simplify(And(a, b), elim_and=True)
Not(Or(Not(a), Not(b)))

There's no equivalent option to simplify that controls this for bit-vectors. In fact, the translation to disjunction happens even before you call the simplifier, see here: https://github.com/Z3Prover/z3/blob/master/src/ast/rewriter/bv_rewriter.cpp#L1980-L1988

Upvotes: 1

Nuno Lopes
Nuno Lopes

Reputation: 868

elim_and is for Boolean expressions, not for bit-vectors. Z3 doesn't have an option to disable specific rewrite rules I'm afraid.

Upvotes: 0

Related Questions