Clever Geek Handbook

Simplifying Z3 Expressions

I am using z3 in Python to simplify some boolean expressions and I have a question. When I execute the following code

x = BitVec('x', 8)
e = ULT(x - 5, 10)
Then('simplify', 'propagate-values', 'ctx-solver-simplify')(e).as_expr()

I get the result:

Not(ULE(10, 251 + x))

However, this is equivalent to

And(UGE(x, 5), ULT(x, 15))

Is there a way to convert (simplify) the first expression (Not) to the second (And)? More specifically, can you ask z3 about the ranges of values ​​that a particular variable can take (in this example, x> = 5 & x <15)?

+3


source to share


1 answer


You can create a simplifier on top of Z3 by synthesizing a simpler expression among a set of templates. But the Z3 doesn't try to accomplish this particular simplification among many others.



+1


source






More articles:


All Articles