mirror of
https://github.com/Z3Prover/z3
synced 2025-04-27 10:55:50 +00:00
Merge branch 'pure' of https://github.com/Z3Prover/z3
Conflicts: src/api/ml/z3.ml src/api/ml/z3.mli src/api/python/z3util.py
This commit is contained in:
Christoph M. Wintersteiger
commit
95dea3922d
1108 changed files with 54208 additions and 8417 deletions
|
|
@ -32,7 +32,7 @@ sat
|
|||
Z3 exceptions:
|
||||
|
||||
>>> try:
|
||||
... x = Int('x')
|
||||
... x = BitVec('x', 32)
|
||||
... y = Bool('y')
|
||||
... # the expression x + y is type incorrect
|
||||
... n = x + y
|
||||
|
|
@ -301,7 +301,6 @@ class AstRef(Z3PPObject):
|
|||
"""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()
|
||||
|
|
@ -455,7 +454,6 @@ class SortRef(AstRef):
|
|||
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.
|
||||
|
||||
|
|
@ -555,6 +553,8 @@ def _to_sort_ref(s, ctx):
|
|||
return ArraySortRef(s, ctx)
|
||||
elif k == Z3_DATATYPE_SORT:
|
||||
return DatatypeSortRef(s, ctx)
|
||||
elif k == Z3_FINITE_DOMAIN_SORT:
|
||||
return FiniteDomainSortRef(s, ctx)
|
||||
elif k == Z3_FLOATING_POINT_SORT:
|
||||
return FPSortRef(s, ctx)
|
||||
elif k == Z3_ROUNDING_MODE_SORT:
|
||||
|
|
@ -1228,6 +1228,16 @@ class BoolSortRef(SortRef):
|
|||
_z3_assert(self.eq(val.sort()), "Value cannot be converted into a Z3 Boolean value")
|
||||
return val
|
||||
|
||||
def subsort(self, other):
|
||||
return isinstance(other, ArithSortRef)
|
||||
|
||||
def is_int(self):
|
||||
return True
|
||||
|
||||
def is_bool(self):
|
||||
return True
|
||||
|
||||
|
||||
class BoolRef(ExprRef):
|
||||
"""All Boolean expressions are instances of this class."""
|
||||
def sort(self):
|
||||
|
|
@ -1900,6 +1910,10 @@ class ArithSortRef(SortRef):
|
|||
return val
|
||||
if val_s.is_int() and self.is_real():
|
||||
return ToReal(val)
|
||||
if val_s.is_bool() and self.is_int():
|
||||
return If(val, 1, 0)
|
||||
if val_s.is_bool() and self.is_real():
|
||||
return ToReal(If(val, 1, 0))
|
||||
if __debug__:
|
||||
_z3_assert(False, "Z3 Integer/Real expression expected" )
|
||||
else:
|
||||
|
|
@ -3906,6 +3920,10 @@ class ArrayRef(ExprRef):
|
|||
arg = self.domain().cast(arg)
|
||||
return _to_expr_ref(Z3_mk_select(self.ctx_ref(), self.as_ast(), arg.as_ast()), self.ctx)
|
||||
|
||||
def mk_default(self):
|
||||
return _to_expr_ref(Z3_mk_array_default(self.ctx_ref(), self.as_ast()), self.ctx)
|
||||
|
||||
|
||||
def is_array(a):
|
||||
"""Return `True` if `a` is a Z3 array expression.
|
||||
|
||||
|
|
@ -3958,6 +3976,14 @@ 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))
|
||||
>>> is_default(d)
|
||||
True
|
||||
"""
|
||||
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.
|
||||
|
||||
|
|
@ -4030,6 +4056,17 @@ 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)
|
||||
>>> prove(Default(b) == 1)
|
||||
proved
|
||||
"""
|
||||
if __debug__:
|
||||
_z3_assert(is_array(a), "First argument must be a Z3 array expression")
|
||||
return a.mk_default()
|
||||
|
||||
|
||||
def Store(a, i, v):
|
||||
"""Return a Z3 store array expression.
|
||||
|
||||
|
|
@ -5603,7 +5640,7 @@ class Statistics:
|
|||
sat
|
||||
>>> st = s.statistics()
|
||||
>>> len(st)
|
||||
2
|
||||
6
|
||||
"""
|
||||
return int(Z3_stats_size(self.ctx.ref(), self.stats))
|
||||
|
||||
|
|
@ -5617,7 +5654,7 @@ class Statistics:
|
|||
sat
|
||||
>>> st = s.statistics()
|
||||
>>> len(st)
|
||||
2
|
||||
6
|
||||
>>> st[0]
|
||||
('nlsat propagations', 2)
|
||||
>>> st[1]
|
||||
|
|
@ -5641,7 +5678,7 @@ class Statistics:
|
|||
sat
|
||||
>>> st = s.statistics()
|
||||
>>> st.keys()
|
||||
['nlsat propagations', 'nlsat stages']
|
||||
['nlsat propagations', 'nlsat stages', 'rlimit count', 'max memory', 'memory', 'num allocs']
|
||||
"""
|
||||
return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))]
|
||||
|
||||
|
|
@ -5678,7 +5715,7 @@ class Statistics:
|
|||
sat
|
||||
>>> st = s.statistics()
|
||||
>>> st.keys()
|
||||
['nlsat propagations', 'nlsat stages']
|
||||
['nlsat propagations', 'nlsat stages', 'rlimit count', 'max memory', 'memory', 'num allocs']
|
||||
>>> st.nlsat_propagations
|
||||
2
|
||||
>>> st.nlsat_stages
|
||||
|
|
@ -6071,8 +6108,6 @@ class Solver(Z3PPObject):
|
|||
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.
|
||||
|
||||
|
|
@ -6333,6 +6368,170 @@ class Fixedpoint(Z3PPObject):
|
|||
else:
|
||||
return Exists(self.vars, fml)
|
||||
|
||||
|
||||
#########################################
|
||||
#
|
||||
# Finite domain sorts
|
||||
#
|
||||
#########################################
|
||||
|
||||
class FiniteDomainSortRef(SortRef):
|
||||
"""Finite domain sort."""
|
||||
|
||||
def size(self):
|
||||
"""Return the size of the finite domain sort"""
|
||||
r = (ctype.c_ulonglong * 1)()
|
||||
if Z3_get_finite_domain_sort_size(self.ctx_ref(), self.ast(), r):
|
||||
return r[0]
|
||||
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"""
|
||||
ctx = _get_ctx(ctx)
|
||||
return FiniteDomainSortRef(Z3_mk_finite_domain_sort(ctx.ref(), name, sz), ctx)
|
||||
|
||||
#########################################
|
||||
#
|
||||
# Optimize
|
||||
#
|
||||
#########################################
|
||||
|
||||
class OptimizeObjective:
|
||||
def __init__(self, opt, value, is_max):
|
||||
self._opt = opt
|
||||
self._value = value
|
||||
self._is_max = is_max
|
||||
|
||||
def lower(self):
|
||||
opt = self._opt
|
||||
return _to_expr_ref(Z3_optimize_get_lower(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
|
||||
|
||||
def upper(self):
|
||||
opt = self._opt
|
||||
return _to_expr_ref(Z3_optimize_get_upper(opt.ctx.ref(), opt.optimize, self._value), opt.ctx)
|
||||
|
||||
def value(self):
|
||||
if self._is_max:
|
||||
return self.upper()
|
||||
else:
|
||||
return self.lower()
|
||||
|
||||
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.optimize = Z3_mk_optimize(self.ctx.ref())
|
||||
Z3_optimize_inc_ref(self.ctx.ref(), self.optimize)
|
||||
|
||||
def __del__(self):
|
||||
if self.optimize != None:
|
||||
Z3_optimize_dec_ref(self.ctx.ref(), self.optimize)
|
||||
|
||||
def set(self, *args, **keys):
|
||||
"""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)
|
||||
|
||||
def help(self):
|
||||
"""Display a string describing all available options."""
|
||||
print(Z3_optimize_get_help(self.ctx.ref(), self.optimize))
|
||||
|
||||
def param_descrs(self):
|
||||
"""Return the parameter description set."""
|
||||
return ParamDescrsRef(Z3_optimize_get_param_descrs(self.ctx.ref(), self.optimize), self.ctx)
|
||||
|
||||
def assert_exprs(self, *args):
|
||||
"""Assert constraints as background axioms for the optimize solver."""
|
||||
args = _get_args(args)
|
||||
for arg in args:
|
||||
if isinstance(arg, Goal) or isinstance(arg, AstVector):
|
||||
for f in arg:
|
||||
Z3_optimize_assert(self.ctx.ref(), self.optimize, f.as_ast())
|
||||
else:
|
||||
Z3_optimize_assert(self.ctx.ref(), self.optimize, arg.as_ast())
|
||||
|
||||
def add(self, *args):
|
||||
"""Assert constraints as background axioms for the optimize solver. Alias for assert_expr."""
|
||||
self.assert_exprs(*args)
|
||||
|
||||
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.
|
||||
Soft constraints are grouped by identifiers. Soft constraints that are
|
||||
added without identifiers are grouped by default.
|
||||
"""
|
||||
if _is_int(weight):
|
||||
weight = "%d" % weight
|
||||
if not isinstance(weight, str):
|
||||
raise Z3Exception("weight should be a string or an integer")
|
||||
if id == None:
|
||||
id = ""
|
||||
id = to_symbol(id, self.ctx)
|
||||
v = Z3_optimize_assert_soft(self.ctx.ref(), self.optimize, arg.as_ast(), weight, id)
|
||||
return OptimizeObjective(self, v, False)
|
||||
|
||||
def maximize(self, arg):
|
||||
"""Add objective function to maximize."""
|
||||
return OptimizeObjective(self, Z3_optimize_maximize(self.ctx.ref(), self.optimize, arg.as_ast()), 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)
|
||||
|
||||
def push(self):
|
||||
"""create a backtracking point for added rules, facts and assertions"""
|
||||
Z3_optimize_push(self.ctx.ref(), self.optimize)
|
||||
|
||||
def pop(self):
|
||||
"""restore to previously created backtracking point"""
|
||||
Z3_optimize_pop(self.ctx.ref(), self.optimize)
|
||||
|
||||
def check(self):
|
||||
"""Check satisfiability while optimizing objective functions."""
|
||||
return CheckSatResult(Z3_optimize_check(self.ctx.ref(), self.optimize))
|
||||
|
||||
def reason_unknown(self):
|
||||
"""Return a string that describes why the last `check()` returned `unknown`."""
|
||||
return Z3_optimize_get_reason_unknown(self.ctx.ref(), self.optimize)
|
||||
|
||||
def model(self):
|
||||
"""Return a model for the last check()."""
|
||||
try:
|
||||
return ModelRef(Z3_optimize_get_model(self.ctx.ref(), self.optimize), self.ctx)
|
||||
except Z3Exception:
|
||||
raise Z3Exception("model is not available")
|
||||
|
||||
def lower(self, obj):
|
||||
if not isinstance(obj, OptimizeObjective):
|
||||
raise Z3Exception("Expecting objective handle returned by maximize/minimize")
|
||||
return obj.lower()
|
||||
|
||||
def upper(self, obj):
|
||||
if not isinstance(obj, OptimizeObjective):
|
||||
raise Z3Exception("Expecting objective handle returned by maximize/minimize")
|
||||
return obj.upper()
|
||||
|
||||
def __repr__(self):
|
||||
"""Return a formatted string with all added rules and constraints."""
|
||||
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 Z3_optimize_to_string(self.ctx.ref(), self.optimize)
|
||||
|
||||
def statistics(self):
|
||||
"""Return statistics for the last `query()`.
|
||||
"""
|
||||
return Statistics(Z3_optimize_get_statistics(self.ctx.ref(), self.optimize), self.ctx)
|
||||
|
||||
|
||||
|
||||
|
||||
#########################################
|
||||
#
|
||||
# ApplyResult
|
||||
|
|
@ -8022,23 +8221,24 @@ def FP(name, fpsort, ctx=None):
|
|||
>>> eq(x, x2)
|
||||
True
|
||||
"""
|
||||
ctx = fpsort.ctx
|
||||
if isinstance(fpsort, FPSortRef):
|
||||
ctx = fpsort.ctx
|
||||
else:
|
||||
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.
|
||||
|
||||
>>> x, y, z = BitVecs('x y z', 16)
|
||||
>>> x.size()
|
||||
16
|
||||
>>> x, y, z = FPs('x y z', FPSort(8, 24))
|
||||
>>> x.sort()
|
||||
BitVec(16)
|
||||
>>> Sum(x, y, z)
|
||||
0 + x + y + z
|
||||
>>> Product(x, y, z)
|
||||
1*x*y*z
|
||||
>>> simplify(Product(x, y, z))
|
||||
x*y*z
|
||||
FPSort(8, 24)
|
||||
>>> x.sbits()
|
||||
24
|
||||
>>> x.ebits()
|
||||
8
|
||||
>>> fpMul(RNE(), fpAdd(RNE(), x, y), z)
|
||||
fpMul(RNE(), fpAdd(RNE(), x, y), z)
|
||||
"""
|
||||
ctx = z3._get_ctx(ctx)
|
||||
if isinstance(names, str):
|
||||
|
|
|
|||
|
|
@ -1017,6 +1017,8 @@ class Formatter:
|
|||
return self.pp_seq(a.assertions(), 0, [])
|
||||
elif isinstance(a, z3.Fixedpoint):
|
||||
return a.sexpr()
|
||||
elif isinstance(a, z3.Optimize):
|
||||
return a.sexpr()
|
||||
elif isinstance(a, z3.ApplyResult):
|
||||
return self.pp_seq_seq(a, 0, [])
|
||||
elif isinstance(a, z3.ModelRef):
|
||||
|
|
|
|||
|
|
@ -1,3 +1,10 @@
|
|||
############################################
|
||||
# Copyright (c) 2012 Microsoft Corporation
|
||||
#
|
||||
# Z3 Python interface
|
||||
#
|
||||
# Author: Leonardo de Moura (leonardo)
|
||||
############################################
|
||||
import z3, doctest
|
||||
|
||||
r = doctest.testmod(z3)
|
||||
|
|
|
|||
|
|
@ -1,3 +1,11 @@
|
|||
############################################
|
||||
# Copyright (c) 2012 Microsoft Corporation
|
||||
#
|
||||
# Z3 Python interface
|
||||
#
|
||||
# Author: Leonardo de Moura (leonardo)
|
||||
############################################
|
||||
|
||||
import ctypes, z3core
|
||||
|
||||
class Z3Exception(Exception):
|
||||
|
|
@ -78,6 +86,10 @@ class FixedpointObj(ctypes.c_void_p):
|
|||
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
|
||||
|
||||
class ModelObj(ctypes.c_void_p):
|
||||
def __init__(self, model): self._as_parameter_ = model
|
||||
def from_param(obj): return obj
|
||||
|
|
|
|||
|
|
@ -1,9 +1,22 @@
|
|||
############################################
|
||||
# Copyright (c) 2012 Microsoft Corporation
|
||||
#
|
||||
# Z3 Python interface
|
||||
#
|
||||
# Authors: Leonardo de Moura (leonardo)
|
||||
# ThanhVu (Vu) Nguyen <tnguyen@cs.unm.edu>
|
||||
############################################
|
||||
"""
|
||||
Usage:
|
||||
import common_z3 as CM_Z3
|
||||
"""
|
||||
|
||||
from z3 import *
|
||||
|
||||
def vset(seq, idfun=None, as_list=True):
|
||||
# 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
|
||||
# It preserves the order of arguments while removing duplicates.
|
||||
# (Thanhu's personal code). It has been copied here to avoid a dependency on vu_common.py.
|
||||
"""
|
||||
order preserving
|
||||
|
||||
|
|
@ -485,7 +498,7 @@ def model_str(m,as_str=True):
|
|||
|
||||
if m :
|
||||
vs = [(v,m[v]) for v in m]
|
||||
vs = sorted(vs,key=lambda a: str(a[0]))
|
||||
vs = sorted(vs,key=lambda a,_: str(a))
|
||||
if as_str:
|
||||
return '\n'.join(['{} = {}'.format(k,v) for (k,v) in vs])
|
||||
else:
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue