From 3e51b69a9ab0a333b819a08d73b16b2cd64f7a2c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 3 Mar 2022 15:03:02 -0800 Subject: [PATCH] no fun! Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 11 +++-------- 1 file changed, 3 insertions(+), 8 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 1a35865c966..cd4aee24f03 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -12,8 +12,6 @@ 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()