mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 02:15:19 +00:00
Code Activity

no fun!

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-03-03 15:03:02 -08:00
parent 2b71d8bc08
commit 3e51b69a9a
1 changed files with 3 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -12,8 +12,6 @@ Z3 is used in many applications such as: software/hardware verification and test
constraint solving, analysis of hybrid systems, security, biology (in silico analysis),
and geometrical problems.
Several online tutorials for Z3Py are available at:
http://rise4fun.com/Z3Py/tutorial/guide
Please send feedback, comments and/or corrections on the Issue tracker for
https://github.com/Z3prover/z3.git. Your comments are very valuable.
@ -103,9 +101,6 @@ def get_version():
def get_full_version():
return Z3_get_full_version()
# We use _z3_assert instead of the assert command because we want to
# produce nice error messages in Z3Py at rise4fun.com
def _z3_assert(cond, msg):
if not cond:
@ -9009,7 +9004,7 @@ def prove(claim, show=False, **keywords):
def _solve_html(*args, **keywords):
"""Version of function `solve` used in RiSE4Fun."""
"""Version of function `solve` that renders HTML output."""
show = keywords.pop("show", False)
s = Solver()
s.set(**keywords)
@ -9033,7 +9028,7 @@ def _solve_html(*args, **keywords):
def _solve_using_html(s, *args, **keywords):
"""Version of function `solve_using` used in RiSE4Fun."""
"""Version of function `solve_using` that renders HTML."""
show = keywords.pop("show", False)
if z3_debug():
_z3_assert(isinstance(s, Solver), "Solver object expected")
@ -9058,7 +9053,7 @@ def _solve_using_html(s, *args, **keywords):
def _prove_html(claim, show=False, **keywords):
"""Version of function `prove` used in RiSE4Fun."""
"""Version of function `prove` that renders HTML."""
if z3_debug():
_z3_assert(is_bool(claim), "Z3 Boolean expression expected")
s = Solver()