mirror of
https://github.com/Z3Prover/z3
synced 2025-04-27 10:55:50 +00:00
Merge branch 'pure' of https://git01.codeplex.com/z3 into contrib
This commit is contained in:
Christoph M. Wintersteiger
commit
6a496a1bfb
560 changed files with 52025 additions and 9358 deletions
|
|
@ -38,7 +38,7 @@ Z3 exceptions:
|
|||
... n = x + y
|
||||
... except Z3Exception as ex:
|
||||
... print("failed: %s" % ex)
|
||||
failed: 'sort mismatch'
|
||||
failed: sort mismatch
|
||||
"""
|
||||
from z3core import *
|
||||
from z3types import *
|
||||
|
|
@ -297,6 +297,11 @@ class AstRef(Z3PPObject):
|
|||
"""Return a pointer to the corresponding C Z3_ast object."""
|
||||
return self.ast
|
||||
|
||||
def get_id(self):
|
||||
"""Return unique identifier for object. It can be used for hash-tables and maps."""
|
||||
return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
|
||||
|
||||
|
||||
def ctx_ref(self):
|
||||
"""Return a reference to the C context where this AST node is stored."""
|
||||
return self.ctx.ref()
|
||||
|
|
@ -447,6 +452,10 @@ class SortRef(AstRef):
|
|||
def as_ast(self):
|
||||
return Z3_sort_to_ast(self.ctx_ref(), self.ast)
|
||||
|
||||
def get_id(self):
|
||||
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.
|
||||
|
||||
|
|
@ -585,8 +594,11 @@ class FuncDeclRef(AstRef):
|
|||
def as_ast(self):
|
||||
return Z3_func_decl_to_ast(self.ctx_ref(), self.ast)
|
||||
|
||||
def get_id(self):
|
||||
return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
|
||||
|
||||
def as_func_decl(self):
|
||||
return self.ast
|
||||
return self.ast
|
||||
|
||||
def name(self):
|
||||
"""Return the name of the function declaration `self`.
|
||||
|
|
@ -730,6 +742,9 @@ class ExprRef(AstRef):
|
|||
def as_ast(self):
|
||||
return self.ast
|
||||
|
||||
def get_id(self):
|
||||
return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
|
||||
|
||||
def sort(self):
|
||||
"""Return the sort of expression `self`.
|
||||
|
||||
|
|
@ -899,6 +914,7 @@ def _coerce_expr_merge(s, a):
|
|||
return s
|
||||
else:
|
||||
if __debug__:
|
||||
_z3_assert(s1.ctx == s.ctx, "context mismatch")
|
||||
_z3_assert(False, "sort mismatch")
|
||||
else:
|
||||
return s
|
||||
|
|
@ -1382,7 +1398,7 @@ def BoolVector(prefix, sz, ctx=None):
|
|||
return [ Bool('%s__%s' % (prefix, i)) for i in range(sz) ]
|
||||
|
||||
def FreshBool(prefix='b', ctx=None):
|
||||
"""Return a fresh Bolean constant in the given context using the given prefix.
|
||||
"""Return a fresh Boolean constant in the given context using the given prefix.
|
||||
|
||||
If `ctx=None`, then the global context is used.
|
||||
|
||||
|
|
@ -1459,9 +1475,18 @@ def And(*args):
|
|||
>>> And(P)
|
||||
And(p__0, p__1, p__2, p__3, p__4)
|
||||
"""
|
||||
args = _get_args(args)
|
||||
ctx = _ctx_from_ast_arg_list(args)
|
||||
last_arg = None
|
||||
if len(args) > 0:
|
||||
last_arg = args[len(args)-1]
|
||||
if isinstance(last_arg, Context):
|
||||
ctx = args[len(args)-1]
|
||||
args = args[:len(args)-1]
|
||||
else:
|
||||
ctx = main_ctx()
|
||||
args = _get_args(args)
|
||||
ctx_args = _ctx_from_ast_arg_list(args, ctx)
|
||||
if __debug__:
|
||||
_z3_assert(ctx_args == None or ctx_args == ctx, "context mismatch")
|
||||
_z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe")
|
||||
if _has_probe(args):
|
||||
return _probe_and(args, ctx)
|
||||
|
|
@ -1480,9 +1505,18 @@ def Or(*args):
|
|||
>>> Or(P)
|
||||
Or(p__0, p__1, p__2, p__3, p__4)
|
||||
"""
|
||||
args = _get_args(args)
|
||||
ctx = _ctx_from_ast_arg_list(args)
|
||||
last_arg = None
|
||||
if len(args) > 0:
|
||||
last_arg = args[len(args)-1]
|
||||
if isinstance(last_arg, Context):
|
||||
ctx = args[len(args)-1]
|
||||
args = args[:len(args)-1]
|
||||
else:
|
||||
ctx = main_ctx()
|
||||
args = _get_args(args)
|
||||
ctx_args = _ctx_from_ast_arg_list(args, ctx)
|
||||
if __debug__:
|
||||
_z3_assert(ctx_args == None or ctx_args == ctx, "context mismatch")
|
||||
_z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe")
|
||||
if _has_probe(args):
|
||||
return _probe_or(args, ctx)
|
||||
|
|
@ -1505,6 +1539,9 @@ class PatternRef(ExprRef):
|
|||
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.
|
||||
|
||||
|
|
@ -1567,6 +1604,9 @@ class QuantifierRef(BoolRef):
|
|||
def as_ast(self):
|
||||
return self.ast
|
||||
|
||||
def get_id(self):
|
||||
return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
|
||||
|
||||
def sort(self):
|
||||
"""Return the Boolean sort."""
|
||||
return BoolSort(self.ctx)
|
||||
|
|
@ -3856,32 +3896,6 @@ def is_array(a):
|
|||
"""
|
||||
return isinstance(a, ArrayRef)
|
||||
|
||||
def is_select(a):
|
||||
"""Return `True` if `a` is a Z3 array select.
|
||||
|
||||
>>> a = Array('a', IntSort(), IntSort())
|
||||
>>> is_select(a)
|
||||
False
|
||||
>>> i = Int('i')
|
||||
>>> is_select(a[i])
|
||||
True
|
||||
"""
|
||||
return is_app_of(a, Z3_OP_SELECT)
|
||||
|
||||
def is_store(a):
|
||||
"""Return `True` if `a` is a Z3 array store.
|
||||
|
||||
>>> a = Array('a', IntSort(), IntSort())
|
||||
>>> is_store(a)
|
||||
False
|
||||
>>> i = Int('i')
|
||||
>>> is_store(a[i])
|
||||
False
|
||||
>>> is_store(Store(a, i, i + 1))
|
||||
True
|
||||
"""
|
||||
return is_app_of(a, Z3_OP_STORE)
|
||||
|
||||
def is_const_array(a):
|
||||
"""Return `True` if `a` is a Z3 constant array.
|
||||
|
||||
|
|
@ -4072,7 +4086,8 @@ def is_select(a):
|
|||
>>> a = Array('a', IntSort(), IntSort())
|
||||
>>> is_select(a)
|
||||
False
|
||||
>>> is_select(a[0])
|
||||
>>> i = Int('i')
|
||||
>>> is_select(a[i])
|
||||
True
|
||||
"""
|
||||
return is_app_of(a, Z3_OP_SELECT)
|
||||
|
|
@ -4153,6 +4168,7 @@ class Datatype:
|
|||
"""
|
||||
if __debug__:
|
||||
_z3_assert(isinstance(name, str), "String expected")
|
||||
_z3_assert(name != "", "Constructor name cannot be empty")
|
||||
return self.declare_core(name, "is_" + name, *args)
|
||||
|
||||
def __repr__(self):
|
||||
|
|
@ -4453,7 +4469,7 @@ def args2params(arguments, keywords, ctx=None):
|
|||
A ':' is added to the keywords, and '_' is replaced with '-'
|
||||
|
||||
>>> args2params(['model', True, 'relevancy', 2], {'elim_and' : True})
|
||||
(params model 1 relevancy 2 elim_and 1)
|
||||
(params model true relevancy 2 elim_and true)
|
||||
"""
|
||||
if __debug__:
|
||||
_z3_assert(len(arguments) % 2 == 0, "Argument list must have an even number of elements.")
|
||||
|
|
@ -6016,6 +6032,24 @@ class Solver(Z3PPObject):
|
|||
"""
|
||||
return Z3_solver_to_string(self.ctx.ref(), self.solver)
|
||||
|
||||
def to_smt2(self):
|
||||
"""return SMTLIB2 formatted benchmark for solver's assertions"""
|
||||
es = self.assertions()
|
||||
sz = len(es)
|
||||
sz1 = sz
|
||||
if sz1 > 0:
|
||||
sz1 -= 1
|
||||
v = (Ast * sz1)()
|
||||
for i in range(sz1):
|
||||
v[i] = es[i].as_ast()
|
||||
if sz > 0:
|
||||
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)
|
||||
|
||||
|
||||
|
||||
def SolverFor(logic, ctx=None):
|
||||
"""Create a solver customized for the given logic.
|
||||
|
||||
|
|
@ -6449,7 +6483,7 @@ class Tactic:
|
|||
_z3_assert(isinstance(goal, Goal) or isinstance(goal, BoolRef), "Z3 Goal or Boolean expressions expected")
|
||||
goal = _to_goal(goal)
|
||||
if len(arguments) > 0 or len(keywords) > 0:
|
||||
p = args2params(arguments, keywords, a.ctx)
|
||||
p = args2params(arguments, keywords, self.ctx)
|
||||
return ApplyResult(Z3_tactic_apply_ex(self.ctx.ref(), self.tactic, goal.goal, p.params), self.ctx)
|
||||
else:
|
||||
return ApplyResult(Z3_tactic_apply(self.ctx.ref(), self.tactic, goal.goal), self.ctx)
|
||||
|
|
@ -6474,7 +6508,7 @@ class Tactic:
|
|||
|
||||
def _to_goal(a):
|
||||
if isinstance(a, BoolRef):
|
||||
goal = Goal()
|
||||
goal = Goal(ctx = a.ctx)
|
||||
goal.add(a)
|
||||
return goal
|
||||
else:
|
||||
|
|
@ -6957,15 +6991,15 @@ def substitute(t, *m):
|
|||
>>> x = Int('x')
|
||||
>>> y = Int('y')
|
||||
>>> substitute(x + 1, (x, y + 1))
|
||||
2 + y
|
||||
y + 1 + 1
|
||||
>>> f = Function('f', IntSort(), IntSort())
|
||||
>>> substitute(f(x) + f(y), (f(x), IntVal(1)), (f(y), IntVal(1)))
|
||||
2
|
||||
1 + 1
|
||||
"""
|
||||
if isinstance(m, tuple):
|
||||
m1 = _get_args(m)
|
||||
if isinstance(m1, list):
|
||||
m = _get_args(m1)
|
||||
m = m1
|
||||
if __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.")
|
||||
|
|
@ -7258,3 +7292,128 @@ def parse_smt2_file(f, sorts={}, decls={}, ctx=None):
|
|||
dsz, dnames, ddecls = _dict2darray(decls, ctx)
|
||||
return _to_expr_ref(Z3_parse_smtlib2_file(ctx.ref(), f, ssz, snames, ssorts, dsz, dnames, ddecls), ctx)
|
||||
|
||||
def Interpolant(a,ctx=None):
|
||||
"""Create an interpolation operator.
|
||||
|
||||
The argument is an interpolation pattern (see tree_interpolant).
|
||||
|
||||
>>> x = Int('x')
|
||||
>>> print Interpolant(x>0)
|
||||
interp(x > 0)
|
||||
"""
|
||||
ctx = _get_ctx(_ctx_from_ast_arg_list([a], ctx))
|
||||
s = BoolSort(ctx)
|
||||
a = s.cast(a)
|
||||
return BoolRef(Z3_mk_interpolant(ctx.ref(), a.as_ast()), ctx)
|
||||
|
||||
def tree_interpolant(pat,p=None,ctx=None):
|
||||
"""Compute interpolant for a tree of formulas.
|
||||
|
||||
The input is an interpolation pattern over a set of formulas C.
|
||||
The pattern pat is a formula combining the formulas in C using
|
||||
logical conjunction and the "interp" operator (see Interp). This
|
||||
interp operator is logically the identity operator. It marks the
|
||||
sub-formulas of the pattern for which interpolants should be
|
||||
computed. The interpolant is a map sigma from marked subformulas
|
||||
to formulas, such that, for each marked subformula phi of pat
|
||||
(where phi sigma is phi with sigma(psi) substituted for each
|
||||
subformula psi of phi such that psi in dom(sigma)):
|
||||
|
||||
1) phi sigma implies sigma(phi), and
|
||||
|
||||
2) sigma(phi) is in the common uninterpreted vocabulary between
|
||||
the formulas of C occurring in phi and those not occurring in
|
||||
phi
|
||||
|
||||
and moreover pat sigma implies false. In the simplest case
|
||||
an interpolant for the pattern "(and (interp A) B)" maps A
|
||||
to an interpolant for A /\ B.
|
||||
|
||||
The return value is a vector of formulas representing sigma. This
|
||||
vector contains sigma(phi) for each marked subformula of pat, in
|
||||
pre-order traversal. This means that subformulas of phi occur before phi
|
||||
in the vector. Also, subformulas that occur multiply in pat will
|
||||
occur multiply in the result vector.
|
||||
|
||||
If pat is satisfiable, raises an object of class ModelRef
|
||||
that represents a model of pat.
|
||||
|
||||
If parameters p are supplied, these are used in creating the
|
||||
solver that determines satisfiability.
|
||||
|
||||
>>> x = Int('x')
|
||||
>>> y = Int('y')
|
||||
>>> print tree_interpolant(And(Interpolant(x < 0), Interpolant(y > 2), x == y))
|
||||
[Not(x >= 0), Not(y <= 2)]
|
||||
|
||||
>>> g = And(Interpolant(x<0),x<2)
|
||||
>>> try:
|
||||
... print tree_interpolant(g).sexpr()
|
||||
... except ModelRef as m:
|
||||
... print m.sexpr()
|
||||
(define-fun x () Int
|
||||
(- 1))
|
||||
"""
|
||||
f = pat
|
||||
ctx = _get_ctx(_ctx_from_ast_arg_list([f], ctx))
|
||||
ptr = (AstVectorObj * 1)()
|
||||
mptr = (Model * 1)()
|
||||
if p == None:
|
||||
p = ParamsRef(ctx)
|
||||
res = Z3_compute_interpolant(ctx.ref(),f.as_ast(),p.params,ptr,mptr)
|
||||
if res == Z3_L_FALSE:
|
||||
return AstVector(ptr[0],ctx)
|
||||
raise ModelRef(mptr[0], ctx)
|
||||
|
||||
def binary_interpolant(a,b,p=None,ctx=None):
|
||||
"""Compute an interpolant for a binary conjunction.
|
||||
|
||||
If a & b is unsatisfiable, returns an interpolant for a & b.
|
||||
This is a formula phi such that
|
||||
|
||||
1) a implies phi
|
||||
2) b implies not phi
|
||||
3) All the uninterpreted symbols of phi occur in both a and b.
|
||||
|
||||
If a & b is satisfiable, raises an object of class ModelRef
|
||||
that represents a model of a &b.
|
||||
|
||||
If parameters p are supplied, these are used in creating the
|
||||
solver that determines satisfiability.
|
||||
|
||||
x = Int('x')
|
||||
print binary_interpolant(x<0,x>2)
|
||||
Not(x >= 0)
|
||||
"""
|
||||
f = And(Interpolant(a),b)
|
||||
return tree_interpolant(f,p,ctx)[0]
|
||||
|
||||
def sequence_interpolant(v,p=None,ctx=None):
|
||||
"""Compute interpolant for a sequence of formulas.
|
||||
|
||||
If len(v) == N, and if the conjunction of the formulas in v is
|
||||
unsatisfiable, the interpolant is a sequence of formulas w
|
||||
such that len(w) = N-1 and v[0] implies w[0] and for i in 0..N-1:
|
||||
|
||||
1) w[i] & v[i+1] implies w[i+1] (or false if i+1 = N)
|
||||
2) All uninterpreted symbols in w[i] occur in both v[0]..v[i]
|
||||
and v[i+1]..v[n]
|
||||
|
||||
Requires len(v) >= 1.
|
||||
|
||||
If a & b is satisfiable, raises an object of class ModelRef
|
||||
that represents a model of a & b.
|
||||
|
||||
If parameters p are supplied, these are used in creating the
|
||||
solver that determines satisfiability.
|
||||
|
||||
>>> x = Int('x')
|
||||
>>> y = Int('y')
|
||||
>>> print sequence_interpolant([x < 0, y == x , y > 2])
|
||||
[Not(x >= 0), Not(y >= 0)]
|
||||
"""
|
||||
f = v[0]
|
||||
for i in range(1,len(v)):
|
||||
f = And(Interpolant(f),v[i])
|
||||
return tree_interpolant(f,p,ctx)
|
||||
|
||||
|
|
|
|||
|
|
@ -386,7 +386,7 @@ def seq3(args, lp='(', rp=')'):
|
|||
else:
|
||||
return group(indent(len(lp), compose(to_format(lp), seq(args), to_format(rp))))
|
||||
|
||||
class StopPPException:
|
||||
class StopPPException(Exception):
|
||||
def __str__(self):
|
||||
return 'pp-interrupted'
|
||||
|
||||
|
|
|
|||
|
|
@ -4,7 +4,7 @@ class Z3Exception(Exception):
|
|||
def __init__(self, value):
|
||||
self.value = value
|
||||
def __str__(self):
|
||||
return repr(self.value)
|
||||
return str(self.value)
|
||||
|
||||
class ContextObj(ctypes.c_void_p):
|
||||
def __init__(self, context): self._as_parameter_ = context
|
||||
|
|
@ -109,3 +109,4 @@ class FuncEntryObj(ctypes.c_void_p):
|
|||
class RCFNumObj(ctypes.c_void_p):
|
||||
def __init__(self, e): self._as_parameter_ = e
|
||||
def from_param(obj): return obj
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue