mirror of
https://github.com/Z3Prover/z3
synced 2025-04-26 18:45:33 +00:00
deprecating interp
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
4f5775c531
commit
a9ca01d8d3
4 changed files with 4 additions and 163 deletions
|
|
@ -28,8 +28,10 @@ Version 4.8.0
|
|||
as lemmas (redundant) and are garbage collected if their glue level is high.
|
||||
|
||||
- Removed features:
|
||||
- interpolation API
|
||||
- duality engine for constrained Horn clauses.
|
||||
- long deprecated API functions have been removed from z3_api.h
|
||||
|
||||
|
||||
|
||||
Version 4.7.1
|
||||
=============
|
||||
|
|
|
|||
|
|
@ -317,14 +317,6 @@ namespace Microsoft.Z3
|
|||
|
||||
#endregion
|
||||
|
||||
#region Interpolation
|
||||
/// <summary>
|
||||
/// Indicates whether the term is marked for interpolation.
|
||||
/// </summary>
|
||||
/// <remarks></remarks>
|
||||
public bool IsInterpolant { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_INTERP; } }
|
||||
#endregion
|
||||
|
||||
#region Arithmetic Terms
|
||||
/// <summary>
|
||||
/// Indicates whether the term is of integer sort.
|
||||
|
|
|
|||
|
|
@ -8269,146 +8269,6 @@ def parse_smt2_file(f, sorts={}, decls={}, ctx=None):
|
|||
except Z3Exception as e:
|
||||
_handle_parse_error(e, 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 neither a proof of unsatisfiability nor a model is obtained
|
||||
(for example, because of a timeout, or because models are disabled)
|
||||
then None is returned.
|
||||
|
||||
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 is 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)
|
||||
if mptr[0]:
|
||||
raise ModelRef(mptr[0], ctx)
|
||||
return None
|
||||
|
||||
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 neither a proof of unsatisfiability nor a model is obtained
|
||||
(for example, because of a timeout, or because models are disabled)
|
||||
then None is returned.
|
||||
|
||||
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)
|
||||
ti = tree_interpolant(f,p,ctx)
|
||||
return ti[0] if ti is not None else None
|
||||
|
||||
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 neither a proof of unsatisfiability nor a model is obtained
|
||||
(for example, because of a timeout, or because models are disabled)
|
||||
then None is returned.
|
||||
|
||||
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)
|
||||
|
||||
|
||||
#########################################
|
||||
#
|
||||
|
|
|
|||
|
|
@ -3,7 +3,7 @@ def_module_params('fixedpoint',
|
|||
export=True,
|
||||
params=(('timeout', UINT, UINT_MAX, 'set timeout'),
|
||||
('engine', SYMBOL, 'auto-config',
|
||||
'Select: auto-config, datalog, duality, pdr, bmc, spacer'),
|
||||
'Select: auto-config, datalog, spacer, pdr, bmc'),
|
||||
('datalog.default_table', SYMBOL, 'sparse',
|
||||
'default table implementation: sparse, hashtable, bitvector, interval'),
|
||||
('datalog.default_relation', SYMBOL, 'pentagon',
|
||||
|
|
@ -56,18 +56,6 @@ def_module_params('fixedpoint',
|
|||
"table columns, if it would have been empty otherwise"),
|
||||
('datalog.subsumption', BOOL, True,
|
||||
"if true, removes/filters predicates with total transitions"),
|
||||
('duality.full_expand', BOOL, False, 'Fully expand derivation trees'),
|
||||
('duality.no_conj', BOOL, False, 'No forced covering (conjectures)'),
|
||||
('duality.feasible_edges', BOOL, True,
|
||||
'Don\'t expand definitely infeasible edges'),
|
||||
('duality.use_underapprox', BOOL, False, 'Use underapproximations'),
|
||||
('duality.stratified_inlining', BOOL, False, 'Use stratified inlining'),
|
||||
('duality.recursion_bound', UINT, UINT_MAX,
|
||||
'Recursion bound for stratified inlining'),
|
||||
('duality.profile', BOOL, False, 'profile run time'),
|
||||
('duality.mbqi', BOOL, True, 'use model-based quantifier instantiation'),
|
||||
('duality.batch_expand', BOOL, False, 'use batch expansion'),
|
||||
('duality.conjecture_file', STRING, '', 'save conjectures to file'),
|
||||
('pdr.bfs_model_search', BOOL, True,
|
||||
"use BFS strategy for expanding model search"),
|
||||
('pdr.farkas', BOOL, True,
|
||||
|
|
@ -161,7 +149,6 @@ def_module_params('fixedpoint',
|
|||
('xform.tail_simplifier_pve', BOOL, True, "propagate_variable_equivalences"),
|
||||
('xform.subsumption_checker', BOOL, True, "Enable subsumption checker (no support for model conversion)"),
|
||||
('xform.coi', BOOL, True, "use cone of influence simplification"),
|
||||
('duality.enable_restarts', BOOL, False, 'DUALITY: enable restarts'),
|
||||
('spacer.order_children', UINT, 0, 'SPACER: order of enqueuing children in non-linear rules : 0 (original), 1 (reverse)'),
|
||||
('spacer.eager_reach_check', BOOL, True, 'SPACER: eagerly check if a query is reachable using reachability facts of predecessors'),
|
||||
('spacer.use_lemma_as_cti', BOOL, False, 'SPACER: use a lemma instead of a CTI in flexible_trace'),
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue