mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

Fix some PEP-8 violations in Python code (#5295)

Browse source 
* 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
This commit is contained in:
Gram 2021-05-23 19:27:55 +02:00 committed by GitHub
parent f1545b04d2
commit 3d8865d925
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
7 changed files with 1669 additions and 910 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

File diff suppressed because it is too large Load diff

92
src/api/python/z3/z3num.py
View file

@ -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]

10
src/api/python/z3/z3poly.py
View file

@ -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:

703
src/api/python/z3/z3printer.py
View file

File diff suppressed because it is too large Load diff

26
src/api/python/z3/z3rcf.py
View file

@ -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)

229
src/api/python/z3/z3types.py
View file

@ -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

208
src/api/python/z3/z3util.py
View file

@ -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