mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

aligning simplifier and rewriter for regression tests

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-09-04 09:43:25 -07:00
parent f12a4f04fd
commit 93474c0263
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/api/python/z3/z3.py
View file

@ -3640,7 +3640,7 @@ def BitVecs(names, bv, ctx=None):
>>> Product(x, y, z)
1*x*y*z
>>> simplify(Product(x, y, z))
z*x*y
x*y*z
"""
ctx = _get_ctx(ctx)
if isinstance(names, str):
@ -7647,7 +7647,7 @@ def simplify(a, *arguments, **keywords):
>>> simplify(x + 1 + y + x + 1)
2 + 2*x + y
>>> simplify((x + 1)*(y + 1), som=True)
1 + x + y + y*x
1 + x + y + x*y
>>> simplify(Distinct(x, y, 1), blast_distinct=True)
And(Not(x == y), Not(x == 1), Not(y == 1))
>>> simplify(And(x == 0, y == 1), elim_and=True)