From 3d8865d925f851858e9fd4cab9a66d806cbaec84 Mon Sep 17 00:00:00 2001
From: Gram <mail@orsinium.dev>
Date: Sun, 23 May 2021 19:27:55 +0200
Subject: [PATCH] Fix some PEP-8 violations in Python code (#5295)
* reformat python code using autopep8
* manually wrap some too long lines and adjust some checks
* run autopep8 in aggressive mode
* run autopep8 in very aggressive mode
* manually reformat z3types.py
* unify: use double quotes
* use sys.version_info instead of sys.version
* drop accidentally commited src/util/z3_version.h
---
src/api/python/z3/z3.py | 1311 +++++++++++++++++++++++---------
src/api/python/z3/z3num.py | 92 +--
src/api/python/z3/z3poly.py | 10 +-
src/api/python/z3/z3printer.py | 703 +++++++++--------
src/api/python/z3/z3rcf.py | 26 +-
src/api/python/z3/z3types.py | 229 ++++--
src/api/python/z3/z3util.py | 208 ++---
7 files changed, 1669 insertions(+), 910 deletions(-)
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 3044760ba..529ed72e8 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -6,12 +6,17 @@
# Author: Leonardo de Moura (leonardo)
############################################
-"""Z3 is a high performance theorem prover developed at Microsoft Research. Z3 is used in many applications such as: software/hardware verification and testing, constraint solving, analysis of hybrid systems, security, biology (in silico analysis), and geometrical problems.
+"""Z3 is a high performance theorem prover developed at Microsoft Research.
+
+Z3 is used in many applications such as: software/hardware verification and testing,
+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.
+Please send feedback, comments and/or corrections on the Issue tracker for
+https://github.com/Z3prover/z3.git. Your comments are very valuable.
Small example:
@@ -50,66 +55,77 @@ import sys
import io
import math
import copy
-if sys.version < '3':
- pass
-else:
+if sys.version_info.major >= 3:
from typing import Iterable
Z3_DEBUG = __debug__
+
def z3_debug():
global Z3_DEBUG
return Z3_DEBUG
-if sys.version < '3':
+
+if sys.version_info.major < 3:
def _is_int(v):
return isinstance(v, (int, long))
else:
def _is_int(v):
return isinstance(v, int)
+
def enable_trace(msg):
Z3_enable_trace(msg)
+
def disable_trace(msg):
Z3_disable_trace(msg)
+
def get_version_string():
- major = ctypes.c_uint(0)
- minor = ctypes.c_uint(0)
- build = ctypes.c_uint(0)
- rev = ctypes.c_uint(0)
- Z3_get_version(major, minor, build, rev)
- return "%s.%s.%s" % (major.value, minor.value, build.value)
+ major = ctypes.c_uint(0)
+ minor = ctypes.c_uint(0)
+ build = ctypes.c_uint(0)
+ rev = ctypes.c_uint(0)
+ Z3_get_version(major, minor, build, rev)
+ return "%s.%s.%s" % (major.value, minor.value, build.value)
+
def get_version():
- major = ctypes.c_uint(0)
- minor = ctypes.c_uint(0)
- build = ctypes.c_uint(0)
- rev = ctypes.c_uint(0)
- Z3_get_version(major, minor, build, rev)
- return (major.value, minor.value, build.value, rev.value)
+ major = ctypes.c_uint(0)
+ minor = ctypes.c_uint(0)
+ build = ctypes.c_uint(0)
+ rev = ctypes.c_uint(0)
+ Z3_get_version(major, minor, build, rev)
+ return (major.value, minor.value, build.value, rev.value)
+
def get_full_version():
- return Z3_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:
raise Z3Exception(msg)
+
def _z3_check_cint_overflow(n, name):
_z3_assert(ctypes.c_int(n).value == n, name + " is too large")
+
def open_log(fname):
"""Log interaction to a file. This function must be invoked immediately after init(). """
Z3_open_log(fname)
+
def append_log(s):
"""Append user-defined string to interaction log. """
Z3_append_log(s)
+
def to_symbol(s, ctx=None):
"""Convert an integer or string into a Z3 symbol."""
if _is_int(s):
@@ -117,6 +133,7 @@ def to_symbol(s, ctx=None):
else:
return Z3_mk_string_symbol(_get_ctx(ctx).ref(), s)
+
def _symbol2py(ctx, s):
"""Convert a Z3 symbol back into a Python object. """
if Z3_get_symbol_kind(ctx.ref(), s) == Z3_INT_SYMBOL:
@@ -127,41 +144,44 @@ def _symbol2py(ctx, s):
# Hack for having nary functions that can receive one argument that is the
# list of arguments.
# Use this when function takes a single list of arguments
+
+
def _get_args(args):
- try:
- if len(args) == 1 and (isinstance(args[0], tuple) or isinstance(args[0], list)):
+ try:
+ if len(args) == 1 and (isinstance(args[0], tuple) or isinstance(args[0], list)):
return args[0]
- elif len(args) == 1 and (isinstance(args[0], set) or isinstance(args[0], AstVector)):
+ elif len(args) == 1 and (isinstance(args[0], set) or isinstance(args[0], AstVector)):
return [arg for arg in args[0]]
- else:
+ else:
return args
- except: # len is not necessarily defined when args is not a sequence (use reflection?)
+ except TypeError: # len is not necessarily defined when args is not a sequence (use reflection?)
return args
# Use this when function takes multiple arguments
+
+
def _get_args_ast_list(args):
try:
- if isinstance(args, set) or isinstance(args, AstVector) or isinstance(args, tuple):
+ if isinstance(args, (set, AstVector, tuple)):
return [arg for arg in args]
else:
return args
- except:
+ except Exception:
return args
+
def _to_param_value(val):
if isinstance(val, bool):
- if val == True:
- return "true"
- else:
- return "false"
- else:
- return str(val)
+ return "true" if val else "false"
+ return str(val)
+
def z3_error_handler(c, e):
# Do nothing error handler, just avoid exit(0)
# The wrappers in z3core.py will raise a Z3Exception if an error is detected
return
+
class Context:
"""A Context manages all other Z3 objects, global configuration options, etc.
@@ -173,6 +193,7 @@ class Context:
computation.
The initialization method receives global configuration options for the new context.
"""
+
def __init__(self, *args, **kws):
if z3_debug():
_z3_assert(len(args) % 2 == 0, "Argument list must have an even number of elements.")
@@ -212,6 +233,8 @@ class Context:
# Global Z3 context
_main_ctx = None
+
+
def main_ctx():
"""Return a reference to the global Z3 context.
@@ -232,15 +255,18 @@ def main_ctx():
_main_ctx = Context()
return _main_ctx
+
def _get_ctx(ctx):
if ctx is None:
return main_ctx()
else:
return ctx
+
def get_ctx(ctx):
return _get_ctx(ctx)
+
def set_param(*args, **kws):
"""Set Z3 global (or module) parameters.
@@ -264,16 +290,19 @@ def set_param(*args, **kws):
Z3_global_param_set(str(prev), _to_param_value(a))
prev = None
+
def reset_params():
"""Reset all global (or module) parameters.
"""
Z3_global_param_reset_all()
+
def set_option(*args, **kws):
"""Alias for 'set_param' for backward compatibility.
"""
return set_param(*args, **kws)
+
def get_param(name):
"""Return the value of a Z3 global (or module) parameter
@@ -293,8 +322,11 @@ def get_param(name):
#########################################
# Mark objects that use pretty printer
+
+
class Z3PPObject:
"""Superclass for all Z3 objects that have support for pretty printing."""
+
def use_pp(self):
return True
@@ -308,15 +340,16 @@ class Z3PPObject:
class AstRef(Z3PPObject):
"""AST are Direct Acyclic Graphs (DAGs) used to represent sorts, declarations and expressions."""
+
def __init__(self, ast, ctx=None):
- self.ast = ast
- self.ctx = _get_ctx(ctx)
+ self.ast = ast
+ self.ctx = _get_ctx(ctx)
Z3_inc_ref(self.ctx.ref(), self.as_ast())
def __del__(self):
if self.ctx.ref() is not None and self.ast is not None:
- Z3_dec_ref(self.ctx.ref(), self.as_ast())
- self.ast = None
+ Z3_dec_ref(self.ctx.ref(), self.as_ast())
+ self.ast = None
def __deepcopy__(self, memo={}):
return _to_ast_ref(self.ast, self.ctx)
@@ -342,7 +375,7 @@ class AstRef(Z3PPObject):
elif is_false(self):
return False
elif is_eq(self) and self.num_args() == 2:
- return self.arg(0).eq(self.arg(1))
+ return self.arg(0).eq(self.arg(1))
else:
raise Z3Exception("Symbolic expressions cannot be cast to concrete Boolean values.")
@@ -413,6 +446,7 @@ class AstRef(Z3PPObject):
"""
return Z3_get_ast_hash(self.ctx_ref(), self.as_ast())
+
def is_ast(a):
"""Return `True` if `a` is an AST node.
@@ -433,6 +467,7 @@ def is_ast(a):
"""
return isinstance(a, AstRef)
+
def eq(a, b):
"""Return `True` if `a` and `b` are structurally identical AST nodes.
@@ -451,11 +486,13 @@ def eq(a, b):
_z3_assert(is_ast(a) and is_ast(b), "Z3 ASTs expected")
return a.eq(b)
+
def _ast_kind(ctx, a):
if is_ast(a):
a = a.as_ast()
return Z3_get_ast_kind(ctx.ref(), a)
+
def _ctx_from_ast_arg_list(args, default_ctx=None):
ctx = None
for a in args:
@@ -469,9 +506,11 @@ def _ctx_from_ast_arg_list(args, default_ctx=None):
ctx = default_ctx
return ctx
+
def _ctx_from_ast_args(*args):
return _ctx_from_ast_arg_list(args)
+
def _to_func_decl_array(args):
sz = len(args)
_args = (FuncDecl * sz)()
@@ -479,6 +518,7 @@ def _to_func_decl_array(args):
_args[i] = args[i].as_func_decl()
return _args, sz
+
def _to_ast_array(args):
sz = len(args)
_args = (Ast * sz)()
@@ -486,6 +526,7 @@ def _to_ast_array(args):
_args[i] = args[i].as_ast()
return _args, sz
+
def _to_ref_array(ref, args):
sz = len(args)
_args = (ref * sz)()
@@ -493,6 +534,7 @@ def _to_ref_array(ref, args):
_args[i] = args[i].as_ast()
return _args, sz
+
def _to_ast_ref(a, ctx):
k = _ast_kind(ctx, a)
if k == Z3_SORT_AST:
@@ -512,8 +554,10 @@ def _to_ast_ref(a, ctx):
def _sort_kind(ctx, s):
return Z3_get_sort_kind(ctx.ref(), s)
+
class SortRef(AstRef):
"""A Sort is essentially a type. Every Z3 expression has a sort. A sort is an AST node."""
+
def as_ast(self):
return Z3_sort_to_ast(self.ctx_ref(), self.ast)
@@ -521,7 +565,8 @@ class SortRef(AstRef):
return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
def kind(self):
- """Return the Z3 internal kind of a sort. This method can be used to test if `self` is one of the Z3 builtin sorts.
+ """Return the Z3 internal kind of a sort.
+ This method can be used to test if `self` is one of the Z3 builtin sorts.
>>> b = BoolSort()
>>> b.kind() == Z3_BOOL_SORT
@@ -597,6 +642,7 @@ class SortRef(AstRef):
""" Hash code. """
return AstRef.__hash__(self)
+
def is_sort(s):
"""Return `True` if `s` is a Z3 sort.
@@ -609,6 +655,7 @@ def is_sort(s):
"""
return isinstance(s, SortRef)
+
def _to_sort_ref(s, ctx):
if z3_debug():
_z3_assert(isinstance(s, Sort), "Z3 Sort expected")
@@ -635,9 +682,11 @@ def _to_sort_ref(s, ctx):
return SeqSortRef(s, ctx)
return SortRef(s, ctx)
+
def _sort(ctx, a):
return _to_sort_ref(Z3_get_sort(ctx.ref(), a), ctx)
+
def DeclareSort(name, ctx=None):
"""Create a new uninterpreted sort named `name`.
@@ -662,6 +711,7 @@ def DeclareSort(name, ctx=None):
#
#########################################
+
class FuncDeclRef(AstRef):
"""Function declaration. Every constant and function have an associated declaration.
@@ -669,6 +719,7 @@ class FuncDeclRef(AstRef):
the sort (i.e., type) of each of its arguments. Note that, in Z3,
a constant is a function with 0 arguments.
"""
+
def as_ast(self):
return Z3_func_decl_to_ast(self.ctx_ref(), self.ast)
@@ -690,7 +741,8 @@ class FuncDeclRef(AstRef):
return _symbol2py(self.ctx, Z3_get_decl_name(self.ctx_ref(), self.ast))
def arity(self):
- """Return the number of arguments of a function declaration. If `self` is a constant, then `self.arity()` is 0.
+ """Return the number of arguments of a function declaration.
+ If `self` is a constant, then `self.arity()` is 0.
>>> f = Function('f', IntSort(), RealSort(), BoolSort())
>>> f.arity()
@@ -699,7 +751,8 @@ class FuncDeclRef(AstRef):
return int(Z3_get_arity(self.ctx_ref(), self.ast))
def domain(self, i):
- """Return the sort of the argument `i` of a function declaration. This method assumes that `0 <= i < self.arity()`.
+ """Return the sort of the argument `i` of a function declaration.
+ This method assumes that `0 <= i < self.arity()`.
>>> f = Function('f', IntSort(), RealSort(), BoolSort())
>>> f.domain(0)
@@ -712,7 +765,8 @@ class FuncDeclRef(AstRef):
return _to_sort_ref(Z3_get_domain(self.ctx_ref(), self.ast, i), self.ctx)
def range(self):
- """Return the sort of the range of a function declaration. For constants, this is the sort of the constant.
+ """Return the sort of the range of a function declaration.
+ For constants, this is the sort of the constant.
>>> f = Function('f', IntSort(), RealSort(), BoolSort())
>>> f.range()
@@ -721,7 +775,8 @@ class FuncDeclRef(AstRef):
return _to_sort_ref(Z3_get_range(self.ctx_ref(), self.ast), self.ctx)
def kind(self):
- """Return the internal kind of a function declaration. It can be used to identify Z3 built-in functions such as addition, multiplication, etc.
+ """Return the internal kind of a function declaration.
+ It can be used to identify Z3 built-in functions such as addition, multiplication, etc.
>>> x = Int('x')
>>> d = (x + 1).decl()
@@ -735,25 +790,25 @@ class FuncDeclRef(AstRef):
def params(self):
ctx = self.ctx
n = Z3_get_decl_num_parameters(self.ctx_ref(), self.ast)
- result = [ None for i in range(n) ]
+ result = [None for i in range(n)]
for i in range(n):
k = Z3_get_decl_parameter_kind(self.ctx_ref(), self.ast, i)
if k == Z3_PARAMETER_INT:
- result[i] = Z3_get_decl_int_parameter(self.ctx_ref(), self.ast, i)
+ result[i] = Z3_get_decl_int_parameter(self.ctx_ref(), self.ast, i)
elif k == Z3_PARAMETER_DOUBLE:
- result[i] = Z3_get_decl_double_parameter(self.ctx_ref(), self.ast, i)
+ result[i] = Z3_get_decl_double_parameter(self.ctx_ref(), self.ast, i)
elif k == Z3_PARAMETER_RATIONAL:
- result[i] = Z3_get_decl_rational_parameter(self.ctx_ref(), self.ast, i)
+ result[i] = Z3_get_decl_rational_parameter(self.ctx_ref(), self.ast, i)
elif k == Z3_PARAMETER_SYMBOL:
- result[i] = Z3_get_decl_symbol_parameter(self.ctx_ref(), self.ast, i)
+ result[i] = Z3_get_decl_symbol_parameter(self.ctx_ref(), self.ast, i)
elif k == Z3_PARAMETER_SORT:
- result[i] = SortRef(Z3_get_decl_sort_parameter(self.ctx_ref(), self.ast, i), ctx)
+ result[i] = SortRef(Z3_get_decl_sort_parameter(self.ctx_ref(), self.ast, i), ctx)
elif k == Z3_PARAMETER_AST:
- result[i] = ExprRef(Z3_get_decl_ast_parameter(self.ctx_ref(), self.ast, i), ctx)
+ result[i] = ExprRef(Z3_get_decl_ast_parameter(self.ctx_ref(), self.ast, i), ctx)
elif k == Z3_PARAMETER_FUNC_DECL:
- result[i] = FuncDeclRef(Z3_get_decl_func_decl_parameter(self.ctx_ref(), self.ast, i), ctx)
+ result[i] = FuncDeclRef(Z3_get_decl_func_decl_parameter(self.ctx_ref(), self.ast, i), ctx)
else:
- assert(False)
+ assert(False)
return result
def __call__(self, *args):
@@ -783,11 +838,12 @@ class FuncDeclRef(AstRef):
for i in range(num):
# self.domain(i).cast(args[i]) may create a new Z3 expression,
# then we must save in 'saved' to prevent it from being garbage collected.
- tmp = self.domain(i).cast(args[i])
+ tmp = self.domain(i).cast(args[i])
saved.append(tmp)
_args[i] = tmp.as_ast()
return _to_expr_ref(Z3_mk_app(self.ctx_ref(), self.ast, len(args), _args), self.ctx)
+
def is_func_decl(a):
"""Return `True` if `a` is a Z3 function declaration.
@@ -800,6 +856,7 @@ def is_func_decl(a):
"""
return isinstance(a, FuncDeclRef)
+
def Function(name, *sig):
"""Create a new Z3 uninterpreted function with the given sorts.
@@ -811,10 +868,10 @@ def Function(name, *sig):
if z3_debug():
_z3_assert(len(sig) > 0, "At least two arguments expected")
arity = len(sig) - 1
- rng = sig[arity]
+ rng = sig[arity]
if z3_debug():
_z3_assert(is_sort(rng), "Z3 sort expected")
- dom = (Sort * arity)()
+ dom = (Sort * arity)()
for i in range(arity):
if z3_debug():
_z3_assert(is_sort(sig[i]), "Z3 sort expected")
@@ -822,6 +879,7 @@ def Function(name, *sig):
ctx = rng.ctx
return FuncDeclRef(Z3_mk_func_decl(ctx.ref(), to_symbol(name, ctx), arity, dom, rng.ast), ctx)
+
def FreshFunction(*sig):
"""Create a new fresh Z3 uninterpreted function with the given sorts.
"""
@@ -838,22 +896,23 @@ def FreshFunction(*sig):
_z3_assert(is_sort(sig[i]), "Z3 sort expected")
dom[i] = sig[i].ast
ctx = rng.ctx
- return FuncDeclRef(Z3_mk_fresh_func_decl(ctx.ref(), 'f', arity, dom, rng.ast), ctx)
+ return FuncDeclRef(Z3_mk_fresh_func_decl(ctx.ref(), "f", arity, dom, rng.ast), ctx)
def _to_func_decl_ref(a, ctx):
return FuncDeclRef(a, ctx)
+
def RecFunction(name, *sig):
"""Create a new Z3 recursive with the given sorts."""
sig = _get_args(sig)
if z3_debug():
_z3_assert(len(sig) > 0, "At least two arguments expected")
arity = len(sig) - 1
- rng = sig[arity]
+ rng = sig[arity]
if z3_debug():
_z3_assert(is_sort(rng), "Z3 sort expected")
- dom = (Sort * arity)()
+ dom = (Sort * arity)()
for i in range(arity):
if z3_debug():
_z3_assert(is_sort(sig[i]), "Z3 sort expected")
@@ -861,10 +920,11 @@ def RecFunction(name, *sig):
ctx = rng.ctx
return FuncDeclRef(Z3_mk_rec_func_decl(ctx.ref(), to_symbol(name, ctx), arity, dom, rng.ast), ctx)
+
def RecAddDefinition(f, args, body):
"""Set the body of a recursive function.
Recursive definitions can be simplified if they are applied to ground
- arguments.
+ arguments.
>>> ctx = Context()
>>> fac = RecFunction('fac', IntSort(ctx), IntSort(ctx))
>>> n = Int('n', ctx)
@@ -879,7 +939,7 @@ def RecAddDefinition(f, args, body):
120
"""
if is_app(args):
- args = [args]
+ args = [args]
ctx = body.ctx
args = _get_args(args)
n = len(args)
@@ -894,6 +954,7 @@ def RecAddDefinition(f, args, body):
#
#########################################
+
class ExprRef(AstRef):
"""Constraints, formulas and terms are expressions in Z3.
@@ -904,6 +965,7 @@ class ExprRef(AstRef):
For quantifier free problems, all expressions are
function applications.
"""
+
def as_ast(self):
return self.ast
@@ -1042,6 +1104,7 @@ class ExprRef(AstRef):
else:
return []
+
def _to_expr_ref(a, ctx):
if isinstance(a, Pattern):
return PatternRef(a, ctx)
@@ -1089,6 +1152,7 @@ def _to_expr_ref(a, ctx):
return ReRef(a, ctx)
return ExprRef(a, ctx)
+
def _coerce_expr_merge(s, a):
if is_expr(a):
s1 = a.sort()
@@ -1107,6 +1171,7 @@ def _coerce_expr_merge(s, a):
else:
return s
+
def _coerce_exprs(a, b, ctx=None):
if not is_expr(a) and not is_expr(b):
a = _py2expr(a, ctx)
@@ -1129,6 +1194,7 @@ def _reduce(f, l, a):
r = f(r, e)
return r
+
def _coerce_expr_list(alist, ctx=None):
has_expr = False
for a in alist:
@@ -1136,9 +1202,10 @@ def _coerce_expr_list(alist, ctx=None):
has_expr = True
break
if not has_expr:
- alist = [ _py2expr(a, ctx) for a in alist ]
+ alist = [_py2expr(a, ctx) for a in alist]
s = _reduce(_coerce_expr_merge, alist, None)
- return [ s.cast(a) for a in alist ]
+ return [s.cast(a) for a in alist]
+
def is_expr(a):
"""Return `True` if `a` is a Z3 expression.
@@ -1162,6 +1229,7 @@ def is_expr(a):
"""
return isinstance(a, ExprRef)
+
def is_app(a):
"""Return `True` if `a` is a Z3 function application.
@@ -1187,6 +1255,7 @@ def is_app(a):
k = _ast_kind(a.ctx, a)
return k == Z3_NUMERAL_AST or k == Z3_APP_AST
+
def is_const(a):
"""Return `True` if `a` is Z3 constant/variable expression.
@@ -1205,6 +1274,7 @@ def is_const(a):
"""
return is_app(a) and a.num_args() == 0
+
def is_var(a):
"""Return `True` if `a` is variable.
@@ -1229,6 +1299,7 @@ def is_var(a):
"""
return is_expr(a) and _ast_kind(a.ctx, a) == Z3_VAR_AST
+
def get_var_index(a):
"""Return the de-Bruijn index of the Z3 bounded variable `a`.
@@ -1261,6 +1332,7 @@ def get_var_index(a):
_z3_assert(is_var(a), "Z3 bound variable expected")
return int(Z3_get_index_value(a.ctx.ref(), a.as_ast()))
+
def is_app_of(a, k):
"""Return `True` if `a` is an application of the given kind `k`.
@@ -1273,6 +1345,7 @@ def is_app_of(a, k):
"""
return is_app(a) and a.decl().kind() == k
+
def If(a, b, c, ctx=None):
"""Create a Z3 if-then-else expression.
@@ -1295,6 +1368,7 @@ def If(a, b, c, ctx=None):
_z3_assert(a.ctx == b.ctx, "Context mismatch")
return _to_expr_ref(Z3_mk_ite(ctx.ref(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)
+
def Distinct(*args):
"""Create a Z3 distinct expression.
@@ -1310,14 +1384,15 @@ def Distinct(*args):
>>> simplify(Distinct(x, y, z), blast_distinct=True)
And(Not(x == y), Not(x == z), Not(y == z))
"""
- args = _get_args(args)
- ctx = _ctx_from_ast_arg_list(args)
+ args = _get_args(args)
+ ctx = _ctx_from_ast_arg_list(args)
if z3_debug():
_z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
- args = _coerce_expr_list(args, ctx)
+ args = _coerce_expr_list(args, ctx)
_args, sz = _to_ast_array(args)
return BoolRef(Z3_mk_distinct(ctx.ref(), sz, _args), ctx)
+
def _mk_bin(f, a, b):
args = (Ast * 2)()
if z3_debug():
@@ -1326,6 +1401,7 @@ def _mk_bin(f, a, b):
args[1] = b.as_ast()
return f(a.ctx.ref(), 2, args)
+
def Const(name, sort):
"""Create a constant of the given sort.
@@ -1337,6 +1413,7 @@ def Const(name, sort):
ctx = sort.ctx
return _to_expr_ref(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), sort.ast), ctx)
+
def Consts(names, sort):
"""Create several constants of the given sort.
@@ -1351,11 +1428,13 @@ def Consts(names, sort):
names = names.split(" ")
return [Const(name, sort) for name in names]
-def FreshConst(sort, prefix='c'):
+
+def FreshConst(sort, prefix="c"):
"""Create a fresh constant of a specified sort"""
ctx = _get_ctx(sort.ctx)
return _to_expr_ref(Z3_mk_fresh_const(ctx.ref(), prefix, sort.ast), ctx)
+
def Var(idx, s):
"""Create a Z3 free variable. Free variables are used to create quantified formulas.
@@ -1368,6 +1447,7 @@ def Var(idx, s):
_z3_assert(is_sort(s), "Z3 sort expected")
return _to_expr_ref(Z3_mk_bound(s.ctx_ref(), idx, s.ast), s.ctx)
+
def RealVar(idx, ctx=None):
"""
Create a real free variable. Free variables are used to create quantified formulas.
@@ -1378,6 +1458,7 @@ def RealVar(idx, ctx=None):
"""
return Var(idx, RealSort(ctx))
+
def RealVarVector(n, ctx=None):
"""
Create a list of Real free variables.
@@ -1387,7 +1468,7 @@ def RealVarVector(n, ctx=None):
>>> x2
Var(2)
"""
- return [ RealVar(i, ctx) for i in range(n) ]
+ return [RealVar(i, ctx) for i in range(n)]
#########################################
#
@@ -1395,8 +1476,10 @@ def RealVarVector(n, ctx=None):
#
#########################################
+
class BoolSortRef(SortRef):
"""Boolean sort."""
+
def cast(self, val):
"""Try to cast `val` as a Boolean.
@@ -1414,9 +1497,10 @@ class BoolSortRef(SortRef):
return BoolVal(val, self.ctx)
if z3_debug():
if not is_expr(val):
- _z3_assert(is_expr(val), "True, False or Z3 Boolean expression expected. Received %s of type %s" % (val, type(val)))
+ msg = "True, False or Z3 Boolean expression expected. Received %s of type %s"
+ _z3_assert(is_expr(val), msg % (val, type(val)))
if not self.eq(val.sort()):
- _z3_assert(self.eq(val.sort()), "Value cannot be converted into a Z3 Boolean value")
+ _z3_assert(self.eq(val.sort()), "Value cannot be converted into a Z3 Boolean value")
return val
def subsort(self, other):
@@ -1431,6 +1515,7 @@ class BoolSortRef(SortRef):
class BoolRef(ExprRef):
"""All Boolean expressions are instances of this class."""
+
def sort(self):
return BoolSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
@@ -1464,6 +1549,7 @@ def is_bool(a):
"""
return isinstance(a, BoolRef)
+
def is_true(a):
"""Return `True` if `a` is the Z3 true expression.
@@ -1481,6 +1567,7 @@ def is_true(a):
"""
return is_app_of(a, Z3_OP_TRUE)
+
def is_false(a):
"""Return `True` if `a` is the Z3 false expression.
@@ -1494,6 +1581,7 @@ def is_false(a):
"""
return is_app_of(a, Z3_OP_FALSE)
+
def is_and(a):
"""Return `True` if `a` is a Z3 and expression.
@@ -1505,6 +1593,7 @@ def is_and(a):
"""
return is_app_of(a, Z3_OP_AND)
+
def is_or(a):
"""Return `True` if `a` is a Z3 or expression.
@@ -1516,6 +1605,7 @@ def is_or(a):
"""
return is_app_of(a, Z3_OP_OR)
+
def is_implies(a):
"""Return `True` if `a` is a Z3 implication expression.
@@ -1527,6 +1617,7 @@ def is_implies(a):
"""
return is_app_of(a, Z3_OP_IMPLIES)
+
def is_not(a):
"""Return `True` if `a` is a Z3 not expression.
@@ -1538,6 +1629,7 @@ def is_not(a):
"""
return is_app_of(a, Z3_OP_NOT)
+
def is_eq(a):
"""Return `True` if `a` is a Z3 equality expression.
@@ -1547,6 +1639,7 @@ def is_eq(a):
"""
return is_app_of(a, Z3_OP_EQ)
+
def is_distinct(a):
"""Return `True` if `a` is a Z3 distinct expression.
@@ -1558,6 +1651,7 @@ def is_distinct(a):
"""
return is_app_of(a, Z3_OP_DISTINCT)
+
def BoolSort(ctx=None):
"""Return the Boolean Z3 sort. If `ctx=None`, then the global context is used.
@@ -1575,6 +1669,7 @@ def BoolSort(ctx=None):
ctx = _get_ctx(ctx)
return BoolSortRef(Z3_mk_bool_sort(ctx.ref()), ctx)
+
def BoolVal(val, ctx=None):
"""Return the Boolean value `True` or `False`. If `ctx=None`, then the global context is used.
@@ -1588,10 +1683,11 @@ def BoolVal(val, ctx=None):
True
"""
ctx = _get_ctx(ctx)
- if val == False:
- return BoolRef(Z3_mk_false(ctx.ref()), ctx)
- else:
+ if val:
return BoolRef(Z3_mk_true(ctx.ref()), ctx)
+ else:
+ return BoolRef(Z3_mk_false(ctx.ref()), ctx)
+
def Bool(name, ctx=None):
"""Return a Boolean constant named `name`. If `ctx=None`, then the global context is used.
@@ -1604,6 +1700,7 @@ def Bool(name, ctx=None):
ctx = _get_ctx(ctx)
return BoolRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), BoolSort(ctx).ast), ctx)
+
def Bools(names, ctx=None):
"""Return a tuple of Boolean constants.
@@ -1619,6 +1716,7 @@ def Bools(names, ctx=None):
names = names.split(" ")
return [Bool(name, ctx) for name in names]
+
def BoolVector(prefix, sz, ctx=None):
"""Return a list of Boolean constants of size `sz`.
@@ -1631,9 +1729,10 @@ def BoolVector(prefix, sz, ctx=None):
>>> And(P)
And(p__0, p__1, p__2)
"""
- return [ Bool('%s__%s' % (prefix, i)) for i in range(sz) ]
+ return [Bool("%s__%s" % (prefix, i)) for i in range(sz)]
-def FreshBool(prefix='b', ctx=None):
+
+def FreshBool(prefix="b", ctx=None):
"""Return a fresh Boolean constant in the given context using the given prefix.
If `ctx=None`, then the global context is used.
@@ -1646,6 +1745,7 @@ def FreshBool(prefix='b', ctx=None):
ctx = _get_ctx(ctx)
return BoolRef(Z3_mk_fresh_const(ctx.ref(), prefix, BoolSort(ctx).ast), ctx)
+
def Implies(a, b, ctx=None):
"""Create a Z3 implies expression.
@@ -1659,6 +1759,7 @@ def Implies(a, b, ctx=None):
b = s.cast(b)
return BoolRef(Z3_mk_implies(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
+
def Xor(a, b, ctx=None):
"""Create a Z3 Xor expression.
@@ -1674,6 +1775,7 @@ def Xor(a, b, ctx=None):
b = s.cast(b)
return BoolRef(Z3_mk_xor(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
+
def Not(a, ctx=None):
"""Create a Z3 not expression or probe.
@@ -1692,12 +1794,14 @@ def Not(a, ctx=None):
a = s.cast(a)
return BoolRef(Z3_mk_not(ctx.ref(), a.as_ast()), ctx)
+
def mk_not(a):
if is_not(a):
return a.arg(0)
else:
return Not(a)
+
def _has_probe(args):
"""Return `True` if one of the elements of the given collection is a Z3 probe."""
for arg in args:
@@ -1705,6 +1809,7 @@ def _has_probe(args):
return True
return False
+
def And(*args):
"""Create a Z3 and-expression or and-probe.
@@ -1717,26 +1822,27 @@ def And(*args):
"""
last_arg = None
if len(args) > 0:
- last_arg = args[len(args)-1]
+ last_arg = args[len(args) - 1]
if isinstance(last_arg, Context):
- ctx = args[len(args)-1]
- args = args[:len(args)-1]
+ ctx = args[len(args) - 1]
+ args = args[:len(args) - 1]
elif len(args) == 1 and isinstance(args[0], AstVector):
ctx = args[0].ctx
args = [a for a in args[0]]
else:
ctx = None
args = _get_args(args)
- ctx = _get_ctx(_ctx_from_ast_arg_list(args, ctx))
+ ctx = _get_ctx(_ctx_from_ast_arg_list(args, ctx))
if z3_debug():
_z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression or probe")
if _has_probe(args):
return _probe_and(args, ctx)
else:
- args = _coerce_expr_list(args, ctx)
+ args = _coerce_expr_list(args, ctx)
_args, sz = _to_ast_array(args)
return BoolRef(Z3_mk_and(ctx.ref(), sz, _args), ctx)
+
def Or(*args):
"""Create a Z3 or-expression or or-probe.
@@ -1749,23 +1855,23 @@ def Or(*args):
"""
last_arg = None
if len(args) > 0:
- last_arg = args[len(args)-1]
+ last_arg = args[len(args) - 1]
if isinstance(last_arg, Context):
- ctx = args[len(args)-1]
- args = args[:len(args)-1]
+ ctx = args[len(args) - 1]
+ args = args[:len(args) - 1]
elif len(args) == 1 and isinstance(args[0], AstVector):
ctx = args[0].ctx
args = [a for a in args[0]]
else:
ctx = None
args = _get_args(args)
- ctx = _get_ctx(_ctx_from_ast_arg_list(args, ctx))
+ ctx = _get_ctx(_ctx_from_ast_arg_list(args, ctx))
if z3_debug():
_z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression or probe")
if _has_probe(args):
return _probe_or(args, ctx)
else:
- args = _coerce_expr_list(args, ctx)
+ args = _coerce_expr_list(args, ctx)
_args, sz = _to_ast_array(args)
return BoolRef(Z3_mk_or(ctx.ref(), sz, _args), ctx)
@@ -1775,16 +1881,19 @@ def Or(*args):
#
#########################################
+
class PatternRef(ExprRef):
"""Patterns are hints for quantifier instantiation.
"""
+
def as_ast(self):
return Z3_pattern_to_ast(self.ctx_ref(), self.ast)
def get_id(self):
return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
+
def is_pattern(a):
"""Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation.
@@ -1802,6 +1911,7 @@ def is_pattern(a):
"""
return isinstance(a, PatternRef)
+
def MultiPattern(*args):
"""Create a Z3 multi-pattern using the given expressions `*args`
@@ -1820,11 +1930,12 @@ def MultiPattern(*args):
"""
if z3_debug():
_z3_assert(len(args) > 0, "At least one argument expected")
- _z3_assert(all([ is_expr(a) for a in args ]), "Z3 expressions expected")
+ _z3_assert(all([is_expr(a) for a in args]), "Z3 expressions expected")
ctx = args[0].ctx
args, sz = _to_ast_array(args)
return PatternRef(Z3_mk_pattern(ctx.ref(), sz, args), ctx)
+
def _to_pattern(arg):
if is_pattern(arg):
return arg
@@ -1837,6 +1948,7 @@ def _to_pattern(arg):
#
#########################################
+
class QuantifierRef(BoolRef):
"""Universally and Existentially quantified formulas."""
@@ -1901,7 +2013,6 @@ class QuantifierRef(BoolRef):
_z3_assert(self.is_lambda(), "quantifier should be a lambda expression")
arg = self.sort().domain().cast(arg)
return _to_expr_ref(Z3_mk_select(self.ctx_ref(), self.as_ast(), arg.as_ast()), self.ctx)
-
def weight(self):
"""Return the weight annotation of `self`.
@@ -2021,7 +2132,8 @@ class QuantifierRef(BoolRef):
>>> q.children()
[f(Var(0)) == 0]
"""
- return [ self.body() ]
+ return [self.body()]
+
def is_quantifier(a):
"""Return `True` if `a` is a Z3 quantifier.
@@ -2036,10 +2148,11 @@ def is_quantifier(a):
"""
return isinstance(a, QuantifierRef)
+
def _mk_quantifier(is_forall, vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
if z3_debug():
_z3_assert(is_bool(body) or is_app(vs) or (len(vs) > 0 and is_app(vs[0])), "Z3 expression expected")
- _z3_assert(is_const(vs) or (len(vs) > 0 and all([ is_const(v) for v in vs])), "Invalid bounded variable(s)")
+ _z3_assert(is_const(vs) or (len(vs) > 0 and all([is_const(v) for v in vs])), "Invalid bounded variable(s)")
_z3_assert(all([is_pattern(a) or is_expr(a) for a in patterns]), "Z3 patterns expected")
_z3_assert(all([is_expr(p) for p in no_patterns]), "no patterns are Z3 expressions")
if is_app(vs):
@@ -2048,21 +2161,21 @@ def _mk_quantifier(is_forall, vs, body, weight=1, qid="", skid="", patterns=[],
else:
ctx = vs[0].ctx
if not is_expr(body):
- body = BoolVal(body, ctx)
+ body = BoolVal(body, ctx)
num_vars = len(vs)
if num_vars == 0:
return body
_vs = (Ast * num_vars)()
for i in range(num_vars):
- ## TODO: Check if is constant
+ # TODO: Check if is constant
_vs[i] = vs[i].as_ast()
- patterns = [ _to_pattern(p) for p in patterns ]
+ patterns = [_to_pattern(p) for p in patterns]
num_pats = len(patterns)
_pats = (Pattern * num_pats)()
for i in range(num_pats):
_pats[i] = patterns[i].ast
_no_pats, num_no_pats = _to_ast_array(no_patterns)
- qid = to_symbol(qid, ctx)
+ qid = to_symbol(qid, ctx)
skid = to_symbol(skid, ctx)
return QuantifierRef(Z3_mk_quantifier_const_ex(ctx.ref(), is_forall, weight, qid, skid,
num_vars, _vs,
@@ -2070,6 +2183,7 @@ def _mk_quantifier(is_forall, vs, body, weight=1, qid="", skid="", patterns=[],
num_no_pats, _no_pats,
body.as_ast()), ctx)
+
def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
"""Create a Z3 forall formula.
@@ -2087,6 +2201,7 @@ def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
"""
return _mk_quantifier(True, vs, body, weight, qid, skid, patterns, no_patterns)
+
def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
"""Create a Z3 exists formula.
@@ -2107,6 +2222,7 @@ def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]):
"""
return _mk_quantifier(False, vs, body, weight, qid, skid, patterns, no_patterns)
+
def Lambda(vs, body):
"""Create a Z3 lambda expression.
@@ -2123,7 +2239,7 @@ def Lambda(vs, body):
num_vars = len(vs)
_vs = (Ast * num_vars)()
for i in range(num_vars):
- ## TODO: Check if is constant
+ # TODO: Check if is constant
_vs[i] = vs[i].as_ast()
return QuantifierRef(Z3_mk_lambda_const(ctx.ref(), num_vars, _vs, body.as_ast()), ctx)
@@ -2133,6 +2249,7 @@ def Lambda(vs, body):
#
#########################################
+
class ArithSortRef(SortRef):
"""Real and Integer sorts."""
@@ -2195,14 +2312,16 @@ class ArithSortRef(SortRef):
if val_s.is_bool() and self.is_real():
return ToReal(If(val, 1, 0))
if z3_debug():
- _z3_assert(False, "Z3 Integer/Real expression expected" )
+ _z3_assert(False, "Z3 Integer/Real expression expected")
else:
if self.is_int():
return IntVal(val, self.ctx)
if self.is_real():
return RealVal(val, self.ctx)
if z3_debug():
- _z3_assert(False, "int, long, float, string (numeral), or Z3 Integer/Real expression expected. Got %s" % self)
+ msg = "int, long, float, string (numeral), or Z3 Integer/Real expression expected. Got %s"
+ _z3_assert(False, msg % self)
+
def is_arith_sort(s):
"""Return `True` if s is an arithmetical sort (type).
@@ -2219,6 +2338,7 @@ def is_arith_sort(s):
"""
return isinstance(s, ArithSortRef)
+
class ArithRef(ExprRef):
"""Integer and Real expressions."""
@@ -2291,7 +2411,7 @@ class ArithRef(ExprRef):
Real
"""
if isinstance(other, BoolRef):
- return If(other, self, 0)
+ return If(other, self, 0)
a, b = _coerce_exprs(self, other)
return ArithRef(_mk_bin(Z3_mk_mul, a, b), self.ctx)
@@ -2503,6 +2623,7 @@ class ArithRef(ExprRef):
a, b = _coerce_exprs(self, other)
return BoolRef(Z3_mk_ge(self.ctx_ref(), a.as_ast(), b.as_ast()), self.ctx)
+
def is_arith(a):
"""Return `True` if `a` is an arithmetical expression.
@@ -2523,6 +2644,7 @@ def is_arith(a):
"""
return isinstance(a, ArithRef)
+
def is_int(a):
"""Return `True` if `a` is an integer expression.
@@ -2541,6 +2663,7 @@ def is_int(a):
"""
return is_arith(a) and a.is_int()
+
def is_real(a):
"""Return `True` if `a` is a real expression.
@@ -2559,12 +2682,15 @@ def is_real(a):
"""
return is_arith(a) and a.is_real()
+
def _is_numeral(ctx, a):
return Z3_is_numeral_ast(ctx.ref(), a)
+
def _is_algebraic(ctx, a):
return Z3_is_algebraic_number(ctx.ref(), a)
+
def is_int_value(a):
"""Return `True` if `a` is an integer value of sort Int.
@@ -2588,6 +2714,7 @@ def is_int_value(a):
"""
return is_arith(a) and a.is_int() and _is_numeral(a.ctx, a.as_ast())
+
def is_rational_value(a):
"""Return `True` if `a` is rational value of sort Real.
@@ -2609,6 +2736,7 @@ def is_rational_value(a):
"""
return is_arith(a) and a.is_real() and _is_numeral(a.ctx, a.as_ast())
+
def is_algebraic_value(a):
"""Return `True` if `a` is an algebraic value of sort Real.
@@ -2622,6 +2750,7 @@ def is_algebraic_value(a):
"""
return is_arith(a) and a.is_real() and _is_algebraic(a.ctx, a.as_ast())
+
def is_add(a):
"""Return `True` if `a` is an expression of the form b + c.
@@ -2633,6 +2762,7 @@ def is_add(a):
"""
return is_app_of(a, Z3_OP_ADD)
+
def is_mul(a):
"""Return `True` if `a` is an expression of the form b * c.
@@ -2644,6 +2774,7 @@ def is_mul(a):
"""
return is_app_of(a, Z3_OP_MUL)
+
def is_sub(a):
"""Return `True` if `a` is an expression of the form b - c.
@@ -2655,6 +2786,7 @@ def is_sub(a):
"""
return is_app_of(a, Z3_OP_SUB)
+
def is_div(a):
"""Return `True` if `a` is an expression of the form b / c.
@@ -2671,6 +2803,7 @@ def is_div(a):
"""
return is_app_of(a, Z3_OP_DIV)
+
def is_idiv(a):
"""Return `True` if `a` is an expression of the form b div c.
@@ -2682,6 +2815,7 @@ def is_idiv(a):
"""
return is_app_of(a, Z3_OP_IDIV)
+
def is_mod(a):
"""Return `True` if `a` is an expression of the form b % c.
@@ -2693,6 +2827,7 @@ def is_mod(a):
"""
return is_app_of(a, Z3_OP_MOD)
+
def is_le(a):
"""Return `True` if `a` is an expression of the form b <= c.
@@ -2704,6 +2839,7 @@ def is_le(a):
"""
return is_app_of(a, Z3_OP_LE)
+
def is_lt(a):
"""Return `True` if `a` is an expression of the form b < c.
@@ -2715,6 +2851,7 @@ def is_lt(a):
"""
return is_app_of(a, Z3_OP_LT)
+
def is_ge(a):
"""Return `True` if `a` is an expression of the form b >= c.
@@ -2726,6 +2863,7 @@ def is_ge(a):
"""
return is_app_of(a, Z3_OP_GE)
+
def is_gt(a):
"""Return `True` if `a` is an expression of the form b > c.
@@ -2737,6 +2875,7 @@ def is_gt(a):
"""
return is_app_of(a, Z3_OP_GT)
+
def is_is_int(a):
"""Return `True` if `a` is an expression of the form IsInt(b).
@@ -2748,6 +2887,7 @@ def is_is_int(a):
"""
return is_app_of(a, Z3_OP_IS_INT)
+
def is_to_real(a):
"""Return `True` if `a` is an expression of the form ToReal(b).
@@ -2762,6 +2902,7 @@ def is_to_real(a):
"""
return is_app_of(a, Z3_OP_TO_REAL)
+
def is_to_int(a):
"""Return `True` if `a` is an expression of the form ToInt(b).
@@ -2776,6 +2917,7 @@ def is_to_int(a):
"""
return is_app_of(a, Z3_OP_TO_INT)
+
class IntNumRef(ArithRef):
"""Integer values."""
@@ -2808,6 +2950,7 @@ class IntNumRef(ArithRef):
"""
return Z3_get_numeral_binary_string(self.ctx_ref(), self.as_ast())
+
class RatNumRef(ArithRef):
"""Rational values."""
@@ -2904,6 +3047,7 @@ class RatNumRef(ArithRef):
"""
return Fraction(self.numerator_as_long(), self.denominator_as_long())
+
class AlgebraicNumRef(ArithRef):
"""Algebraic irrational values."""
@@ -2918,8 +3062,10 @@ class AlgebraicNumRef(ArithRef):
2965821/2097152
"""
return RatNumRef(Z3_get_algebraic_number_upper(self.ctx_ref(), self.as_ast(), precision), self.ctx)
+
def as_decimal(self, prec):
- """Return a string representation of the algebraic number `self` in decimal notation using `prec` decimal places
+ """Return a string representation of the algebraic number `self` in decimal notation
+ using `prec` decimal places.
>>> x = simplify(Sqrt(2))
>>> x.as_decimal(10)
@@ -2935,6 +3081,7 @@ class AlgebraicNumRef(ArithRef):
def index(self):
return Z3_algebraic_get_i(self.ctx_ref(), self.as_ast())
+
def _py2expr(a, ctx=None):
if isinstance(a, bool):
return BoolVal(a, ctx)
@@ -2949,6 +3096,7 @@ def _py2expr(a, ctx=None):
if z3_debug():
_z3_assert(False, "Python bool, int, long or float expected")
+
def IntSort(ctx=None):
"""Return the integer sort in the given context. If `ctx=None`, then the global context is used.
@@ -2965,6 +3113,7 @@ def IntSort(ctx=None):
ctx = _get_ctx(ctx)
return ArithSortRef(Z3_mk_int_sort(ctx.ref()), ctx)
+
def RealSort(ctx=None):
"""Return the real sort in the given context. If `ctx=None`, then the global context is used.
@@ -2981,6 +3130,7 @@ def RealSort(ctx=None):
ctx = _get_ctx(ctx)
return ArithSortRef(Z3_mk_real_sort(ctx.ref()), ctx)
+
def _to_int_str(val):
if isinstance(val, float):
return str(int(val))
@@ -2996,6 +3146,7 @@ def _to_int_str(val):
if z3_debug():
_z3_assert(False, "Python value cannot be used as a Z3 integer")
+
def IntVal(val, ctx=None):
"""Return a Z3 integer value. If `ctx=None`, then the global context is used.
@@ -3007,6 +3158,7 @@ def IntVal(val, ctx=None):
ctx = _get_ctx(ctx)
return IntNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), IntSort(ctx).ast), ctx)
+
def RealVal(val, ctx=None):
"""Return a Z3 real value.
@@ -3025,6 +3177,7 @@ def RealVal(val, ctx=None):
ctx = _get_ctx(ctx)
return RatNumRef(Z3_mk_numeral(ctx.ref(), str(val), RealSort(ctx).ast), ctx)
+
def RatVal(a, b, ctx=None):
"""Return a Z3 rational a/b.
@@ -3038,7 +3191,8 @@ def RatVal(a, b, ctx=None):
if z3_debug():
_z3_assert(_is_int(a) or isinstance(a, str), "First argument cannot be converted into an integer")
_z3_assert(_is_int(b) or isinstance(b, str), "Second argument cannot be converted into an integer")
- return simplify(RealVal(a, ctx)/RealVal(b, ctx))
+ return simplify(RealVal(a, ctx) / RealVal(b, ctx))
+
def Q(a, b, ctx=None):
"""Return a Z3 rational a/b.
@@ -3052,6 +3206,7 @@ def Q(a, b, ctx=None):
"""
return simplify(RatVal(a, b))
+
def Int(name, ctx=None):
"""Return an integer constant named `name`. If `ctx=None`, then the global context is used.
@@ -3064,6 +3219,7 @@ def Int(name, ctx=None):
ctx = _get_ctx(ctx)
return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), IntSort(ctx).ast), ctx)
+
def Ints(names, ctx=None):
"""Return a tuple of Integer constants.
@@ -3076,6 +3232,7 @@ def Ints(names, ctx=None):
names = names.split(" ")
return [Int(name, ctx) for name in names]
+
def IntVector(prefix, sz, ctx=None):
"""Return a list of integer constants of size `sz`.
@@ -3086,9 +3243,10 @@ def IntVector(prefix, sz, ctx=None):
x__0 + x__1 + x__2
"""
ctx = _get_ctx(ctx)
- return [ Int('%s__%s' % (prefix, i), ctx) for i in range(sz) ]
+ return [Int("%s__%s" % (prefix, i), ctx) for i in range(sz)]
-def FreshInt(prefix='x', ctx=None):
+
+def FreshInt(prefix="x", ctx=None):
"""Return a fresh integer constant in the given context using the given prefix.
>>> x = FreshInt()
@@ -3101,6 +3259,7 @@ def FreshInt(prefix='x', ctx=None):
ctx = _get_ctx(ctx)
return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, IntSort(ctx).ast), ctx)
+
def Real(name, ctx=None):
"""Return a real constant named `name`. If `ctx=None`, then the global context is used.
@@ -3113,6 +3272,7 @@ def Real(name, ctx=None):
ctx = _get_ctx(ctx)
return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), RealSort(ctx).ast), ctx)
+
def Reals(names, ctx=None):
"""Return a tuple of real constants.
@@ -3127,6 +3287,7 @@ def Reals(names, ctx=None):
names = names.split(" ")
return [Real(name, ctx) for name in names]
+
def RealVector(prefix, sz, ctx=None):
"""Return a list of real constants of size `sz`.
@@ -3139,9 +3300,10 @@ def RealVector(prefix, sz, ctx=None):
Real
"""
ctx = _get_ctx(ctx)
- return [ Real('%s__%s' % (prefix, i), ctx) for i in range(sz) ]
+ return [Real("%s__%s" % (prefix, i), ctx) for i in range(sz)]
-def FreshReal(prefix='b', ctx=None):
+
+def FreshReal(prefix="b", ctx=None):
"""Return a fresh real constant in the given context using the given prefix.
>>> x = FreshReal()
@@ -3154,6 +3316,7 @@ def FreshReal(prefix='b', ctx=None):
ctx = _get_ctx(ctx)
return ArithRef(Z3_mk_fresh_const(ctx.ref(), prefix, RealSort(ctx).ast), ctx)
+
def ToReal(a):
""" Return the Z3 expression ToReal(a).
@@ -3171,6 +3334,7 @@ def ToReal(a):
ctx = a.ctx
return ArithRef(Z3_mk_int2real(ctx.ref(), a.as_ast()), ctx)
+
def ToInt(a):
""" Return the Z3 expression ToInt(a).
@@ -3188,6 +3352,7 @@ def ToInt(a):
ctx = a.ctx
return ArithRef(Z3_mk_real2int(ctx.ref(), a.as_ast()), ctx)
+
def IsInt(a):
""" Return the Z3 predicate IsInt(a).
@@ -3204,6 +3369,7 @@ def IsInt(a):
ctx = a.ctx
return BoolRef(Z3_mk_is_int(ctx.ref(), a.as_ast()), ctx)
+
def Sqrt(a, ctx=None):
""" Return a Z3 expression which represents the square root of a.
@@ -3216,6 +3382,7 @@ def Sqrt(a, ctx=None):
a = RealVal(a, ctx)
return a ** "1/2"
+
def Cbrt(a, ctx=None):
""" Return a Z3 expression which represents the cubic root of a.
@@ -3234,6 +3401,7 @@ def Cbrt(a, ctx=None):
#
#########################################
+
class BitVecSortRef(SortRef):
"""Bit-vector sort."""
@@ -3266,6 +3434,7 @@ class BitVecSortRef(SortRef):
else:
return BitVecVal(val, self)
+
def is_bv_sort(s):
"""Return True if `s` is a Z3 bit-vector sort.
@@ -3276,6 +3445,7 @@ def is_bv_sort(s):
"""
return isinstance(s, BitVecSortRef)
+
class BitVecRef(ExprRef):
"""Bit-vector expressions."""
@@ -3688,6 +3858,7 @@ class BitVecRef(ExprRef):
a, b = _coerce_exprs(self, other)
return BitVecRef(Z3_mk_bvshl(self.ctx_ref(), b.as_ast(), a.as_ast()), self.ctx)
+
class BitVecNumRef(BitVecRef):
"""Bit-vector values."""
@@ -3703,7 +3874,8 @@ class BitVecNumRef(BitVecRef):
return int(self.as_string())
def as_signed_long(self):
- """Return a Z3 bit-vector numeral as a Python long (bignum) numeral. The most significant bit is assumed to be the sign.
+ """Return a Z3 bit-vector numeral as a Python long (bignum) numeral.
+ The most significant bit is assumed to be the sign.
>>> BitVecVal(4, 3).as_signed_long()
-4
@@ -3729,7 +3901,7 @@ class BitVecNumRef(BitVecRef):
def as_binary_string(self):
return Z3_get_numeral_binary_string(self.ctx_ref(), self.as_ast())
-
+
def is_bv(a):
"""Return `True` if `a` is a Z3 bit-vector expression.
@@ -3744,6 +3916,7 @@ def is_bv(a):
"""
return isinstance(a, BitVecRef)
+
def is_bv_value(a):
"""Return `True` if `a` is a Z3 bit-vector numeral value.
@@ -3758,6 +3931,7 @@ def is_bv_value(a):
"""
return is_bv(a) and _is_numeral(a.ctx, a.as_ast())
+
def BV2Int(a, is_signed=False):
"""Return the Z3 expression BV2Int(a).
@@ -3777,9 +3951,10 @@ def BV2Int(a, is_signed=False):
if z3_debug():
_z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
ctx = a.ctx
- ## investigate problem with bv2int
+ # investigate problem with bv2int
return ArithRef(Z3_mk_bv2int(ctx.ref(), a.as_ast(), is_signed), ctx)
+
def Int2BV(a, num_bits):
"""Return the z3 expression Int2BV(a, num_bits).
It is a bit-vector of width num_bits and represents the
@@ -3788,6 +3963,7 @@ def Int2BV(a, num_bits):
ctx = a.ctx
return BitVecRef(Z3_mk_int2bv(ctx.ref(), num_bits, a.as_ast()), ctx)
+
def BitVecSort(sz, ctx=None):
"""Return a Z3 bit-vector sort of the given size. If `ctx=None`, then the global context is used.
@@ -3802,6 +3978,7 @@ def BitVecSort(sz, ctx=None):
ctx = _get_ctx(ctx)
return BitVecSortRef(Z3_mk_bv_sort(ctx.ref(), sz), ctx)
+
def BitVecVal(val, bv, ctx=None):
"""Return a bit-vector value with the given number of bits. If `ctx=None`, then the global context is used.
@@ -3818,6 +3995,7 @@ def BitVecVal(val, bv, ctx=None):
ctx = _get_ctx(ctx)
return BitVecNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), BitVecSort(bv, ctx).ast), ctx)
+
def BitVec(name, bv, ctx=None):
"""Return a bit-vector constant named `name`. `bv` may be the number of bits of a bit-vector sort.
If `ctx=None`, then the global context is used.
@@ -3841,6 +4019,7 @@ def BitVec(name, bv, ctx=None):
bv = BitVecSort(bv, ctx)
return BitVecRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), bv.ast), ctx)
+
def BitVecs(names, bv, ctx=None):
"""Return a tuple of bit-vector constants of size bv.
@@ -3861,6 +4040,7 @@ def BitVecs(names, bv, ctx=None):
names = names.split(" ")
return [BitVec(name, bv, ctx) for name in names]
+
def Concat(*args):
"""Create a Z3 bit-vector concatenation expression.
@@ -3892,20 +4072,21 @@ def Concat(*args):
return SeqRef(Z3_mk_seq_concat(ctx.ref(), sz, v), ctx)
if is_re(args[0]):
- if z3_debug():
- _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
- v = (Ast * sz)()
- for i in range(sz):
- v[i] = args[i].as_ast()
- return ReRef(Z3_mk_re_concat(ctx.ref(), sz, v), ctx)
+ if z3_debug():
+ _z3_assert(all([is_re(a) for a in args]), "All arguments must be regular expressions.")
+ v = (Ast * sz)()
+ for i in range(sz):
+ v[i] = args[i].as_ast()
+ return ReRef(Z3_mk_re_concat(ctx.ref(), sz, v), ctx)
if z3_debug():
_z3_assert(all([is_bv(a) for a in args]), "All arguments must be Z3 bit-vector expressions.")
- r = args[0]
+ r = args[0]
for i in range(sz - 1):
- r = BitVecRef(Z3_mk_concat(ctx.ref(), r.as_ast(), args[i+1].as_ast()), ctx)
+ r = BitVecRef(Z3_mk_concat(ctx.ref(), r.as_ast(), args[i + 1].as_ast()), ctx)
return r
+
def Extract(high, low, a):
"""Create a Z3 bit-vector extraction expression, or create a string extraction expression.
@@ -3925,14 +4106,17 @@ def Extract(high, low, a):
return SeqRef(Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx)
if z3_debug():
_z3_assert(low <= high, "First argument must be greater than or equal to second argument")
- _z3_assert(_is_int(high) and high >= 0 and _is_int(low) and low >= 0, "First and second arguments must be non negative integers")
+ _z3_assert(_is_int(high) and high >= 0 and _is_int(low) and low >= 0,
+ "First and second arguments must be non negative integers")
_z3_assert(is_bv(a), "Third argument must be a Z3 bit-vector expression")
return BitVecRef(Z3_mk_extract(a.ctx_ref(), high, low, a.as_ast()), a.ctx)
+
def _check_bv_args(a, b):
if z3_debug():
_z3_assert(is_bv(a) or is_bv(b), "First or second argument must be a Z3 bit-vector expression")
+
def ULE(a, b):
"""Create the Z3 expression (unsigned) `other <= self`.
@@ -3950,6 +4134,7 @@ def ULE(a, b):
a, b = _coerce_exprs(a, b)
return BoolRef(Z3_mk_bvule(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
+
def ULT(a, b):
"""Create the Z3 expression (unsigned) `other < self`.
@@ -3967,6 +4152,7 @@ def ULT(a, b):
a, b = _coerce_exprs(a, b)
return BoolRef(Z3_mk_bvult(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
+
def UGE(a, b):
"""Create the Z3 expression (unsigned) `other >= self`.
@@ -3984,6 +4170,7 @@ def UGE(a, b):
a, b = _coerce_exprs(a, b)
return BoolRef(Z3_mk_bvuge(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
+
def UGT(a, b):
"""Create the Z3 expression (unsigned) `other > self`.
@@ -4001,6 +4188,7 @@ def UGT(a, b):
a, b = _coerce_exprs(a, b)
return BoolRef(Z3_mk_bvugt(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
+
def UDiv(a, b):
"""Create the Z3 expression (unsigned) division `self / other`.
@@ -4021,6 +4209,7 @@ def UDiv(a, b):
a, b = _coerce_exprs(a, b)
return BitVecRef(Z3_mk_bvudiv(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
+
def URem(a, b):
"""Create the Z3 expression (unsigned) remainder `self % other`.
@@ -4041,6 +4230,7 @@ def URem(a, b):
a, b = _coerce_exprs(a, b)
return BitVecRef(Z3_mk_bvurem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
+
def SRem(a, b):
"""Create the Z3 expression signed remainder.
@@ -4061,6 +4251,7 @@ def SRem(a, b):
a, b = _coerce_exprs(a, b)
return BitVecRef(Z3_mk_bvsrem(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
+
def LShR(a, b):
"""Create the Z3 expression logical right shift.
@@ -4092,6 +4283,7 @@ def LShR(a, b):
a, b = _coerce_exprs(a, b)
return BitVecRef(Z3_mk_bvlshr(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
+
def RotateLeft(a, b):
"""Return an expression representing `a` rotated to the left `b` times.
@@ -4107,6 +4299,7 @@ def RotateLeft(a, b):
a, b = _coerce_exprs(a, b)
return BitVecRef(Z3_mk_ext_rotate_left(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
+
def RotateRight(a, b):
"""Return an expression representing `a` rotated to the right `b` times.
@@ -4122,6 +4315,7 @@ def RotateRight(a, b):
a, b = _coerce_exprs(a, b)
return BitVecRef(Z3_mk_ext_rotate_right(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
+
def SignExt(n, a):
"""Return a bit-vector expression with `n` extra sign-bits.
@@ -4151,6 +4345,7 @@ def SignExt(n, a):
_z3_assert(is_bv(a), "Second argument must be a Z3 bit-vector expression")
return BitVecRef(Z3_mk_sign_ext(a.ctx_ref(), n, a.as_ast()), a.ctx)
+
def ZeroExt(n, a):
"""Return a bit-vector expression with `n` extra zero-bits.
@@ -4178,6 +4373,7 @@ def ZeroExt(n, a):
_z3_assert(is_bv(a), "Second argument must be a Z3 bit-vector expression")
return BitVecRef(Z3_mk_zero_ext(a.ctx_ref(), n, a.as_ast()), a.ctx)
+
def RepeatBitVec(n, a):
"""Return an expression representing `n` copies of `a`.
@@ -4201,30 +4397,35 @@ def RepeatBitVec(n, a):
_z3_assert(is_bv(a), "Second argument must be a Z3 bit-vector expression")
return BitVecRef(Z3_mk_repeat(a.ctx_ref(), n, a.as_ast()), a.ctx)
+
def BVRedAnd(a):
"""Return the reduction-and expression of `a`."""
if z3_debug():
_z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
return BitVecRef(Z3_mk_bvredand(a.ctx_ref(), a.as_ast()), a.ctx)
+
def BVRedOr(a):
"""Return the reduction-or expression of `a`."""
if z3_debug():
_z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
return BitVecRef(Z3_mk_bvredor(a.ctx_ref(), a.as_ast()), a.ctx)
+
def BVAddNoOverflow(a, b, signed):
"""A predicate the determines that bit-vector addition does not overflow"""
_check_bv_args(a, b)
a, b = _coerce_exprs(a, b)
return BoolRef(Z3_mk_bvadd_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
+
def BVAddNoUnderflow(a, b):
"""A predicate the determines that signed bit-vector addition does not underflow"""
_check_bv_args(a, b)
a, b = _coerce_exprs(a, b)
return BoolRef(Z3_mk_bvadd_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
+
def BVSubNoOverflow(a, b):
"""A predicate the determines that bit-vector subtraction does not overflow"""
_check_bv_args(a, b)
@@ -4238,18 +4439,21 @@ def BVSubNoUnderflow(a, b, signed):
a, b = _coerce_exprs(a, b)
return BoolRef(Z3_mk_bvsub_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed), a.ctx)
+
def BVSDivNoOverflow(a, b):
"""A predicate the determines that bit-vector signed division does not overflow"""
_check_bv_args(a, b)
a, b = _coerce_exprs(a, b)
return BoolRef(Z3_mk_bvsdiv_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
+
def BVSNegNoOverflow(a):
"""A predicate the determines that bit-vector unary negation does not overflow"""
if z3_debug():
_z3_assert(is_bv(a), "First argument must be a Z3 bit-vector expression")
return BoolRef(Z3_mk_bvneg_no_overflow(a.ctx_ref(), a.as_ast()), a.ctx)
+
def BVMulNoOverflow(a, b, signed):
"""A predicate the determines that bit-vector multiplication does not overflow"""
_check_bv_args(a, b)
@@ -4264,7 +4468,6 @@ def BVMulNoUnderflow(a, b):
return BoolRef(Z3_mk_bvmul_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
-
#########################################
#
# Arrays
@@ -4292,6 +4495,7 @@ class ArraySortRef(SortRef):
"""
return _to_sort_ref(Z3_get_array_sort_range(self.ctx_ref(), self.ast), self.ctx)
+
class ArrayRef(ExprRef):
"""Array expressions. """
@@ -4338,6 +4542,7 @@ class ArrayRef(ExprRef):
def default(self):
return _to_expr_ref(Z3_mk_array_default(self.ctx_ref(), self.as_ast()), self.ctx)
+
def is_array_sort(a):
return Z3_get_sort_kind(a.ctx.ref(), Z3_get_sort(a.ctx.ref(), a.ast)) == Z3_ARRAY_SORT
@@ -4355,6 +4560,7 @@ def is_array(a):
"""
return isinstance(a, ArrayRef)
+
def is_const_array(a):
"""Return `True` if `a` is a Z3 constant array.
@@ -4367,6 +4573,7 @@ def is_const_array(a):
"""
return is_app_of(a, Z3_OP_CONST_ARRAY)
+
def is_K(a):
"""Return `True` if `a` is a Z3 constant array.
@@ -4379,6 +4586,7 @@ def is_K(a):
"""
return is_app_of(a, Z3_OP_CONST_ARRAY)
+
def is_map(a):
"""Return `True` if `a` is a Z3 map array expression.
@@ -4394,6 +4602,7 @@ def is_map(a):
"""
return is_app_of(a, Z3_OP_ARRAY_MAP)
+
def is_default(a):
"""Return `True` if `a` is a Z3 default array expression.
>>> d = Default(K(IntSort(), 10))
@@ -4402,6 +4611,7 @@ def is_default(a):
"""
return is_app_of(a, Z3_OP_ARRAY_DEFAULT)
+
def get_map_func(a):
"""Return the function declaration associated with a Z3 map array expression.
@@ -4417,7 +4627,14 @@ def get_map_func(a):
"""
if z3_debug():
_z3_assert(is_map(a), "Z3 array map expression expected.")
- return FuncDeclRef(Z3_to_func_decl(a.ctx_ref(), Z3_get_decl_ast_parameter(a.ctx_ref(), a.decl().ast, 0)), a.ctx)
+ return FuncDeclRef(
+ Z3_to_func_decl(
+ a.ctx_ref(),
+ Z3_get_decl_ast_parameter(a.ctx_ref(), a.decl().ast, 0),
+ ),
+ ctx=a.ctx,
+ )
+
def ArraySort(*sig):
"""Return the Z3 array sort with the given domain and range sorts.
@@ -4451,6 +4668,7 @@ def ArraySort(*sig):
dom[i] = sig[i].ast
return ArraySortRef(Z3_mk_array_sort_n(ctx.ref(), arity, dom, r.ast), ctx)
+
def Array(name, dom, rng):
"""Return an array constant named `name` with the given domain and range sorts.
@@ -4464,6 +4682,7 @@ def Array(name, dom, rng):
ctx = s.ctx
return ArrayRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), s.ast), ctx)
+
def Update(a, i, v):
"""Return a Z3 store array expression.
@@ -4485,6 +4704,7 @@ def Update(a, i, v):
ctx = a.ctx
return _to_expr_ref(Z3_mk_store(ctx.ref(), a.as_ast(), i.as_ast(), v.as_ast()), ctx)
+
def Default(a):
""" Return a default value for array expression.
>>> b = K(IntSort(), 1)
@@ -4512,6 +4732,7 @@ def Store(a, i, v):
"""
return Update(a, i, v)
+
def Select(a, i):
"""Return a Z3 select array expression.
@@ -4549,6 +4770,7 @@ def Map(f, *args):
ctx = f.ctx
return ArrayRef(Z3_mk_map(ctx.ref(), f.ast, sz, _args), ctx)
+
def K(dom, v):
"""Return a Z3 constant array expression.
@@ -4570,6 +4792,7 @@ def K(dom, v):
v = _py2expr(v, ctx)
return ArrayRef(Z3_mk_const_array(ctx.ref(), dom.ast, v.as_ast()), ctx)
+
def Ext(a, b):
"""Return extensionality index for one-dimensional arrays.
>> a, b = Consts('a b', SetSort(IntSort()))
@@ -4581,11 +4804,13 @@ def Ext(a, b):
_z3_assert(is_array_sort(a) and is_array(b), "arguments must be arrays")
return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
+
def SetHasSize(a, k):
ctx = a.ctx
k = _py2expr(k, ctx)
return _to_expr_ref(Z3_mk_set_has_size(ctx.ref(), a.as_ast(), k.as_ast()), ctx)
+
def is_select(a):
"""Return `True` if `a` is a Z3 array select application.
@@ -4598,6 +4823,7 @@ def is_select(a):
"""
return is_app_of(a, Z3_OP_SELECT)
+
def is_store(a):
"""Return `True` if `a` is a Z3 array store application.
@@ -4620,6 +4846,7 @@ def SetSort(s):
""" Create a set sort over element sort s"""
return ArraySort(s, BoolSort())
+
def EmptySet(s):
"""Create the empty set
>>> EmptySet(IntSort())
@@ -4628,6 +4855,7 @@ def EmptySet(s):
ctx = s.ctx
return ArrayRef(Z3_mk_empty_set(ctx.ref(), s.ast), ctx)
+
def FullSet(s):
"""Create the full set
>>> FullSet(IntSort())
@@ -4636,6 +4864,7 @@ def FullSet(s):
ctx = s.ctx
return ArrayRef(Z3_mk_full_set(ctx.ref(), s.ast), ctx)
+
def SetUnion(*args):
""" Take the union of sets
>>> a = Const('a', SetSort(IntSort()))
@@ -4648,6 +4877,7 @@ def SetUnion(*args):
_args, sz = _to_ast_array(args)
return ArrayRef(Z3_mk_set_union(ctx.ref(), sz, _args), ctx)
+
def SetIntersect(*args):
""" Take the union of sets
>>> a = Const('a', SetSort(IntSort()))
@@ -4660,26 +4890,29 @@ def SetIntersect(*args):
_args, sz = _to_ast_array(args)
return ArrayRef(Z3_mk_set_intersect(ctx.ref(), sz, _args), ctx)
+
def SetAdd(s, e):
""" Add element e to set s
>>> a = Const('a', SetSort(IntSort()))
>>> SetAdd(a, 1)
Store(a, 1, True)
"""
- ctx = _ctx_from_ast_arg_list([s,e])
+ ctx = _ctx_from_ast_arg_list([s, e])
e = _py2expr(e, ctx)
return ArrayRef(Z3_mk_set_add(ctx.ref(), s.as_ast(), e.as_ast()), ctx)
+
def SetDel(s, e):
""" Remove element e to set s
>>> a = Const('a', SetSort(IntSort()))
>>> SetDel(a, 1)
Store(a, 1, False)
"""
- ctx = _ctx_from_ast_arg_list([s,e])
+ ctx = _ctx_from_ast_arg_list([s, e])
e = _py2expr(e, ctx)
return ArrayRef(Z3_mk_set_del(ctx.ref(), s.as_ast(), e.as_ast()), ctx)
+
def SetComplement(s):
""" The complement of set s
>>> a = Const('a', SetSort(IntSort()))
@@ -4689,6 +4922,7 @@ def SetComplement(s):
ctx = s.ctx
return ArrayRef(Z3_mk_set_complement(ctx.ref(), s.as_ast()), ctx)
+
def SetDifference(a, b):
""" The set difference of a and b
>>> a = Const('a', SetSort(IntSort()))
@@ -4699,16 +4933,18 @@ def SetDifference(a, b):
ctx = _ctx_from_ast_arg_list([a, b])
return ArrayRef(Z3_mk_set_difference(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
+
def IsMember(e, s):
""" Check if e is a member of set s
>>> a = Const('a', SetSort(IntSort()))
>>> IsMember(1, a)
a[1]
"""
- ctx = _ctx_from_ast_arg_list([s,e])
+ ctx = _ctx_from_ast_arg_list([s, e])
e = _py2expr(e, ctx)
return BoolRef(Z3_mk_set_member(ctx.ref(), e.as_ast(), s.as_ast()), ctx)
+
def IsSubset(a, b):
""" Check if a is a subset of b
>>> a = Const('a', SetSort(IntSort()))
@@ -4728,7 +4964,12 @@ def IsSubset(a, b):
def _valid_accessor(acc):
"""Return `True` if acc is pair of the form (String, Datatype or Sort). """
- return isinstance(acc, tuple) and len(acc) == 2 and isinstance(acc[0], str) and (isinstance(acc[1], Datatype) or is_sort(acc[1]))
+ if not isinstance(acc, tuple):
+ return False
+ if len(acc) != 2:
+ return False
+ return isinstance(acc[0], str) and (isinstance(acc[1], Datatype) or is_sort(acc[1]))
+
class Datatype:
"""Helper class for declaring Z3 datatypes.
@@ -4756,9 +4997,10 @@ class Datatype:
>>> simplify(car(n))
1
"""
+
def __init__(self, name, ctx=None):
- self.ctx = _get_ctx(ctx)
- self.name = name
+ self.ctx = _get_ctx(ctx)
+ self.name = name
self.constructors = []
def __deepcopy__(self, memo={}):
@@ -4770,18 +5012,22 @@ class Datatype:
if z3_debug():
_z3_assert(isinstance(name, str), "String expected")
_z3_assert(isinstance(rec_name, str), "String expected")
- _z3_assert(all([_valid_accessor(a) for a in args]), "Valid list of accessors expected. An accessor is a pair of the form (String, Datatype|Sort)")
+ _z3_assert(
+ all([_valid_accessor(a) for a in args]),
+ "Valid list of accessors expected. An accessor is a pair of the form (String, Datatype|Sort)",
+ )
self.constructors.append((name, rec_name, args))
def declare(self, name, *args):
"""Declare constructor named `name` with the given accessors `args`.
- Each accessor is a pair `(name, sort)`, where `name` is a string and `sort` a Z3 sort or a reference to the datatypes being declared.
+ Each accessor is a pair `(name, sort)`, where `name` is a string and `sort` a Z3 sort
+ or a reference to the datatypes being declared.
In the following example `List.declare('cons', ('car', IntSort()), ('cdr', List))`
declares the constructor named `cons` that builds a new List using an integer and a List.
- It also declares the accessors `car` and `cdr`. The accessor `car` extracts the integer of a `cons` cell,
- and `cdr` the list of a `cons` cell. After all constructors were declared, we use the method create() to create
- the actual datatype in Z3.
+ It also declares the accessors `car` and `cdr`. The accessor `car` extracts the integer
+ of a `cons` cell, and `cdr` the list of a `cons` cell. After all constructors were declared,
+ we use the method create() to create the actual datatype in Z3.
>>> List = Datatype('List')
>>> List.declare('cons', ('car', IntSort()), ('cdr', List))
@@ -4812,23 +5058,30 @@ class Datatype:
"""
return CreateDatatypes([self])[0]
+
class ScopedConstructor:
"""Auxiliary object used to create Z3 datatypes."""
+
def __init__(self, c, ctx):
- self.c = c
+ self.c = c
self.ctx = ctx
+
def __del__(self):
if self.ctx.ref() is not None:
- Z3_del_constructor(self.ctx.ref(), self.c)
+ Z3_del_constructor(self.ctx.ref(), self.c)
+
class ScopedConstructorList:
"""Auxiliary object used to create Z3 datatypes."""
+
def __init__(self, c, ctx):
- self.c = c
+ self.c = c
self.ctx = ctx
+
def __del__(self):
if self.ctx.ref() is not None:
- Z3_del_constructor_list(self.ctx.ref(), self.c)
+ Z3_del_constructor_list(self.ctx.ref(), self.c)
+
def CreateDatatypes(*ds):
"""Create mutually recursive Z3 datatypes using 1 or more Datatype helper objects.
@@ -4861,60 +5114,63 @@ def CreateDatatypes(*ds):
if z3_debug():
_z3_assert(len(ds) > 0, "At least one Datatype must be specified")
_z3_assert(all([isinstance(d, Datatype) for d in ds]), "Arguments must be Datatypes")
- _z3_assert(all([d.ctx == ds[0].ctx for d in ds]), "Context mismatch")
+ _z3_assert(all([d.ctx == ds[0].ctx for d in ds]), "Context mismatch")
_z3_assert(all([d.constructors != [] for d in ds]), "Non-empty Datatypes expected")
ctx = ds[0].ctx
- num = len(ds)
- names = (Symbol * num)()
- out = (Sort * num)()
+ num = len(ds)
+ names = (Symbol * num)()
+ out = (Sort * num)()
clists = (ConstructorList * num)()
to_delete = []
for i in range(num):
- d = ds[i]
+ d = ds[i]
names[i] = to_symbol(d.name, ctx)
- num_cs = len(d.constructors)
- cs = (Constructor * num_cs)()
+ num_cs = len(d.constructors)
+ cs = (Constructor * num_cs)()
for j in range(num_cs):
- c = d.constructors[j]
- cname = to_symbol(c[0], ctx)
- rname = to_symbol(c[1], ctx)
- fs = c[2]
+ c = d.constructors[j]
+ cname = to_symbol(c[0], ctx)
+ rname = to_symbol(c[1], ctx)
+ fs = c[2]
num_fs = len(fs)
fnames = (Symbol * num_fs)()
- sorts = (Sort * num_fs)()
- refs = (ctypes.c_uint * num_fs)()
+ sorts = (Sort * num_fs)()
+ refs = (ctypes.c_uint * num_fs)()
for k in range(num_fs):
fname = fs[k][0]
ftype = fs[k][1]
fnames[k] = to_symbol(fname, ctx)
if isinstance(ftype, Datatype):
if z3_debug():
- _z3_assert(ds.count(ftype) == 1, "One and only one occurrence of each datatype is expected")
+ _z3_assert(
+ ds.count(ftype) == 1,
+ "One and only one occurrence of each datatype is expected",
+ )
sorts[k] = None
- refs[k] = ds.index(ftype)
+ refs[k] = ds.index(ftype)
else:
if z3_debug():
_z3_assert(is_sort(ftype), "Z3 sort expected")
sorts[k] = ftype.ast
- refs[k] = 0
+ refs[k] = 0
cs[j] = Z3_mk_constructor(ctx.ref(), cname, rname, num_fs, fnames, sorts, refs)
to_delete.append(ScopedConstructor(cs[j], ctx))
clists[i] = Z3_mk_constructor_list(ctx.ref(), num_cs, cs)
to_delete.append(ScopedConstructorList(clists[i], ctx))
Z3_mk_datatypes(ctx.ref(), num, names, out, clists)
result = []
- ## Create a field for every constructor, recognizer and accessor
+ # Create a field for every constructor, recognizer and accessor
for i in range(num):
dref = DatatypeSortRef(out[i], ctx)
num_cs = dref.num_constructors()
for j in range(num_cs):
- cref = dref.constructor(j)
- cref_name = cref.name()
+ cref = dref.constructor(j)
+ cref_name = cref.name()
cref_arity = cref.arity()
if cref.arity() == 0:
cref = cref()
setattr(dref, cref_name, cref)
- rref = dref.recognizer(j)
+ rref = dref.recognizer(j)
setattr(dref, "is_" + cref_name, rref)
for k in range(cref_arity):
aref = dref.accessor(j, k)
@@ -4922,8 +5178,10 @@ def CreateDatatypes(*ds):
result.append(dref)
return tuple(result)
+
class DatatypeSortRef(SortRef):
"""Datatype sorts."""
+
def num_constructors(self):
"""Return the number of constructors in the given Z3 datatype.
@@ -4985,7 +5243,8 @@ class DatatypeSortRef(SortRef):
return FuncDeclRef(Z3_get_datatype_sort_recognizer(self.ctx_ref(), self.ast, idx), self.ctx)
def accessor(self, i, j):
- """In Z3, each constructor has 0 or more accessor. The number of accessors is equal to the arity of the constructor.
+ """In Z3, each constructor has 0 or more accessor.
+ The number of accessors is equal to the arity of the constructor.
>>> List = Datatype('List')
>>> List.declare('cons', ('car', IntSort()), ('cdr', List))
@@ -5011,25 +5270,32 @@ class DatatypeSortRef(SortRef):
if z3_debug():
_z3_assert(i < self.num_constructors(), "Invalid constructor index")
_z3_assert(j < self.constructor(i).arity(), "Invalid accessor index")
- return FuncDeclRef(Z3_get_datatype_sort_constructor_accessor(self.ctx_ref(), self.ast, i, j), self.ctx)
+ return FuncDeclRef(
+ Z3_get_datatype_sort_constructor_accessor(self.ctx_ref(), self.ast, i, j),
+ ctx=self.ctx,
+ )
+
class DatatypeRef(ExprRef):
"""Datatype expressions."""
+
def sort(self):
"""Return the datatype sort of the datatype expression `self`."""
return DatatypeSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
-def TupleSort(name, sorts, ctx = None):
+
+def TupleSort(name, sorts, ctx=None):
"""Create a named tuple sort base on a set of underlying sorts
Example:
>>> pair, mk_pair, (first, second) = TupleSort("pair", [IntSort(), StringSort()])
"""
tuple = Datatype(name, ctx)
- projects = [ ('project%d' % i, sorts[i]) for i in range(len(sorts)) ]
+ projects = [("project%d" % i, sorts[i]) for i in range(len(sorts))]
tuple.declare(name, *projects)
tuple = tuple.create()
return tuple, tuple.constructor(0), [tuple.accessor(0, i) for i in range(len(sorts))]
+
def DisjointSum(name, sorts, ctx=None):
"""Create a named tagged union sort base on a set of underlying sorts
Example:
@@ -5055,10 +5321,10 @@ def EnumSort(name, values, ctx=None):
_z3_assert(len(values) > 0, "At least one value expected")
ctx = _get_ctx(ctx)
num = len(values)
- _val_names = (Symbol * num)()
+ _val_names = (Symbol * num)()
for i in range(num):
_val_names[i] = to_symbol(values[i])
- _values = (FuncDecl * num)()
+ _values = (FuncDecl * num)()
_testers = (FuncDecl * num)()
name = to_symbol(name)
S = DatatypeSortRef(Z3_mk_enumeration_sort(ctx.ref(), name, num, _val_names, _values, _testers), ctx)
@@ -5074,13 +5340,15 @@ def EnumSort(name, values, ctx=None):
#
#########################################
+
class ParamsRef:
"""Set of parameters used to configure Solvers, Tactics and Simplifiers in Z3.
Consider using the function `args2params` to create instances of this object.
"""
+
def __init__(self, ctx=None, params=None):
- self.ctx = _get_ctx(ctx)
+ self.ctx = _get_ctx(ctx)
if params is None:
self.params = Z3_mk_params(self.ctx.ref())
else:
@@ -5092,7 +5360,7 @@ class ParamsRef:
def __del__(self):
if self.ctx.ref() is not None:
- Z3_params_dec_ref(self.ctx.ref(), self.params)
+ Z3_params_dec_ref(self.ctx.ref(), self.params)
def set(self, name, val):
"""Set parameter name with value val."""
@@ -5118,6 +5386,7 @@ class ParamsRef:
_z3_assert(isinstance(ds, ParamDescrsRef), "parameter description set expected")
Z3_params_validate(self.ctx.ref(), self.params, ds.descr)
+
def args2params(arguments, keywords, ctx=None):
"""Convert python arguments into a Z3_params object.
A ':' is added to the keywords, and '_' is replaced with '-'
@@ -5128,7 +5397,7 @@ def args2params(arguments, keywords, ctx=None):
if z3_debug():
_z3_assert(len(arguments) % 2 == 0, "Argument list must have an even number of elements.")
prev = None
- r = ParamsRef(ctx)
+ r = ParamsRef(ctx)
for a in arguments:
if prev is None:
prev = a
@@ -5140,13 +5409,15 @@ def args2params(arguments, keywords, ctx=None):
r.set(k, v)
return r
+
class ParamDescrsRef:
"""Set of parameter descriptions for Solvers, Tactics and Simplifiers in Z3.
"""
+
def __init__(self, descr, ctx=None):
_z3_assert(isinstance(descr, ParamDescrs), "parameter description object expected")
- self.ctx = _get_ctx(ctx)
- self.descr = descr
+ self.ctx = _get_ctx(ctx)
+ self.descr = descr
Z3_param_descrs_inc_ref(self.ctx.ref(), self.descr)
def __deepcopy__(self, memo={}):
@@ -5154,7 +5425,7 @@ class ParamDescrsRef:
def __del__(self):
if self.ctx.ref() is not None:
- Z3_param_descrs_dec_ref(self.ctx.ref(), self.descr)
+ Z3_param_descrs_dec_ref(self.ctx.ref(), self.descr)
def size(self):
"""Return the size of in the parameter description `self`.
@@ -5196,6 +5467,7 @@ class ParamDescrsRef:
#
#########################################
+
class Goal(Z3PPObject):
"""Goal is a collection of constraints we want to find a solution or show to be unsatisfiable (infeasible).
@@ -5206,11 +5478,12 @@ class Goal(Z3PPObject):
def __init__(self, models=True, unsat_cores=False, proofs=False, ctx=None, goal=None):
if z3_debug():
- _z3_assert(goal is None or ctx is not None, "If goal is different from None, then ctx must be also different from None")
- self.ctx = _get_ctx(ctx)
- self.goal = goal
+ _z3_assert(goal is None or ctx is not None,
+ "If goal is different from None, then ctx must be also different from None")
+ self.ctx = _get_ctx(ctx)
+ self.goal = goal
if self.goal is None:
- self.goal = Z3_mk_goal(self.ctx.ref(), models, unsat_cores, proofs)
+ self.goal = Z3_mk_goal(self.ctx.ref(), models, unsat_cores, proofs)
Z3_goal_inc_ref(self.ctx.ref(), self.goal)
def __deepcopy__(self, memo={}):
@@ -5221,7 +5494,8 @@ class Goal(Z3PPObject):
Z3_goal_dec_ref(self.ctx.ref(), self.goal)
def depth(self):
- """Return the depth of the goal `self`. The depth corresponds to the number of tactics applied to `self`.
+ """Return the depth of the goal `self`.
+ The depth corresponds to the number of tactics applied to `self`.
>>> x, y = Ints('x y')
>>> g = Goal()
@@ -5349,7 +5623,7 @@ class Goal(Z3PPObject):
[x > 0, x < 2]
"""
args = _get_args(args)
- s = BoolSort(self.ctx)
+ s = BoolSort(self.ctx)
for arg in args:
arg = s.cast(arg)
Z3_goal_assert(self.ctx.ref(), self.goal, arg.as_ast())
@@ -5423,7 +5697,7 @@ class Goal(Z3PPObject):
"""Return a textual representation of the s-expression representing the goal."""
return Z3_goal_to_string(self.ctx.ref(), self.goal)
- def dimacs(self, include_names = True):
+ def dimacs(self, include_names=True):
"""Return a textual representation of the goal in DIMACS format."""
return Z3_goal_to_dimacs_string(self.ctx.ref(), self.goal, include_names)
@@ -5473,7 +5747,7 @@ class Goal(Z3PPObject):
>>> g
[x + 1 >= 2]
"""
- t = Tactic('simplify')
+ t = Tactic("simplify")
return t.apply(self, *arguments, **keywords)[0]
def as_expr(self):
@@ -5496,13 +5770,15 @@ class Goal(Z3PPObject):
elif sz == 1:
return self.get(0)
else:
- return And([ self.get(i) for i in range(len(self)) ], self.ctx)
+ return And([self.get(i) for i in range(len(self))], self.ctx)
#########################################
#
# AST Vector
#
#########################################
+
+
class AstVector(Z3PPObject):
"""A collection (vector) of ASTs."""
@@ -5514,7 +5790,7 @@ class AstVector(Z3PPObject):
else:
self.vector = v
assert ctx is not None
- self.ctx = ctx
+ self.ctx = ctx
Z3_ast_vector_inc_ref(self.ctx.ref(), self.vector)
def __deepcopy__(self, memo={}):
@@ -5560,7 +5836,6 @@ class AstVector(Z3PPObject):
elif isinstance(i, slice):
return [_to_ast_ref(Z3_ast_vector_get(self.ctx.ref(), self.vector, ii), self.ctx) for ii in range(*i.indices(self.__len__()))]
-
def __setitem__(self, i, v):
"""Update AST at position `i`.
@@ -5636,7 +5911,10 @@ class AstVector(Z3PPObject):
>>> B
[x]
"""
- return AstVector(Z3_ast_vector_translate(self.ctx.ref(), self.vector, other_ctx.ref()), other_ctx)
+ return AstVector(
+ Z3_ast_vector_translate(self.ctx.ref(), self.vector, other_ctx.ref()),
+ ctx=other_ctx,
+ )
def __copy__(self):
return self.translate(self.ctx)
@@ -5656,6 +5934,8 @@ class AstVector(Z3PPObject):
# AST Map
#
#########################################
+
+
class AstMap:
"""A mapping from ASTs to ASTs."""
@@ -5667,7 +5947,7 @@ class AstMap:
else:
self.map = m
assert ctx is not None
- self.ctx = ctx
+ self.ctx = ctx
Z3_ast_map_inc_ref(self.ctx.ref(), self.map)
def __deepcopy__(self, memo={}):
@@ -5780,12 +6060,13 @@ class AstMap:
#
#########################################
+
class FuncEntry:
"""Store the value of the interpretation of a function in a particular point."""
def __init__(self, entry, ctx):
self.entry = entry
- self.ctx = ctx
+ self.ctx = ctx
Z3_func_entry_inc_ref(self.ctx.ref(), self.entry)
def __deepcopy__(self, memo={}):
@@ -5793,7 +6074,7 @@ class FuncEntry:
def __del__(self):
if self.ctx.ref() is not None:
- Z3_func_entry_dec_ref(self.ctx.ref(), self.entry)
+ Z3_func_entry_dec_ref(self.ctx.ref(), self.entry)
def num_args(self):
"""Return the number of arguments in the given entry.
@@ -5881,18 +6162,19 @@ class FuncEntry:
>>> e.as_list()
[1, 2, 20]
"""
- args = [ self.arg_value(i) for i in range(self.num_args())]
+ args = [self.arg_value(i) for i in range(self.num_args())]
args.append(self.value())
return args
def __repr__(self):
return repr(self.as_list())
+
class FuncInterp(Z3PPObject):
"""Stores the interpretation of a function in a Z3 model."""
def __init__(self, f, ctx):
- self.f = f
+ self.f = f
self.ctx = ctx
if self.f is not None:
Z3_func_interp_inc_ref(self.ctx.ref(), self.f)
@@ -6001,25 +6283,26 @@ class FuncInterp(Z3PPObject):
>>> m[f].as_list()
[[2, 0], 1]
"""
- r = [ self.entry(i).as_list() for i in range(self.num_entries())]
+ r = [self.entry(i).as_list() for i in range(self.num_entries())]
r.append(self.else_value())
return r
def __repr__(self):
return obj_to_string(self)
+
class ModelRef(Z3PPObject):
"""Model/Solution of a satisfiability problem (aka system of constraints)."""
def __init__(self, m, ctx):
assert ctx is not None
self.model = m
- self.ctx = ctx
+ self.ctx = ctx
Z3_model_inc_ref(self.ctx.ref(), self.model)
def __del__(self):
if self.ctx.ref() is not None:
- Z3_model_dec_ref(self.ctx.ref(), self.model)
+ Z3_model_dec_ref(self.ctx.ref(), self.model)
def __repr__(self):
return obj_to_string(self)
@@ -6029,7 +6312,9 @@ class ModelRef(Z3PPObject):
return Z3_model_to_string(self.ctx.ref(), self.model)
def eval(self, t, model_completion=False):
- """Evaluate the expression `t` in the model `self`. If `model_completion` is enabled, then a default interpretation is automatically added for symbols that do not have an interpretation in the model `self`.
+ """Evaluate the expression `t` in the model `self`.
+ If `model_completion` is enabled, then a default interpretation is automatically added
+ for symbols that do not have an interpretation in the model `self`.
>>> x = Int('x')
>>> s = Solver()
@@ -6096,7 +6381,9 @@ class ModelRef(Z3PPObject):
>>> len(m)
2
"""
- return int(Z3_model_get_num_consts(self.ctx.ref(), self.model)) + int(Z3_model_get_num_funcs(self.ctx.ref(), self.model))
+ num_consts = int(Z3_model_get_num_consts(self.ctx.ref(), self.model))
+ num_funcs = int(Z3_model_get_num_funcs(self.ctx.ref(), self.model))
+ return num_consts + num_funcs
def get_interp(self, decl):
"""Return the interpretation for a given declaration or constant.
@@ -6185,7 +6472,7 @@ class ModelRef(Z3PPObject):
>>> m.sorts()
[A, B]
"""
- return [ self.get_sort(i) for i in range(self.num_sorts()) ]
+ return [self.get_sort(i) for i in range(self.num_sorts())]
def get_universe(self, s):
"""Return the interpretation for the uninterpreted sort `s` in the model `self`.
@@ -6208,7 +6495,8 @@ class ModelRef(Z3PPObject):
return None
def __getitem__(self, idx):
- """If `idx` is an integer, then the declaration at position `idx` in the model `self` is returned. If `idx` is a declaration, then the actual interpretation is returned.
+ """If `idx` is an integer, then the declaration at position `idx` in the model `self` is returned.
+ If `idx` is a declaration, then the actual interpretation is returned.
The elements can be retrieved using position or the actual declaration.
@@ -6285,14 +6573,16 @@ class ModelRef(Z3PPObject):
return self.translate(self.ctx)
-def Model(ctx = None):
+def Model(ctx=None):
ctx = _get_ctx(ctx)
return ModelRef(Z3_mk_model(ctx.ref()), ctx)
+
def is_as_array(n):
"""Return true if n is a Z3 expression of the form (_ as-array f)."""
return isinstance(n, ExprRef) and Z3_is_as_array(n.ctx.ref(), n.as_ast())
+
def get_as_array_func(n):
"""Return the function declaration f associated with a Z3 expression of the form (_ as-array f)."""
if z3_debug():
@@ -6304,12 +6594,14 @@ def get_as_array_func(n):
# Statistics
#
#########################################
+
+
class Statistics:
"""Statistics for `Solver.check()`."""
def __init__(self, stats, ctx):
self.stats = stats
- self.ctx = ctx
+ self.ctx = ctx
Z3_stats_inc_ref(self.ctx.ref(), self.stats)
def __deepcopy__(self, memo={}):
@@ -6317,7 +6609,7 @@ class Statistics:
def __del__(self):
if self.ctx.ref() is not None:
- Z3_stats_dec_ref(self.ctx.ref(), self.stats)
+ Z3_stats_dec_ref(self.ctx.ref(), self.stats)
def __repr__(self):
if in_html_mode():
@@ -6329,10 +6621,10 @@ class Statistics:
out.write(u('<tr style="background-color:#CFCFCF">'))
even = False
else:
- out.write(u('<tr>'))
+ out.write(u("<tr>"))
even = True
- out.write(u('<td>%s</td><td>%s</td></tr>' % (k, v)))
- out.write(u('</table>'))
+ out.write(u("<td>%s</td><td>%s</td></tr>" % (k, v)))
+ out.write(u("</table>"))
return out.getvalue()
else:
return Z3_stats_to_string(self.ctx.ref(), self.stats)
@@ -6424,7 +6716,7 @@ class Statistics:
>>> st.nlsat_stages
2
"""
- key = name.replace('_', ' ')
+ key = name.replace("_", " ")
try:
return self.get_key_value(key)
except Z3Exception:
@@ -6435,6 +6727,8 @@ class Statistics:
# Solver
#
#########################################
+
+
class CheckSatResult:
"""Represents the result of a satisfiability check: sat, unsat, unknown.
@@ -6481,16 +6775,21 @@ class CheckSatResult:
set_html_mode(in_html)
return res
-sat = CheckSatResult(Z3_L_TRUE)
-unsat = CheckSatResult(Z3_L_FALSE)
+
+sat = CheckSatResult(Z3_L_TRUE)
+unsat = CheckSatResult(Z3_L_FALSE)
unknown = CheckSatResult(Z3_L_UNDEF)
+
class Solver(Z3PPObject):
- """Solver API provides methods for implementing the main SMT 2.0 commands: push, pop, check, get-model, etc."""
+ """
+ Solver API provides methods for implementing the main SMT 2.0 commands:
+ push, pop, check, get-model, etc.
+ """
def __init__(self, solver=None, ctx=None, logFile=None):
assert solver is None or ctx is not None
- self.ctx = _get_ctx(ctx)
+ self.ctx = _get_ctx(ctx)
self.backtrack_level = 4000000000
self.solver = None
if solver is None:
@@ -6506,7 +6805,8 @@ class Solver(Z3PPObject):
Z3_solver_dec_ref(self.ctx.ref(), self.solver)
def set(self, *args, **keys):
- """Set a configuration option. The method `help()` return a string containing all available options.
+ """Set a configuration option.
+ The method `help()` return a string containing all available options.
>>> s = Solver()
>>> # The option MBQI can be set using three different approaches.
@@ -6540,7 +6840,7 @@ class Solver(Z3PPObject):
Z3_solver_push(self.ctx.ref(), self.solver)
def pop(self, num=1):
- """Backtrack \c num backtracking points.
+ """Backtrack \\c num backtracking points.
>>> x = Int('x')
>>> s = Solver()
@@ -6603,7 +6903,7 @@ class Solver(Z3PPObject):
[x > 0, x < 2]
"""
args = _get_args(args)
- s = BoolSort(self.ctx)
+ s = BoolSort(self.ctx)
for arg in args:
if isinstance(arg, Goal) or isinstance(arg, AstVector):
for f in arg:
@@ -6786,9 +7086,10 @@ class Solver(Z3PPObject):
_z3_assert(isinstance(assumptions, AstVector), "ast vector expected")
_z3_assert(isinstance(variables, AstVector), "ast vector expected")
consequences = AstVector(None, self.ctx)
- r = Z3_solver_get_consequences(self.ctx.ref(), self.solver, assumptions.vector, variables.vector, consequences.vector)
+ r = Z3_solver_get_consequences(self.ctx.ref(), self.solver, assumptions.vector,
+ variables.vector, consequences.vector)
sz = len(consequences)
- consequences = [ consequences[i] for i in range(sz) ]
+ consequences = [consequences[i] for i in range(sz)]
return CheckSatResult(r), consequences
def from_file(self, filename):
@@ -6799,7 +7100,7 @@ class Solver(Z3PPObject):
"""Parse assertions from a string"""
Z3_solver_from_string(self.ctx.ref(), self.solver, s)
- def cube(self, vars = None):
+ def cube(self, vars=None):
"""Get set of cubes
The method takes an optional set of variables that restrict which
variables may be used as a starting point for cubing.
@@ -6808,8 +7109,8 @@ class Solver(Z3PPObject):
"""
self.cube_vs = AstVector(None, self.ctx)
if vars is not None:
- for v in vars:
- self.cube_vs.push(v)
+ for v in vars:
+ self.cube_vs.push(v)
while True:
lvl = self.backtrack_level
self.backtrack_level = 4000000000
@@ -6931,7 +7232,8 @@ class Solver(Z3PPObject):
return self.translate(self.ctx)
def sexpr(self):
- """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
+ """Return a formatted string (in Lisp-like format) with all added constraints.
+ We say the string is in s-expression format.
>>> x = Int('x')
>>> s = Solver()
@@ -6959,7 +7261,10 @@ class Solver(Z3PPObject):
e = es[sz1].as_ast()
else:
e = BoolVal(True, self.ctx).as_ast()
- return Z3_benchmark_to_smtlib_string(self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e)
+ return Z3_benchmark_to_smtlib_string(
+ self.ctx.ref(), "benchmark generated from python API", "", "unknown", "", sz1, v, e,
+ )
+
def SolverFor(logic, ctx=None, logFile=None):
"""Create a solver customized for the given logic.
@@ -6981,6 +7286,7 @@ def SolverFor(logic, ctx=None, logFile=None):
logic = to_symbol(logic)
return Solver(Z3_mk_solver_for_logic(ctx.ref(), logic), ctx, logFile)
+
def SimpleSolver(ctx=None, logFile=None):
"""Return a simple general purpose solver with limited amount of preprocessing.
@@ -6999,12 +7305,13 @@ def SimpleSolver(ctx=None, logFile=None):
#
#########################################
+
class Fixedpoint(Z3PPObject):
"""Fixedpoint API provides methods for solving with recursive predicates"""
def __init__(self, fixedpoint=None, ctx=None):
assert fixedpoint is None or ctx is not None
- self.ctx = _get_ctx(ctx)
+ self.ctx = _get_ctx(ctx)
self.fixedpoint = None
if fixedpoint is None:
self.fixedpoint = Z3_mk_fixedpoint(self.ctx.ref())
@@ -7037,7 +7344,7 @@ class Fixedpoint(Z3PPObject):
def assert_exprs(self, *args):
"""Assert constraints as background axioms for the fixedpoint solver."""
args = _get_args(args)
- s = BoolSort(self.ctx)
+ s = BoolSort(self.ctx)
for arg in args:
if isinstance(arg, Goal) or isinstance(arg, AstVector):
for f in arg:
@@ -7064,7 +7371,7 @@ class Fixedpoint(Z3PPObject):
"""Assert constraints as background axioms for the fixedpoint solver. Alias for assert_expr."""
self.assert_exprs(*args)
- def add_rule(self, head, body = None, name = None):
+ def add_rule(self, head, body=None, name=None):
"""Assert rules defining recursive predicates to the fixedpoint solver.
>>> a = Bool('a')
>>> b = Bool('b')
@@ -7084,14 +7391,14 @@ class Fixedpoint(Z3PPObject):
Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, head.as_ast(), name)
else:
body = _get_args(body)
- f = self.abstract(Implies(And(body, self.ctx),head))
+ f = self.abstract(Implies(And(body, self.ctx), head))
Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
- def rule(self, head, body = None, name = None):
+ def rule(self, head, body=None, name=None):
"""Assert rules defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
self.add_rule(head, body, name)
- def fact(self, head, name = None):
+ def fact(self, head, name=None):
"""Assert facts defining recursive predicates to the fixedpoint solver. Alias for add_rule."""
self.add_rule(head, None, name)
@@ -7117,20 +7424,20 @@ class Fixedpoint(Z3PPObject):
r = Z3_fixedpoint_query(self.ctx.ref(), self.fixedpoint, query.as_ast())
return CheckSatResult(r)
- def query_from_lvl (self, lvl, *query):
+ def query_from_lvl(self, lvl, *query):
"""Query the fixedpoint engine whether formula is derivable starting at the given query level.
"""
query = _get_args(query)
sz = len(query)
if sz >= 1 and isinstance(query[0], FuncDecl):
- _z3_assert (False, "unsupported")
+ _z3_assert(False, "unsupported")
else:
if sz == 1:
query = query[0]
else:
query = And(query)
query = self.abstract(query, False)
- r = Z3_fixedpoint_query_from_lvl (self.ctx.ref(), self.fixedpoint, query.as_ast(), lvl)
+ r = Z3_fixedpoint_query_from_lvl(self.ctx.ref(), self.fixedpoint, query.as_ast(), lvl)
return CheckSatResult(r)
def update_rule(self, head, body, name):
@@ -7139,7 +7446,7 @@ class Fixedpoint(Z3PPObject):
name = ""
name = to_symbol(name, self.ctx)
body = _get_args(body)
- f = self.abstract(Implies(And(body, self.ctx),head))
+ f = self.abstract(Implies(And(body, self.ctx), head))
Z3_fixedpoint_update_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
def get_answer(self):
@@ -7160,21 +7467,25 @@ class Fixedpoint(Z3PPObject):
"""retrieve rule names along the counterexample trace"""
# this is a hack as I don't know how to return a list of symbols from C++;
# obtain names as a single string separated by semicolons
- names = _symbol2py (self.ctx, Z3_fixedpoint_get_rule_names_along_trace(self.ctx.ref(), self.fixedpoint))
+ names = _symbol2py(self.ctx, Z3_fixedpoint_get_rule_names_along_trace(self.ctx.ref(), self.fixedpoint))
# split into individual names
- return names.split (';')
+ return names.split(";")
def get_num_levels(self, predicate):
"""Retrieve number of levels used for predicate in PDR engine"""
return Z3_fixedpoint_get_num_levels(self.ctx.ref(), self.fixedpoint, predicate.ast)
def get_cover_delta(self, level, predicate):
- """Retrieve properties known about predicate for the level'th unfolding. -1 is treated as the limit (infinity)"""
+ """Retrieve properties known about predicate for the level'th unfolding.
+ -1 is treated as the limit (infinity)
+ """
r = Z3_fixedpoint_get_cover_delta(self.ctx.ref(), self.fixedpoint, level, predicate.ast)
return _to_expr_ref(r, self.ctx)
def add_cover(self, level, predicate, property):
- """Add property to predicate for the level'th unfolding. -1 is treated as infinity (infinity)"""
+ """Add property to predicate for the level'th unfolding.
+ -1 is treated as infinity (infinity)
+ """
Z3_fixedpoint_add_cover(self.ctx.ref(), self.fixedpoint, level, predicate.ast, property.ast)
def register_relation(self, *relations):
@@ -7214,7 +7525,8 @@ class Fixedpoint(Z3PPObject):
return self.sexpr()
def sexpr(self):
- """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
+ """Return a formatted string (in Lisp-like format) with all added constraints.
+ We say the string is in s-expression format.
"""
return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, 0, (Ast * 0)())
@@ -7271,6 +7583,7 @@ class FiniteDomainSortRef(SortRef):
else:
raise Z3Exception("Failed to retrieve finite domain sort size")
+
def FiniteDomainSort(name, sz, ctx=None):
"""Create a named finite domain sort of a given size sz"""
if not isinstance(name, Symbol):
@@ -7278,6 +7591,7 @@ def FiniteDomainSort(name, sz, ctx=None):
ctx = _get_ctx(ctx)
return FiniteDomainSortRef(Z3_mk_finite_domain_sort(ctx.ref(), name, sz), ctx)
+
def is_finite_domain_sort(s):
"""Return True if `s` is a Z3 finite-domain sort.
@@ -7300,6 +7614,7 @@ class FiniteDomainRef(ExprRef):
"""Return a Z3 floating point expression as a Python string."""
return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
+
def is_finite_domain(a):
"""Return `True` if `a` is a Z3 finite-domain expression.
@@ -7349,10 +7664,11 @@ def FiniteDomainVal(val, sort, ctx=None):
100
"""
if z3_debug():
- _z3_assert(is_finite_domain_sort(sort), "Expected finite-domain sort" )
+ _z3_assert(is_finite_domain_sort(sort), "Expected finite-domain sort")
ctx = sort.ctx
return FiniteDomainNumRef(Z3_mk_numeral(ctx.ref(), _to_int_str(val), sort.ast), ctx)
+
def is_finite_domain_value(a):
"""Return `True` if `a` is a Z3 finite-domain value.
@@ -7407,20 +7723,22 @@ class OptimizeObjective:
return "%s:%s" % (self._value, self._is_max)
-
_on_models = {}
+
def _global_on_model(ctx):
(fn, mdl) = _on_models[ctx]
fn(mdl)
-
+
+
_on_model_eh = on_model_eh_type(_global_on_model)
+
class Optimize(Z3PPObject):
"""Optimize API provides methods for solving using objective functions and weighted soft constraints"""
def __init__(self, ctx=None):
- self.ctx = _get_ctx(ctx)
+ self.ctx = _get_ctx(ctx)
self.optimize = Z3_mk_optimize(self.ctx.ref())
self._on_models_id = None
Z3_optimize_inc_ref(self.ctx.ref(), self.optimize)
@@ -7435,7 +7753,8 @@ class Optimize(Z3PPObject):
del _on_models[self._on_models_id]
def set(self, *args, **keys):
- """Set a configuration option. The method `help()` return a string containing all available options.
+ """Set a configuration option.
+ The method `help()` return a string containing all available options.
"""
p = args2params(args, keys, self.ctx)
Z3_optimize_set_params(self.ctx.ref(), self.optimize, p.params)
@@ -7451,7 +7770,7 @@ class Optimize(Z3PPObject):
def assert_exprs(self, *args):
"""Assert constraints as background axioms for the optimize solver."""
args = _get_args(args)
- s = BoolSort(self.ctx)
+ s = BoolSort(self.ctx)
for arg in args:
if isinstance(arg, Goal) or isinstance(arg, AstVector):
for f in arg:
@@ -7497,7 +7816,7 @@ class Optimize(Z3PPObject):
_z3_assert(isinstance(p, BoolRef) and is_const(p), "Boolean expression expected")
Z3_optimize_assert_and_track(self.ctx.ref(), self.optimize, a.as_ast(), p.as_ast())
- def add_soft(self, arg, weight = "1", id = None):
+ def add_soft(self, arg, weight="1", id=None):
"""Add soft constraint with optional weight and optional identifier.
If no weight is supplied, then the penalty for violating the soft constraint
is 1.
@@ -7513,20 +7832,29 @@ class Optimize(Z3PPObject):
if id is None:
id = ""
id = to_symbol(id, self.ctx)
+
def asoft(a):
v = Z3_optimize_assert_soft(self.ctx.ref(), self.optimize, a.as_ast(), weight, id)
return OptimizeObjective(self, v, False)
- if sys.version >= '3' and isinstance(arg, Iterable):
+ if sys.version_info.major >= 3 and isinstance(arg, Iterable):
return [asoft(a) for a in arg]
return asoft(arg)
def maximize(self, arg):
"""Add objective function to maximize."""
- return OptimizeObjective(self, Z3_optimize_maximize(self.ctx.ref(), self.optimize, arg.as_ast()), True)
+ return OptimizeObjective(
+ self,
+ Z3_optimize_maximize(self.ctx.ref(), self.optimize, arg.as_ast()),
+ is_max=True,
+ )
def minimize(self, arg):
"""Add objective function to minimize."""
- return OptimizeObjective(self, Z3_optimize_minimize(self.ctx.ref(), self.optimize, arg.as_ast()), False)
+ return OptimizeObjective(
+ self,
+ Z3_optimize_minimize(self.ctx.ref(), self.optimize, arg.as_ast()),
+ is_max=False,
+ )
def push(self):
"""create a backtracking point for added rules, facts and assertions"""
@@ -7600,7 +7928,8 @@ class Optimize(Z3PPObject):
return self.sexpr()
def sexpr(self):
- """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
+ """Return a formatted string (in Lisp-like format) with all added constraints.
+ We say the string is in s-expression format.
"""
return Z3_optimize_to_string(self.ctx.ref(), self.optimize)
@@ -7615,11 +7944,13 @@ class Optimize(Z3PPObject):
The life-time of the model is limited to the callback so the
model has to be (deep) copied if it is to be used after the callback
"""
- id = len(_on_models) + 41
+ id = len(_on_models) + 41
mdl = Model(self.ctx)
_on_models[id] = (on_model, mdl)
self._on_models_id = id
- Z3_optimize_register_model_eh(self.ctx.ref(), self.optimize, mdl.model, ctypes.c_void_p(id), _on_model_eh)
+ Z3_optimize_register_model_eh(
+ self.ctx.ref(), self.optimize, mdl.model, ctypes.c_void_p(id), _on_model_eh,
+ )
#########################################
@@ -7628,11 +7959,13 @@ class Optimize(Z3PPObject):
#
#########################################
class ApplyResult(Z3PPObject):
- """An ApplyResult object contains the subgoals produced by a tactic when applied to a goal. It also contains model and proof converters."""
+ """An ApplyResult object contains the subgoals produced by a tactic when applied to a goal.
+ It also contains model and proof converters.
+ """
def __init__(self, result, ctx):
self.result = result
- self.ctx = ctx
+ self.ctx = ctx
Z3_apply_result_inc_ref(self.ctx.ref(), self.result)
def __deepcopy__(self, memo={}):
@@ -7685,7 +8018,6 @@ class ApplyResult(Z3PPObject):
"""Return a textual representation of the s-expression representing the set of subgoals in `self`."""
return Z3_apply_result_to_string(self.ctx.ref(), self.result)
-
def as_expr(self):
"""Return a Z3 expression consisting of all subgoals.
@@ -7710,20 +8042,25 @@ class ApplyResult(Z3PPObject):
elif sz == 1:
return self[0].as_expr()
else:
- return Or([ self[i].as_expr() for i in range(len(self)) ])
+ return Or([self[i].as_expr() for i in range(len(self))])
#########################################
#
# Tactics
#
#########################################
-class Tactic:
- """Tactics transform, solver and/or simplify sets of constraints (Goal). A Tactic can be converted into a Solver using the method solver().
- Several combinators are available for creating new tactics using the built-in ones: Then(), OrElse(), FailIf(), Repeat(), When(), Cond().
+
+class Tactic:
+ """Tactics transform, solver and/or simplify sets of constraints (Goal).
+ A Tactic can be converted into a Solver using the method solver().
+
+ Several combinators are available for creating new tactics using the built-in ones:
+ Then(), OrElse(), FailIf(), Repeat(), When(), Cond().
"""
+
def __init__(self, tactic, ctx=None):
- self.ctx = _get_ctx(ctx)
+ self.ctx = _get_ctx(ctx)
self.tactic = None
if isinstance(tactic, TacticObj):
self.tactic = tactic
@@ -7769,7 +8106,7 @@ class Tactic:
[[y >= 1]]
"""
if z3_debug():
- _z3_assert(isinstance(goal, Goal) or isinstance(goal, BoolRef), "Z3 Goal or Boolean expressions expected")
+ _z3_assert(isinstance(goal, (Goal, BoolRef)), "Z3 Goal or Boolean expressions expected")
goal = _to_goal(goal)
if len(arguments) > 0 or len(keywords) > 0:
p = args2params(arguments, keywords, self.ctx)
@@ -7795,20 +8132,23 @@ class Tactic:
"""Return the parameter description set."""
return ParamDescrsRef(Z3_tactic_get_param_descrs(self.ctx.ref(), self.tactic), self.ctx)
+
def _to_goal(a):
if isinstance(a, BoolRef):
- goal = Goal(ctx = a.ctx)
+ goal = Goal(ctx=a.ctx)
goal.add(a)
return goal
else:
return a
+
def _to_tactic(t, ctx=None):
if isinstance(t, Tactic):
return t
else:
return Tactic(t, ctx)
+
def _and_then(t1, t2, ctx=None):
t1 = _to_tactic(t1, ctx)
t2 = _to_tactic(t2, ctx)
@@ -7816,6 +8156,7 @@ def _and_then(t1, t2, ctx=None):
_z3_assert(t1.ctx == t2.ctx, "Context mismatch")
return Tactic(Z3_tactic_and_then(t1.ctx.ref(), t1.tactic, t2.tactic), t1.ctx)
+
def _or_else(t1, t2, ctx=None):
t1 = _to_tactic(t1, ctx)
t2 = _to_tactic(t2, ctx)
@@ -7823,6 +8164,7 @@ def _or_else(t1, t2, ctx=None):
_z3_assert(t1.ctx == t2.ctx, "Context mismatch")
return Tactic(Z3_tactic_or_else(t1.ctx.ref(), t1.tactic, t2.tactic), t1.ctx)
+
def AndThen(*ts, **ks):
"""Return a tactic that applies the tactics in `*ts` in sequence.
@@ -7835,13 +8177,14 @@ def AndThen(*ts, **ks):
"""
if z3_debug():
_z3_assert(len(ts) >= 2, "At least two arguments expected")
- ctx = ks.get('ctx', None)
+ ctx = ks.get("ctx", None)
num = len(ts)
r = ts[0]
for i in range(num - 1):
- r = _and_then(r, ts[i+1], ctx)
+ r = _and_then(r, ts[i + 1], ctx)
return r
+
def Then(*ts, **ks):
"""Return a tactic that applies the tactics in `*ts` in sequence. Shorthand for AndThen(*ts, **ks).
@@ -7854,6 +8197,7 @@ def Then(*ts, **ks):
"""
return AndThen(*ts, **ks)
+
def OrElse(*ts, **ks):
"""Return a tactic that applies the tactics in `*ts` until one of them succeeds (it doesn't fail).
@@ -7867,13 +8211,14 @@ def OrElse(*ts, **ks):
"""
if z3_debug():
_z3_assert(len(ts) >= 2, "At least two arguments expected")
- ctx = ks.get('ctx', None)
+ ctx = ks.get("ctx", None)
num = len(ts)
r = ts[0]
for i in range(num - 1):
- r = _or_else(r, ts[i+1], ctx)
+ r = _or_else(r, ts[i + 1], ctx)
return r
+
def ParOr(*ts, **ks):
"""Return a tactic that applies the tactics in `*ts` in parallel until one of them succeeds (it doesn't fail).
@@ -7884,16 +8229,18 @@ def ParOr(*ts, **ks):
"""
if z3_debug():
_z3_assert(len(ts) >= 2, "At least two arguments expected")
- ctx = _get_ctx(ks.get('ctx', None))
- ts = [ _to_tactic(t, ctx) for t in ts ]
- sz = len(ts)
+ ctx = _get_ctx(ks.get("ctx", None))
+ ts = [_to_tactic(t, ctx) for t in ts]
+ sz = len(ts)
_args = (TacticObj * sz)()
for i in range(sz):
_args[i] = ts[i].tactic
return Tactic(Z3_tactic_par_or(ctx.ref(), sz, _args), ctx)
+
def ParThen(t1, t2, ctx=None):
- """Return a tactic that applies t1 and then t2 to every subgoal produced by t1. The subgoals are processed in parallel.
+ """Return a tactic that applies t1 and then t2 to every subgoal produced by t1.
+ The subgoals are processed in parallel.
>>> x, y = Ints('x y')
>>> t = ParThen(Tactic('split-clause'), Tactic('propagate-values'))
@@ -7906,10 +8253,12 @@ def ParThen(t1, t2, ctx=None):
_z3_assert(t1.ctx == t2.ctx, "Context mismatch")
return Tactic(Z3_tactic_par_and_then(t1.ctx.ref(), t1.tactic, t2.tactic), t1.ctx)
+
def ParAndThen(t1, t2, ctx=None):
"""Alias for ParThen(t1, t2, ctx)."""
return ParThen(t1, t2, ctx)
+
def With(t, *args, **keys):
"""Return a tactic that applies tactic `t` using the given configuration options.
@@ -7918,11 +8267,12 @@ def With(t, *args, **keys):
>>> t((x + 1)*(y + 2) == 0)
[[2*x + y + x*y == -2]]
"""
- ctx = keys.pop('ctx', None)
+ ctx = keys.pop("ctx", None)
t = _to_tactic(t, ctx)
p = args2params(args, keys, t.ctx)
return Tactic(Z3_tactic_using_params(t.ctx.ref(), t.tactic, p.params), t.ctx)
+
def WithParams(t, p):
"""Return a tactic that applies tactic `t` using the given configuration options.
@@ -7936,8 +8286,10 @@ def WithParams(t, p):
t = _to_tactic(t, None)
return Tactic(Z3_tactic_using_params(t.ctx.ref(), t.tactic, p.params), t.ctx)
+
def Repeat(t, max=4294967295, ctx=None):
- """Return a tactic that keeps applying `t` until the goal is not modified anymore or the maximum number of iterations `max` is reached.
+ """Return a tactic that keeps applying `t` until the goal is not modified anymore
+ or the maximum number of iterations `max` is reached.
>>> x, y = Ints('x y')
>>> c = And(Or(x == 0, x == 1), Or(y == 0, y == 1), x > y)
@@ -7955,6 +8307,7 @@ def Repeat(t, max=4294967295, ctx=None):
t = _to_tactic(t, ctx)
return Tactic(Z3_tactic_repeat(t.ctx.ref(), t.tactic, max), t.ctx)
+
def TryFor(t, ms, ctx=None):
"""Return a tactic that applies `t` to a given goal for `ms` milliseconds.
@@ -7963,6 +8316,7 @@ def TryFor(t, ms, ctx=None):
t = _to_tactic(t, ctx)
return Tactic(Z3_tactic_try_for(t.ctx.ref(), t.tactic, ms), t.ctx)
+
def tactics(ctx=None):
"""Return a list of all available tactics in Z3.
@@ -7971,7 +8325,8 @@ def tactics(ctx=None):
True
"""
ctx = _get_ctx(ctx)
- return [ Z3_get_tactic_name(ctx.ref(), i) for i in range(Z3_get_num_tactics(ctx.ref())) ]
+ return [Z3_get_tactic_name(ctx.ref(), i) for i in range(Z3_get_num_tactics(ctx.ref()))]
+
def tactic_description(name, ctx=None):
"""Return a short description for the tactic named `name`.
@@ -7981,6 +8336,7 @@ def tactic_description(name, ctx=None):
ctx = _get_ctx(ctx)
return Z3_tactic_get_descr(ctx.ref(), name)
+
def describe_tactics():
"""Display a (tabular) description of all available tactics in Z3."""
if in_html_mode():
@@ -7991,19 +8347,23 @@ def describe_tactics():
print('<tr style="background-color:#CFCFCF">')
even = False
else:
- print('<tr>')
+ print("<tr>")
even = True
- print('<td>%s</td><td>%s</td></tr>' % (t, insert_line_breaks(tactic_description(t), 40)))
- print('</table>')
+ print("<td>%s</td><td>%s</td></tr>" % (t, insert_line_breaks(tactic_description(t), 40)))
+ print("</table>")
else:
for t in tactics():
- print('%s : %s' % (t, tactic_description(t)))
+ print("%s : %s" % (t, tactic_description(t)))
+
class Probe:
- """Probes are used to inspect a goal (aka problem) and collect information that may be used to decide which solver and/or preprocessing step will be used."""
+ """Probes are used to inspect a goal (aka problem) and collect information that may be used
+ to decide which solver and/or preprocessing step will be used.
+ """
+
def __init__(self, probe, ctx=None):
- self.ctx = _get_ctx(ctx)
- self.probe = None
+ self.ctx = _get_ctx(ctx)
+ self.probe = None
if isinstance(probe, ProbeObj):
self.probe = probe
elif isinstance(probe, float):
@@ -8032,7 +8392,8 @@ class Probe:
Z3_probe_dec_ref(self.ctx.ref(), self.probe)
def __lt__(self, other):
- """Return a probe that evaluates to "true" when the value returned by `self` is less than the value returned by `other`.
+ """Return a probe that evaluates to "true" when the value returned by `self`
+ is less than the value returned by `other`.
>>> p = Probe('size') < 10
>>> x = Int('x')
@@ -8045,7 +8406,8 @@ class Probe:
return Probe(Z3_probe_lt(self.ctx.ref(), self.probe, _to_probe(other, self.ctx).probe), self.ctx)
def __gt__(self, other):
- """Return a probe that evaluates to "true" when the value returned by `self` is greater than the value returned by `other`.
+ """Return a probe that evaluates to "true" when the value returned by `self`
+ is greater than the value returned by `other`.
>>> p = Probe('size') > 10
>>> x = Int('x')
@@ -8058,7 +8420,8 @@ class Probe:
return Probe(Z3_probe_gt(self.ctx.ref(), self.probe, _to_probe(other, self.ctx).probe), self.ctx)
def __le__(self, other):
- """Return a probe that evaluates to "true" when the value returned by `self` is less than or equal to the value returned by `other`.
+ """Return a probe that evaluates to "true" when the value returned by `self`
+ is less than or equal to the value returned by `other`.
>>> p = Probe('size') <= 2
>>> x = Int('x')
@@ -8071,7 +8434,8 @@ class Probe:
return Probe(Z3_probe_le(self.ctx.ref(), self.probe, _to_probe(other, self.ctx).probe), self.ctx)
def __ge__(self, other):
- """Return a probe that evaluates to "true" when the value returned by `self` is greater than or equal to the value returned by `other`.
+ """Return a probe that evaluates to "true" when the value returned by `self`
+ is greater than or equal to the value returned by `other`.
>>> p = Probe('size') >= 2
>>> x = Int('x')
@@ -8084,7 +8448,8 @@ class Probe:
return Probe(Z3_probe_ge(self.ctx.ref(), self.probe, _to_probe(other, self.ctx).probe), self.ctx)
def __eq__(self, other):
- """Return a probe that evaluates to "true" when the value returned by `self` is equal to the value returned by `other`.
+ """Return a probe that evaluates to "true" when the value returned by `self`
+ is equal to the value returned by `other`.
>>> p = Probe('size') == 2
>>> x = Int('x')
@@ -8097,7 +8462,8 @@ class Probe:
return Probe(Z3_probe_eq(self.ctx.ref(), self.probe, _to_probe(other, self.ctx).probe), self.ctx)
def __ne__(self, other):
- """Return a probe that evaluates to "true" when the value returned by `self` is not equal to the value returned by `other`.
+ """Return a probe that evaluates to "true" when the value returned by `self`
+ is not equal to the value returned by `other`.
>>> p = Probe('size') != 2
>>> x = Int('x')
@@ -8134,10 +8500,11 @@ class Probe:
1.0
"""
if z3_debug():
- _z3_assert(isinstance(goal, Goal) or isinstance(goal, BoolRef), "Z3 Goal or Boolean expression expected")
+ _z3_assert(isinstance(goal, (Goal, BoolRef)), "Z3 Goal or Boolean expression expected")
goal = _to_goal(goal)
return Z3_probe_apply(self.ctx.ref(), self.probe, goal.goal)
+
def is_probe(p):
"""Return `True` if `p` is a Z3 probe.
@@ -8148,12 +8515,14 @@ def is_probe(p):
"""
return isinstance(p, Probe)
+
def _to_probe(p, ctx=None):
if is_probe(p):
return p
else:
return Probe(p, ctx)
+
def probes(ctx=None):
"""Return a list of all available probes in Z3.
@@ -8162,7 +8531,8 @@ def probes(ctx=None):
True
"""
ctx = _get_ctx(ctx)
- return [ Z3_get_probe_name(ctx.ref(), i) for i in range(Z3_get_num_probes(ctx.ref())) ]
+ return [Z3_get_probe_name(ctx.ref(), i) for i in range(Z3_get_num_probes(ctx.ref()))]
+
def probe_description(name, ctx=None):
"""Return a short description for the probe named `name`.
@@ -8172,6 +8542,7 @@ def probe_description(name, ctx=None):
ctx = _get_ctx(ctx)
return Z3_probe_get_descr(ctx.ref(), name)
+
def describe_probes():
"""Display a (tabular) description of all available probes in Z3."""
if in_html_mode():
@@ -8182,13 +8553,14 @@ def describe_probes():
print('<tr style="background-color:#CFCFCF">')
even = False
else:
- print('<tr>')
+ print("<tr>")
even = True
- print('<td>%s</td><td>%s</td></tr>' % (p, insert_line_breaks(probe_description(p), 40)))
- print('</table>')
+ print("<td>%s</td><td>%s</td></tr>" % (p, insert_line_breaks(probe_description(p), 40)))
+ print("</table>")
else:
for p in probes():
- print('%s : %s' % (p, probe_description(p)))
+ print("%s : %s" % (p, probe_description(p)))
+
def _probe_nary(f, args, ctx):
if z3_debug():
@@ -8196,19 +8568,24 @@ def _probe_nary(f, args, ctx):
num = len(args)
r = _to_probe(args[0], ctx)
for i in range(num - 1):
- r = Probe(f(ctx.ref(), r.probe, _to_probe(args[i+1], ctx).probe), ctx)
+ r = Probe(f(ctx.ref(), r.probe, _to_probe(args[i + 1], ctx).probe), ctx)
return r
+
def _probe_and(args, ctx):
return _probe_nary(Z3_probe_and, args, ctx)
+
def _probe_or(args, ctx):
return _probe_nary(Z3_probe_or, args, ctx)
-def FailIf(p, ctx=None):
- """Return a tactic that fails if the probe `p` evaluates to true. Otherwise, it returns the input goal unmodified.
- In the following example, the tactic applies 'simplify' if and only if there are more than 2 constraints in the goal.
+def FailIf(p, ctx=None):
+ """Return a tactic that fails if the probe `p` evaluates to true.
+ Otherwise, it returns the input goal unmodified.
+
+ In the following example, the tactic applies 'simplify' if and only if there are
+ more than 2 constraints in the goal.
>>> t = OrElse(FailIf(Probe('size') > 2), Tactic('simplify'))
>>> x, y = Ints('x y')
@@ -8224,8 +8601,10 @@ def FailIf(p, ctx=None):
p = _to_probe(p, ctx)
return Tactic(Z3_tactic_fail_if(p.ctx.ref(), p.probe), p.ctx)
+
def When(p, t, ctx=None):
- """Return a tactic that applies tactic `t` only if probe `p` evaluates to true. Otherwise, it returns the input goal unmodified.
+ """Return a tactic that applies tactic `t` only if probe `p` evaluates to true.
+ Otherwise, it returns the input goal unmodified.
>>> t = When(Probe('size') > 2, Tactic('simplify'))
>>> x, y = Ints('x y')
@@ -8242,6 +8621,7 @@ def When(p, t, ctx=None):
t = _to_tactic(t, ctx)
return Tactic(Z3_tactic_when(t.ctx.ref(), p.probe, t.tactic), t.ctx)
+
def Cond(p, t1, t2, ctx=None):
"""Return a tactic that applies tactic `t1` to a goal if probe `p` evaluates to true, and `t2` otherwise.
@@ -8258,6 +8638,7 @@ def Cond(p, t1, t2, ctx=None):
#
#########################################
+
def simplify(a, *arguments, **keywords):
"""Simplify the expression `a` using the given options.
@@ -8282,16 +8663,20 @@ def simplify(a, *arguments, **keywords):
else:
return _to_expr_ref(Z3_simplify(a.ctx_ref(), a.as_ast()), a.ctx)
+
def help_simplify():
"""Return a string describing all options available for Z3 `simplify` procedure."""
print(Z3_simplify_get_help(main_ctx().ref()))
+
def simplify_param_descrs():
"""Return the set of parameter descriptions for Z3 `simplify` procedure."""
return ParamDescrsRef(Z3_simplify_get_param_descrs(main_ctx().ref()), main_ctx())
+
def substitute(t, *m):
- """Apply substitution m on t, m is a list of pairs of the form (from, to). Every occurrence in t of from is replaced with to.
+ """Apply substitution m on t, m is a list of pairs of the form (from, to).
+ Every occurrence in t of from is replaced with to.
>>> x = Int('x')
>>> y = Int('y')
@@ -8307,15 +8692,17 @@ def substitute(t, *m):
m = m1
if z3_debug():
_z3_assert(is_expr(t), "Z3 expression expected")
- _z3_assert(all([isinstance(p, tuple) and is_expr(p[0]) and is_expr(p[1]) and p[0].sort().eq(p[1].sort()) for p in m]), "Z3 invalid substitution, expression pairs expected.")
+ _z3_assert(all([isinstance(p, tuple) and is_expr(p[0]) and is_expr(p[1]) and p[0].sort().eq(
+ p[1].sort()) for p in m]), "Z3 invalid substitution, expression pairs expected.")
num = len(m)
_from = (Ast * num)()
- _to = (Ast * num)()
+ _to = (Ast * num)()
for i in range(num):
_from[i] = m[i][0].as_ast()
- _to[i] = m[i][1].as_ast()
+ _to[i] = m[i][1].as_ast()
return _to_expr_ref(Z3_substitute(t.ctx.ref(), t.as_ast(), num, _from, _to), t.ctx)
+
def substitute_vars(t, *m):
"""Substitute the free variables in t with the expression in m.
@@ -8331,11 +8718,12 @@ def substitute_vars(t, *m):
_z3_assert(is_expr(t), "Z3 expression expected")
_z3_assert(all([is_expr(n) for n in m]), "Z3 invalid substitution, list of expressions expected.")
num = len(m)
- _to = (Ast * num)()
+ _to = (Ast * num)()
for i in range(num):
_to[i] = m[i].as_ast()
return _to_expr_ref(Z3_substitute_vars(t.ctx.ref(), t.as_ast(), num, _to), t.ctx)
+
def Sum(*args):
"""Create the sum of the Z3 expressions.
@@ -8348,13 +8736,13 @@ def Sum(*args):
>>> Sum(A)
a__0 + a__1 + a__2 + a__3 + a__4
"""
- args = _get_args(args)
+ args = _get_args(args)
if len(args) == 0:
return 0
- ctx = _ctx_from_ast_arg_list(args)
+ ctx = _ctx_from_ast_arg_list(args)
if ctx is None:
return _reduce(lambda a, b: a + b, args, 0)
- args = _coerce_expr_list(args, ctx)
+ args = _coerce_expr_list(args, ctx)
if is_bv(args[0]):
return _reduce(lambda a, b: a + b, args, 0)
else:
@@ -8374,29 +8762,30 @@ def Product(*args):
>>> Product(A)
a__0*a__1*a__2*a__3*a__4
"""
- args = _get_args(args)
+ args = _get_args(args)
if len(args) == 0:
return 1
- ctx = _ctx_from_ast_arg_list(args)
+ ctx = _ctx_from_ast_arg_list(args)
if ctx is None:
return _reduce(lambda a, b: a * b, args, 1)
- args = _coerce_expr_list(args, ctx)
+ args = _coerce_expr_list(args, ctx)
if is_bv(args[0]):
return _reduce(lambda a, b: a * b, args, 1)
else:
_args, sz = _to_ast_array(args)
return ArithRef(Z3_mk_mul(ctx.ref(), sz, _args), ctx)
+
def AtMost(*args):
"""Create an at-most Pseudo-Boolean k constraint.
>>> a, b, c = Bools('a b c')
>>> f = AtMost(a, b, c, 2)
"""
- args = _get_args(args)
+ args = _get_args(args)
if z3_debug():
_z3_assert(len(args) > 1, "Non empty list of arguments expected")
- ctx = _ctx_from_ast_arg_list(args)
+ ctx = _ctx_from_ast_arg_list(args)
if z3_debug():
_z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
args1 = _coerce_expr_list(args[:-1], ctx)
@@ -8404,16 +8793,17 @@ def AtMost(*args):
_args, sz = _to_ast_array(args1)
return BoolRef(Z3_mk_atmost(ctx.ref(), sz, _args, k), ctx)
+
def AtLeast(*args):
"""Create an at-most Pseudo-Boolean k constraint.
>>> a, b, c = Bools('a b c')
>>> f = AtLeast(a, b, c, 2)
"""
- args = _get_args(args)
+ args = _get_args(args)
if z3_debug():
_z3_assert(len(args) > 1, "Non empty list of arguments expected")
- ctx = _ctx_from_ast_arg_list(args)
+ ctx = _ctx_from_ast_arg_list(args)
if z3_debug():
_z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
args1 = _coerce_expr_list(args[:-1], ctx)
@@ -8421,21 +8811,23 @@ def AtLeast(*args):
_args, sz = _to_ast_array(args1)
return BoolRef(Z3_mk_atleast(ctx.ref(), sz, _args, k), ctx)
+
def _reorder_pb_arg(arg):
a, b = arg
if not _is_int(b) and _is_int(a):
return b, a
return arg
-def _pb_args_coeffs(args, default_ctx = None):
- args = _get_args_ast_list(args)
+
+def _pb_args_coeffs(args, default_ctx=None):
+ args = _get_args_ast_list(args)
if len(args) == 0:
- return _get_ctx(default_ctx), 0, (Ast * 0)(), (ctypes.c_int * 0)()
+ return _get_ctx(default_ctx), 0, (Ast * 0)(), (ctypes.c_int * 0)()
args = [_reorder_pb_arg(arg) for arg in args]
args, coeffs = zip(*args)
if z3_debug():
_z3_assert(len(args) > 0, "Non empty list of arguments expected")
- ctx = _ctx_from_ast_arg_list(args)
+ ctx = _ctx_from_ast_arg_list(args)
if z3_debug():
_z3_assert(ctx is not None, "At least one of the arguments must be a Z3 expression")
args = _coerce_expr_list(args, ctx)
@@ -8446,6 +8838,7 @@ def _pb_args_coeffs(args, default_ctx = None):
_coeffs[i] = coeffs[i]
return ctx, sz, _args, _coeffs
+
def PbLe(args, k):
"""Create a Pseudo-Boolean inequality k constraint.
@@ -8456,6 +8849,7 @@ def PbLe(args, k):
ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
return BoolRef(Z3_mk_pble(ctx.ref(), sz, _args, _coeffs, k), ctx)
+
def PbGe(args, k):
"""Create a Pseudo-Boolean inequality k constraint.
@@ -8466,7 +8860,8 @@ def PbGe(args, k):
ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
return BoolRef(Z3_mk_pbge(ctx.ref(), sz, _args, _coeffs, k), ctx)
-def PbEq(args, k, ctx = None):
+
+def PbEq(args, k, ctx=None):
"""Create a Pseudo-Boolean inequality k constraint.
>>> a, b, c = Bools('a b c')
@@ -8506,6 +8901,7 @@ def solve(*args, **keywords):
else:
print(s.model())
+
def solve_using(s, *args, **keywords):
"""Solve the constraints `*args` using solver `s`.
@@ -8536,6 +8932,7 @@ def solve_using(s, *args, **keywords):
print("Solution:")
print(s.model())
+
def prove(claim, show=False, **keywords):
"""Try to prove the given claim.
@@ -8563,6 +8960,7 @@ def prove(claim, show=False, **keywords):
print("counterexample")
print(s.model())
+
def _solve_html(*args, **keywords):
"""Version of function `solve` used in RiSE4Fun."""
show = keywords.pop("show", False)
@@ -8586,6 +8984,7 @@ def _solve_html(*args, **keywords):
print("<b>Solution:</b>")
print(s.model())
+
def _solve_using_html(s, *args, **keywords):
"""Version of function `solve_using` used in RiSE4Fun."""
show = keywords.pop("show", False)
@@ -8610,6 +9009,7 @@ def _solve_using_html(s, *args, **keywords):
print("<b>Solution:</b>")
print(s.model())
+
def _prove_html(claim, show=False, **keywords):
"""Version of function `prove` used in RiSE4Fun."""
if z3_debug():
@@ -8629,10 +9029,11 @@ def _prove_html(claim, show=False, **keywords):
print("<b>counterexample</b>")
print(s.model())
+
def _dict2sarray(sorts, ctx):
sz = len(sorts)
_names = (Symbol * sz)()
- _sorts = (Sort * sz) ()
+ _sorts = (Sort * sz)()
i = 0
for k in sorts:
v = sorts[k]
@@ -8644,10 +9045,11 @@ def _dict2sarray(sorts, ctx):
i = i + 1
return sz, _names, _sorts
+
def _dict2darray(decls, ctx):
sz = len(decls)
_names = (Symbol * sz)()
- _decls = (FuncDecl * sz) ()
+ _decls = (FuncDecl * sz)()
i = 0
for k in decls:
v = decls[k]
@@ -8683,6 +9085,7 @@ def parse_smt2_string(s, sorts={}, decls={}, ctx=None):
dsz, dnames, ddecls = _dict2darray(decls, ctx)
return AstVector(Z3_parse_smtlib2_string(ctx.ref(), s, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
+
def parse_smt2_file(f, sorts={}, decls={}, ctx=None):
"""Parse a file in SMT 2.0 format using the given sorts and decls.
@@ -8706,6 +9109,7 @@ _dflt_rounding_mode = Z3_OP_FPA_RM_TOWARD_ZERO
_dflt_fpsort_ebits = 11
_dflt_fpsort_sbits = 53
+
def get_default_rounding_mode(ctx=None):
"""Retrieves the global default rounding mode."""
global _dflt_rounding_mode
@@ -8720,6 +9124,7 @@ def get_default_rounding_mode(ctx=None):
elif _dflt_rounding_mode == Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY:
return RNA(ctx)
+
def set_default_rounding_mode(rm, ctx=None):
global _dflt_rounding_mode
if is_fprm_value(rm):
@@ -8733,21 +9138,26 @@ def set_default_rounding_mode(rm, ctx=None):
"illegal rounding mode")
_dflt_rounding_mode = rm
+
def get_default_fp_sort(ctx=None):
return FPSort(_dflt_fpsort_ebits, _dflt_fpsort_sbits, ctx)
+
def set_default_fp_sort(ebits, sbits, ctx=None):
global _dflt_fpsort_ebits
global _dflt_fpsort_sbits
_dflt_fpsort_ebits = ebits
_dflt_fpsort_sbits = sbits
+
def _dflt_rm(ctx=None):
return get_default_rounding_mode(ctx)
+
def _dflt_fps(ctx=None):
return get_default_fp_sort(ctx)
+
def _coerce_fp_expr_list(alist, ctx):
first_fp_sort = None
for a in alist:
@@ -8755,7 +9165,7 @@ def _coerce_fp_expr_list(alist, ctx):
if first_fp_sort is None:
first_fp_sort = a.sort()
elif first_fp_sort == a.sort():
- pass # OK, same as before
+ pass # OK, same as before
else:
# we saw at least 2 different float sorts; something will
# throw a sort mismatch later, for now assume None.
@@ -8765,33 +9175,34 @@ def _coerce_fp_expr_list(alist, ctx):
r = []
for i in range(len(alist)):
a = alist[i]
- if (isinstance(a, str) and a.contains('2**(') and a.endswith(')')) or _is_int(a) or isinstance(a, float) or isinstance(a, bool):
+ is_repr = isinstance(a, str) and a.contains("2**(") and a.endswith(")")
+ if is_repr or _is_int(a) or isinstance(a, (float, bool)):
r.append(FPVal(a, None, first_fp_sort, ctx))
else:
r.append(a)
return _coerce_expr_list(r, ctx)
-### FP Sorts
+# FP Sorts
class FPSortRef(SortRef):
"""Floating-point sort."""
def ebits(self):
- """Retrieves the number of bits reserved for the exponent in the FloatingPoint sort `self`.
- >>> b = FPSort(8, 24)
- >>> b.ebits()
- 8
- """
- return int(Z3_fpa_get_ebits(self.ctx_ref(), self.ast))
+ """Retrieves the number of bits reserved for the exponent in the FloatingPoint sort `self`.
+ >>> b = FPSort(8, 24)
+ >>> b.ebits()
+ 8
+ """
+ return int(Z3_fpa_get_ebits(self.ctx_ref(), self.ast))
def sbits(self):
- """Retrieves the number of bits reserved for the significand in the FloatingPoint sort `self`.
- >>> b = FPSort(8, 24)
- >>> b.sbits()
- 24
- """
- return int(Z3_fpa_get_sbits(self.ctx_ref(), self.ast))
+ """Retrieves the number of bits reserved for the significand in the FloatingPoint sort `self`.
+ >>> b = FPSort(8, 24)
+ >>> b.sbits()
+ 24
+ """
+ return int(Z3_fpa_get_sbits(self.ctx_ref(), self.ast))
def cast(self, val):
"""Try to cast `val` as a floating-point expression.
@@ -8814,41 +9225,49 @@ def Float16(ctx=None):
ctx = _get_ctx(ctx)
return FPSortRef(Z3_mk_fpa_sort_16(ctx.ref()), ctx)
+
def FloatHalf(ctx=None):
"""Floating-point 16-bit (half) sort."""
ctx = _get_ctx(ctx)
return FPSortRef(Z3_mk_fpa_sort_half(ctx.ref()), ctx)
+
def Float32(ctx=None):
"""Floating-point 32-bit (single) sort."""
ctx = _get_ctx(ctx)
return FPSortRef(Z3_mk_fpa_sort_32(ctx.ref()), ctx)
+
def FloatSingle(ctx=None):
"""Floating-point 32-bit (single) sort."""
ctx = _get_ctx(ctx)
return FPSortRef(Z3_mk_fpa_sort_single(ctx.ref()), ctx)
+
def Float64(ctx=None):
"""Floating-point 64-bit (double) sort."""
ctx = _get_ctx(ctx)
return FPSortRef(Z3_mk_fpa_sort_64(ctx.ref()), ctx)
+
def FloatDouble(ctx=None):
"""Floating-point 64-bit (double) sort."""
ctx = _get_ctx(ctx)
return FPSortRef(Z3_mk_fpa_sort_double(ctx.ref()), ctx)
+
def Float128(ctx=None):
"""Floating-point 128-bit (quadruple) sort."""
ctx = _get_ctx(ctx)
return FPSortRef(Z3_mk_fpa_sort_128(ctx.ref()), ctx)
+
def FloatQuadruple(ctx=None):
"""Floating-point 128-bit (quadruple) sort."""
ctx = _get_ctx(ctx)
return FPSortRef(Z3_mk_fpa_sort_quadruple(ctx.ref()), ctx)
+
class FPRMSortRef(SortRef):
""""Floating-point rounding mode sort."""
@@ -8863,6 +9282,7 @@ def is_fp_sort(s):
"""
return isinstance(s, FPSortRef)
+
def is_fprm_sort(s):
"""Return True if `s` is a Z3 floating-point rounding mode sort.
@@ -8873,7 +9293,8 @@ def is_fprm_sort(s):
"""
return isinstance(s, FPRMSortRef)
-### FP Expressions
+# FP Expressions
+
class FPRef(ExprRef):
"""Floating-point expressions."""
@@ -8890,20 +9311,20 @@ class FPRef(ExprRef):
return FPSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
def ebits(self):
- """Retrieves the number of bits reserved for the exponent in the FloatingPoint expression `self`.
- >>> b = FPSort(8, 24)
- >>> b.ebits()
- 8
- """
- return self.sort().ebits();
+ """Retrieves the number of bits reserved for the exponent in the FloatingPoint expression `self`.
+ >>> b = FPSort(8, 24)
+ >>> b.ebits()
+ 8
+ """
+ return self.sort().ebits()
def sbits(self):
- """Retrieves the number of bits reserved for the exponent in the FloatingPoint expression `self`.
- >>> b = FPSort(8, 24)
- >>> b.sbits()
- 24
- """
- return self.sort().sbits();
+ """Retrieves the number of bits reserved for the exponent in the FloatingPoint expression `self`.
+ >>> b = FPSort(8, 24)
+ >>> b.sbits()
+ 24
+ """
+ return self.sort().sbits()
def as_string(self):
"""Return a Z3 floating point expression as a Python string."""
@@ -9052,6 +9473,7 @@ class FPRef(ExprRef):
"""Create the Z3 expression mod `other % self`."""
return fpRem(other, self)
+
class FPRMRef(ExprRef):
"""Floating-point rounding mode expressions"""
@@ -9064,42 +9486,52 @@ def RoundNearestTiesToEven(ctx=None):
ctx = _get_ctx(ctx)
return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_even(ctx.ref()), ctx)
-def RNE (ctx=None):
+
+def RNE(ctx=None):
ctx = _get_ctx(ctx)
return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_even(ctx.ref()), ctx)
+
def RoundNearestTiesToAway(ctx=None):
ctx = _get_ctx(ctx)
return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_away(ctx.ref()), ctx)
-def RNA (ctx=None):
+
+def RNA(ctx=None):
ctx = _get_ctx(ctx)
return FPRMRef(Z3_mk_fpa_round_nearest_ties_to_away(ctx.ref()), ctx)
+
def RoundTowardPositive(ctx=None):
ctx = _get_ctx(ctx)
return FPRMRef(Z3_mk_fpa_round_toward_positive(ctx.ref()), ctx)
+
def RTP(ctx=None):
ctx = _get_ctx(ctx)
return FPRMRef(Z3_mk_fpa_round_toward_positive(ctx.ref()), ctx)
+
def RoundTowardNegative(ctx=None):
ctx = _get_ctx(ctx)
return FPRMRef(Z3_mk_fpa_round_toward_negative(ctx.ref()), ctx)
+
def RTN(ctx=None):
ctx = _get_ctx(ctx)
return FPRMRef(Z3_mk_fpa_round_toward_negative(ctx.ref()), ctx)
+
def RoundTowardZero(ctx=None):
ctx = _get_ctx(ctx)
return FPRMRef(Z3_mk_fpa_round_toward_zero(ctx.ref()), ctx)
+
def RTZ(ctx=None):
ctx = _get_ctx(ctx)
return FPRMRef(Z3_mk_fpa_round_toward_zero(ctx.ref()), ctx)
+
def is_fprm(a):
"""Return `True` if `a` is a Z3 floating-point rounding mode expression.
@@ -9112,11 +9544,13 @@ def is_fprm(a):
"""
return isinstance(a, FPRMRef)
+
def is_fprm_value(a):
"""Return `True` if `a` is a Z3 floating-point rounding mode numeral value."""
return is_fprm(a) and _is_numeral(a.ctx, a.ast)
-### FP Numerals
+# FP Numerals
+
class FPNumRef(FPRef):
"""The sign of the numeral.
@@ -9128,6 +9562,7 @@ class FPNumRef(FPRef):
>>> x.sign()
True
"""
+
def sign(self):
l = (ctypes.c_int)()
if Z3_fpa_get_numeral_sign(self.ctx.ref(), self.as_ast(), byref(l)) == False:
@@ -9138,6 +9573,7 @@ class FPNumRef(FPRef):
Remark: NaN's are invalid arguments.
"""
+
def sign_as_bv(self):
return BitVecNumRef(Z3_fpa_get_numeral_sign_bv(self.ctx.ref(), self.as_ast()), self.ctx)
@@ -9147,6 +9583,7 @@ class FPNumRef(FPRef):
>>> x.significand()
1.25
"""
+
def significand(self):
return Z3_fpa_get_numeral_significand_string(self.ctx.ref(), self.as_ast())
@@ -9156,6 +9593,7 @@ class FPNumRef(FPRef):
>>> x.significand_as_long()
1.25
"""
+
def significand_as_long(self):
ptr = (ctypes.c_ulonglong * 1)()
if not Z3_fpa_get_numeral_significand_uint64(self.ctx.ref(), self.as_ast(), ptr):
@@ -9166,6 +9604,7 @@ class FPNumRef(FPRef):
Remark: NaN are invalid arguments.
"""
+
def significand_as_bv(self):
return BitVecNumRef(Z3_fpa_get_numeral_significand_bv(self.ctx.ref(), self.as_ast()), self.ctx)
@@ -9175,6 +9614,7 @@ class FPNumRef(FPRef):
>>> x.exponent()
1
"""
+
def exponent(self, biased=True):
return Z3_fpa_get_numeral_exponent_string(self.ctx.ref(), self.as_ast(), biased)
@@ -9184,6 +9624,7 @@ class FPNumRef(FPRef):
>>> x.exponent_as_long()
1
"""
+
def exponent_as_long(self, biased=True):
ptr = (ctypes.c_longlong * 1)()
if not Z3_fpa_get_numeral_exponent_int64(self.ctx.ref(), self.as_ast(), ptr, biased):
@@ -9194,34 +9635,42 @@ class FPNumRef(FPRef):
Remark: NaNs are invalid arguments.
"""
+
def exponent_as_bv(self, biased=True):
return BitVecNumRef(Z3_fpa_get_numeral_exponent_bv(self.ctx.ref(), self.as_ast(), biased), self.ctx)
"""Indicates whether the numeral is a NaN."""
+
def isNaN(self):
return Z3_fpa_is_numeral_nan(self.ctx.ref(), self.as_ast())
"""Indicates whether the numeral is +oo or -oo."""
+
def isInf(self):
return Z3_fpa_is_numeral_inf(self.ctx.ref(), self.as_ast())
"""Indicates whether the numeral is +zero or -zero."""
+
def isZero(self):
return Z3_fpa_is_numeral_zero(self.ctx.ref(), self.as_ast())
"""Indicates whether the numeral is normal."""
+
def isNormal(self):
return Z3_fpa_is_numeral_normal(self.ctx.ref(), self.as_ast())
"""Indicates whether the numeral is subnormal."""
+
def isSubnormal(self):
return Z3_fpa_is_numeral_subnormal(self.ctx.ref(), self.as_ast())
"""Indicates whether the numeral is positive."""
+
def isPositive(self):
return Z3_fpa_is_numeral_positive(self.ctx.ref(), self.as_ast())
"""Indicates whether the numeral is negative."""
+
def isNegative(self):
return Z3_fpa_is_numeral_negative(self.ctx.ref(), self.as_ast())
@@ -9232,10 +9681,12 @@ class FPNumRef(FPRef):
>>> x.as_string()
1.25*(2**4)
"""
+
def as_string(self):
s = Z3_get_numeral_string(self.ctx.ref(), self.as_ast())
return ("FPVal(%s, %s)" % (s, self.sort()))
+
def is_fp(a):
"""Return `True` if `a` is a Z3 floating-point expression.
@@ -9249,6 +9700,7 @@ def is_fp(a):
"""
return isinstance(a, FPRef)
+
def is_fp_value(a):
"""Return `True` if `a` is a Z3 floating-point numeral value.
@@ -9263,6 +9715,7 @@ def is_fp_value(a):
"""
return is_fp(a) and _is_numeral(a.ctx, a.ast)
+
def FPSort(ebits, sbits, ctx=None):
"""Return a Z3 floating-point sort of the given sizes. If `ctx=None`, then the global context is used.
@@ -9277,6 +9730,7 @@ def FPSort(ebits, sbits, ctx=None):
ctx = _get_ctx(ctx)
return FPSortRef(Z3_mk_fpa_sort(ctx.ref(), ebits, sbits), ctx)
+
def _to_float_str(val, exp=0):
if isinstance(val, float):
if math.isnan(val):
@@ -9295,8 +9749,8 @@ def _to_float_str(val, exp=0):
v = val.as_integer_ratio()
num = v[0]
den = v[1]
- rvs = str(num) + '/' + str(den)
- res = rvs + 'p' + _to_int_str(exp)
+ rvs = str(num) + "/" + str(den)
+ res = rvs + "p" + _to_int_str(exp)
elif isinstance(val, bool):
if val:
res = "1.0"
@@ -9305,12 +9759,12 @@ def _to_float_str(val, exp=0):
elif _is_int(val):
res = str(val)
elif isinstance(val, str):
- inx = val.find('*(2**')
+ inx = val.find("*(2**")
if inx == -1:
res = val
- elif val[-1] == ')':
+ elif val[-1] == ")":
res = val[0:inx]
- exp = str(int(val[inx+5:-1]) + int(exp))
+ exp = str(int(val[inx + 5:-1]) + int(exp))
else:
_z3_assert(False, "String does not have floating-point numeral form.")
elif z3_debug():
@@ -9318,7 +9772,7 @@ def _to_float_str(val, exp=0):
if exp == 0:
return res
else:
- return res + 'p' + exp
+ return res + "p" + exp
def fpNaN(s):
@@ -9337,6 +9791,7 @@ def fpNaN(s):
_z3_assert(isinstance(s, FPSortRef), "sort mismatch")
return FPNumRef(Z3_mk_fpa_nan(s.ctx_ref(), s.ast), s.ctx)
+
def fpPlusInfinity(s):
"""Create a Z3 floating-point +oo term.
@@ -9353,35 +9808,42 @@ def fpPlusInfinity(s):
_z3_assert(isinstance(s, FPSortRef), "sort mismatch")
return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, False), s.ctx)
+
def fpMinusInfinity(s):
"""Create a Z3 floating-point -oo term."""
_z3_assert(isinstance(s, FPSortRef), "sort mismatch")
return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, True), s.ctx)
+
def fpInfinity(s, negative):
"""Create a Z3 floating-point +oo or -oo term."""
_z3_assert(isinstance(s, FPSortRef), "sort mismatch")
_z3_assert(isinstance(negative, bool), "expected Boolean flag")
return FPNumRef(Z3_mk_fpa_inf(s.ctx_ref(), s.ast, negative), s.ctx)
+
def fpPlusZero(s):
"""Create a Z3 floating-point +0.0 term."""
_z3_assert(isinstance(s, FPSortRef), "sort mismatch")
return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, False), s.ctx)
+
def fpMinusZero(s):
"""Create a Z3 floating-point -0.0 term."""
_z3_assert(isinstance(s, FPSortRef), "sort mismatch")
return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, True), s.ctx)
+
def fpZero(s, negative):
"""Create a Z3 floating-point +0.0 or -0.0 term."""
_z3_assert(isinstance(s, FPSortRef), "sort mismatch")
_z3_assert(isinstance(negative, bool), "expected Boolean flag")
return FPNumRef(Z3_mk_fpa_zero(s.ctx_ref(), s.ast, negative), s.ctx)
+
def FPVal(sig, exp=None, fps=None, ctx=None):
- """Return a floating-point value of value `val` and sort `fps`. If `ctx=None`, then the global context is used.
+ """Return a floating-point value of value `val` and sort `fps`.
+ If `ctx=None`, then the global context is used.
>>> v = FPVal(20.0, FPSort(8, 24))
>>> v
@@ -9424,6 +9886,7 @@ def FPVal(sig, exp=None, fps=None, ctx=None):
else:
return FPNumRef(Z3_mk_numeral(ctx.ref(), val, fps.ast), ctx)
+
def FP(name, fpsort, ctx=None):
"""Return a floating-point constant named `name`.
`fpsort` is the floating-point sort.
@@ -9447,6 +9910,7 @@ def FP(name, fpsort, ctx=None):
ctx = _get_ctx(ctx)
return FPRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), fpsort.ast), ctx)
+
def FPs(names, fpsort, ctx=None):
"""Return an array of floating-point constants.
@@ -9465,6 +9929,7 @@ def FPs(names, fpsort, ctx=None):
names = names.split(" ")
return [FP(name, fpsort, ctx) for name in names]
+
def fpAbs(a, ctx=None):
"""Create a Z3 floating-point absolute value expression.
@@ -9487,6 +9952,7 @@ def fpAbs(a, ctx=None):
[a] = _coerce_fp_expr_list([a], ctx)
return FPRef(Z3_mk_fpa_abs(ctx.ref(), a.as_ast()), ctx)
+
def fpNeg(a, ctx=None):
"""Create a Z3 floating-point addition expression.
@@ -9502,6 +9968,7 @@ def fpNeg(a, ctx=None):
[a] = _coerce_fp_expr_list([a], ctx)
return FPRef(Z3_mk_fpa_neg(ctx.ref(), a.as_ast()), ctx)
+
def _mk_fp_unary(f, rm, a, ctx):
ctx = _get_ctx(ctx)
[a] = _coerce_fp_expr_list([a], ctx)
@@ -9510,6 +9977,7 @@ def _mk_fp_unary(f, rm, a, ctx):
_z3_assert(is_fp(a), "Second argument must be a Z3 floating-point expression")
return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast()), ctx)
+
def _mk_fp_unary_pred(f, a, ctx):
ctx = _get_ctx(ctx)
[a] = _coerce_fp_expr_list([a], ctx)
@@ -9517,6 +9985,7 @@ def _mk_fp_unary_pred(f, a, ctx):
_z3_assert(is_fp(a), "First argument must be a Z3 floating-point expression")
return BoolRef(f(ctx.ref(), a.as_ast()), ctx)
+
def _mk_fp_bin(f, rm, a, b, ctx):
ctx = _get_ctx(ctx)
[a, b] = _coerce_fp_expr_list([a, b], ctx)
@@ -9525,6 +9994,7 @@ def _mk_fp_bin(f, rm, a, b, ctx):
_z3_assert(is_fp(a) or is_fp(b), "Second or third argument must be a Z3 floating-point expression")
return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast(), b.as_ast()), ctx)
+
def _mk_fp_bin_norm(f, a, b, ctx):
ctx = _get_ctx(ctx)
[a, b] = _coerce_fp_expr_list([a, b], ctx)
@@ -9532,6 +10002,7 @@ def _mk_fp_bin_norm(f, a, b, ctx):
_z3_assert(is_fp(a) or is_fp(b), "First or second argument must be a Z3 floating-point expression")
return FPRef(f(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
+
def _mk_fp_bin_pred(f, a, b, ctx):
ctx = _get_ctx(ctx)
[a, b] = _coerce_fp_expr_list([a, b], ctx)
@@ -9539,14 +10010,17 @@ def _mk_fp_bin_pred(f, a, b, ctx):
_z3_assert(is_fp(a) or is_fp(b), "First or second argument must be a Z3 floating-point expression")
return BoolRef(f(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
+
def _mk_fp_tern(f, rm, a, b, c, ctx):
ctx = _get_ctx(ctx)
[a, b, c] = _coerce_fp_expr_list([a, b, c], ctx)
if z3_debug():
_z3_assert(is_fprm(rm), "First argument must be a Z3 floating-point rounding mode expression")
- _z3_assert(is_fp(a) or is_fp(b) or is_fp(c), "Second, third or fourth argument must be a Z3 floating-point expression")
+ _z3_assert(is_fp(a) or is_fp(b) or is_fp(
+ c), "Second, third or fourth argument must be a Z3 floating-point expression")
return FPRef(f(ctx.ref(), rm.as_ast(), a.as_ast(), b.as_ast(), c.as_ast()), ctx)
+
def fpAdd(rm, a, b, ctx=None):
"""Create a Z3 floating-point addition expression.
@@ -9563,6 +10037,7 @@ def fpAdd(rm, a, b, ctx=None):
"""
return _mk_fp_bin(Z3_mk_fpa_add, rm, a, b, ctx)
+
def fpSub(rm, a, b, ctx=None):
"""Create a Z3 floating-point subtraction expression.
@@ -9577,6 +10052,7 @@ def fpSub(rm, a, b, ctx=None):
"""
return _mk_fp_bin(Z3_mk_fpa_sub, rm, a, b, ctx)
+
def fpMul(rm, a, b, ctx=None):
"""Create a Z3 floating-point multiplication expression.
@@ -9591,6 +10067,7 @@ def fpMul(rm, a, b, ctx=None):
"""
return _mk_fp_bin(Z3_mk_fpa_mul, rm, a, b, ctx)
+
def fpDiv(rm, a, b, ctx=None):
"""Create a Z3 floating-point division expression.
@@ -9605,6 +10082,7 @@ def fpDiv(rm, a, b, ctx=None):
"""
return _mk_fp_bin(Z3_mk_fpa_div, rm, a, b, ctx)
+
def fpRem(a, b, ctx=None):
"""Create a Z3 floating-point remainder expression.
@@ -9618,6 +10096,7 @@ def fpRem(a, b, ctx=None):
"""
return _mk_fp_bin_norm(Z3_mk_fpa_rem, a, b, ctx)
+
def fpMin(a, b, ctx=None):
"""Create a Z3 floating-point minimum expression.
@@ -9632,6 +10111,7 @@ def fpMin(a, b, ctx=None):
"""
return _mk_fp_bin_norm(Z3_mk_fpa_min, a, b, ctx)
+
def fpMax(a, b, ctx=None):
"""Create a Z3 floating-point maximum expression.
@@ -9646,21 +10126,25 @@ def fpMax(a, b, ctx=None):
"""
return _mk_fp_bin_norm(Z3_mk_fpa_max, a, b, ctx)
+
def fpFMA(rm, a, b, c, ctx=None):
"""Create a Z3 floating-point fused multiply-add expression.
"""
return _mk_fp_tern(Z3_mk_fpa_fma, rm, a, b, c, ctx)
+
def fpSqrt(rm, a, ctx=None):
"""Create a Z3 floating-point square root expression.
"""
return _mk_fp_unary(Z3_mk_fpa_sqrt, rm, a, ctx)
+
def fpRoundToIntegral(rm, a, ctx=None):
"""Create a Z3 floating-point roundToIntegral expression.
"""
return _mk_fp_unary(Z3_mk_fpa_round_to_integral, rm, a, ctx)
+
def fpIsNaN(a, ctx=None):
"""Create a Z3 floating-point isNaN expression.
@@ -9672,6 +10156,7 @@ def fpIsNaN(a, ctx=None):
"""
return _mk_fp_unary_pred(Z3_mk_fpa_is_nan, a, ctx)
+
def fpIsInf(a, ctx=None):
"""Create a Z3 floating-point isInfinite expression.
@@ -9682,35 +10167,42 @@ def fpIsInf(a, ctx=None):
"""
return _mk_fp_unary_pred(Z3_mk_fpa_is_infinite, a, ctx)
+
def fpIsZero(a, ctx=None):
"""Create a Z3 floating-point isZero expression.
"""
return _mk_fp_unary_pred(Z3_mk_fpa_is_zero, a, ctx)
+
def fpIsNormal(a, ctx=None):
"""Create a Z3 floating-point isNormal expression.
"""
return _mk_fp_unary_pred(Z3_mk_fpa_is_normal, a, ctx)
+
def fpIsSubnormal(a, ctx=None):
"""Create a Z3 floating-point isSubnormal expression.
"""
return _mk_fp_unary_pred(Z3_mk_fpa_is_subnormal, a, ctx)
+
def fpIsNegative(a, ctx=None):
"""Create a Z3 floating-point isNegative expression.
"""
return _mk_fp_unary_pred(Z3_mk_fpa_is_negative, a, ctx)
+
def fpIsPositive(a, ctx=None):
"""Create a Z3 floating-point isPositive expression.
"""
return _mk_fp_unary_pred(Z3_mk_fpa_is_positive, a, ctx)
+
def _check_fp_args(a, b):
if z3_debug():
_z3_assert(is_fp(a) or is_fp(b), "First or second argument must be a Z3 floating-point expression")
+
def fpLT(a, b, ctx=None):
"""Create the Z3 floating-point expression `other < self`.
@@ -9722,6 +10214,7 @@ def fpLT(a, b, ctx=None):
"""
return _mk_fp_bin_pred(Z3_mk_fpa_lt, a, b, ctx)
+
def fpLEQ(a, b, ctx=None):
"""Create the Z3 floating-point expression `other <= self`.
@@ -9733,6 +10226,7 @@ def fpLEQ(a, b, ctx=None):
"""
return _mk_fp_bin_pred(Z3_mk_fpa_leq, a, b, ctx)
+
def fpGT(a, b, ctx=None):
"""Create the Z3 floating-point expression `other > self`.
@@ -9744,6 +10238,7 @@ def fpGT(a, b, ctx=None):
"""
return _mk_fp_bin_pred(Z3_mk_fpa_gt, a, b, ctx)
+
def fpGEQ(a, b, ctx=None):
"""Create the Z3 floating-point expression `other >= self`.
@@ -9755,6 +10250,7 @@ def fpGEQ(a, b, ctx=None):
"""
return _mk_fp_bin_pred(Z3_mk_fpa_geq, a, b, ctx)
+
def fpEQ(a, b, ctx=None):
"""Create the Z3 floating-point expression `fpEQ(other, self)`.
@@ -9766,6 +10262,7 @@ def fpEQ(a, b, ctx=None):
"""
return _mk_fp_bin_pred(Z3_mk_fpa_eq, a, b, ctx)
+
def fpNEQ(a, b, ctx=None):
"""Create the Z3 floating-point expression `Not(fpEQ(other, self))`.
@@ -9777,6 +10274,7 @@ def fpNEQ(a, b, ctx=None):
"""
return Not(fpEQ(a, b, ctx))
+
def fpFP(sgn, exp, sig, ctx=None):
"""Create the Z3 floating-point value `fpFP(sgn, sig, exp)` from the three bit-vectors sgn, sig, and exp.
@@ -9805,6 +10303,7 @@ def fpFP(sgn, exp, sig, ctx=None):
_z3_assert(ctx == sgn.ctx == exp.ctx == sig.ctx, "context mismatch")
return FPRef(Z3_mk_fpa_fp(ctx.ref(), sgn.ast, exp.ast, sig.ast), ctx)
+
def fpToFP(a1, a2=None, a3=None, ctx=None):
"""Create a Z3 floating-point conversion expression from other term sorts
to floating-point.
@@ -9843,6 +10342,7 @@ def fpToFP(a1, a2=None, a3=None, ctx=None):
else:
raise Z3Exception("Unsupported combination of arguments for conversion to floating-point term.")
+
def fpBVToFP(v, sort, ctx=None):
"""Create a Z3 floating-point conversion expression that represents the
conversion from a bit-vector term to a floating-point term.
@@ -9859,6 +10359,7 @@ def fpBVToFP(v, sort, ctx=None):
ctx = _get_ctx(ctx)
return FPRef(Z3_mk_fpa_to_fp_bv(ctx.ref(), v.ast, sort.ast), ctx)
+
def fpFPToFP(rm, v, sort, ctx=None):
"""Create a Z3 floating-point conversion expression that represents the
conversion from a floating-point term to a floating-point term of different precision.
@@ -9878,6 +10379,7 @@ def fpFPToFP(rm, v, sort, ctx=None):
ctx = _get_ctx(ctx)
return FPRef(Z3_mk_fpa_to_fp_float(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
+
def fpRealToFP(rm, v, sort, ctx=None):
"""Create a Z3 floating-point conversion expression that represents the
conversion from a real term to a floating-point term.
@@ -9895,6 +10397,7 @@ def fpRealToFP(rm, v, sort, ctx=None):
ctx = _get_ctx(ctx)
return FPRef(Z3_mk_fpa_to_fp_real(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
+
def fpSignedToFP(rm, v, sort, ctx=None):
"""Create a Z3 floating-point conversion expression that represents the
conversion from a signed bit-vector term (encoding an integer) to a floating-point term.
@@ -9912,6 +10415,7 @@ def fpSignedToFP(rm, v, sort, ctx=None):
ctx = _get_ctx(ctx)
return FPRef(Z3_mk_fpa_to_fp_signed(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
+
def fpUnsignedToFP(rm, v, sort, ctx=None):
"""Create a Z3 floating-point conversion expression that represents the
conversion from an unsigned bit-vector term (encoding an integer) to a floating-point term.
@@ -9929,6 +10433,7 @@ def fpUnsignedToFP(rm, v, sort, ctx=None):
ctx = _get_ctx(ctx)
return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, v.ast, sort.ast), ctx)
+
def fpToFPUnsigned(rm, x, s, ctx=None):
"""Create a Z3 floating-point conversion expression, from unsigned bit-vector to floating-point expression."""
if z3_debug():
@@ -9938,6 +10443,7 @@ def fpToFPUnsigned(rm, x, s, ctx=None):
ctx = _get_ctx(ctx)
return FPRef(Z3_mk_fpa_to_fp_unsigned(ctx.ref(), rm.ast, x.ast, s.ast), ctx)
+
def fpToSBV(rm, x, s, ctx=None):
"""Create a Z3 floating-point conversion expression, from floating-point expression to signed bit-vector.
@@ -9959,6 +10465,7 @@ def fpToSBV(rm, x, s, ctx=None):
ctx = _get_ctx(ctx)
return BitVecRef(Z3_mk_fpa_to_sbv(ctx.ref(), rm.ast, x.ast, s.size()), ctx)
+
def fpToUBV(rm, x, s, ctx=None):
"""Create a Z3 floating-point conversion expression, from floating-point expression to unsigned bit-vector.
@@ -9980,6 +10487,7 @@ def fpToUBV(rm, x, s, ctx=None):
ctx = _get_ctx(ctx)
return BitVecRef(Z3_mk_fpa_to_ubv(ctx.ref(), rm.ast, x.ast, s.size()), ctx)
+
def fpToReal(x, ctx=None):
"""Create a Z3 floating-point conversion expression, from floating-point expression to real.
@@ -9999,6 +10507,7 @@ def fpToReal(x, ctx=None):
ctx = _get_ctx(ctx)
return ArithRef(Z3_mk_fpa_to_real(ctx.ref(), x.ast), ctx)
+
def fpToIEEEBV(x, ctx=None):
"""\brief Conversion of a floating-point term into a bit-vector term in IEEE 754-2008 format.
@@ -10025,7 +10534,6 @@ def fpToIEEEBV(x, ctx=None):
return BitVecRef(Z3_mk_fpa_to_ieee_bv(ctx.ref(), x.ast), ctx)
-
#########################################
#
# Strings, Sequences and Regular expressions
@@ -10068,6 +10576,7 @@ def SeqSort(s):
"""
return SeqSortRef(Z3_mk_seq_sort(s.ctx_ref(), s.ast), s.ctx)
+
class SeqRef(ExprRef):
"""Sequence expression."""
@@ -10096,13 +10605,12 @@ class SeqRef(ExprRef):
def is_string_value(self):
return Z3_is_string(self.ctx_ref(), self.as_ast())
-
def as_string(self):
"""Return a string representation of sequence expression."""
if self.is_string_value():
string_length = ctypes.c_uint()
chars = Z3_get_lstring(self.ctx_ref(), self.as_ast(), byref(string_length))
- return string_at(chars, size=string_length.value).decode('latin-1')
+ return string_at(chars, size=string_length.value).decode("latin-1")
return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
def __le__(self, other):
@@ -10128,6 +10636,7 @@ def _coerce_seq(s, ctx=None):
raise Z3Exception("Non-sequence passed as a sequence")
return s
+
def _get_ctx2(a, b, ctx=None):
if is_expr(a):
return a.ctx
@@ -10137,6 +10646,7 @@ def _get_ctx2(a, b, ctx=None):
ctx = main_ctx()
return ctx
+
def is_seq(a):
"""Return `True` if `a` is a Z3 sequence expression.
>>> print (is_seq(Unit(IntVal(0))))
@@ -10146,6 +10656,7 @@ def is_seq(a):
"""
return isinstance(a, SeqRef)
+
def is_string(a):
"""Return `True` if `a` is a Z3 string expression.
>>> print (is_string(StringVal("ab")))
@@ -10153,6 +10664,7 @@ def is_string(a):
"""
return isinstance(a, SeqRef) and a.is_string()
+
def is_string_value(a):
"""return 'True' if 'a' is a Z3 string constant expression.
>>> print (is_string_value(StringVal("a")))
@@ -10169,6 +10681,7 @@ def StringVal(s, ctx=None):
ctx = _get_ctx(ctx)
return SeqRef(Z3_mk_lstring(ctx.ref(), len(s), s), ctx)
+
def String(name, ctx=None):
"""Return a string constant named `name`. If `ctx=None`, then the global context is used.
@@ -10177,6 +10690,7 @@ def String(name, ctx=None):
ctx = _get_ctx(ctx)
return SeqRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), StringSort(ctx).ast), ctx)
+
def Strings(names, ctx=None):
"""Return string constants"""
ctx = _get_ctx(ctx)
@@ -10184,14 +10698,17 @@ def Strings(names, ctx=None):
names = names.split(" ")
return [String(name, ctx) for name in names]
+
def SubString(s, offset, length):
"""Extract substring or subsequence starting at offset"""
return Extract(s, offset, length)
+
def SubSeq(s, offset, length):
"""Extract substring or subsequence starting at offset"""
return Extract(s, offset, length)
+
def Strings(names, ctx=None):
"""Return a tuple of String constants. """
ctx = _get_ctx(ctx)
@@ -10199,6 +10716,7 @@ def Strings(names, ctx=None):
names = names.split(" ")
return [String(name, ctx) for name in names]
+
def Empty(s):
"""Create the empty sequence of the given sort
>>> e = Empty(StringSort())
@@ -10213,11 +10731,12 @@ def Empty(s):
Empty(ReSort(Seq(Int)))
"""
if isinstance(s, SeqSortRef):
- return SeqRef(Z3_mk_seq_empty(s.ctx_ref(), s.ast), s.ctx)
+ return SeqRef(Z3_mk_seq_empty(s.ctx_ref(), s.ast), s.ctx)
if isinstance(s, ReSortRef):
- return ReRef(Z3_mk_re_empty(s.ctx_ref(), s.ast), s.ctx)
+ return ReRef(Z3_mk_re_empty(s.ctx_ref(), s.ast), s.ctx)
raise Z3Exception("Non-sequence, non-regular expression sort passed to Empty")
+
def Full(s):
"""Create the regular expression that accepts the universal language
>>> e = Full(ReSort(SeqSort(IntSort())))
@@ -10228,7 +10747,7 @@ def Full(s):
Full(ReSort(String))
"""
if isinstance(s, ReSortRef):
- return ReRef(Z3_mk_re_full(s.ctx_ref(), s.ast), s.ctx)
+ return ReRef(Z3_mk_re_full(s.ctx_ref(), s.ast), s.ctx)
raise Z3Exception("Non-sequence, non-regular expression sort passed to Full")
@@ -10236,6 +10755,7 @@ def Unit(a):
"""Create a singleton sequence"""
return SeqRef(Z3_mk_seq_unit(a.ctx_ref(), a.as_ast()), a.ctx)
+
def PrefixOf(a, b):
"""Check if 'a' is a prefix of 'b'
>>> s1 = PrefixOf("ab", "abc")
@@ -10250,6 +10770,7 @@ def PrefixOf(a, b):
b = _coerce_seq(b, ctx)
return BoolRef(Z3_mk_seq_prefix(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
+
def SuffixOf(a, b):
"""Check if 'a' is a suffix of 'b'
>>> s1 = SuffixOf("ab", "abc")
@@ -10264,6 +10785,7 @@ def SuffixOf(a, b):
b = _coerce_seq(b, ctx)
return BoolRef(Z3_mk_seq_suffix(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
+
def Contains(a, b):
"""Check if 'a' contains 'b'
>>> s1 = Contains("abc", "ab")
@@ -10294,12 +10816,14 @@ def Replace(s, src, dst):
ctx = src.ctx
src = _coerce_seq(src, ctx)
dst = _coerce_seq(dst, ctx)
- s = _coerce_seq(s, ctx)
+ s = _coerce_seq(s, ctx)
return SeqRef(Z3_mk_seq_replace(src.ctx_ref(), s.as_ast(), src.as_ast(), dst.as_ast()), s.ctx)
+
def IndexOf(s, substr):
return IndexOf(s, substr, IntVal(0))
+
def IndexOf(s, substr, offset):
"""Retrieve the index of substring within a string starting at a specified offset.
>>> simplify(IndexOf("abcabc", "bc", 0))
@@ -10317,6 +10841,7 @@ def IndexOf(s, substr, offset):
offset = IntVal(offset, ctx)
return ArithRef(Z3_mk_seq_index(s.ctx_ref(), s.as_ast(), substr.as_ast(), offset.as_ast()), s.ctx)
+
def LastIndexOf(s, substr):
"""Retrieve the last index of substring within a string"""
ctx = None
@@ -10335,6 +10860,7 @@ def Length(s):
s = _coerce_seq(s)
return ArithRef(Z3_mk_seq_length(s.ctx_ref(), s.as_ast()), s.ctx)
+
def StrToInt(s):
"""Convert string expression to integer
>>> a = StrToInt("1")
@@ -10368,9 +10894,7 @@ def Re(s, ctx=None):
return ReRef(Z3_mk_seq_to_re(s.ctx_ref(), s.as_ast()), s.ctx)
-
-
-## Regular expressions
+# Regular expressions
class ReSortRef(SortRef):
"""Regular expression sort."""
@@ -10378,6 +10902,7 @@ class ReSortRef(SortRef):
def basis(self):
return _to_sort_ref(Z3_get_re_sort_basis(self.ctx_ref(), self.ast), self.ctx)
+
def ReSort(s):
if is_ast(s):
return ReSortRef(Z3_mk_re_sort(s.ctx.ref(), s.ast), s.ctx)
@@ -10393,6 +10918,7 @@ class ReRef(ExprRef):
def __add__(self, other):
return Union(self, other)
+
def is_re(s):
return isinstance(s, ReRef)
@@ -10410,6 +10936,7 @@ def InRe(s, re):
s = _coerce_seq(s, re.ctx)
return BoolRef(Z3_mk_seq_in_re(s.ctx_ref(), s.as_ast(), re.as_ast()), s.ctx)
+
def Union(*args):
"""Create union of regular expressions.
>>> re = Union(Re("a"), Re("b"), Re("c"))
@@ -10429,6 +10956,7 @@ def Union(*args):
v[i] = args[i].as_ast()
return ReRef(Z3_mk_re_union(ctx.ref(), sz, v), ctx)
+
def Intersect(*args):
"""Create intersection of regular expressions.
>>> re = Intersect(Re("a"), Re("b"), Re("c"))
@@ -10446,6 +10974,7 @@ def Intersect(*args):
v[i] = args[i].as_ast()
return ReRef(Z3_mk_re_intersect(ctx.ref(), sz, v), ctx)
+
def Plus(re):
"""Create the regular expression accepting one or more repetitions of argument.
>>> re = Plus(Re("a"))
@@ -10458,6 +10987,7 @@ def Plus(re):
"""
return ReRef(Z3_mk_re_plus(re.ctx_ref(), re.as_ast()), re.ctx)
+
def Option(re):
"""Create the regular expression that optionally accepts the argument.
>>> re = Option(Re("a"))
@@ -10470,10 +11000,12 @@ def Option(re):
"""
return ReRef(Z3_mk_re_option(re.ctx_ref(), re.as_ast()), re.ctx)
+
def Complement(re):
"""Create the complement regular expression."""
return ReRef(Z3_mk_re_complement(re.ctx_ref(), re.as_ast()), re.ctx)
+
def Star(re):
"""Create the regular expression accepting zero or more repetitions of argument.
>>> re = Star(Re("a"))
@@ -10486,6 +11018,7 @@ def Star(re):
"""
return ReRef(Z3_mk_re_star(re.ctx_ref(), re.as_ast()), re.ctx)
+
def Loop(re, lo, hi=0):
"""Create the regular expression accepting between a lower and upper bound repetitions
>>> re = Loop(Re("a"), 1, 3)
@@ -10498,7 +11031,8 @@ def Loop(re, lo, hi=0):
"""
return ReRef(Z3_mk_re_loop(re.ctx_ref(), re.as_ast(), lo, hi), re.ctx)
-def Range(lo, hi, ctx = None):
+
+def Range(lo, hi, ctx=None):
"""Create the range regular expression over two sequences of length 1
>>> range = Range("a","z")
>>> print(simplify(InRe("b", range)))
@@ -10512,17 +11046,22 @@ def Range(lo, hi, ctx = None):
# Special Relations
+
def PartialOrder(a, index):
- return FuncDeclRef(Z3_mk_partial_order(a.ctx_ref(), a.ast, index), a.ctx);
+ return FuncDeclRef(Z3_mk_partial_order(a.ctx_ref(), a.ast, index), a.ctx)
+
def LinearOrder(a, index):
- return FuncDeclRef(Z3_mk_linear_order(a.ctx_ref(), a.ast, index), a.ctx);
+ return FuncDeclRef(Z3_mk_linear_order(a.ctx_ref(), a.ast, index), a.ctx)
+
def TreeOrder(a, index):
- return FuncDeclRef(Z3_mk_tree_order(a.ctx_ref(), a.ast, index), a.ctx);
+ return FuncDeclRef(Z3_mk_tree_order(a.ctx_ref(), a.ast, index), a.ctx)
+
def PiecewiseLinearOrder(a, index):
- return FuncDeclRef(Z3_mk_piecewise_linear_order(a.ctx_ref(), a.ast, index), a.ctx);
+ return FuncDeclRef(Z3_mk_piecewise_linear_order(a.ctx_ref(), a.ast, index), a.ctx)
+
def TransitiveClosure(f):
"""Given a binary relation R, such that the two arguments have the same sort
@@ -10543,36 +11082,47 @@ class PropClosures:
self.lock = threading.thread.Lock()
def get(self, ctx):
- if self.lock: self.lock.acquire()
+ if self.lock:
+ self.lock.acquire()
r = self.bases[ctx]
- if self.lock: self.lock.release()
+ if self.lock:
+ self.lock.release()
return r
def set(self, ctx, r):
- if self.lock: self.lock.acquire()
+ if self.lock:
+ self.lock.acquire()
self.bases[ctx] = r
- if self.lock: self.lock.release()
+ if self.lock:
+ self.lock.release()
def insert(self, r):
- if self.lock: self.lock.acquire()
+ if self.lock:
+ self.lock.acquire()
id = len(self.bases) + 3
self.bases[id] = r
- if self.lock: self.lock.release()
+ if self.lock:
+ self.lock.release()
return id
+
_prop_closures = None
+
def ensure_prop_closures():
global _prop_closures
if _prop_closures is None:
_prop_closures = PropClosures()
+
def user_prop_push(ctx):
- _prop_closures.get(ctx).push();
+ _prop_closures.get(ctx).push()
+
def user_prop_pop(ctx, num_scopes):
_prop_closures.get(ctx).pop(num_scopes)
+
def user_prop_fresh(id, ctx):
prop = _prop_closures.get(id)
_prop_closures.set_threaded()
@@ -10580,38 +11130,44 @@ def user_prop_fresh(id, ctx):
_prop_closures.set(new_prop.id, new_prop.fresh())
return ctypes.c_void_p(new_prop.id)
+
def user_prop_fixed(ctx, cb, id, value):
prop = _prop_closures.get(ctx)
prop.cb = cb
prop.fixed(id, _to_expr_ref(ctypes.c_void_p(value), prop.ctx()))
prop.cb = None
+
def user_prop_final(ctx, cb):
prop = _prop_closures.get(ctx)
prop.cb = cb
prop.final()
prop.cb = None
+
def user_prop_eq(ctx, cb, x, y):
prop = _prop_closures.get(ctx)
prop.cb = cb
prop.eq(x, y)
prop.cb = None
+
def user_prop_diseq(ctx, cb, x, y):
prop = _prop_closures.get(ctx)
prop.cb = cb
prop.diseq(x, y)
prop.cb = None
-_user_prop_push = push_eh_type(user_prop_push)
-_user_prop_pop = pop_eh_type(user_prop_pop)
+
+_user_prop_push = push_eh_type(user_prop_push)
+_user_prop_pop = pop_eh_type(user_prop_pop)
_user_prop_fresh = fresh_eh_type(user_prop_fresh)
_user_prop_fixed = fixed_eh_type(user_prop_fixed)
_user_prop_final = final_eh_type(user_prop_final)
-_user_prop_eq = eq_eh_type(user_prop_eq)
+_user_prop_eq = eq_eh_type(user_prop_eq)
_user_prop_diseq = eq_eh_type(user_prop_diseq)
+
class UserPropagateBase:
#
@@ -10620,17 +11176,17 @@ class UserPropagateBase:
# to "fresh" inherit the context of that is supplied
# as argument to the callback.
# This context should not be deleted. It is owned by the solver.
- #
- def __init__(self, s, ctx = None):
+ #
+ def __init__(self, s, ctx=None):
assert s is None or ctx is None
ensure_prop_closures()
- self.solver = s
+ self.solver = s
self._ctx = None
self.cb = None
self.id = _prop_closures.insert(self)
self.fixed = None
self.final = None
- self.eq = None
+ self.eq = None
self.diseq = None
if ctx:
self._ctx = Context()
@@ -10655,16 +11211,16 @@ class UserPropagateBase:
return self._ctx
else:
return self.solver.ctx
-
+
def ctx_ref(self):
return self.ctx().ref()
-
+
def add_fixed(self, fixed):
assert not self.fixed
assert not self._ctx
Z3_solver_propagate_fixed(self.ctx_ref(), self.solver.solver, _user_prop_fixed)
self.fixed = fixed
-
+
def add_final(self, final):
assert not self.final
assert not self._ctx
@@ -10691,7 +11247,7 @@ class UserPropagateBase:
def fresh(self):
raise Z3Exception("fresh needs to be overwritten")
-
+
def add(self, e):
assert self.solver
assert not self._ctx
@@ -10699,8 +11255,8 @@ class UserPropagateBase:
#
# Propagation can only be invoked as during a fixed or final callback.
- #
- def propagate(self, e, ids, eqs = []):
+ #
+ def propagate(self, e, ids, eqs=[]):
num_fixed = len(ids)
_ids = (ctypes.c_uint * num_fixed)()
for i in range(num_fixed):
@@ -10711,7 +11267,8 @@ class UserPropagateBase:
for i in range(num_eqs):
_lhs[i] = eqs[i][0]
_rhs[i] = eqs[i][1]
- Z3_solver_propagate_consequence(e.ctx.ref(), ctypes.c_void_p(self.cb), num_fixed, _ids, num_eqs, _lhs, _rhs, e.ast)
+ Z3_solver_propagate_consequence(e.ctx.ref(), ctypes.c_void_p(
+ self.cb), num_fixed, _ids, num_eqs, _lhs, _rhs, e.ast)
def conflict(self, ids):
self.propagate(BoolVal(False, self.ctx()), ids, eqs=[])
diff --git a/src/api/python/z3/z3num.py b/src/api/python/z3/z3num.py
index b1af58dc3..09415d474 100644
--- a/src/api/python/z3/z3num.py
+++ b/src/api/python/z3/z3num.py
@@ -1,6 +1,6 @@
############################################
# Copyright (c) 2012 Microsoft Corporation
-#
+#
# Z3 Python interface for Z3 numerals
#
# Author: Leonardo de Moura (leonardo)
@@ -12,18 +12,20 @@ from fractions import Fraction
from .z3 import _get_ctx
+
def _to_numeral(num, ctx=None):
if isinstance(num, Numeral):
return num
else:
return Numeral(num, ctx)
+
class Numeral:
"""
A Z3 numeral can be used to perform computations over arbitrary
precision integers, rationals and real algebraic numbers.
It also automatically converts python numeric values.
-
+
>>> Numeral(2)
2
>>> Numeral("3/2") + 1
@@ -35,9 +37,9 @@ class Numeral:
>>> Numeral(Sqrt(2)) + Numeral(Sqrt(3))
3.1462643699?
- Z3 numerals can be used to perform computations with
+ Z3 numerals can be used to perform computations with
values in a Z3 model.
-
+
>>> s = Solver()
>>> x = Real('x')
>>> s.add(x*x == 2)
@@ -49,34 +51,34 @@ class Numeral:
1.4142135623?
>>> m[x] + 1
1.4142135623? + 1
-
+
The previous result is a Z3 expression.
>>> (m[x] + 1).sexpr()
'(+ (root-obj (+ (^ x 2) (- 2)) 2) 1.0)'
-
+
>>> Numeral(m[x]) + 1
2.4142135623?
>>> Numeral(m[x]).is_pos()
True
>>> Numeral(m[x])**2
2
-
+
We can also isolate the roots of polynomials.
>>> x0, x1, x2 = RealVarVector(3)
>>> r0 = isolate_roots(x0**5 - x0 - 1)
>>> r0
[1.1673039782?]
-
+
In the following example, we are isolating the roots
of a univariate polynomial (on x1) obtained after substituting
x0 -> r0[0]
-
+
>>> r1 = isolate_roots(x1**2 - x0 + 1, [ r0[0] ])
>>> r1
[-0.4090280898?, 0.4090280898?]
-
+
Similarly, in the next example we isolate the roots of
a univariate polynomial (on x2) obtained after substituting
x0 -> r0[0] and x1 -> r1[0]
@@ -85,10 +87,11 @@ class Numeral:
[2.8538479564?]
"""
+
def __init__(self, num, ctx=None):
if isinstance(num, Ast):
- self.ast = num
- self.ctx = _get_ctx(ctx)
+ self.ast = num
+ self.ctx = _get_ctx(ctx)
elif isinstance(num, RatNumRef) or isinstance(num, AlgebraicNumRef):
self.ast = num.ast
self.ctx = num.ctx
@@ -102,13 +105,13 @@ class Numeral:
self.ctx = v.ctx
Z3_inc_ref(self.ctx_ref(), self.as_ast())
assert Z3_algebraic_is_value(self.ctx_ref(), self.ast)
-
+
def __del__(self):
Z3_dec_ref(self.ctx_ref(), self.as_ast())
def is_integer(self):
""" Return True if the numeral is integer.
-
+
>>> Numeral(2).is_integer()
True
>>> (Numeral(Sqrt(2)) * Numeral(Sqrt(2))).is_integer()
@@ -129,13 +132,13 @@ class Numeral:
True
>>> Numeral(Sqrt(2)).is_rational()
False
-
+
"""
return Z3_get_ast_kind(self.ctx_ref(), self.as_ast()) == Z3_NUMERAL_AST
def denominator(self):
""" Return the denominator if `self` is rational.
-
+
>>> Numeral("2/3").denominator()
3
"""
@@ -144,14 +147,13 @@ class Numeral:
def numerator(self):
""" Return the numerator if `self` is rational.
-
+
>>> Numeral("2/3").numerator()
2
"""
assert(self.is_rational())
return Numeral(Z3_get_numerator(self.ctx_ref(), self.as_ast()), self.ctx)
-
def is_irrational(self):
""" Return True if the numeral is irrational.
@@ -169,7 +171,7 @@ class Numeral:
"""
assert(self.is_integer())
- if sys.version_info[0] >= 3:
+ if sys.version_info.major >= 3:
return int(Z3_get_numeral_string(self.ctx_ref(), self.as_ast()))
else:
return long(Z3_get_numeral_string(self.ctx_ref(), self.as_ast()))
@@ -183,9 +185,9 @@ class Numeral:
return Fraction(self.numerator().as_long(), self.denominator().as_long())
def approx(self, precision=10):
- """Return a numeral that approximates the numeral `self`.
- The result `r` is such that |r - self| <= 1/10^precision
-
+ """Return a numeral that approximates the numeral `self`.
+ The result `r` is such that |r - self| <= 1/10^precision
+
If `self` is rational, then the result is `self`.
>>> x = Numeral(2).root(2)
@@ -199,9 +201,9 @@ class Numeral:
return self.upper(precision)
def upper(self, precision=10):
- """Return a upper bound that approximates the numeral `self`.
- The result `r` is such that r - self <= 1/10^precision
-
+ """Return a upper bound that approximates the numeral `self`.
+ The result `r` is such that r - self <= 1/10^precision
+
If `self` is rational, then the result is `self`.
>>> x = Numeral(2).root(2)
@@ -218,9 +220,9 @@ class Numeral:
return Numeral(Z3_get_algebraic_number_upper(self.ctx_ref(), self.as_ast(), precision), self.ctx)
def lower(self, precision=10):
- """Return a lower bound that approximates the numeral `self`.
- The result `r` is such that self - r <= 1/10^precision
-
+ """Return a lower bound that approximates the numeral `self`.
+ The result `r` is such that self - r <= 1/10^precision
+
If `self` is rational, then the result is `self`.
>>> x = Numeral(2).root(2)
@@ -236,7 +238,7 @@ class Numeral:
def sign(self):
""" Return the sign of the numeral.
-
+
>>> Numeral(2).sign()
1
>>> Numeral(-3).sign()
@@ -245,10 +247,10 @@ class Numeral:
0
"""
return Z3_algebraic_sign(self.ctx_ref(), self.ast)
-
+
def is_pos(self):
""" Return True if the numeral is positive.
-
+
>>> Numeral(2).is_pos()
True
>>> Numeral(-3).is_pos()
@@ -260,7 +262,7 @@ class Numeral:
def is_neg(self):
""" Return True if the numeral is negative.
-
+
>>> Numeral(2).is_neg()
False
>>> Numeral(-3).is_neg()
@@ -272,7 +274,7 @@ class Numeral:
def is_zero(self):
""" Return True if the numeral is zero.
-
+
>>> Numeral(2).is_zero()
False
>>> Numeral(-3).is_zero()
@@ -353,7 +355,7 @@ class Numeral:
def __rdiv__(self, other):
""" Return the numeral `other / self`.
- >>> 3 / Numeral(2)
+ >>> 3 / Numeral(2)
3/2
>>> 3 / Numeral(2).root(2)
2.1213203435?
@@ -388,7 +390,7 @@ class Numeral:
3
"""
return Numeral(Z3_algebraic_power(self.ctx_ref(), self.ast, k), self.ctx)
-
+
def __pow__(self, k):
""" Return the numeral `self^k`.
@@ -415,7 +417,7 @@ class Numeral:
def __rlt__(self, other):
""" Return True if `other < self`.
- >>> 2 < Numeral(Sqrt(2))
+ >>> 2 < Numeral(Sqrt(2))
False
"""
return self > other
@@ -440,7 +442,6 @@ class Numeral:
"""
return self < other
-
def __le__(self, other):
""" Return True if `self <= other`.
@@ -456,7 +457,7 @@ class Numeral:
def __rle__(self, other):
""" Return True if `other <= self`.
- >>> 2 <= Numeral(Sqrt(2))
+ >>> 2 <= Numeral(Sqrt(2))
False
"""
return self >= other
@@ -523,13 +524,14 @@ class Numeral:
def ctx_ref(self):
return self.ctx.ref()
+
def eval_sign_at(p, vs):
- """
+ """
Evaluate the sign of the polynomial `p` at `vs`. `p` is a Z3
Expression containing arithmetic operators: +, -, *, ^k where k is
an integer; and free variables x that is_var(x) is True. Moreover,
all variables must be real.
-
+
The result is 1 if the polynomial is positive at the given point,
-1 if negative, and 0 if zero.
@@ -547,15 +549,16 @@ def eval_sign_at(p, vs):
_vs[i] = vs[i].ast
return Z3_algebraic_eval(p.ctx_ref(), p.as_ast(), num, _vs)
+
def isolate_roots(p, vs=[]):
"""
- Given a multivariate polynomial p(x_0, ..., x_{n-1}, x_n), returns the
+ Given a multivariate polynomial p(x_0, ..., x_{n-1}, x_n), returns the
roots of the univariate polynomial p(vs[0], ..., vs[len(vs)-1], x_n).
-
+
Remarks:
* p is a Z3 expression that contains only arithmetic terms and free variables.
* forall i in [0, n) vs is a numeral.
-
+
The result is a list of numerals
>>> x0 = RealVar(0)
@@ -573,5 +576,4 @@ def isolate_roots(p, vs=[]):
for i in range(num):
_vs[i] = vs[i].ast
_roots = AstVector(Z3_algebraic_roots(p.ctx_ref(), p.as_ast(), num, _vs), p.ctx)
- return [ Numeral(r) for r in _roots ]
-
+ return [Numeral(r) for r in _roots]
diff --git a/src/api/python/z3/z3poly.py b/src/api/python/z3/z3poly.py
index 169944291..9c6e217f8 100644
--- a/src/api/python/z3/z3poly.py
+++ b/src/api/python/z3/z3poly.py
@@ -1,6 +1,6 @@
############################################
# Copyright (c) 2012 Microsoft Corporation
-#
+#
# Z3 Python interface for Z3 polynomials
#
# Author: Leonardo de Moura (leonardo)
@@ -8,16 +8,17 @@
from .z3 import *
+
def subresultants(p, q, x):
"""
Return the non-constant subresultants of 'p' and 'q' with respect to the "variable" 'x'.
'p', 'q' and 'x' are Z3 expressions where 'p' and 'q' are arithmetic terms.
Note that, any subterm that cannot be viewed as a polynomial is assumed to be a variable.
- Example: f(a) is a considered to be a variable b in the polynomial
+ Example: f(a) is a considered to be a variable b in the polynomial
+
+ f(a)*f(a) + 2*f(a) + 1
- f(a)*f(a) + 2*f(a) + 1
-
>>> x, y = Reals('x y')
>>> subresultants(2*x + y, 3*x - 2*y + 2, x)
[-7*y + 4]
@@ -29,6 +30,7 @@ def subresultants(p, q, x):
"""
return AstVector(Z3_polynomial_subresultants(p.ctx_ref(), p.as_ast(), q.as_ast(), x.as_ast()), p.ctx)
+
if __name__ == "__main__":
import doctest
if doctest.testmod().failed:
diff --git a/src/api/python/z3/z3printer.py b/src/api/python/z3/z3printer.py
index 34e4bd69e..471c2e951 100644
--- a/src/api/python/z3/z3printer.py
+++ b/src/api/python/z3/z3printer.py
@@ -1,15 +1,16 @@
############################################
# Copyright (c) 2012 Microsoft Corporation
-#
+#
# Z3 Python interface
#
# Author: Leonardo de Moura (leonardo)
############################################
-import sys, io
+import sys
+import io
# We want to import submodule z3 here, but there's no way
# to do that that works correctly on both Python 2 and 3.
-if sys.version < '3':
+if sys.version_info.major < 3:
# In Python 2: an implicit-relative import of submodule z3.
# In Python 3: an undesirable import of global package z3.
import z3
@@ -22,6 +23,7 @@ from .z3consts import *
from .z3core import *
from ctypes import *
+
def _z3_assert(cond, msg):
if not cond:
raise Z3Exception(msg)
@@ -32,165 +34,173 @@ def _z3_assert(cond, msg):
#
##############################
+
# Z3 operator names to Z3Py
_z3_op_to_str = {
- Z3_OP_TRUE : 'True', Z3_OP_FALSE : 'False', Z3_OP_EQ : '==', Z3_OP_DISTINCT : 'Distinct',
- Z3_OP_ITE : 'If', Z3_OP_AND : 'And', Z3_OP_OR : 'Or', Z3_OP_IFF : '==', Z3_OP_XOR : 'Xor',
- Z3_OP_NOT : 'Not', Z3_OP_IMPLIES : 'Implies', Z3_OP_IDIV : '/', Z3_OP_MOD : '%',
- Z3_OP_TO_REAL : 'ToReal', Z3_OP_TO_INT : 'ToInt', Z3_OP_POWER : '**', Z3_OP_IS_INT : 'IsInt',
- Z3_OP_BADD : '+', Z3_OP_BSUB : '-', Z3_OP_BMUL : '*', Z3_OP_BOR : '|', Z3_OP_BAND : '&',
- Z3_OP_BNOT : '~', Z3_OP_BXOR : '^', Z3_OP_BNEG : '-', Z3_OP_BUDIV : 'UDiv', Z3_OP_BSDIV : '/', Z3_OP_BSMOD : '%',
- Z3_OP_BSREM : 'SRem', Z3_OP_BUREM : 'URem', Z3_OP_EXT_ROTATE_LEFT : 'RotateLeft', Z3_OP_EXT_ROTATE_RIGHT : 'RotateRight',
- Z3_OP_SLEQ : '<=', Z3_OP_SLT : '<', Z3_OP_SGEQ : '>=', Z3_OP_SGT : '>',
- Z3_OP_ULEQ : 'ULE', Z3_OP_ULT : 'ULT', Z3_OP_UGEQ : 'UGE', Z3_OP_UGT : 'UGT',
- Z3_OP_SIGN_EXT : 'SignExt', Z3_OP_ZERO_EXT : 'ZeroExt', Z3_OP_REPEAT : 'RepeatBitVec',
- Z3_OP_BASHR : '>>', Z3_OP_BSHL : '<<', Z3_OP_BLSHR : 'LShR',
- Z3_OP_CONCAT : 'Concat', Z3_OP_EXTRACT : 'Extract', Z3_OP_BV2INT : 'BV2Int',
- Z3_OP_ARRAY_MAP : 'Map', Z3_OP_SELECT : 'Select', Z3_OP_STORE : 'Store',
- Z3_OP_CONST_ARRAY : 'K', Z3_OP_ARRAY_EXT : 'Ext',
- Z3_OP_PB_AT_MOST : 'AtMost', Z3_OP_PB_LE : 'PbLe', Z3_OP_PB_GE : 'PbGe', Z3_OP_PB_EQ : 'PbEq',
- Z3_OP_SEQ_CONCAT : 'Concat', Z3_OP_SEQ_PREFIX : 'PrefixOf', Z3_OP_SEQ_SUFFIX : 'SuffixOf',
- Z3_OP_SEQ_UNIT : 'Unit', Z3_OP_SEQ_CONTAINS : 'Contains' , Z3_OP_SEQ_REPLACE : 'Replace',
- Z3_OP_SEQ_AT : 'At', Z3_OP_SEQ_NTH : 'Nth', Z3_OP_SEQ_INDEX : 'IndexOf',
- Z3_OP_SEQ_LAST_INDEX : 'LastIndexOf', Z3_OP_SEQ_LENGTH : 'Length', Z3_OP_STR_TO_INT : 'StrToInt', Z3_OP_INT_TO_STR : 'IntToStr',
- Z3_OP_SEQ_IN_RE : 'InRe', Z3_OP_SEQ_TO_RE : 'Re',
- Z3_OP_RE_PLUS : 'Plus', Z3_OP_RE_STAR : 'Star', Z3_OP_RE_OPTION : 'Option', Z3_OP_RE_UNION : 'Union', Z3_OP_RE_RANGE : 'Range',
- Z3_OP_RE_INTERSECT : 'Intersect', Z3_OP_RE_COMPLEMENT : 'Complement',
- Z3_OP_FPA_IS_NAN : 'fpIsNaN', Z3_OP_FPA_IS_INF : 'fpIsInf', Z3_OP_FPA_IS_ZERO : 'fpIsZero',
- Z3_OP_FPA_IS_NORMAL : 'fpIsNormal', Z3_OP_FPA_IS_SUBNORMAL : 'fpIsSubnormal',
- Z3_OP_FPA_IS_NEGATIVE : 'fpIsNegative', Z3_OP_FPA_IS_POSITIVE : 'fpIsPositive',
- }
+ Z3_OP_TRUE: "True", Z3_OP_FALSE: "False", Z3_OP_EQ: "==", Z3_OP_DISTINCT: "Distinct",
+ Z3_OP_ITE: "If", Z3_OP_AND: "And", Z3_OP_OR: "Or", Z3_OP_IFF: "==", Z3_OP_XOR: "Xor",
+ Z3_OP_NOT: "Not", Z3_OP_IMPLIES: "Implies", Z3_OP_IDIV: "/", Z3_OP_MOD: "%",
+ Z3_OP_TO_REAL: "ToReal", Z3_OP_TO_INT: "ToInt", Z3_OP_POWER: "**", Z3_OP_IS_INT: "IsInt",
+ Z3_OP_BADD: "+", Z3_OP_BSUB: "-", Z3_OP_BMUL: "*", Z3_OP_BOR: "|", Z3_OP_BAND: "&",
+ Z3_OP_BNOT: "~", Z3_OP_BXOR: "^", Z3_OP_BNEG: "-", Z3_OP_BUDIV: "UDiv", Z3_OP_BSDIV: "/", Z3_OP_BSMOD: "%",
+ Z3_OP_BSREM: "SRem", Z3_OP_BUREM: "URem", Z3_OP_EXT_ROTATE_LEFT: "RotateLeft", Z3_OP_EXT_ROTATE_RIGHT: "RotateRight",
+ Z3_OP_SLEQ: "<=", Z3_OP_SLT: "<", Z3_OP_SGEQ: ">=", Z3_OP_SGT: ">",
+ Z3_OP_ULEQ: "ULE", Z3_OP_ULT: "ULT", Z3_OP_UGEQ: "UGE", Z3_OP_UGT: "UGT",
+ Z3_OP_SIGN_EXT: "SignExt", Z3_OP_ZERO_EXT: "ZeroExt", Z3_OP_REPEAT: "RepeatBitVec",
+ Z3_OP_BASHR: ">>", Z3_OP_BSHL: "<<", Z3_OP_BLSHR: "LShR",
+ Z3_OP_CONCAT: "Concat", Z3_OP_EXTRACT: "Extract", Z3_OP_BV2INT: "BV2Int",
+ Z3_OP_ARRAY_MAP: "Map", Z3_OP_SELECT: "Select", Z3_OP_STORE: "Store",
+ Z3_OP_CONST_ARRAY: "K", Z3_OP_ARRAY_EXT: "Ext",
+ Z3_OP_PB_AT_MOST: "AtMost", Z3_OP_PB_LE: "PbLe", Z3_OP_PB_GE: "PbGe", Z3_OP_PB_EQ: "PbEq",
+ Z3_OP_SEQ_CONCAT: "Concat", Z3_OP_SEQ_PREFIX: "PrefixOf", Z3_OP_SEQ_SUFFIX: "SuffixOf",
+ Z3_OP_SEQ_UNIT: "Unit", Z3_OP_SEQ_CONTAINS: "Contains", Z3_OP_SEQ_REPLACE: "Replace",
+ Z3_OP_SEQ_AT: "At", Z3_OP_SEQ_NTH: "Nth", Z3_OP_SEQ_INDEX: "IndexOf",
+ Z3_OP_SEQ_LAST_INDEX: "LastIndexOf", Z3_OP_SEQ_LENGTH: "Length", Z3_OP_STR_TO_INT: "StrToInt", Z3_OP_INT_TO_STR: "IntToStr",
+ Z3_OP_SEQ_IN_RE: "InRe", Z3_OP_SEQ_TO_RE: "Re",
+ Z3_OP_RE_PLUS: "Plus", Z3_OP_RE_STAR: "Star", Z3_OP_RE_OPTION: "Option", Z3_OP_RE_UNION: "Union", Z3_OP_RE_RANGE: "Range",
+ Z3_OP_RE_INTERSECT: "Intersect", Z3_OP_RE_COMPLEMENT: "Complement",
+ Z3_OP_FPA_IS_NAN: "fpIsNaN", Z3_OP_FPA_IS_INF: "fpIsInf", Z3_OP_FPA_IS_ZERO: "fpIsZero",
+ Z3_OP_FPA_IS_NORMAL: "fpIsNormal", Z3_OP_FPA_IS_SUBNORMAL: "fpIsSubnormal",
+ Z3_OP_FPA_IS_NEGATIVE: "fpIsNegative", Z3_OP_FPA_IS_POSITIVE: "fpIsPositive",
+}
# List of infix operators
-_z3_infix = [
+_z3_infix = [
Z3_OP_EQ, Z3_OP_IFF, Z3_OP_ADD, Z3_OP_SUB, Z3_OP_MUL, Z3_OP_DIV, Z3_OP_IDIV, Z3_OP_MOD, Z3_OP_POWER,
Z3_OP_LE, Z3_OP_LT, Z3_OP_GE, Z3_OP_GT, Z3_OP_BADD, Z3_OP_BSUB, Z3_OP_BMUL, Z3_OP_BSDIV, Z3_OP_BSMOD, Z3_OP_BOR, Z3_OP_BAND,
Z3_OP_BXOR, Z3_OP_BSDIV, Z3_OP_SLEQ, Z3_OP_SLT, Z3_OP_SGEQ, Z3_OP_SGT, Z3_OP_BASHR, Z3_OP_BSHL
- ]
+]
-_z3_unary = [ Z3_OP_UMINUS, Z3_OP_BNOT, Z3_OP_BNEG ]
+_z3_unary = [Z3_OP_UMINUS, Z3_OP_BNOT, Z3_OP_BNEG]
# Precedence
_z3_precedence = {
- Z3_OP_POWER : 0,
- Z3_OP_UMINUS : 1, Z3_OP_BNEG : 1, Z3_OP_BNOT : 1,
- Z3_OP_MUL : 2, Z3_OP_DIV : 2, Z3_OP_IDIV : 2, Z3_OP_MOD : 2, Z3_OP_BMUL : 2, Z3_OP_BSDIV : 2, Z3_OP_BSMOD : 2,
- Z3_OP_ADD : 3, Z3_OP_SUB : 3, Z3_OP_BADD : 3, Z3_OP_BSUB : 3,
- Z3_OP_BASHR : 4, Z3_OP_BSHL : 4,
- Z3_OP_BAND : 5,
- Z3_OP_BXOR : 6,
- Z3_OP_BOR : 7,
- Z3_OP_LE : 8, Z3_OP_LT : 8, Z3_OP_GE : 8, Z3_OP_GT : 8, Z3_OP_EQ : 8, Z3_OP_SLEQ : 8, Z3_OP_SLT : 8, Z3_OP_SGEQ : 8, Z3_OP_SGT : 8,
- Z3_OP_IFF : 8,
-
- Z3_OP_FPA_NEG : 1,
- Z3_OP_FPA_MUL : 2, Z3_OP_FPA_DIV : 2, Z3_OP_FPA_REM : 2, Z3_OP_FPA_FMA : 2,
- Z3_OP_FPA_ADD: 3, Z3_OP_FPA_SUB : 3,
- Z3_OP_FPA_LE : 8, Z3_OP_FPA_LT : 8, Z3_OP_FPA_GE : 8, Z3_OP_FPA_GT : 8, Z3_OP_FPA_EQ : 8
- }
+ Z3_OP_POWER: 0,
+ Z3_OP_UMINUS: 1, Z3_OP_BNEG: 1, Z3_OP_BNOT: 1,
+ Z3_OP_MUL: 2, Z3_OP_DIV: 2, Z3_OP_IDIV: 2, Z3_OP_MOD: 2, Z3_OP_BMUL: 2, Z3_OP_BSDIV: 2, Z3_OP_BSMOD: 2,
+ Z3_OP_ADD: 3, Z3_OP_SUB: 3, Z3_OP_BADD: 3, Z3_OP_BSUB: 3,
+ Z3_OP_BASHR: 4, Z3_OP_BSHL: 4,
+ Z3_OP_BAND: 5,
+ Z3_OP_BXOR: 6,
+ Z3_OP_BOR: 7,
+ Z3_OP_LE: 8, Z3_OP_LT: 8, Z3_OP_GE: 8, Z3_OP_GT: 8, Z3_OP_EQ: 8, Z3_OP_SLEQ: 8, Z3_OP_SLT: 8, Z3_OP_SGEQ: 8, Z3_OP_SGT: 8,
+ Z3_OP_IFF: 8,
-# FPA operators
-_z3_op_to_fpa_normal_str = {
- Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN : 'RoundNearestTiesToEven()', Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY : 'RoundNearestTiesToAway()',
- Z3_OP_FPA_RM_TOWARD_POSITIVE : 'RoundTowardPositive()', Z3_OP_FPA_RM_TOWARD_NEGATIVE : 'RoundTowardNegative()',
- Z3_OP_FPA_RM_TOWARD_ZERO : 'RoundTowardZero()',
- Z3_OP_FPA_PLUS_INF : 'fpPlusInfinity', Z3_OP_FPA_MINUS_INF : 'fpMinusInfinity',
- Z3_OP_FPA_NAN : 'fpNaN', Z3_OP_FPA_PLUS_ZERO : 'fpPZero', Z3_OP_FPA_MINUS_ZERO : 'fpNZero',
- Z3_OP_FPA_ADD : 'fpAdd', Z3_OP_FPA_SUB : 'fpSub', Z3_OP_FPA_NEG : 'fpNeg', Z3_OP_FPA_MUL : 'fpMul',
- Z3_OP_FPA_DIV : 'fpDiv', Z3_OP_FPA_REM : 'fpRem', Z3_OP_FPA_ABS : 'fpAbs',
- Z3_OP_FPA_MIN : 'fpMin', Z3_OP_FPA_MAX : 'fpMax',
- Z3_OP_FPA_FMA : 'fpFMA', Z3_OP_FPA_SQRT : 'fpSqrt', Z3_OP_FPA_ROUND_TO_INTEGRAL : 'fpRoundToIntegral',
-
- Z3_OP_FPA_EQ : 'fpEQ', Z3_OP_FPA_LT : 'fpLT', Z3_OP_FPA_GT : 'fpGT', Z3_OP_FPA_LE : 'fpLEQ',
- Z3_OP_FPA_GE : 'fpGEQ',
-
- Z3_OP_FPA_FP : 'fpFP', Z3_OP_FPA_TO_FP : 'fpToFP', Z3_OP_FPA_TO_FP_UNSIGNED: 'fpToFPUnsigned',
- Z3_OP_FPA_TO_UBV : 'fpToUBV', Z3_OP_FPA_TO_SBV : 'fpToSBV', Z3_OP_FPA_TO_REAL: 'fpToReal',
- Z3_OP_FPA_TO_IEEE_BV : 'fpToIEEEBV'
- }
-
-_z3_op_to_fpa_pretty_str = {
- Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN : 'RNE()', Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY : 'RNA()',
- Z3_OP_FPA_RM_TOWARD_POSITIVE : 'RTP()', Z3_OP_FPA_RM_TOWARD_NEGATIVE : 'RTN()',
- Z3_OP_FPA_RM_TOWARD_ZERO : 'RTZ()',
- Z3_OP_FPA_PLUS_INF : '+oo', Z3_OP_FPA_MINUS_INF : '-oo',
- Z3_OP_FPA_NAN : 'NaN', Z3_OP_FPA_PLUS_ZERO : '+0.0', Z3_OP_FPA_MINUS_ZERO : '-0.0',
-
- Z3_OP_FPA_ADD : '+', Z3_OP_FPA_SUB : '-', Z3_OP_FPA_MUL : '*', Z3_OP_FPA_DIV : '/',
- Z3_OP_FPA_REM : '%', Z3_OP_FPA_NEG : '-',
-
- Z3_OP_FPA_EQ : 'fpEQ', Z3_OP_FPA_LT : '<', Z3_OP_FPA_GT : '>', Z3_OP_FPA_LE : '<=', Z3_OP_FPA_GE : '>='
+ Z3_OP_FPA_NEG: 1,
+ Z3_OP_FPA_MUL: 2, Z3_OP_FPA_DIV: 2, Z3_OP_FPA_REM: 2, Z3_OP_FPA_FMA: 2,
+ Z3_OP_FPA_ADD: 3, Z3_OP_FPA_SUB: 3,
+ Z3_OP_FPA_LE: 8, Z3_OP_FPA_LT: 8, Z3_OP_FPA_GE: 8, Z3_OP_FPA_GT: 8, Z3_OP_FPA_EQ: 8
}
-
+
+# FPA operators
+_z3_op_to_fpa_normal_str = {
+ Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN: "RoundNearestTiesToEven()", Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY: "RoundNearestTiesToAway()",
+ Z3_OP_FPA_RM_TOWARD_POSITIVE: "RoundTowardPositive()", Z3_OP_FPA_RM_TOWARD_NEGATIVE: "RoundTowardNegative()",
+ Z3_OP_FPA_RM_TOWARD_ZERO: "RoundTowardZero()",
+ Z3_OP_FPA_PLUS_INF: "fpPlusInfinity", Z3_OP_FPA_MINUS_INF: "fpMinusInfinity",
+ Z3_OP_FPA_NAN: "fpNaN", Z3_OP_FPA_PLUS_ZERO: "fpPZero", Z3_OP_FPA_MINUS_ZERO: "fpNZero",
+ Z3_OP_FPA_ADD: "fpAdd", Z3_OP_FPA_SUB: "fpSub", Z3_OP_FPA_NEG: "fpNeg", Z3_OP_FPA_MUL: "fpMul",
+ Z3_OP_FPA_DIV: "fpDiv", Z3_OP_FPA_REM: "fpRem", Z3_OP_FPA_ABS: "fpAbs",
+ Z3_OP_FPA_MIN: "fpMin", Z3_OP_FPA_MAX: "fpMax",
+ Z3_OP_FPA_FMA: "fpFMA", Z3_OP_FPA_SQRT: "fpSqrt", Z3_OP_FPA_ROUND_TO_INTEGRAL: "fpRoundToIntegral",
+
+ Z3_OP_FPA_EQ: "fpEQ", Z3_OP_FPA_LT: "fpLT", Z3_OP_FPA_GT: "fpGT", Z3_OP_FPA_LE: "fpLEQ",
+ Z3_OP_FPA_GE: "fpGEQ",
+
+ Z3_OP_FPA_FP: "fpFP", Z3_OP_FPA_TO_FP: "fpToFP", Z3_OP_FPA_TO_FP_UNSIGNED: "fpToFPUnsigned",
+ Z3_OP_FPA_TO_UBV: "fpToUBV", Z3_OP_FPA_TO_SBV: "fpToSBV", Z3_OP_FPA_TO_REAL: "fpToReal",
+ Z3_OP_FPA_TO_IEEE_BV: "fpToIEEEBV"
+}
+
+_z3_op_to_fpa_pretty_str = {
+ Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN: "RNE()", Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY: "RNA()",
+ Z3_OP_FPA_RM_TOWARD_POSITIVE: "RTP()", Z3_OP_FPA_RM_TOWARD_NEGATIVE: "RTN()",
+ Z3_OP_FPA_RM_TOWARD_ZERO: "RTZ()",
+ Z3_OP_FPA_PLUS_INF: "+oo", Z3_OP_FPA_MINUS_INF: "-oo",
+ Z3_OP_FPA_NAN: "NaN", Z3_OP_FPA_PLUS_ZERO: "+0.0", Z3_OP_FPA_MINUS_ZERO: "-0.0",
+
+ Z3_OP_FPA_ADD: "+", Z3_OP_FPA_SUB: "-", Z3_OP_FPA_MUL: "*", Z3_OP_FPA_DIV: "/",
+ Z3_OP_FPA_REM: "%", Z3_OP_FPA_NEG: "-",
+
+ Z3_OP_FPA_EQ: "fpEQ", Z3_OP_FPA_LT: "<", Z3_OP_FPA_GT: ">", Z3_OP_FPA_LE: "<=", Z3_OP_FPA_GE: ">="
+}
+
_z3_fpa_infix = [
Z3_OP_FPA_ADD, Z3_OP_FPA_SUB, Z3_OP_FPA_MUL, Z3_OP_FPA_DIV, Z3_OP_FPA_REM,
Z3_OP_FPA_LT, Z3_OP_FPA_GT, Z3_OP_FPA_LE, Z3_OP_FPA_GE
]
+
def _is_assoc(k):
return k == Z3_OP_BOR or k == Z3_OP_BXOR or k == Z3_OP_BAND or k == Z3_OP_ADD or k == Z3_OP_BADD or k == Z3_OP_MUL or k == Z3_OP_BMUL
+
def _is_left_assoc(k):
return _is_assoc(k) or k == Z3_OP_SUB or k == Z3_OP_BSUB
+
def _is_html_assoc(k):
return k == Z3_OP_AND or k == Z3_OP_OR or k == Z3_OP_IFF or _is_assoc(k)
+
def _is_html_left_assoc(k):
return _is_html_assoc(k) or k == Z3_OP_SUB or k == Z3_OP_BSUB
+
def _is_add(k):
return k == Z3_OP_ADD or k == Z3_OP_BADD
+
def _is_sub(k):
return k == Z3_OP_SUB or k == Z3_OP_BSUB
-import sys
-if sys.version < '3':
+
+if sys.version_info.major < 3:
import codecs
+
def u(x):
return codecs.unicode_escape_decode(x)[0]
else:
def u(x):
return x
-_z3_infix_compact = [ Z3_OP_MUL, Z3_OP_BMUL, Z3_OP_POWER, Z3_OP_DIV, Z3_OP_IDIV, Z3_OP_MOD, Z3_OP_BSDIV, Z3_OP_BSMOD ]
+_z3_infix_compact = [Z3_OP_MUL, Z3_OP_BMUL, Z3_OP_POWER, Z3_OP_DIV, Z3_OP_IDIV, Z3_OP_MOD, Z3_OP_BSDIV, Z3_OP_BSMOD]
-_ellipses = '...'
+_ellipses = "..."
-_html_ellipses = '…'
+_html_ellipses = "…"
# Overwrite some of the operators for HTML
-_z3_pre_html_op_to_str = { Z3_OP_EQ : '=', Z3_OP_IFF : '=', Z3_OP_NOT : '¬',
- Z3_OP_AND : '∧', Z3_OP_OR : '∨', Z3_OP_IMPLIES : '⇒',
- Z3_OP_LT : '<', Z3_OP_GT : '>', Z3_OP_LE : '≤', Z3_OP_GE : '≥',
- Z3_OP_MUL : '·',
- Z3_OP_SLEQ : '≤', Z3_OP_SLT : '<', Z3_OP_SGEQ : '≥', Z3_OP_SGT : '>',
- Z3_OP_ULEQ : '≤<sub>u</sub>', Z3_OP_ULT : '<<sub>u</sub>',
- Z3_OP_UGEQ : '≥<sub>u</sub>', Z3_OP_UGT : '><sub>u</sub>',
- Z3_OP_BMUL : '·',
- Z3_OP_BUDIV : '/<sub>u</sub>', Z3_OP_BUREM : '%<sub>u</sub>',
- Z3_OP_BASHR : '>>', Z3_OP_BSHL : '<<',
- Z3_OP_BLSHR : '>><sub>u</sub>'
- }
+_z3_pre_html_op_to_str = {Z3_OP_EQ: "=", Z3_OP_IFF: "=", Z3_OP_NOT: "¬",
+ Z3_OP_AND: "∧", Z3_OP_OR: "∨", Z3_OP_IMPLIES: "⇒",
+ Z3_OP_LT: "<", Z3_OP_GT: ">", Z3_OP_LE: "≤", Z3_OP_GE: "≥",
+ Z3_OP_MUL: "·",
+ Z3_OP_SLEQ: "≤", Z3_OP_SLT: "<", Z3_OP_SGEQ: "≥", Z3_OP_SGT: ">",
+ Z3_OP_ULEQ: "≤<sub>u</sub>", Z3_OP_ULT: "<<sub>u</sub>",
+ Z3_OP_UGEQ: "≥<sub>u</sub>", Z3_OP_UGT: "><sub>u</sub>",
+ Z3_OP_BMUL: "·",
+ Z3_OP_BUDIV: "/<sub>u</sub>", Z3_OP_BUREM: "%<sub>u</sub>",
+ Z3_OP_BASHR: ">>", Z3_OP_BSHL: "<<",
+ Z3_OP_BLSHR: ">><sub>u</sub>"
+ }
# Extra operators that are infix/unary for HTML
-_z3_html_infix = [ Z3_OP_AND, Z3_OP_OR, Z3_OP_IMPLIES,
- Z3_OP_ULEQ, Z3_OP_ULT, Z3_OP_UGEQ, Z3_OP_UGT, Z3_OP_BUDIV, Z3_OP_BUREM, Z3_OP_BLSHR
- ]
+_z3_html_infix = [Z3_OP_AND, Z3_OP_OR, Z3_OP_IMPLIES,
+ Z3_OP_ULEQ, Z3_OP_ULT, Z3_OP_UGEQ, Z3_OP_UGT, Z3_OP_BUDIV, Z3_OP_BUREM, Z3_OP_BLSHR
+ ]
-_z3_html_unary = [ Z3_OP_NOT ]
+_z3_html_unary = [Z3_OP_NOT]
# Extra Precedence for HTML
-_z3_pre_html_precedence = { Z3_OP_BUDIV : 2, Z3_OP_BUREM : 2,
- Z3_OP_BLSHR : 4,
- Z3_OP_ULEQ : 8, Z3_OP_ULT : 8,
- Z3_OP_UGEQ : 8, Z3_OP_UGT : 8,
- Z3_OP_ULEQ : 8, Z3_OP_ULT : 8,
- Z3_OP_UGEQ : 8, Z3_OP_UGT : 8,
- Z3_OP_NOT : 1,
- Z3_OP_AND : 10,
- Z3_OP_OR : 11,
- Z3_OP_IMPLIES : 12 }
+_z3_pre_html_precedence = {Z3_OP_BUDIV: 2, Z3_OP_BUREM: 2,
+ Z3_OP_BLSHR: 4,
+ Z3_OP_ULEQ: 8, Z3_OP_ULT: 8,
+ Z3_OP_UGEQ: 8, Z3_OP_UGT: 8,
+ Z3_OP_ULEQ: 8, Z3_OP_ULT: 8,
+ Z3_OP_UGEQ: 8, Z3_OP_UGT: 8,
+ Z3_OP_NOT: 1,
+ Z3_OP_AND: 10,
+ Z3_OP_OR: 11,
+ Z3_OP_IMPLIES: 12}
##############################
#
@@ -198,9 +208,11 @@ _z3_pre_html_precedence = { Z3_OP_BUDIV : 2, Z3_OP_BUREM : 2,
#
##############################
+
def _support_pp(a):
return isinstance(a, z3.Z3PPObject) or isinstance(a, list) or isinstance(a, tuple)
+
_infix_map = {}
_unary_map = {}
_infix_compact_map = {}
@@ -209,22 +221,26 @@ for _k in _z3_infix:
_infix_map[_k] = True
for _k in _z3_unary:
_unary_map[_k] = True
-
+
for _k in _z3_infix_compact:
_infix_compact_map[_k] = True
+
def _is_infix(k):
global _infix_map
return _infix_map.get(k, False)
+
def _is_infix_compact(k):
global _infix_compact_map
return _infix_compact_map.get(k, False)
+
def _is_unary(k):
global _unary_map
return _unary_map.get(k, False)
+
def _op_name(a):
if isinstance(a, z3.FuncDeclRef):
f = a
@@ -232,15 +248,17 @@ def _op_name(a):
f = a.decl()
k = f.kind()
n = _z3_op_to_str.get(k, None)
- if n == None:
+ if n is None:
return f.name()
else:
return n
+
def _get_precedence(k):
global _z3_precedence
return _z3_precedence.get(k, 100000)
+
_z3_html_op_to_str = {}
for _k in _z3_op_to_str:
_v = _z3_op_to_str[_k]
@@ -268,14 +286,17 @@ for _k in _z3_unary:
for _k in _z3_html_unary:
_html_unary_map[_k] = True
+
def _is_html_infix(k):
global _html_infix_map
return _html_infix_map.get(k, False)
+
def _is_html_unary(k):
global _html_unary_map
return _html_unary_map.get(k, False)
+
def _html_op_name(a):
global _z3_html_op_to_str
if isinstance(a, z3.FuncDeclRef):
@@ -284,7 +305,7 @@ def _html_op_name(a):
f = a.decl()
k = f.kind()
n = _z3_html_op_to_str.get(k, None)
- if n == None:
+ if n is None:
sym = Z3_get_decl_name(f.ctx_ref(), f.ast)
if Z3_get_symbol_kind(f.ctx_ref(), sym) == Z3_INT_SYMBOL:
return "ζ<sub>%s</sub>" % Z3_get_symbol_int(f.ctx_ref(), sym)
@@ -294,44 +315,60 @@ def _html_op_name(a):
else:
return n
+
def _get_html_precedence(k):
global _z3_html_predence
return _z3_html_precedence.get(k, 100000)
+
class FormatObject:
def is_compose(self):
return False
+
def is_choice(self):
return False
+
def is_indent(self):
return False
+
def is_string(self):
return False
+
def is_linebreak(self):
return False
+
def is_nil(self):
return True
+
def children(self):
return []
+
def as_tuple(self):
return None
+
def space_upto_nl(self):
return (0, False)
+
def flat(self):
return self
+
class NAryFormatObject(FormatObject):
def __init__(self, fs):
assert all([isinstance(a, FormatObject) for a in fs])
self.children = fs
+
def children(self):
return self.children
+
class ComposeFormatObject(NAryFormatObject):
def is_compose(sef):
return True
+
def as_tuple(self):
- return ('compose', [ a.as_tuple() for a in self.children ])
+ return ("compose", [a.as_tuple() for a in self.children])
+
def space_upto_nl(self):
r = 0
for child in self.children:
@@ -340,135 +377,168 @@ class ComposeFormatObject(NAryFormatObject):
if nl:
return (r, True)
return (r, False)
+
def flat(self):
- return compose([a.flat() for a in self.children ])
+ return compose([a.flat() for a in self.children])
+
class ChoiceFormatObject(NAryFormatObject):
def is_choice(sef):
return True
+
def as_tuple(self):
- return ('choice', [ a.as_tuple() for a in self.children ])
+ return ("choice", [a.as_tuple() for a in self.children])
+
def space_upto_nl(self):
return self.children[0].space_upto_nl()
+
def flat(self):
return self.children[0].flat()
+
class IndentFormatObject(FormatObject):
def __init__(self, indent, child):
assert isinstance(child, FormatObject)
self.indent = indent
- self.child = child
+ self.child = child
+
def children(self):
return [self.child]
+
def as_tuple(self):
- return ('indent', self.indent, self.child.as_tuple())
+ return ("indent", self.indent, self.child.as_tuple())
+
def space_upto_nl(self):
return self.child.space_upto_nl()
+
def flat(self):
return indent(self.indent, self.child.flat())
+
def is_indent(self):
return True
+
class LineBreakFormatObject(FormatObject):
def __init__(self):
- self.space = ' '
+ self.space = " "
+
def is_linebreak(self):
return True
+
def as_tuple(self):
- return '<line-break>'
+ return "<line-break>"
+
def space_upto_nl(self):
return (0, True)
+
def flat(self):
return to_format(self.space)
+
class StringFormatObject(FormatObject):
def __init__(self, string):
assert isinstance(string, str)
self.string = string
+
def is_string(self):
return True
+
def as_tuple(self):
return self.string
+
def space_upto_nl(self):
- return (getattr(self, 'size', len(self.string)), False)
+ return (getattr(self, "size", len(self.string)), False)
+
def fits(f, space_left):
s, nl = f.space_upto_nl()
return s <= space_left
+
def to_format(arg, size=None):
if isinstance(arg, FormatObject):
return arg
else:
r = StringFormatObject(str(arg))
- if size != None:
+ if size is not None:
r.size = size
return r
+
def compose(*args):
if len(args) == 1 and (isinstance(args[0], list) or isinstance(args[0], tuple)):
args = args[0]
return ComposeFormatObject(args)
+
def indent(i, arg):
return IndentFormatObject(i, arg)
+
def group(arg):
return ChoiceFormatObject([arg.flat(), arg])
+
def line_break():
return LineBreakFormatObject()
+
def _len(a):
if isinstance(a, StringFormatObject):
- return getattr(a, 'size', len(a.string))
+ return getattr(a, "size", len(a.string))
else:
return len(a)
-def seq(args, sep=',', space=True):
+
+def seq(args, sep=",", space=True):
nl = line_break()
if not space:
- nl.space = ''
+ nl.space = ""
r = []
r.append(args[0])
- num = len(args)
+ num = len(args)
for i in range(num - 1):
r.append(to_format(sep))
r.append(nl)
- r.append(args[i+1])
+ r.append(args[i + 1])
return compose(r)
-def seq1(header, args, lp='(', rp=')'):
+
+def seq1(header, args, lp="(", rp=")"):
return group(compose(to_format(header),
to_format(lp),
indent(len(lp) + _len(header),
seq(args)),
to_format(rp)))
-def seq2(header, args, i=4, lp='(', rp=')'):
+
+def seq2(header, args, i=4, lp="(", rp=")"):
if len(args) == 0:
return compose(to_format(header), to_format(lp), to_format(rp))
else:
return group(compose(indent(len(lp), compose(to_format(lp), to_format(header))),
indent(i, compose(seq(args), to_format(rp)))))
-def seq3(args, lp='(', rp=')'):
+
+def seq3(args, lp="(", rp=")"):
if len(args) == 0:
return compose(to_format(lp), to_format(rp))
else:
return group(indent(len(lp), compose(to_format(lp), seq(args), to_format(rp))))
+
class StopPPException(Exception):
def __str__(self):
- return 'pp-interrupted'
+ return "pp-interrupted"
+
class PP:
def __init__(self):
- self.max_lines = 200
- self.max_width = 60
- self.bounded = False
+ self.max_lines = 200
+ self.max_width = 60
+ self.bounded = False
self.max_indent = 40
-
+
def pp_string(self, f, indent):
if not self.bounded or self.pos <= self.max_width:
sz = _len(f)
@@ -489,17 +559,17 @@ class PP:
self.pp(f.children[0], indent)
else:
self.pp(f.children[1], indent)
-
+
def pp_line_break(self, f, indent):
self.pos = indent
self.ribbon_pos = 0
self.line = self.line + 1
- if self.line < self.max_lines:
- self.out.write(u('\n'))
+ if self.line < self.max_lines:
+ self.out.write(u("\n"))
for i in range(indent):
- self.out.write(u(' '))
+ self.out.write(u(" "))
else:
- self.out.write(u('\n...'))
+ self.out.write(u("\n..."))
raise StopPPException()
def pp(self, f, indent):
@@ -523,37 +593,38 @@ class PP:
self.pos = 0
self.ribbon_pos = 0
self.line = 0
- self.out = out
+ self.out = out
self.pp(f, 0)
except StopPPException:
return
-
+
+
class Formatter:
def __init__(self):
global _ellipses
- self.max_depth = 20
- self.max_args = 128
+ self.max_depth = 20
+ self.max_args = 128
self.rational_to_decimal = False
- self.precision = 10
- self.ellipses = to_format(_ellipses)
- self.max_visited = 10000
- self.fpa_pretty = True
-
+ self.precision = 10
+ self.ellipses = to_format(_ellipses)
+ self.max_visited = 10000
+ self.fpa_pretty = True
+
def pp_ellipses(self):
return self.ellipses
def pp_arrow(self):
- return ' ->'
+ return " ->"
def pp_unknown(self):
- return '<unknown>'
-
+ return "<unknown>"
+
def pp_name(self, a):
return to_format(_op_name(a))
def is_infix(self, a):
return _is_infix(a)
-
+
def is_unary(self, a):
return _is_unary(a)
@@ -564,24 +635,24 @@ class Formatter:
return _is_infix_compact(a)
def is_infix_unary(self, a):
- return self.is_infix(a) or self.is_unary(a)
+ return self.is_infix(a) or self.is_unary(a)
def add_paren(self, a):
- return compose(to_format('('), indent(1, a), to_format(')'))
-
+ return compose(to_format("("), indent(1, a), to_format(")"))
+
def pp_sort(self, s):
if isinstance(s, z3.ArraySortRef):
- return seq1('Array', (self.pp_sort(s.domain()), self.pp_sort(s.range())))
+ return seq1("Array", (self.pp_sort(s.domain()), self.pp_sort(s.range())))
elif isinstance(s, z3.BitVecSortRef):
- return seq1('BitVec', (to_format(s.size()), ))
+ return seq1("BitVec", (to_format(s.size()), ))
elif isinstance(s, z3.FPSortRef):
- return seq1('FPSort', (to_format(s.ebits()), to_format(s.sbits())))
+ return seq1("FPSort", (to_format(s.ebits()), to_format(s.sbits())))
elif isinstance(s, z3.ReSortRef):
- return seq1('ReSort', (self.pp_sort(s.basis()), ))
+ return seq1("ReSort", (self.pp_sort(s.basis()), ))
elif isinstance(s, z3.SeqSortRef):
if s.is_string():
return to_format("String")
- return seq1('Seq', (self.pp_sort(s.basis()), ))
+ return seq1("Seq", (self.pp_sort(s.basis()), ))
else:
return to_format(s.name())
@@ -597,7 +668,7 @@ class Formatter:
def pp_int(self, a):
return to_format(a.as_string())
-
+
def pp_rational(self, a):
if not self.rational_to_decimal:
return to_format(a.as_string())
@@ -617,53 +688,53 @@ class Formatter:
return to_format(a.as_string())
def pp_fprm_value(self, a):
- _z3_assert(z3.is_fprm_value(a), 'expected FPRMNumRef')
+ _z3_assert(z3.is_fprm_value(a), "expected FPRMNumRef")
if self.fpa_pretty and (a.decl().kind() in _z3_op_to_fpa_pretty_str):
return to_format(_z3_op_to_fpa_pretty_str.get(a.decl().kind()))
else:
return to_format(_z3_op_to_fpa_normal_str.get(a.decl().kind()))
def pp_fp_value(self, a):
- _z3_assert(isinstance(a, z3.FPNumRef), 'type mismatch')
+ _z3_assert(isinstance(a, z3.FPNumRef), "type mismatch")
if not self.fpa_pretty:
r = []
if (a.isNaN()):
r.append(to_format(_z3_op_to_fpa_normal_str[Z3_OP_FPA_NAN]))
- r.append(to_format('('))
+ r.append(to_format("("))
r.append(to_format(a.sort()))
- r.append(to_format(')'))
+ r.append(to_format(")"))
return compose(r)
elif (a.isInf()):
if (a.isNegative()):
r.append(to_format(_z3_op_to_fpa_normal_str[Z3_OP_FPA_MINUS_INF]))
else:
- r.append(to_format(_z3_op_to_fpa_normal_str[Z3_OP_FPA_PLUS_INF]))
- r.append(to_format('('))
+ r.append(to_format(_z3_op_to_fpa_normal_str[Z3_OP_FPA_PLUS_INF]))
+ r.append(to_format("("))
r.append(to_format(a.sort()))
- r.append(to_format(')'))
+ r.append(to_format(")"))
return compose(r)
elif (a.isZero()):
if (a.isNegative()):
- return to_format('-zero')
+ return to_format("-zero")
else:
- return to_format('+zero')
+ return to_format("+zero")
else:
- _z3_assert(z3.is_fp_value(a), 'expecting FP num ast')
+ _z3_assert(z3.is_fp_value(a), "expecting FP num ast")
r = []
sgn = c_int(0)
sgnb = Z3_fpa_get_numeral_sign(a.ctx_ref(), a.ast, byref(sgn))
exp = Z3_fpa_get_numeral_exponent_string(a.ctx_ref(), a.ast, False)
sig = Z3_fpa_get_numeral_significand_string(a.ctx_ref(), a.ast)
- r.append(to_format('FPVal('))
+ r.append(to_format("FPVal("))
if sgnb and sgn.value != 0:
- r.append(to_format('-'))
+ r.append(to_format("-"))
r.append(to_format(sig))
- r.append(to_format('*(2**'))
+ r.append(to_format("*(2**"))
r.append(to_format(exp))
- r.append(to_format(', '))
+ r.append(to_format(", "))
r.append(to_format(a.sort()))
- r.append(to_format('))'))
+ r.append(to_format("))"))
return compose(r)
else:
if (a.isNaN()):
@@ -679,75 +750,74 @@ class Formatter:
else:
return to_format(_z3_op_to_fpa_pretty_str[Z3_OP_FPA_PLUS_ZERO])
else:
- _z3_assert(z3.is_fp_value(a), 'expecting FP num ast')
+ _z3_assert(z3.is_fp_value(a), "expecting FP num ast")
r = []
sgn = (ctypes.c_int)(0)
sgnb = Z3_fpa_get_numeral_sign(a.ctx_ref(), a.ast, byref(sgn))
exp = Z3_fpa_get_numeral_exponent_string(a.ctx_ref(), a.ast, False)
sig = Z3_fpa_get_numeral_significand_string(a.ctx_ref(), a.ast)
if sgnb and sgn.value != 0:
- r.append(to_format('-'))
+ r.append(to_format("-"))
r.append(to_format(sig))
- if (exp != '0'):
- r.append(to_format('*(2**'))
+ if (exp != "0"):
+ r.append(to_format("*(2**"))
r.append(to_format(exp))
- r.append(to_format(')'))
+ r.append(to_format(")"))
return compose(r)
-
def pp_fp(self, a, d, xs):
_z3_assert(isinstance(a, z3.FPRef), "type mismatch")
k = a.decl().kind()
- op = '?'
+ op = "?"
if (self.fpa_pretty and k in _z3_op_to_fpa_pretty_str):
op = _z3_op_to_fpa_pretty_str[k]
elif k in _z3_op_to_fpa_normal_str:
op = _z3_op_to_fpa_normal_str[k]
elif k in _z3_op_to_str:
- op = _z3_op_to_str[k]
+ op = _z3_op_to_str[k]
n = a.num_args()
if self.fpa_pretty:
- if self.is_infix(k) and n >= 3:
+ if self.is_infix(k) and n >= 3:
rm = a.arg(0)
if z3.is_fprm_value(rm) and z3.get_default_rounding_mode(a.ctx).eq(rm):
- arg1 = to_format(self.pp_expr(a.arg(1), d+1, xs))
- arg2 = to_format(self.pp_expr(a.arg(2), d+1, xs))
+ arg1 = to_format(self.pp_expr(a.arg(1), d + 1, xs))
+ arg2 = to_format(self.pp_expr(a.arg(2), d + 1, xs))
r = []
r.append(arg1)
- r.append(to_format(' '))
+ r.append(to_format(" "))
r.append(to_format(op))
- r.append(to_format(' '))
+ r.append(to_format(" "))
r.append(arg2)
return compose(r)
elif k == Z3_OP_FPA_NEG:
- return compose([to_format('-') , to_format(self.pp_expr(a.arg(0), d+1, xs))])
+ return compose([to_format("-"), to_format(self.pp_expr(a.arg(0), d + 1, xs))])
if k in _z3_op_to_fpa_normal_str:
op = _z3_op_to_fpa_normal_str[k]
-
- r = []
+
+ r = []
r.append(to_format(op))
if not z3.is_const(a):
- r.append(to_format('('))
+ r.append(to_format("("))
first = True
- for c in a.children():
+ for c in a.children():
if first:
first = False
else:
- r.append(to_format(', '))
- r.append(self.pp_expr(c, d+1, xs))
- r.append(to_format(')'))
+ r.append(to_format(", "))
+ r.append(self.pp_expr(c, d + 1, xs))
+ r.append(to_format(")"))
return compose(r)
else:
return to_format(a.as_string())
def pp_prefix(self, a, d, xs):
- r = []
+ r = []
sz = 0
- for child in a.children():
- r.append(self.pp_expr(child, d+1, xs))
+ for child in a.children():
+ r.append(self.pp_expr(child, d + 1, xs))
sz = sz + 1
if sz > self.max_args:
r.append(self.pp_ellipses())
@@ -762,11 +832,11 @@ class Formatter:
def infix_args_core(self, a, d, xs, r):
sz = len(r)
- k = a.decl().kind()
- p = self.get_precedence(k)
+ k = a.decl().kind()
+ p = self.get_precedence(k)
first = True
for child in a.children():
- child_pp = self.pp_expr(child, d+1, xs)
+ child_pp = self.pp_expr(child, d + 1, xs)
child_k = None
if z3.is_app(child):
child_k = child.decl().kind()
@@ -779,7 +849,7 @@ class Formatter:
child_p = self.get_precedence(child_k)
if p > child_p or (_is_add(k) and _is_sub(child_k)) or (_is_sub(k) and first and _is_add(child_k)):
r.append(child_pp)
- else:
+ else:
r.append(self.add_paren(child_pp))
sz = sz + 1
elif z3.is_quantifier(child):
@@ -798,25 +868,25 @@ class Formatter:
return r
def pp_infix(self, a, d, xs):
- k = a.decl().kind()
+ k = a.decl().kind()
if self.is_infix_compact(k):
op = self.pp_name(a)
return group(seq(self.infix_args(a, d, xs), op, False))
else:
op = self.pp_name(a)
sz = _len(op)
- op.string = ' ' + op.string
- op.size = sz + 1
+ op.string = " " + op.string
+ op.size = sz + 1
return group(seq(self.infix_args(a, d, xs), op))
def pp_unary(self, a, d, xs):
- k = a.decl().kind()
- p = self.get_precedence(k)
- child = a.children()[0]
- child_k = None
+ k = a.decl().kind()
+ p = self.get_precedence(k)
+ child = a.children()[0]
+ child_k = None
if z3.is_app(child):
child_k = child.decl().kind()
- child_pp = self.pp_expr(child, d+1, xs)
+ child_pp = self.pp_expr(child, d + 1, xs)
if k != child_k and self.is_infix_unary(child_k):
child_p = self.get_precedence(child_k)
if p <= child_p:
@@ -827,7 +897,7 @@ class Formatter:
return compose(to_format(name), indent(_len(name), child_pp))
def pp_power_arg(self, arg, d, xs):
- r = self.pp_expr(arg, d+1, xs)
+ r = self.pp_expr(arg, d + 1, xs)
k = None
if z3.is_app(arg):
k = arg.decl().kind()
@@ -837,9 +907,9 @@ class Formatter:
return r
def pp_power(self, a, d, xs):
- arg1_pp = self.pp_power_arg(a.arg(0), d+1, xs)
- arg2_pp = self.pp_power_arg(a.arg(1), d+1, xs)
- return group(seq((arg1_pp, arg2_pp), '**', False))
+ arg1_pp = self.pp_power_arg(a.arg(0), d + 1, xs)
+ arg2_pp = self.pp_power_arg(a.arg(1), d + 1, xs)
+ return group(seq((arg1_pp, arg2_pp), "**", False))
def pp_neq(self):
return to_format("!=")
@@ -848,8 +918,8 @@ class Formatter:
if a.num_args() == 2:
op = self.pp_neq()
sz = _len(op)
- op.string = ' ' + op.string
- op.size = sz + 1
+ op.string = " " + op.string
+ op.size = sz + 1
return group(seq(self.infix_args(a, d, xs), op))
else:
return self.pp_prefix(a, d, xs)
@@ -858,28 +928,28 @@ class Formatter:
if a.num_args() != 2:
return self.pp_prefix(a, d, xs)
else:
- arg1_pp = self.pp_expr(a.arg(0), d+1, xs)
- arg2_pp = self.pp_expr(a.arg(1), d+1, xs)
- return compose(arg1_pp, indent(2, compose(to_format('['), arg2_pp, to_format(']'))))
+ arg1_pp = self.pp_expr(a.arg(0), d + 1, xs)
+ arg2_pp = self.pp_expr(a.arg(1), d + 1, xs)
+ return compose(arg1_pp, indent(2, compose(to_format("["), arg2_pp, to_format("]"))))
def pp_unary_param(self, a, d, xs):
- p = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 0)
- arg = self.pp_expr(a.arg(0), d+1, xs)
- return seq1(self.pp_name(a), [ to_format(p), arg ])
+ p = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 0)
+ arg = self.pp_expr(a.arg(0), d + 1, xs)
+ return seq1(self.pp_name(a), [to_format(p), arg])
def pp_extract(self, a, d, xs):
- h = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 0)
- l = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 1)
- arg = self.pp_expr(a.arg(0), d+1, xs)
- return seq1(self.pp_name(a), [ to_format(h), to_format(l), arg ])
+ h = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 0)
+ l = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 1)
+ arg = self.pp_expr(a.arg(0), d + 1, xs)
+ return seq1(self.pp_name(a), [to_format(h), to_format(l), arg])
def pp_loop(self, a, d, xs):
- l = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 0)
- arg = self.pp_expr(a.arg(0), d+1, xs)
+ l = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 0)
+ arg = self.pp_expr(a.arg(0), d + 1, xs)
if Z3_get_decl_num_parameters(a.ctx_ref(), a.decl().ast) > 1:
- h = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 1)
- return seq1("Loop", [ arg, to_format(l), to_format(h) ])
- return seq1("Loop", [ arg, to_format(l) ])
+ h = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 1)
+ return seq1("Loop", [arg, to_format(l), to_format(h)])
+ return seq1("Loop", [arg, to_format(l)])
def pp_set(self, id, a):
return seq1(id, [self.pp_sort(a.sort())])
@@ -888,22 +958,22 @@ class Formatter:
if a.num_args() == 1:
return self.pp_expr(a.arg(0), d, xs)
else:
- return seq1('MultiPattern', [ self.pp_expr(arg, d+1, xs) for arg in a.children() ])
+ return seq1("MultiPattern", [self.pp_expr(arg, d + 1, xs) for arg in a.children()])
def pp_is(self, a, d, xs):
- f = a.params()[0]
+ f = a.params()[0]
return self.pp_fdecl(f, a, d, xs)
def pp_map(self, a, d, xs):
- f = z3.get_map_func(a)
+ f = z3.get_map_func(a)
return self.pp_fdecl(f, a, d, xs)
def pp_fdecl(self, f, a, d, xs):
- r = []
+ r = []
sz = 0
r.append(to_format(f.name()))
- for child in a.children():
- r.append(self.pp_expr(child, d+1, xs))
+ for child in a.children():
+ r.append(self.pp_expr(child, d + 1, xs))
sz = sz + 1
if sz > self.max_args:
r.append(self.pp_ellipses())
@@ -911,28 +981,27 @@ class Formatter:
return seq1(self.pp_name(a), r)
def pp_K(self, a, d, xs):
- return seq1(self.pp_name(a), [ self.pp_sort(a.domain()), self.pp_expr(a.arg(0), d+1, xs) ])
+ return seq1(self.pp_name(a), [self.pp_sort(a.domain()), self.pp_expr(a.arg(0), d + 1, xs)])
def pp_atmost(self, a, d, f, xs):
- k = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 0)
- return seq1(self.pp_name(a), [seq3([ self.pp_expr(ch, d+1, xs) for ch in a.children()]), to_format(k)])
+ k = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 0)
+ return seq1(self.pp_name(a), [seq3([self.pp_expr(ch, d + 1, xs) for ch in a.children()]), to_format(k)])
def pp_pbcmp(self, a, d, f, xs):
chs = a.children()
rchs = range(len(chs))
- k = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 0)
- ks = [Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, i+1) for i in rchs]
- ls = [ seq3([self.pp_expr(chs[i], d+1,xs), to_format(ks[i])]) for i in rchs]
+ k = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 0)
+ ks = [Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, i + 1) for i in rchs]
+ ls = [seq3([self.pp_expr(chs[i], d + 1, xs), to_format(ks[i])]) for i in rchs]
return seq1(self.pp_name(a), [seq3(ls), to_format(k)])
-
def pp_app(self, a, d, xs):
if z3.is_int_value(a):
return self.pp_int(a)
elif z3.is_rational_value(a):
return self.pp_rational(a)
elif z3.is_algebraic_value(a):
- return self.pp_algebraic(a)
+ return self.pp_algebraic(a)
elif z3.is_bv_value(a):
return self.pp_bv(a)
elif z3.is_finite_domain_value(a):
@@ -987,26 +1056,26 @@ class Formatter:
def pp_var(self, a, d, xs):
idx = z3.get_var_index(a)
- sz = len(xs)
+ sz = len(xs)
if idx >= sz:
- return seq1('Var', (to_format(idx),))
+ return seq1("Var", (to_format(idx),))
else:
return to_format(xs[sz - idx - 1])
-
+
def pp_quantifier(self, a, d, xs):
- ys = [ to_format(a.var_name(i)) for i in range(a.num_vars()) ]
- new_xs = xs + ys
- body_pp = self.pp_expr(a.body(), d+1, new_xs)
+ ys = [to_format(a.var_name(i)) for i in range(a.num_vars())]
+ new_xs = xs + ys
+ body_pp = self.pp_expr(a.body(), d + 1, new_xs)
if len(ys) == 1:
ys_pp = ys[0]
else:
- ys_pp = seq3(ys, '[', ']')
+ ys_pp = seq3(ys, "[", "]")
if a.is_forall():
- header = 'ForAll'
+ header = "ForAll"
elif a.is_exists():
- header = 'Exists'
+ header = "Exists"
else:
- header = 'Lambda'
+ header = "Lambda"
return seq1(header, (ys_pp, body_pp))
def pp_expr(self, a, d, xs):
@@ -1025,10 +1094,10 @@ class Formatter:
def pp_decl(self, f):
k = f.kind()
if k == Z3_OP_DT_IS or k == Z3_OP_ARRAY_MAP:
- g = f.params()[0]
- r = [ to_format(g.name()) ]
- return seq1(self.pp_name(f), r)
- return self.pp_name(f)
+ g = f.params()[0]
+ r = [to_format(g.name())]
+ return seq1(self.pp_name(f), r)
+ return self.pp_name(f)
def pp_seq_core(self, f, a, d, xs):
self.visited = self.visited + 1
@@ -1037,13 +1106,13 @@ class Formatter:
r = []
sz = 0
for elem in a:
- r.append(f(elem, d+1, xs))
+ r.append(f(elem, d + 1, xs))
sz = sz + 1
if sz > self.max_args:
r.append(self.pp_ellipses())
break
- return seq3(r, '[', ']')
-
+ return seq3(r, "[", "]")
+
def pp_seq(self, a, d, xs):
return self.pp_seq_core(self.pp_expr, a, d, xs)
@@ -1060,12 +1129,12 @@ class Formatter:
else:
i_pp = self.pp_expr(i, 0, [])
name = self.pp_name(d)
- r.append(compose(name, to_format(' = '), indent(_len(name) + 3, i_pp)))
+ r.append(compose(name, to_format(" = "), indent(_len(name) + 3, i_pp)))
sz = sz + 1
if sz > self.max_args:
r.append(self.pp_ellipses())
break
- return seq3(r, '[', ']')
+ return seq3(r, "[", "]")
def pp_func_entry(self, e):
num = e.num_args()
@@ -1075,8 +1144,8 @@ class Formatter:
args.append(self.pp_expr(e.arg_value(i), 0, []))
args_pp = group(seq3(args))
else:
- args_pp = self.pp_expr(e.arg_value(0), 0, [])
- value_pp = self.pp_expr(e.value(), 0, [])
+ args_pp = self.pp_expr(e.arg_value(0), 0, [])
+ value_pp = self.pp_expr(e.value(), 0, [])
return group(seq((args_pp, value_pp), self.pp_arrow()))
def pp_func_interp(self, f):
@@ -1091,12 +1160,12 @@ class Formatter:
break
if sz <= self.max_args:
else_val = f.else_value()
- if else_val == None:
- else_pp = to_format('#unspecified')
+ if else_val is None:
+ else_pp = to_format("#unspecified")
else:
- else_pp = self.pp_expr(else_val, 0, [])
- r.append(group(seq((to_format('else'), else_pp), self.pp_arrow())))
- return seq3(r, '[', ']')
+ else_pp = self.pp_expr(else_val, 0, [])
+ r.append(group(seq((to_format("else"), else_pp), self.pp_arrow())))
+ return seq3(r, "[", "]")
def pp_list(self, a):
r = []
@@ -1113,7 +1182,7 @@ class Formatter:
if isinstance(a, tuple):
return seq3(r)
else:
- return seq3(r, '[', ']')
+ return seq3(r, "[", "]")
def main(self, a):
if z3.is_expr(a):
@@ -1145,6 +1214,7 @@ class Formatter:
self.visited = 0
return self.main(a)
+
class HTMLFormatter(Formatter):
def __init__(self):
Formatter.__init__(self)
@@ -1152,17 +1222,17 @@ class HTMLFormatter(Formatter):
self.ellipses = to_format(_html_ellipses)
def pp_arrow(self):
- return to_format(' →', 1)
+ return to_format(" →", 1)
def pp_unknown(self):
- return '<b>unknown</b>'
-
+ return "<b>unknown</b>"
+
def pp_name(self, a):
r = _html_op_name(a)
- if r[0] == '&' or r[0] == '/' or r[0] == '%':
+ if r[0] == "&" or r[0] == "/" or r[0] == "%":
return to_format(r, 1)
else:
- pos = r.find('__')
+ pos = r.find("__")
if pos == -1 or pos == 0:
return to_format(r)
else:
@@ -1170,7 +1240,7 @@ class HTMLFormatter(Formatter):
if pos + 2 == sz:
return to_format(r)
else:
- return to_format('%s<sub>%s</sub>' % (r[0:pos], r[pos+2:sz]), sz - 2)
+ return to_format("%s<sub>%s</sub>" % (r[0:pos], r[pos + 2:sz]), sz - 2)
def is_assoc(self, k):
return _is_html_assoc(k)
@@ -1180,7 +1250,7 @@ class HTMLFormatter(Formatter):
def is_infix(self, a):
return _is_html_infix(a)
-
+
def is_unary(self, a):
return _is_html_unary(a)
@@ -1191,67 +1261,71 @@ class HTMLFormatter(Formatter):
return to_format("≠")
def pp_power(self, a, d, xs):
- arg1_pp = self.pp_power_arg(a.arg(0), d+1, xs)
- arg2_pp = self.pp_expr(a.arg(1), d+1, xs)
- return compose(arg1_pp, to_format('<sup>', 1), arg2_pp, to_format('</sup>', 1))
+ arg1_pp = self.pp_power_arg(a.arg(0), d + 1, xs)
+ arg2_pp = self.pp_expr(a.arg(1), d + 1, xs)
+ return compose(arg1_pp, to_format("<sup>", 1), arg2_pp, to_format("</sup>", 1))
def pp_var(self, a, d, xs):
idx = z3.get_var_index(a)
- sz = len(xs)
+ sz = len(xs)
if idx >= sz:
# 957 is the greek letter nu
- return to_format('ν<sub>%s</sub>' % idx, 1)
+ return to_format("ν<sub>%s</sub>" % idx, 1)
else:
return to_format(xs[sz - idx - 1])
def pp_quantifier(self, a, d, xs):
- ys = [ to_format(a.var_name(i)) for i in range(a.num_vars()) ]
- new_xs = xs + ys
- body_pp = self.pp_expr(a.body(), d+1, new_xs)
+ ys = [to_format(a.var_name(i)) for i in range(a.num_vars())]
+ new_xs = xs + ys
+ body_pp = self.pp_expr(a.body(), d + 1, new_xs)
ys_pp = group(seq(ys))
if a.is_forall():
- header = '∀'
+ header = "∀"
else:
- header = '∃'
- return group(compose(to_format(header, 1),
- indent(1, compose(ys_pp, to_format(' :'), line_break(), body_pp))))
+ header = "∃"
+ return group(compose(to_format(header, 1),
+ indent(1, compose(ys_pp, to_format(" :"), line_break(), body_pp))))
-_PP = PP()
+_PP = PP()
_Formatter = Formatter()
+
def set_pp_option(k, v):
- if k == 'html_mode':
+ if k == "html_mode":
if v:
set_html_mode(True)
else:
set_html_mode(False)
return True
- if k == 'fpa_pretty':
+ if k == "fpa_pretty":
if v:
set_fpa_pretty(True)
else:
set_fpa_pretty(False)
return True
val = getattr(_PP, k, None)
- if val != None:
- _z3_assert(type(v) == type(val), "Invalid pretty print option value")
+ if val is not None:
+ _z3_assert(isinstance(v, type(val)), "Invalid pretty print option value")
setattr(_PP, k, v)
return True
val = getattr(_Formatter, k, None)
- if val != None:
- _z3_assert(type(v) == type(val), "Invalid pretty print option value")
+ if val is not None:
+ _z3_assert(isinstance(v, type(val)), "Invalid pretty print option value")
setattr(_Formatter, k, v)
return True
return False
+
def obj_to_string(a):
out = io.StringIO()
_PP(out, _Formatter(a))
return out.getvalue()
+
_html_out = None
+
def set_html_mode(flag=True):
global _Formatter
if flag:
@@ -1259,36 +1333,42 @@ def set_html_mode(flag=True):
else:
_Formatter = Formatter()
+
def set_fpa_pretty(flag=True):
global _Formatter
global _z3_op_to_str
_Formatter.fpa_pretty = flag
if flag:
- for (_k,_v) in _z3_op_to_fpa_pretty_str.items():
+ for (_k, _v) in _z3_op_to_fpa_pretty_str.items():
_z3_op_to_str[_k] = _v
for _k in _z3_fpa_infix:
_infix_map[_k] = True
else:
- for (_k,_v) in _z3_op_to_fpa_normal_str.items():
+ for (_k, _v) in _z3_op_to_fpa_normal_str.items():
_z3_op_to_str[_k] = _v
for _k in _z3_fpa_infix:
_infix_map[_k] = False
+
set_fpa_pretty(True)
+
def get_fpa_pretty():
global Formatter
return _Formatter.fpa_pretty
+
def in_html_mode():
return isinstance(_Formatter, HTMLFormatter)
+
def pp(a):
if _support_pp(a):
print(obj_to_string(a))
else:
print(a)
+
def print_matrix(m):
_z3_assert(isinstance(m, list) or isinstance(m, tuple), "matrix expected")
if not in_html_mode():
@@ -1297,12 +1377,13 @@ def print_matrix(m):
print('<table cellpadding="2", cellspacing="0", border="1">')
for r in m:
_z3_assert(isinstance(r, list) or isinstance(r, tuple), "matrix expected")
- print('<tr>')
+ print("<tr>")
for c in r:
- print('<td>%s</td>' % c)
- print('</tr>')
- print('</table>')
-
+ print("<td>%s</td>" % c)
+ print("</tr>")
+ print("</table>")
+
+
def insert_line_breaks(s, width):
"""Break s in lines of size width (approx)"""
sz = len(s)
@@ -1311,8 +1392,8 @@ def insert_line_breaks(s, width):
new_str = io.StringIO()
w = 0
for i in range(sz):
- if w > width and s[i] == ' ':
- new_str.write(u('<br />'))
+ if w > width and s[i] == " ":
+ new_str.write(u("<br />"))
w = 0
else:
new_str.write(u(s[i]))
diff --git a/src/api/python/z3/z3rcf.py b/src/api/python/z3/z3rcf.py
index 76d22bbca..d8175b2d1 100644
--- a/src/api/python/z3/z3rcf.py
+++ b/src/api/python/z3/z3rcf.py
@@ -1,8 +1,8 @@
############################################
# Copyright (c) 2013 Microsoft Corporation
-#
+#
# Z3 Python interface for Z3 Real Closed Fields
-# that may contain
+# that may contain
# - computable transcendentals
# - infinitesimals
# - algebraic extensions
@@ -14,42 +14,48 @@ from .z3core import *
from .z3printer import *
from fractions import Fraction
+
def _to_rcfnum(num, ctx=None):
if isinstance(num, RCFNum):
return num
else:
return RCFNum(num, ctx)
+
def Pi(ctx=None):
ctx = z3.get_ctx(ctx)
return RCFNum(Z3_rcf_mk_pi(ctx.ref()), ctx)
+
def E(ctx=None):
ctx = z3.get_ctx(ctx)
return RCFNum(Z3_rcf_mk_e(ctx.ref()), ctx)
+
def MkInfinitesimal(name="eps", ctx=None):
# Todo: remove parameter name.
# For now, we keep it for backward compatibility.
ctx = z3.get_ctx(ctx)
return RCFNum(Z3_rcf_mk_infinitesimal(ctx.ref()), ctx)
+
def MkRoots(p, ctx=None):
ctx = z3.get_ctx(ctx)
num = len(p)
- _tmp = []
- _as = (RCFNumObj * num)()
- _rs = (RCFNumObj * num)()
+ _tmp = []
+ _as = (RCFNumObj * num)()
+ _rs = (RCFNumObj * num)()
for i in range(num):
_a = _to_rcfnum(p[i], ctx)
- _tmp.append(_a) # prevent GC
+ _tmp.append(_a) # prevent GC
_as[i] = _a.num
nr = Z3_rcf_mk_roots(ctx.ref(), num, _as, _rs)
- r = []
+ r = []
for i in range(nr):
r.append(RCFNum(_rs[i], ctx))
return r
+
class RCFNum:
def __init__(self, num, ctx=None):
# TODO: add support for converting AST numeral values into RCFNum
@@ -65,7 +71,7 @@ class RCFNum:
def ctx_ref(self):
return self.ctx.ref()
-
+
def __repr__(self):
return Z3_rcf_num_to_string(self.ctx_ref(), self.num, False, in_html_mode())
@@ -112,10 +118,10 @@ class RCFNum:
def __pow__(self, k):
return self.power(k)
-
+
def decimal(self, prec=5):
return Z3_rcf_num_to_decimal_string(self.ctx_ref(), self.num, prec)
-
+
def __lt__(self, other):
v = _to_rcfnum(other, self.ctx)
return Z3_rcf_lt(self.ctx_ref(), self.num, v.num)
diff --git a/src/api/python/z3/z3types.py b/src/api/python/z3/z3types.py
index 5c93b27a2..6c93c0bee 100644
--- a/src/api/python/z3/z3types.py
+++ b/src/api/python/z3/z3types.py
@@ -1,6 +1,6 @@
############################################
# Copyright (c) 2012 Microsoft Corporation
-#
+#
# Z3 Python interface
#
# Author: Leonardo de Moura (leonardo)
@@ -8,123 +8,234 @@
import ctypes
+
class Z3Exception(Exception):
def __init__(self, value):
self.value = value
+
def __str__(self):
return str(self.value)
+
class ContextObj(ctypes.c_void_p):
- def __init__(self, context): self._as_parameter_ = context
- def from_param(obj): return obj
+ def __init__(self, context):
+ self._as_parameter_ = context
+
+ def from_param(obj):
+ return obj
+
class Config(ctypes.c_void_p):
- def __init__(self, config): self._as_parameter_ = config
- def from_param(obj): return obj
+ def __init__(self, config):
+ self._as_parameter_ = config
+
+ def from_param(obj):
+ return obj
+
class Symbol(ctypes.c_void_p):
- def __init__(self, symbol): self._as_parameter_ = symbol
- def from_param(obj): return obj
+ def __init__(self, symbol):
+ self._as_parameter_ = symbol
+
+ def from_param(obj):
+ return obj
+
class Sort(ctypes.c_void_p):
- def __init__(self, sort): self._as_parameter_ = sort
- def from_param(obj): return obj
+ def __init__(self, sort):
+ self._as_parameter_ = sort
+
+ def from_param(obj):
+ return obj
+
class FuncDecl(ctypes.c_void_p):
- def __init__(self, decl): self._as_parameter_ = decl
- def from_param(obj): return obj
+ def __init__(self, decl):
+ self._as_parameter_ = decl
+
+ def from_param(obj):
+ return obj
+
class Ast(ctypes.c_void_p):
- def __init__(self, ast): self._as_parameter_ = ast
- def from_param(obj): return obj
+ def __init__(self, ast):
+ self._as_parameter_ = ast
+
+ def from_param(obj):
+ return obj
+
class Pattern(ctypes.c_void_p):
- def __init__(self, pattern): self._as_parameter_ = pattern
- def from_param(obj): return obj
+ def __init__(self, pattern):
+ self._as_parameter_ = pattern
+
+ def from_param(obj):
+ return obj
+
class Model(ctypes.c_void_p):
- def __init__(self, model): self._as_parameter_ = model
- def from_param(obj): return obj
+ def __init__(self, model):
+ self._as_parameter_ = model
+
+ def from_param(obj):
+ return obj
+
class Literals(ctypes.c_void_p):
- def __init__(self, literals): self._as_parameter_ = literals
- def from_param(obj): return obj
+ def __init__(self, literals):
+ self._as_parameter_ = literals
+
+ def from_param(obj):
+ return obj
+
class Constructor(ctypes.c_void_p):
- def __init__(self, constructor): self._as_parameter_ = constructor
- def from_param(obj): return obj
+ def __init__(self, constructor):
+ self._as_parameter_ = constructor
+
+ def from_param(obj):
+ return obj
+
class ConstructorList(ctypes.c_void_p):
- def __init__(self, constructor_list): self._as_parameter_ = constructor_list
- def from_param(obj): return obj
+ def __init__(self, constructor_list):
+ self._as_parameter_ = constructor_list
+
+ def from_param(obj):
+ return obj
+
class GoalObj(ctypes.c_void_p):
- def __init__(self, goal): self._as_parameter_ = goal
- def from_param(obj): return obj
+ def __init__(self, goal):
+ self._as_parameter_ = goal
+
+ def from_param(obj):
+ return obj
+
class TacticObj(ctypes.c_void_p):
- def __init__(self, tactic): self._as_parameter_ = tactic
- def from_param(obj): return obj
+ def __init__(self, tactic):
+ self._as_parameter_ = tactic
+
+ def from_param(obj):
+ return obj
+
class ProbeObj(ctypes.c_void_p):
- def __init__(self, probe): self._as_parameter_ = probe
- def from_param(obj): return obj
+ def __init__(self, probe):
+ self._as_parameter_ = probe
+
+ def from_param(obj):
+ return obj
+
class ApplyResultObj(ctypes.c_void_p):
- def __init__(self, obj): self._as_parameter_ = obj
- def from_param(obj): return obj
+ def __init__(self, obj):
+ self._as_parameter_ = obj
+
+ def from_param(obj):
+ return obj
+
class StatsObj(ctypes.c_void_p):
- def __init__(self, statistics): self._as_parameter_ = statistics
- def from_param(obj): return obj
+ def __init__(self, statistics):
+ self._as_parameter_ = statistics
+
+ def from_param(obj):
+ return obj
+
class SolverObj(ctypes.c_void_p):
- def __init__(self, solver): self._as_parameter_ = solver
- def from_param(obj): return obj
+ def __init__(self, solver):
+ self._as_parameter_ = solver
+
+ def from_param(obj):
+ return obj
+
class SolverCallbackObj(ctypes.c_void_p):
- def __init__(self, solver): self._as_parameter_ = solver
- def from_param(obj): return obj
+ def __init__(self, solver):
+ self._as_parameter_ = solver
+
+ def from_param(obj):
+ return obj
+
class FixedpointObj(ctypes.c_void_p):
- def __init__(self, fixedpoint): self._as_parameter_ = fixedpoint
- def from_param(obj): return obj
+ def __init__(self, fixedpoint):
+ self._as_parameter_ = fixedpoint
+
+ def from_param(obj):
+ return obj
+
class OptimizeObj(ctypes.c_void_p):
- def __init__(self, optimize): self._as_parameter_ = optimize
- def from_param(obj): return obj
+ def __init__(self, optimize):
+ self._as_parameter_ = optimize
+
+ def from_param(obj):
+ return obj
+
class ModelObj(ctypes.c_void_p):
- def __init__(self, model): self._as_parameter_ = model
- def from_param(obj): return obj
+ def __init__(self, model):
+ self._as_parameter_ = model
+
+ def from_param(obj):
+ return obj
+
class AstVectorObj(ctypes.c_void_p):
- def __init__(self, vector): self._as_parameter_ = vector
- def from_param(obj): return obj
+ def __init__(self, vector):
+ self._as_parameter_ = vector
+
+ def from_param(obj):
+ return obj
+
class AstMapObj(ctypes.c_void_p):
- def __init__(self, ast_map): self._as_parameter_ = ast_map
- def from_param(obj): return obj
+ def __init__(self, ast_map):
+ self._as_parameter_ = ast_map
+
+ def from_param(obj):
+ return obj
+
class Params(ctypes.c_void_p):
- def __init__(self, params): self._as_parameter_ = params
- def from_param(obj): return obj
+ def __init__(self, params):
+ self._as_parameter_ = params
+
+ def from_param(obj):
+ return obj
+
class ParamDescrs(ctypes.c_void_p):
- def __init__(self, paramdescrs): self._as_parameter_ = paramdescrs
- def from_param(obj): return obj
+ def __init__(self, paramdescrs):
+ self._as_parameter_ = paramdescrs
+
+ def from_param(obj):
+ return obj
+
class FuncInterpObj(ctypes.c_void_p):
- def __init__(self, f): self._as_parameter_ = f
- def from_param(obj): return obj
+ def __init__(self, f):
+ self._as_parameter_ = f
+
+ def from_param(obj):
+ return obj
+
class FuncEntryObj(ctypes.c_void_p):
- def __init__(self, e): self._as_parameter_ = e
- def from_param(obj): return obj
+ def __init__(self, e):
+ self._as_parameter_ = e
+
+ def from_param(obj):
+ return obj
+
class RCFNumObj(ctypes.c_void_p):
- def __init__(self, e): self._as_parameter_ = e
- def from_param(obj): return obj
+ def __init__(self, e):
+ self._as_parameter_ = e
-
-
+ def from_param(obj):
+ return obj
diff --git a/src/api/python/z3/z3util.py b/src/api/python/z3/z3util.py
index b37d6b649..fac432895 100644
--- a/src/api/python/z3/z3util.py
+++ b/src/api/python/z3/z3util.py
@@ -1,21 +1,22 @@
############################################
# Copyright (c) 2012 Microsoft Corporation
-#
+#
# Z3 Python interface
#
# Authors: Leonardo de Moura (leonardo)
# ThanhVu (Vu) Nguyen <tnguyen@cs.unm.edu>
############################################
"""
-Usage:
+Usage:
import common_z3 as CM_Z3
"""
import ctypes
from .z3 import *
+
def vset(seq, idfun=None, as_list=True):
- # This functions preserves the order of arguments while removing duplicates.
+ # This functions preserves the order of arguments while removing duplicates.
# This function is from https://code.google.com/p/common-python-vu/source/browse/vu_common.py
# (Thanhu's personal code). It has been copied here to avoid a dependency on vu_common.py.
"""
@@ -24,36 +25,36 @@ def vset(seq, idfun=None, as_list=True):
>>> vset([[11,2],1, [10,['9',1]],2, 1, [11,2],[3,3],[10,99],1,[10,['9',1]]],idfun=repr)
[[11, 2], 1, [10, ['9', 1]], 2, [3, 3], [10, 99]]
"""
-
+
def _uniq_normal(seq):
d_ = {}
for s in seq:
if s not in d_:
d_[s] = None
yield s
-
- def _uniq_idfun(seq,idfun):
+
+ def _uniq_idfun(seq, idfun):
d_ = {}
for s in seq:
h_ = idfun(s)
if h_ not in d_:
d_[h_] = None
yield s
-
+
if idfun is None:
res = _uniq_normal(seq)
- else:
- res = _uniq_idfun(seq,idfun)
-
- return list(res) if as_list else res
+ else:
+ res = _uniq_idfun(seq, idfun)
+
+ return list(res) if as_list else res
def get_z3_version(as_str=False):
major = ctypes.c_uint(0)
minor = ctypes.c_uint(0)
build = ctypes.c_uint(0)
- rev = ctypes.c_uint(0)
- Z3_get_version(major,minor, build, rev)
+ rev = ctypes.c_uint(0)
+ Z3_get_version(major, minor, build, rev)
rs = map(int, (major.value, minor.value, build.value, rev.value))
if as_str:
return "{}.{}.{}.{}".format(*rs)
@@ -64,9 +65,9 @@ def get_z3_version(as_str=False):
def ehash(v):
"""
Returns a 'stronger' hash value than the default hash() method.
- The result from hash() is not enough to distinguish between 2
+ The result from hash() is not enough to distinguish between 2
z3 expressions in some cases.
-
+
Note: the following doctests will fail with Python 2.x as the
default formatting doesn't match that of 3.x.
>>> x1 = Bool('x'); x2 = Bool('x'); x3 = Int('x')
@@ -74,7 +75,7 @@ def ehash(v):
783810685 783810685 783810685
>>> print(ehash(x1), ehash(x2), ehash(x3))
x_783810685_1 x_783810685_1 x_783810685_2
-
+
"""
if z3_debug():
assert is_expr(v)
@@ -83,10 +84,11 @@ def ehash(v):
"""
-In Z3, variables are called *uninterpreted* consts and
+In Z3, variables are called *uninterpreted* consts and
variables are *interpreted* consts.
"""
+
def is_expr_var(v):
"""
EXAMPLES:
@@ -111,7 +113,8 @@ def is_expr_var(v):
True
"""
- return is_const(v) and v.decl().kind()==Z3_OP_UNINTERPRETED
+ return is_const(v) and v.decl().kind() == Z3_OP_UNINTERPRETED
+
def is_expr_val(v):
"""
@@ -135,13 +138,11 @@ def is_expr_val(v):
False
>>> is_expr_val(SafetyInjection)
False
- """
- return is_const(v) and v.decl().kind()!=Z3_OP_UNINTERPRETED
+ """
+ return is_const(v) and v.decl().kind() != Z3_OP_UNINTERPRETED
-
-
-def get_vars(f, rs = None):
+def get_vars(f, rs=None):
"""
>>> x,y = Ints('x y')
>>> a,b = Bools('a b')
@@ -151,15 +152,15 @@ def get_vars(f, rs = None):
"""
if rs is None:
rs = []
-
+
if z3_debug():
assert is_expr(f)
if is_const(f):
if is_expr_val(f):
return rs
- else: #variable
- return vset(rs + [f],str)
+ else: # variable
+ return vset(rs + [f], str)
else:
for f_ in f.children():
@@ -168,7 +169,6 @@ def get_vars(f, rs = None):
return vset(rs, str)
-
def mk_var(name, vsort):
if vsort.kind() == Z3_INT_SORT:
v = Int(name)
@@ -179,13 +179,12 @@ def mk_var(name, vsort):
elif vsort.kind() == Z3_DATATYPE_SORT:
v = Const(name, vsort)
else:
- raise TypeError('Cannot handle this sort (s: %sid: %d)' %(vsort,vsort.kind()))
-
+ raise TypeError("Cannot handle this sort (s: %sid: %d)" % (vsort, vsort.kind()))
+
return v
-
-def prove(claim,assume=None,verbose=0):
+def prove(claim, assume=None, verbose=0):
"""
>>> r,m = prove(BoolVal(True),verbose=0); r,model_str(m,as_str=False)
(True, None)
@@ -204,11 +203,11 @@ def prove(claim,assume=None,verbose=0):
AssertionError: Assumption is always False!
>>> r,m = prove(Implies(x,x),assume=y,verbose=2); r,model_str(m,as_str=False)
- assume:
+ assume:
y
- claim:
+ claim:
Implies(x, x)
- to_prove:
+ to_prove:
Implies(y, Implies(x, x))
(True, None)
@@ -236,52 +235,52 @@ def prove(claim,assume=None,verbose=0):
to_prove = claim
if assume:
if z3_debug():
- is_proved,_ = prove(Not(assume))
+ is_proved, _ = prove(Not(assume))
def _f():
emsg = "Assumption is always False!"
if verbose >= 2:
- emsg = "{}\n{}".format(assume,emsg)
+ emsg = "{}\n{}".format(assume, emsg)
return emsg
- assert is_proved==False, _f()
+ assert is_proved == False, _f()
- to_prove = Implies(assume,to_prove)
+ to_prove = Implies(assume, to_prove)
if verbose >= 2:
- print('assume: ')
+ print("assume: ")
print(assume)
- print('claim: ')
+ print("claim: ")
print(claim)
- print('to_prove: ')
+ print("to_prove: ")
print(to_prove)
f = Not(to_prove)
- models = get_models(f,k=1)
- if models is None: #unknown
- print('E: cannot solve !')
+ models = get_models(f, k=1)
+ if models is None: # unknown
+ print("E: cannot solve !")
return None, None
- elif models == False: #unsat
- return True,None
- else: #sat
+ elif models == False: # unsat
+ return True, None
+ else: # sat
if z3_debug():
- assert isinstance(models,list)
+ assert isinstance(models, list)
if models:
- return False, models[0] #the first counterexample
+ return False, models[0] # the first counterexample
else:
- return False, [] #infinite counterexample,models
-
+ return False, [] # infinite counterexample,models
-def get_models(f,k):
+
+def get_models(f, k):
"""
Returns the first k models satisfiying f.
If f is not satisfiable, returns False.
If f cannot be solved, returns None
If f is satisfiable, returns the first k models
- Note that if f is a tautology, e.g.\ True, then the result is []
-
+ Note that if f is a tautology, e.g.\\ True, then the result is []
+
Based on http://stackoverflow.com/questions/11867611/z3py-checking-all-solutions-for-equation
EXAMPLES:
@@ -314,7 +313,7 @@ def get_models(f,k):
if z3_debug():
assert is_expr(f)
assert k >= 1
-
+
s = Solver()
s.add(f)
@@ -323,16 +322,14 @@ def get_models(f,k):
while s.check() == sat and i < k:
i = i + 1
m = s.model()
- if not m: #if m == []
+ if not m: # if m == []
break
models.append(m)
-
- #create new constraint to block the current model
+ # create new constraint to block the current model
block = Not(And([v() == m[v] for v in m]))
s.add(block)
-
if s.check() == unknown:
return None
elif s.check() == unsat and i == 0:
@@ -340,7 +337,8 @@ def get_models(f,k):
else:
return models
-def is_tautology(claim,verbose=0):
+
+def is_tautology(claim, verbose=0):
"""
>>> is_tautology(Implies(Bool('x'),Bool('x')))
True
@@ -355,38 +353,38 @@ def is_tautology(claim,verbose=0):
False
"""
- return prove(claim=claim,assume=None,verbose=verbose)[0]
+ return prove(claim=claim, assume=None, verbose=verbose)[0]
-def is_contradiction(claim,verbose=0):
+def is_contradiction(claim, verbose=0):
"""
>>> x,y=Bools('x y')
>>> is_contradiction(BoolVal(False))
True
-
+
>>> is_contradiction(BoolVal(True))
False
-
+
>>> is_contradiction(x)
False
-
+
>>> is_contradiction(Implies(x,y))
False
-
+
>>> is_contradiction(Implies(x,x))
False
-
+
>>> is_contradiction(And(x,Not(x)))
True
"""
- return prove(claim=Not(claim),assume=None,verbose=verbose)[0]
+ return prove(claim=Not(claim), assume=None, verbose=verbose)[0]
def exact_one_model(f):
"""
return True if f has exactly 1 model, False otherwise.
-
+
EXAMPLES:
>>> x, y = Ints('x y')
@@ -403,30 +401,29 @@ def exact_one_model(f):
False
"""
- models = get_models(f,k=2)
- if isinstance(models,list):
- return len(models)==1
+ models = get_models(f, k=2)
+ if isinstance(models, list):
+ return len(models) == 1
else:
return False
-
-
-def myBinOp(op,*L):
+
+def myBinOp(op, *L):
"""
>>> myAnd(*[Bool('x'),Bool('y')])
And(x, y)
-
+
>>> myAnd(*[Bool('x'),None])
x
-
+
>>> myAnd(*[Bool('x')])
x
-
+
>>> myAnd(*[])
-
+
>>> myAnd(Bool('x'),Bool('y'))
And(x, y)
-
+
>>> myAnd(*[Bool('x'),Bool('y')])
And(x, y)
@@ -435,7 +432,7 @@ def myBinOp(op,*L):
>>> myAnd((Bool('x'),Bool('y')))
And(x, y)
-
+
>>> myAnd(*[Bool('x'),Bool('y'),True])
Traceback (most recent call last):
...
@@ -444,59 +441,62 @@ def myBinOp(op,*L):
if z3_debug():
assert op == Z3_OP_OR or op == Z3_OP_AND or op == Z3_OP_IMPLIES
-
- if len(L)==1 and (isinstance(L[0],list) or isinstance(L[0],tuple)):
+
+ if len(L) == 1 and (isinstance(L[0], list) or isinstance(L[0], tuple)):
L = L[0]
if z3_debug():
- assert all(not isinstance(l,bool) for l in L)
+ assert all(not isinstance(l, bool) for l in L)
L = [l for l in L if is_expr(l)]
if L:
- if len(L)==1:
+ if len(L) == 1:
return L[0]
- if op == Z3_OP_OR:
+ if op == Z3_OP_OR:
return Or(L)
if op == Z3_OP_AND:
- return And(L)
- return Implies(L[0],L[1])
+ return And(L)
+ return Implies(L[0], L[1])
else:
return None
def myAnd(*L):
- return myBinOp(Z3_OP_AND,*L)
+ return myBinOp(Z3_OP_AND, *L)
+
def myOr(*L):
- return myBinOp(Z3_OP_OR,*L)
+ return myBinOp(Z3_OP_OR, *L)
-def myImplies(a,b):
- return myBinOp(Z3_OP_IMPLIES,[a,b])
-
-Iff = lambda f: And(Implies(f[0],f[1]),Implies(f[1],f[0]))
+def myImplies(a, b):
+ return myBinOp(Z3_OP_IMPLIES, [a, b])
-def model_str(m,as_str=True):
+
+def Iff(f):
+ return And(Implies(f[0], f[1]), Implies(f[1], f[0]))
+
+
+def model_str(m, as_str=True):
"""
Returned a 'sorted' model (so that it's easier to see)
- The model is sorted by its key,
- e.g. if the model is y = 3 , x = 10, then the result is
+ The model is sorted by its key,
+ e.g. if the model is y = 3 , x = 10, then the result is
x = 10, y = 3
EXAMPLES:
- see doctest exampels from function prove()
+ see doctest exampels from function prove()
"""
if z3_debug():
- assert m is None or m == [] or isinstance(m,ModelRef)
+ assert m is None or m == [] or isinstance(m, ModelRef)
- if m :
- vs = [(v,m[v]) for v in m]
- vs = sorted(vs,key=lambda a,_: str(a))
+ if m:
+ vs = [(v, m[v]) for v in m]
+ vs = sorted(vs, key=lambda a, _: str(a))
if as_str:
- return '\n'.join(['{} = {}'.format(k,v) for (k,v) in vs])
+ return "\n".join(["{} = {}".format(k, v) for (k, v) in vs])
else:
return vs
else:
return str(m) if as_str else m
-