diff --git a/RELEASE_NOTES b/RELEASE_NOTES
index a2b526550..7439342de 100644
--- a/RELEASE_NOTES
+++ b/RELEASE_NOTES
@@ -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
=============
diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs
index 9310d1e7d..f09eecbdd 100644
--- a/src/api/dotnet/Expr.cs
+++ b/src/api/dotnet/Expr.cs
@@ -317,14 +317,6 @@ namespace Microsoft.Z3
#endregion
- #region Interpolation
- ///
- /// Indicates whether the term is marked for interpolation.
- ///
- ///
- public bool IsInterpolant { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_INTERP; } }
- #endregion
-
#region Arithmetic Terms
///
/// Indicates whether the term is of integer sort.
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 978141de9..784228120 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -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)
-
#########################################
#
diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg
index 753a45e06..8d6c750d5 100644
--- a/src/muz/base/fixedpoint_params.pyg
+++ b/src/muz/base/fixedpoint_params.pyg
@@ -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'),