mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

making tests deterministic

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-12-05 16:21:38 -08:00
parent 5e4d1151eb
commit 2b66b50c75
1 changed files with 10 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -23,8 +23,11 @@ Small example:
>>> s.add(y == x + 1)
>>> s.check()
sat
>>> s.model()
[y = 2, x = 1]
>>> m = s.model()
>>> m[x]
1
>>> m[y]
2
Z3 exceptions:
@ -1728,10 +1731,11 @@ def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
>>> q = Exists([x, y], f(x, y) >= x, skid="foo")
>>> q
Exists([x, y], f(x, y) >= x)
>>> Tactic('nnf')(q)
[[f(x!foo!1, y!foo!0) >= x!foo!1]]
>>> Tactic('nnf')(q).as_expr()
f(x!foo!3, y!foo!2) >= x!foo!3
>>> is_quantifier(q)
True
>>> r = Tactic('nnf')(q).as_expr()
>>> is_quantifier(r)
False
"""
return _mk_quantifier(False, vs, body, weight, qid, skid, patterns, no_patterns)