mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +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:53:54 -08:00
parent 2f3daf14b5
commit 3cefa0a1f7
1 changed files with 12 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -5787,8 +5787,15 @@ class Solver(Z3PPObject):
>>> s.assert_and_track(x < 0, p3) >>> s.assert_and_track(x < 0, p3)
>>> print s.check() >>> print s.check()
unsat unsat
>>> print s.unsat_core() >>> c = s.unsat_core()
[p3, p1] >>> len(c)
2
>>> Bool('p1') in c
True
>>> Bool('p2') in c
False
>>> p3 in c
True
""" """
if isinstance(p, str): if isinstance(p, str):
p = Bool(p, self.ctx) p = Bool(p, self.ctx)
@ -6985,9 +6992,9 @@ def solve(*args, **keywords):
configure it using the options in `keywords`, adds the constraints configure it using the options in `keywords`, adds the constraints
in `args`, and invokes check. in `args`, and invokes check.
>>> a, b = Ints('a b') >>> a = Int('a')
>>> solve(a + b == 3, Or(a == 0, a == 1), a != 0) >>> solve(a > 0, a < 2)
[b = 2, a = 1] [a = 1]
""" """
s = Solver() s = Solver()
s.set(**keywords) s.set(**keywords)