diff --git a/RELEASE_NOTES b/RELEASE_NOTES
index 67aa3d810..a2b526550 100644
--- a/RELEASE_NOTES
+++ b/RELEASE_NOTES
@@ -35,7 +35,7 @@ Version 4.7.1
=============
- New requirements:
- - uses stdbool and stdint as part of z3.h
+ - uses stdbool and stdint as part of z3.
- New features:
- none
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index d8a773747..9020c9e4b 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -12,7 +12,6 @@ set(Z3_API_HEADER_FILES_TO_SCAN
z3_rcf.h
z3_fixedpoint.h
z3_optimization.h
- z3_interp.h
z3_fpa.h
z3_spacer.h
)
@@ -63,7 +62,6 @@ add_subdirectory(sat/tactic)
add_subdirectory(tactic/arith)
add_subdirectory(nlsat/tactic)
add_subdirectory(ackermannization)
-add_subdirectory(interp)
add_subdirectory(cmd_context)
add_subdirectory(cmd_context/extra_cmds)
add_subdirectory(parsers/smt2)
@@ -79,7 +77,6 @@ add_subdirectory(tactic/bv)
add_subdirectory(smt/tactic)
add_subdirectory(tactic/sls)
add_subdirectory(qe)
-add_subdirectory(duality)
add_subdirectory(muz/base)
add_subdirectory(muz/dataflow)
add_subdirectory(muz/transforms)
@@ -89,7 +86,6 @@ add_subdirectory(muz/clp)
add_subdirectory(muz/tab)
add_subdirectory(muz/bmc)
add_subdirectory(muz/ddnf)
-add_subdirectory(muz/duality)
add_subdirectory(muz/spacer)
add_subdirectory(muz/fp)
add_subdirectory(tactic/ufbv)
@@ -159,7 +155,6 @@ set (libz3_public_headers
z3_fpa.h
z3.h
c++/z3++.h
- z3_interp.h
z3_macros.h
z3_optimization.h
z3_polynomial.h
diff --git a/src/api/CMakeLists.txt b/src/api/CMakeLists.txt
index fcdbb1651..4a5514a7b 100644
--- a/src/api/CMakeLists.txt
+++ b/src/api/CMakeLists.txt
@@ -48,7 +48,6 @@ z3_add_component(api
api_datatype.cpp
api_fpa.cpp
api_goal.cpp
- api_interp.cpp
api_log.cpp
api_model.cpp
api_numeral.cpp
@@ -67,7 +66,6 @@ z3_add_component(api
z3_replayer.cpp
${full_path_generated_files}
COMPONENT_DEPENDENCIES
- interp
opt
portfolio
realclosure
diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index 1f4a86903..536b94fb2 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -195,7 +195,6 @@ extern "C" {
MK_BINARY(Z3_mk_xor, mk_c(c)->get_basic_fid(), OP_XOR, SKIP);
MK_NARY(Z3_mk_and, mk_c(c)->get_basic_fid(), OP_AND, SKIP);
MK_NARY(Z3_mk_or, mk_c(c)->get_basic_fid(), OP_OR, SKIP);
- MK_UNARY(Z3_mk_interpolant, mk_c(c)->get_basic_fid(), OP_INTERP, SKIP);
Z3_ast mk_ite_core(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3) {
expr * result = mk_c(c)->m().mk_ite(to_expr(t1), to_expr(t2), to_expr(t3));
@@ -900,7 +899,6 @@ extern "C" {
case OP_NOT: return Z3_OP_NOT;
case OP_IMPLIES: return Z3_OP_IMPLIES;
case OP_OEQ: return Z3_OP_OEQ;
- case OP_INTERP: return Z3_OP_INTERP;
case PR_UNDEF: return Z3_OP_PR_UNDEF;
case PR_TRUE: return Z3_OP_PR_TRUE;
diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt
index add1b0ded..76516bf39 100644
--- a/src/api/dotnet/CMakeLists.txt
+++ b/src/api/dotnet/CMakeLists.txt
@@ -80,7 +80,6 @@ set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE
Global.cs
Goal.cs
IDecRefQueue.cs
- InterpolationContext.cs
IntExpr.cs
IntNum.cs
IntSort.cs
diff --git a/src/api/dotnet/InterpolationContext.cs b/src/api/dotnet/InterpolationContext.cs
deleted file mode 100644
index e2b814983..000000000
--- a/src/api/dotnet/InterpolationContext.cs
+++ /dev/null
@@ -1,161 +0,0 @@
-
-/*++
-Copyright (c) 2015 Microsoft Corporation
-
---*/
-
-using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-using System.Diagnostics.Contracts;
-using System.Runtime.InteropServices;
-
-namespace Microsoft.Z3
-{
- ///
- /// The InterpolationContext is suitable for generation of interpolants.
- ///
- /// For more information on interpolation please refer
- /// too the C/C++ API, which is well documented.
- [ContractVerification(true)]
- public class InterpolationContext : Context
- {
-
- ///
- /// Constructor.
- ///
- public InterpolationContext() : base() { }
-
- ///
- /// Constructor.
- ///
- ///
- public InterpolationContext(Dictionary settings) : base(settings) { }
-
- #region Terms
- ///
- /// Create an expression that marks a formula position for interpolation.
- ///
- public BoolExpr MkInterpolant(BoolExpr a)
- {
- Contract.Requires(a != null);
- Contract.Ensures(Contract.Result() != null);
-
- CheckContextMatch(a);
- return new BoolExpr(this, Native.Z3_mk_interpolant(nCtx, a.NativeObject));
- }
- #endregion
-
- ///
- /// Computes an interpolant.
- ///
- /// For more information on interpolation please refer
- /// too the function Z3_get_interpolant in the C/C++ API, which is
- /// well documented.
- public BoolExpr[] GetInterpolant(Expr pf, Expr pat, Params p)
- {
- Contract.Requires(pf != null);
- Contract.Requires(pat != null);
- Contract.Requires(p != null);
- Contract.Ensures(Contract.Result() != null);
-
- CheckContextMatch(pf);
- CheckContextMatch(pat);
- CheckContextMatch(p);
-
- ASTVector seq = new ASTVector(this, Native.Z3_get_interpolant(nCtx, pf.NativeObject, pat.NativeObject, p.NativeObject));
- return seq.ToBoolExprArray();
- }
-
- ///
- /// Computes an interpolant.
- ///
- /// For more information on interpolation please refer
- /// too the function Z3_compute_interpolant in the C/C++ API, which is
- /// well documented.
- public Z3_lbool ComputeInterpolant(Expr pat, Params p, out BoolExpr[] interp, out Model model)
- {
- Contract.Requires(pat != null);
- Contract.Requires(p != null);
- Contract.Ensures(Contract.ValueAtReturn(out interp) != null);
- Contract.Ensures(Contract.ValueAtReturn(out model) != null);
-
- CheckContextMatch(pat);
- CheckContextMatch(p);
-
- IntPtr i = IntPtr.Zero, m = IntPtr.Zero;
- int r = Native.Z3_compute_interpolant(nCtx, pat.NativeObject, p.NativeObject, ref i, ref m);
- interp = new ASTVector(this, i).ToBoolExprArray();
- model = new Model(this, m);
- return (Z3_lbool)r;
- }
-
- ///
- /// Return a string summarizing cumulative time used for interpolation.
- ///
- /// For more information on interpolation please refer
- /// too the function Z3_interpolation_profile in the C/C++ API, which is
- /// well documented.
- public string InterpolationProfile()
- {
- return Native.Z3_interpolation_profile(nCtx);
- }
-
- ///
- /// Checks the correctness of an interpolant.
- ///
- /// For more information on interpolation please refer
- /// too the function Z3_check_interpolant in the C/C++ API, which is
- /// well documented.
- public int CheckInterpolant(Expr[] cnsts, uint[] parents, BoolExpr[] interps, out string error, Expr[] theory)
- {
- Contract.Requires(cnsts.Length == parents.Length);
- Contract.Requires(cnsts.Length == interps.Length + 1);
- IntPtr n_err_str;
- int r = Native.Z3_check_interpolant(nCtx,
- (uint)cnsts.Length,
- Expr.ArrayToNative(cnsts),
- parents,
- Expr.ArrayToNative(interps),
- out n_err_str,
- (uint)theory.Length,
- Expr.ArrayToNative(theory));
- error = Marshal.PtrToStringAnsi(n_err_str);
- return r;
- }
-
- ///
- /// Reads an interpolation problem from a file.
- ///
- /// For more information on interpolation please refer
- /// too the function Z3_read_interpolation_problem in the C/C++ API, which is
- /// well documented.
- public int ReadInterpolationProblem(string filename, out Expr[] cnsts, out uint[] parents, out string error, out Expr[] theory)
- {
- uint num = 0;
- IntPtr n_err_str;
- ASTVector _cnsts = new ASTVector(this);
- ASTVector _theory = new ASTVector(this);
-
- int r = Native.Z3_read_interpolation_problem(nCtx, _cnsts.NativeObject, ref num, out parents, filename, out n_err_str, _theory.NativeObject);
- error = Marshal.PtrToStringAnsi(n_err_str);
- cnsts = _cnsts.ToExprArray();
- parents = new uint[num];
- theory = _theory.ToExprArray();
- return r;
- }
-
- ///
- /// Writes an interpolation problem to a file.
- ///
- /// For more information on interpolation please refer
- /// too the function Z3_write_interpolation_problem in the C/C++ API, which is
- /// well documented.
- public void WriteInterpolationProblem(string filename, Expr[] cnsts, uint[] parents, Expr[] theory)
- {
- Contract.Requires(cnsts.Length == parents.Length);
- Native.Z3_write_interpolation_problem(nCtx, (uint)cnsts.Length, Expr.ArrayToNative(cnsts), parents, filename, (uint)theory.Length, Expr.ArrayToNative(theory));
- }
- }
-}
diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt
index dce2bc4ea..7f0774955 100644
--- a/src/api/java/CMakeLists.txt
+++ b/src/api/java/CMakeLists.txt
@@ -137,7 +137,6 @@ set(Z3_JAVA_JAR_SOURCE_FILES
GoalDecRefQueue.java
Goal.java
IDecRefQueue.java
- InterpolationContext.java
IntExpr.java
IntNum.java
IntSort.java
diff --git a/src/api/java/InterpolationContext.java b/src/api/java/InterpolationContext.java
deleted file mode 100644
index bce789807..000000000
--- a/src/api/java/InterpolationContext.java
+++ /dev/null
@@ -1,210 +0,0 @@
-/**
-Copyright (c) 2012-2014 Microsoft Corporation
-
-Module Name:
-
- InterpolationContext.java
-
-Abstract:
-
-Author:
-
- @author Christoph Wintersteiger (cwinter) 2012-03-15
-
-Notes:
-
-**/
-
-package com.microsoft.z3;
-
-import com.microsoft.z3.enumerations.Z3_lbool;
-
-import java.util.Map;
-
-/**
- * The InterpolationContext is suitable for generation of interpolants.
- *
- * Remarks: For more information on interpolation please refer
- * too the C/C++ API, which is well documented.
- **/
-public class InterpolationContext extends Context
-{
- /**
- * Constructor.
- **/
- public static InterpolationContext mkContext()
- {
- long m_ctx;
- synchronized(creation_lock) {
- m_ctx = Native.mkInterpolationContext(0);
- }
- return new InterpolationContext(m_ctx);
- }
-
- /**
- * Constructor.
- *
- *
- * Remarks:
- * @see Context#Context
- **/
- public static InterpolationContext mkContext(Map settings)
- {
- long m_ctx;
- synchronized(creation_lock) {
- long cfg = Native.mkConfig();
- for (Map.Entry kv : settings.entrySet())
- Native.setParamValue(cfg, kv.getKey(), kv.getValue());
- m_ctx = Native.mkInterpolationContext(cfg);
- Native.delConfig(cfg);
- }
- return new InterpolationContext(m_ctx);
- }
-
- private InterpolationContext(long m_ctx) {
- super(m_ctx);
- }
-
- /**
- * Create an expression that marks a formula position for interpolation.
- * @throws Z3Exception
- **/
- public BoolExpr MkInterpolant(BoolExpr a)
- {
- checkContextMatch(a);
- return new BoolExpr(this, Native.mkInterpolant(nCtx(), a.getNativeObject()));
- }
-
- /**
- * Computes an interpolant.
- * Remarks: For more information on interpolation please refer
- * too the function Z3_get_interpolant in the C/C++ API, which is
- * well documented.
- * @throws Z3Exception
- **/
- public BoolExpr[] GetInterpolant(Expr pf, Expr pat, Params p)
- {
- checkContextMatch(pf);
- checkContextMatch(pat);
- checkContextMatch(p);
-
- ASTVector seq = new ASTVector(this, Native.getInterpolant(nCtx(), pf.getNativeObject(), pat.getNativeObject(), p.getNativeObject()));
- return seq.ToBoolExprArray();
- }
-
- public class ComputeInterpolantResult
- {
- public Z3_lbool status = Z3_lbool.Z3_L_UNDEF;
- public BoolExpr[] interp = null;
- public Model model = null;
- };
-
- /**
- * Computes an interpolant.
- * Remarks: For more information on interpolation please refer
- * too the function Z3_compute_interpolant in the C/C++ API, which is
- * well documented.
- * @throws Z3Exception
- **/
- public ComputeInterpolantResult ComputeInterpolant(Expr pat, Params p)
- {
- checkContextMatch(pat);
- checkContextMatch(p);
-
- ComputeInterpolantResult res = new ComputeInterpolantResult();
- Native.LongPtr n_i = new Native.LongPtr();
- Native.LongPtr n_m = new Native.LongPtr();
- res.status = Z3_lbool.fromInt(Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m));
- if (res.status == Z3_lbool.Z3_L_FALSE)
- res.interp = (new ASTVector(this, n_i.value)).ToBoolExprArray();
- if (res.status == Z3_lbool.Z3_L_TRUE)
- res.model = new Model(this, n_m.value);
- return res;
- }
-
- ///
- /// Return a string summarizing cumulative time used for interpolation.
- ///
- /// Remarks: For more information on interpolation please refer
- /// too the function Z3_interpolation_profile in the C/C++ API, which is
- /// well documented.
- public String InterpolationProfile()
- {
- return Native.interpolationProfile(nCtx());
- }
-
- public class CheckInterpolantResult
- {
- public int return_value = 0;
- public String error = null;
- }
-
- ///
- /// Checks the correctness of an interpolant.
- ///
- /// Remarks: For more information on interpolation please refer
- /// too the function Z3_check_interpolant in the C/C++ API, which is
- /// well documented.
- public CheckInterpolantResult CheckInterpolant(Expr[] cnsts, int[] parents, BoolExpr[] interps, String error, Expr[] theory)
- {
- CheckInterpolantResult res = new CheckInterpolantResult();
- Native.StringPtr n_err_str = new Native.StringPtr();
- res.return_value = Native.checkInterpolant(nCtx(),
- cnsts.length,
- Expr.arrayToNative(cnsts),
- parents,
- Expr.arrayToNative(interps),
- n_err_str,
- theory.length,
- Expr.arrayToNative(theory));
- res.error = n_err_str.value;
- return res;
- }
-
- public class ReadInterpolationProblemResult
- {
- public int return_value = 0;
- public Expr[] cnsts;
- public int[] parents;
- public String error;
- public Expr[] theory;
- };
-
- ///
- /// Reads an interpolation problem from a file.
- ///
- /// Remarks: For more information on interpolation please refer
- /// too the function Z3_read_interpolation_problem in the C/C++ API, which is
- /// well documented.
- public ReadInterpolationProblemResult ReadInterpolationProblem(String filename)
- {
- ReadInterpolationProblemResult res = new ReadInterpolationProblemResult();
- Native.UIntArrayPtr n_parents = new Native.UIntArrayPtr();
- ASTVector _cnsts = new ASTVector(this);
- ASTVector _theory = new ASTVector(this);
- Native.StringPtr n_err_str = new Native.StringPtr();
- Native.IntPtr n_num = new Native.IntPtr();
- res.return_value = Native.readInterpolationProblem(nCtx(), _cnsts.getNativeObject(), n_num,
- n_parents, filename, n_err_str, _theory.getNativeObject());
- res.error = n_err_str.value;
- res.theory = _theory.ToExprArray();
- res.cnsts = _cnsts.ToExprArray();
- int num = n_num.value;
- res.parents = new int[num];
- for (int i = 0; i < num; i++) {
- res.parents[i] = n_parents.value[i];
- }
- return res;
- }
-
- ///
- /// Writes an interpolation problem to a file.
- ///
- /// Remarks: For more information on interpolation please refer
- /// too the function Z3_write_interpolation_problem in the C/C++ API, which is
- /// well documented.
- public void WriteInterpolationProblem(String filename, Expr[] cnsts, int[] parents, String error, Expr[] theory)
- {
- Native.writeInterpolationProblem(nCtx(), cnsts.length, Expr.arrayToNative(cnsts), parents, filename, theory.length, Expr.arrayToNative(theory));
- }
-}
diff --git a/src/api/z3.h b/src/api/z3.h
index 37ea68f84..382bc4b07 100644
--- a/src/api/z3.h
+++ b/src/api/z3.h
@@ -32,7 +32,6 @@ Notes:
#include "z3_rcf.h"
#include "z3_fixedpoint.h"
#include "z3_optimization.h"
-#include "z3_interp.h"
#include "z3_fpa.h"
#include "z3_spacer.h"
#endif
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index d5c279d63..3e47833b4 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -212,8 +212,6 @@ typedef enum
- Z3_OP_OEQ Binary equivalence modulo namings. This binary predicate is used in proof terms.
It captures equisatisfiability and equivalence modulo renamings.
- - Z3_OP_INTERP Marks a sub-formula for interpolation.
-
- Z3_OP_ANUM Arithmetic numeral.
- Z3_OP_AGNUM Arithmetic algebraic numeral. Algebraic numbers are used to represent irrational numbers in Z3.
@@ -991,7 +989,6 @@ typedef enum {
Z3_OP_NOT,
Z3_OP_IMPLIES,
Z3_OP_OEQ,
- Z3_OP_INTERP,
// Arithmetic
Z3_OP_ANUM = 0x200,
diff --git a/src/api/z3_interp.h b/src/api/z3_interp.h
deleted file mode 100644
index 765870bd5..000000000
--- a/src/api/z3_interp.h
+++ /dev/null
@@ -1,283 +0,0 @@
-/*++
-Copyright (c) 2014 Microsoft Corporation
-
-Module Name:
-
- z3_interp.h
-
-Abstract:
-
- API for interpolation
-
-Author:
-
- Kenneth McMillan (kenmcmil)
-
-Notes:
-
---*/
-#ifndef Z3_INTERPOLATION_H_
-#define Z3_INTERPOLATION_H_
-
-#ifdef __cplusplus
-extern "C" {
-#endif // __cplusplus
-
- /** \defgroup capi C API */
- /*@{*/
-
- /** @name Interpolation facilities */
- /*@{*/
- /**
- \brief Create an AST node marking a formula position for interpolation.
-
- The node \c a must have Boolean sort.
-
- def_API('Z3_mk_interpolant', AST, (_in(CONTEXT), _in(AST)))
- */
- Z3_ast Z3_API Z3_mk_interpolant(Z3_context c, Z3_ast a);
-
-
- /** \brief This function generates a Z3 context suitable for generation of
- interpolants. Formulas can be generated as abstract syntax trees in
- this context using the Z3 C API.
-
- Interpolants are also generated as AST's in this context.
-
- If cfg is non-null, it will be used as the base configuration
- for the Z3 context. This makes it possible to set Z3 options
- to be used during interpolation. This feature should be used
- with some caution however, as it may be that certain Z3 options
- are incompatible with interpolation.
-
- def_API('Z3_mk_interpolation_context', CONTEXT, (_in(CONFIG),))
-
- */
-
- Z3_context Z3_API Z3_mk_interpolation_context(Z3_config cfg);
-
- /** Compute an interpolant from a refutation. This takes a proof of
- "false" from a set of formulas C, and an interpolation
- pattern. The pattern pat is a formula combining the formulas in C
- using logical conjunction and the "interp" operator (see
- #Z3_mk_interpolant). 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. The
- 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.
-
- In particular, calling Z3_get_interpolant on a pattern of the
- form (interp ... (interp (and (interp A_1) A_2)) ... A_N) will
- result in a sequence interpolant for A_1, A_2,... A_N.
-
- Neglecting interp markers, the pattern must be a conjunction of
- formulas in C, the set of premises of the proof. Otherwise an
- error is flagged.
-
- Any premises of the proof not present in the pattern are
- treated as "background theory". Predicate and function symbols
- occurring in the background theory are treated as interpreted and
- thus always allowed in the interpolant.
-
- Interpolant may not necessarily be computable from all
- proofs. To be sure an interpolant can be computed, the proof
- must be generated by an SMT solver for which interpolation is
- supported, and the premises must be expressed using only
- theories and operators for which interpolation is supported.
-
- Currently, the only SMT solver that is supported is the legacy
- SMT solver. Such a solver is available as the default solver in
- \c Z3_context objects produced by #Z3_mk_interpolation_context.
- Currently, the theories supported are equality with
- uninterpreted functions, linear integer arithmetic, and the
- theory of arrays (in SMT-LIB terms, this is AUFLIA).
- Quantifiers are allowed. Use of any other operators (including
- "labels") may result in failure to compute an interpolant from a
- proof.
-
- Parameters:
-
- \param c logical context.
- \param pf a refutation from premises (assertions) C
- \param pat an interpolation pattern over C
- \param p parameters
-
- def_API('Z3_get_interpolant', AST_VECTOR, (_in(CONTEXT), _in(AST), _in(AST), _in(PARAMS)))
- */
-
- Z3_ast_vector Z3_API Z3_get_interpolant(Z3_context c, Z3_ast pf, Z3_ast pat, Z3_params p);
-
- /* Compute an interpolant for an unsatisfiable conjunction of formulas.
-
- This takes as an argument an interpolation pattern as in
- #Z3_get_interpolant. This is a conjunction, some subformulas of
- which are marked with the "interp" operator (see #Z3_mk_interpolant).
-
- The conjunction is first checked for unsatisfiability. The result
- of this check is returned in the out parameter "status". If the result
- is unsat, an interpolant is computed from the refutation as in #Z3_get_interpolant
- and returned as a vector of formulas. Otherwise the return value is
- an empty formula.
-
- See #Z3_get_interpolant for a discussion of supported theories.
-
- The advantage of this function over #Z3_get_interpolant is that
- it is not necessary to create a suitable SMT solver and generate
- a proof. The disadvantage is that it is not possible to use the
- solver incrementally.
-
- Parameters:
-
- \param c logical context.
- \param pat an interpolation pattern
- \param p parameters for solver creation
- \param status returns the status of the sat check
- \param model returns model if satisfiable
-
- Return value: status of SAT check
-
- def_API('Z3_compute_interpolant', INT, (_in(CONTEXT), _in(AST), _in(PARAMS), _out(AST_VECTOR), _out(MODEL)))
- */
-
- Z3_lbool Z3_API Z3_compute_interpolant(Z3_context c,
- Z3_ast pat,
- Z3_params p,
- Z3_ast_vector *interp,
- Z3_model *model);
-
- /** Return a string summarizing cumulative time used for
- interpolation. This string is purely for entertainment purposes
- and has no semantics.
-
- \param ctx The context (currently ignored)
-
-
- def_API('Z3_interpolation_profile', STRING, (_in(CONTEXT),))
- */
-
- Z3_string Z3_API Z3_interpolation_profile(Z3_context ctx);
-
- /**
- \brief Read an interpolation problem from file.
-
- \param ctx The Z3 context. This resets the error handler of ctx.
- \param filename The file name to read.
- \param num Returns length of sequence.
- \param cnsts Returns sequence of formulas (do not free)
- \param parents Returns the parents vector (or NULL for sequence)
- \param error Returns an error message in case of failure (do not free the string)
- \param num_theory Number of theory terms
- \param theory Theory terms
-
- Returns true on success.
-
- File formats: Currently two formats are supported, based on
- SMT-LIB2. For sequence interpolants, the sequence of constraints is
- represented by the sequence of "assert" commands in the file.
-
- For tree interpolants, one symbol of type bool is associated to
- each vertex of the tree. For each vertex v there is an "assert"
- of the form:
-
- (implies (and c1 ... cn f) v)
-
- where c1 .. cn are the children of v (which must precede v in the file)
- and f is the formula associated to node v. The last formula in the
- file is the root vertex, and is represented by the predicate "false".
-
- A solution to a tree interpolation problem can be thought of as a
- valuation of the vertices that makes all the implications true
- where each value is represented using the common symbols between
- the formulas in the subtree and the remainder of the formulas.
-
- def_API('Z3_read_interpolation_problem', INT, (_in(CONTEXT), _in(AST_VECTOR), _out(UINT), _out_managed_array(2, UINT), _in(STRING), _out(STRING), _in(AST_VECTOR)))
-
- */
-
- int Z3_API Z3_read_interpolation_problem(Z3_context ctx,
- Z3_ast_vector cnsts,
- unsigned* num,
- unsigned* parents[],
- Z3_string filename,
- Z3_string_ptr error,
- Z3_ast_vector theory);
-
-
-
- /** Check the correctness of an interpolant. The Z3 context must
- have no constraints asserted when this call is made. That means
- that after interpolating, you must first fully pop the Z3
- context before calling this. See Z3_interpolate for meaning of parameters.
-
- \param ctx The Z3 context. Must be generated by Z3_mk_interpolation_context
- \param num The number of constraints in the sequence
- \param cnsts Array of constraints (AST's in context ctx)
- \param parents The parents vector (or NULL for sequence)
- \param interps The interpolant to check
- \param error Returns an error message if interpolant incorrect (do not free the string)
- \param num_theory Number of theory terms
- \param theory Theory terms
-
- Return value is Z3_L_TRUE if interpolant is verified, Z3_L_FALSE if
- incorrect, and Z3_L_UNDEF if unknown.
-
- def_API('Z3_check_interpolant', INT, (_in(CONTEXT), _in(UINT), _in_array(1, AST), _in_array(1, UINT), _in_array(1, AST), _out(STRING), _in(UINT), _in_array(6, AST)))
- */
-
- int Z3_API Z3_check_interpolant(Z3_context ctx,
- unsigned num,
- Z3_ast cnsts[],
- unsigned parents[],
- Z3_ast *interps,
- Z3_string_ptr error,
- unsigned num_theory,
- Z3_ast theory[]);
-
- /** Write an interpolation problem to file suitable for reading with
- Z3_read_interpolation_problem. The output file is a sequence
- of SMT-LIB2 format commands, suitable for reading with command-line Z3
- or other interpolating solvers.
-
- \param ctx The Z3 context. Must be generated by z3_mk_interpolation_context
- \param num The number of constraints in the sequence
- \param cnsts Array of constraints
- \param parents The parents vector (or NULL for sequence)
- \param filename The file name to write
- \param num_theory Number of theory terms
- \param theory Theory terms
-
- def_API('Z3_write_interpolation_problem', VOID, (_in(CONTEXT), _in(UINT), _in_array(1, AST), _in_array(1, UINT), _in(STRING), _in(UINT), _in_array(5, AST)))
- */
-
- void Z3_API Z3_write_interpolation_problem(Z3_context ctx,
- unsigned num,
- Z3_ast cnsts[],
- unsigned parents[],
- Z3_string filename,
- unsigned num_theory,
- Z3_ast theory[]);
- /*@}*/
- /*@}*/
-
-#ifdef __cplusplus
-}
-#endif // __cplusplus
-
-#endif
diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index a07be0b22..cae1618c0 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -646,7 +646,6 @@ basic_decl_plugin::basic_decl_plugin():
m_iff_decl(nullptr),
m_xor_decl(nullptr),
m_not_decl(nullptr),
- m_interp_decl(nullptr),
m_implies_decl(nullptr),
m_proof_sort(nullptr),
@@ -865,7 +864,6 @@ void basic_decl_plugin::set_manager(ast_manager * m, family_id id) {
m_iff_decl = mk_bool_op_decl("iff", OP_IFF, 2, false, true, false, false, true);
m_xor_decl = mk_bool_op_decl("xor", OP_XOR, 2, true, true);
m_not_decl = mk_bool_op_decl("not", OP_NOT, 1);
- m_interp_decl = mk_bool_op_decl("interp", OP_INTERP, 1);
m_implies_decl = mk_implies_decl();
m_proof_sort = m->mk_sort(symbol("Proof"), sort_info(id, PROOF_SORT));
@@ -890,7 +888,6 @@ void basic_decl_plugin::get_op_names(svector & op_names, symbol co
op_names.push_back(builtin_name("or", OP_OR));
op_names.push_back(builtin_name("xor", OP_XOR));
op_names.push_back(builtin_name("not", OP_NOT));
- op_names.push_back(builtin_name("interp", OP_INTERP));
op_names.push_back(builtin_name("=>", OP_IMPLIES));
if (logic == symbol::null) {
// user friendly aliases
@@ -902,7 +899,6 @@ void basic_decl_plugin::get_op_names(svector & op_names, symbol co
op_names.push_back(builtin_name("||", OP_OR));
op_names.push_back(builtin_name("equals", OP_EQ));
op_names.push_back(builtin_name("equiv", OP_IFF));
- op_names.push_back(builtin_name("@@", OP_INTERP));
}
}
@@ -923,7 +919,6 @@ void basic_decl_plugin::finalize() {
DEC_REF(m_and_decl);
DEC_REF(m_or_decl);
DEC_REF(m_not_decl);
- DEC_REF(m_interp_decl);
DEC_REF(m_iff_decl);
DEC_REF(m_xor_decl);
DEC_REF(m_implies_decl);
@@ -1056,7 +1051,6 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
case OP_AND: return m_and_decl;
case OP_OR: return m_or_decl;
case OP_NOT: return m_not_decl;
- case OP_INTERP: return m_interp_decl;
case OP_IFF: return m_iff_decl;
case OP_IMPLIES: return m_implies_decl;
case OP_XOR: return m_xor_decl;
@@ -1099,7 +1093,6 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
case OP_AND: return m_and_decl;
case OP_OR: return m_or_decl;
case OP_NOT: return m_not_decl;
- case OP_INTERP: return m_interp_decl;
case OP_IFF: return m_iff_decl;
case OP_IMPLIES: return m_implies_decl;
case OP_XOR: return m_xor_decl;
diff --git a/src/ast/ast.h b/src/ast/ast.h
index 2db0fde04..e85f164e1 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -1041,7 +1041,7 @@ enum basic_sort_kind {
};
enum basic_op_kind {
- OP_TRUE, OP_FALSE, OP_EQ, OP_DISTINCT, OP_ITE, OP_AND, OP_OR, OP_IFF, OP_XOR, OP_NOT, OP_IMPLIES, OP_OEQ, OP_INTERP, LAST_BASIC_OP,
+ OP_TRUE, OP_FALSE, OP_EQ, OP_DISTINCT, OP_ITE, OP_AND, OP_OR, OP_IFF, OP_XOR, OP_NOT, OP_IMPLIES, OP_OEQ, LAST_BASIC_OP,
PR_UNDEF, PR_TRUE, PR_ASSERTED, PR_GOAL, PR_MODUS_PONENS, PR_REFLEXIVITY, PR_SYMMETRY, PR_TRANSITIVITY, PR_TRANSITIVITY_STAR, PR_MONOTONICITY, PR_QUANT_INTRO,
PR_DISTRIBUTIVITY, PR_AND_ELIM, PR_NOT_OR_ELIM, PR_REWRITE, PR_REWRITE_STAR, PR_PULL_QUANT,
@@ -1063,7 +1063,6 @@ protected:
func_decl * m_iff_decl;
func_decl * m_xor_decl;
func_decl * m_not_decl;
- func_decl * m_interp_decl;
func_decl * m_implies_decl;
ptr_vector m_eq_decls; // cached eqs
ptr_vector m_ite_decls; // cached ites
@@ -2054,7 +2053,6 @@ public:
app * mk_true() const { return m_true; }
app * mk_false() const { return m_false; }
app * mk_bool_val(bool b) { return b?m_true:m_false; }
- app * mk_interp(expr * arg) { return mk_app(m_basic_family_id, OP_INTERP, arg); }
func_decl* mk_and_decl() {
diff --git a/src/cmd_context/CMakeLists.txt b/src/cmd_context/CMakeLists.txt
index f7b888343..8da871f9a 100644
--- a/src/cmd_context/CMakeLists.txt
+++ b/src/cmd_context/CMakeLists.txt
@@ -8,14 +8,12 @@ z3_add_component(cmd_context
context_params.cpp
echo_tactic.cpp
eval_cmd.cpp
- interpolant_cmds.cpp
parametric_cmd.cpp
pdecl.cpp
simplify_cmd.cpp
tactic_cmds.cpp
tactic_manager.cpp
COMPONENT_DEPENDENCIES
- interp
rewriter
solver
EXTRA_REGISTER_MODULE_HEADERS
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index e42f884d6..7d2b2f17a 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -46,7 +46,6 @@ Notes:
#include "tactic/generic_model_converter.h"
#include "solver/smt_logics.h"
#include "cmd_context/basic_cmds.h"
-#include "cmd_context/interpolant_cmds.h"
#include "cmd_context/cmd_context.h"
func_decls::func_decls(ast_manager & m, func_decl * f):
@@ -484,7 +483,6 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l):
install_basic_cmds(*this);
install_ext_basic_cmds(*this);
install_core_tactic_cmds(*this);
- install_interpolant_cmds(*this);
SASSERT(m != 0 || !has_manager());
if (m_main_ctx) {
set_verbose_stream(diagnostic_stream());
diff --git a/src/cmd_context/interpolant_cmds.cpp b/src/cmd_context/interpolant_cmds.cpp
deleted file mode 100644
index dd1d0acec..000000000
--- a/src/cmd_context/interpolant_cmds.cpp
+++ /dev/null
@@ -1,263 +0,0 @@
-/*++
- Copyright (c) 2013 Microsoft Corporation
-
- Module Name:
-
- interpolant_cmds.cpp
-
- Abstract:
- Commands for interpolation.
-
- Author:
-
- Leonardo (leonardo) 2011-12-23
-
- Notes:
-
- --*/
-#include
-#include "cmd_context/cmd_context.h"
-#include "cmd_context/cmd_util.h"
-#include "util/scoped_timer.h"
-#include "util/scoped_ctrl_c.h"
-#include "util/cancel_eh.h"
-#include "ast/ast_pp.h"
-#include "ast/ast_smt_pp.h"
-#include "ast/ast_smt2_pp.h"
-#include "cmd_context/parametric_cmd.h"
-#include "util/mpq.h"
-#include "ast/expr2var.h"
-#include "ast/pp.h"
-#include "interp/iz3interp.h"
-#include "interp/iz3checker.h"
-#include "interp/iz3profiling.h"
-#include "interp/interp_params.hpp"
-#include "ast/scoped_proof.h"
-
-static void show_interpolant_and_maybe_check(cmd_context & ctx,
- ptr_vector &cnsts,
- expr *t,
- ptr_vector &interps,
- params_ref &m_params,
- bool check)
-{
-
- if (m_params.get_bool("som", false))
- m_params.set_bool("flat", true);
- th_rewriter s(ctx.m(), m_params);
-
- ctx.regular_stream() << "(interpolants";
- for(unsigned i = 0; i < interps.size(); i++){
- expr_ref r(ctx.m());
- proof_ref pr(ctx.m());
- s(to_expr(interps[i]),r,pr);
- ctx.regular_stream() << "\n " << r;
- }
- ctx.regular_stream() << ")\n";
-
- s.cleanup();
-
- // verify, for the paranoid...
- if(check || interp_params(m_params).check()){
- std::ostringstream err;
- ast_manager &_m = ctx.m();
-
- // need a solver -- make one here FIXME is this right?
- bool proofs_enabled, models_enabled, unsat_core_enabled;
- params_ref p;
- ctx.params().get_solver_params(_m, p, proofs_enabled, models_enabled, unsat_core_enabled);
- scoped_ptr sp = (ctx.get_solver_factory())(_m, p, false, true, false, ctx.get_logic());
-
- if(iz3check(_m,sp.get(),err,cnsts,t,interps))
- ctx.regular_stream() << "correct\n";
- else
- ctx.regular_stream() << "incorrect: " << err.str().c_str() << "\n";
- }
-
- for(unsigned i = 0; i < interps.size(); i++){
- ctx.m().dec_ref(interps[i]);
- }
-
- interp_params itp_params(m_params);
- if(itp_params.profile())
- profiling::print(ctx.regular_stream());
-
-}
-
-static void check_can_interpolate(cmd_context & ctx){
- if (!ctx.produce_interpolants())
- throw cmd_exception("interpolation is not enabled, use command (set-option :produce-interpolants true)");
-}
-
-
-static void get_interpolant_and_maybe_check(cmd_context & ctx, expr * t, params_ref &m_params, bool check) {
-
- check_can_interpolate(ctx);
-
- // get the proof, if there is one
-
- if (!ctx.has_manager() ||
- ctx.cs_state() != cmd_context::css_unsat)
- throw cmd_exception("proof is not available");
- expr_ref pr(ctx.m());
- pr = ctx.get_check_sat_result()->get_proof();
- if (pr == 0)
- throw cmd_exception("proof is not available");
-
- // get the assertions from the context
-
- ptr_vector::const_iterator it = ctx.begin_assertions();
- ptr_vector::const_iterator end = ctx.end_assertions();
- ptr_vector cnsts((unsigned)(end - it));
- for (int i = 0; it != end; ++it, ++i)
- cnsts[i] = *it;
-
- // compute an interpolant
-
- ptr_vector interps;
-
- try {
- iz3interpolate(ctx.m(),pr.get(),cnsts,t,interps,nullptr);
- }
- catch (iz3_bad_tree &) {
- throw cmd_exception("interpolation pattern contains non-asserted formula");
- }
- catch (iz3_incompleteness &) {
- throw cmd_exception("incompleteness in interpolator");
- }
-
- show_interpolant_and_maybe_check(ctx, cnsts, t, interps, m_params, check);
-}
-
-static void get_interpolant(cmd_context & ctx, expr * t, params_ref &m_params) {
- get_interpolant_and_maybe_check(ctx,t,m_params,false);
-}
-
-#if 0
-static void get_and_check_interpolant(cmd_context & ctx, params_ref &m_params, expr * t) {
- get_interpolant_and_maybe_check(ctx,t,m_params,true);
-}
-#endif
-
-static void compute_interpolant_and_maybe_check(cmd_context & ctx, expr * t, params_ref &m_params, bool check){
-
- // create a fresh solver suitable for interpolation
- bool proofs_enabled, models_enabled, unsat_core_enabled;
- params_ref p;
- ast_manager &_m = ctx.m();
- // TODO: the following is a HACK to enable proofs in the old smt solver
- // When we stop using that solver, this hack can be removed
- scoped_proof_mode spm(_m,PGM_ENABLED);
- ctx.params().get_solver_params(_m, p, proofs_enabled, models_enabled, unsat_core_enabled);
- p.set_bool("proof", true);
- scoped_ptr sp = (ctx.get_interpolating_solver_factory())(_m, p, true, models_enabled, false, ctx.get_logic());
-
- ptr_vector cnsts;
- ptr_vector interps;
- model_ref m;
-
- // compute an interpolant
-
- lbool res;
- try {
- res = iz3interpolate(_m, *sp.get(), t, cnsts, interps, m, nullptr);
- }
- catch (iz3_incompleteness &) {
- throw cmd_exception("incompleteness in interpolator");
- }
-
- switch(res){
- case l_false:
- ctx.regular_stream() << "unsat\n";
- show_interpolant_and_maybe_check(ctx, cnsts, t, interps, m_params, check);
- break;
-
- case l_true:
- ctx.regular_stream() << "sat\n";
- // TODO: how to return the model to the context, if it exists?
- break;
-
- case l_undef:
- ctx.regular_stream() << "unknown\n";
- // TODO: how to return the model to the context, if it exists?
- break;
- }
-
- for(unsigned i = 0; i < cnsts.size(); i++)
- ctx.m().dec_ref(cnsts[i]);
-
-}
-
-static expr *make_tree(cmd_context & ctx, const ptr_vector &exprs){
- if(exprs.size() == 0)
- throw cmd_exception("not enough arguments");
- expr *foo = exprs[0];
- for(unsigned i = 1; i < exprs.size(); i++){
- foo = ctx.m().mk_and(ctx.m().mk_interp(foo),exprs[i]);
- }
- return foo;
-}
-
-static void get_interpolant(cmd_context & ctx, const ptr_vector &exprs, params_ref &m_params) {
- expr_ref foo(make_tree(ctx, exprs),ctx.m());
- get_interpolant(ctx,foo.get(),m_params);
-}
-
-static void compute_interpolant(cmd_context & ctx, const ptr_vector &exprs, params_ref &m_params) {
- expr_ref foo(make_tree(ctx, exprs),ctx.m());
- compute_interpolant_and_maybe_check(ctx,foo.get(),m_params,false);
-}
-
-
-// UNARY_CMD(get_interpolant_cmd, "get-interpolant", "", "get interpolant for marked positions in fmla", CPK_EXPR, expr *, get_interpolant(ctx, arg););
-
-// UNARY_CMD(get_and_check_interpolant_cmd, "get-and-check-interpolant", "", "get and check interpolant for marked positions in fmla", CPK_EXPR, expr *, get_and_check_interpolant(ctx, arg););
-
-class get_interpolant_cmd : public parametric_cmd {
-protected:
- ptr_vector m_targets;
-public:
- get_interpolant_cmd(char const * name = "get-interpolant"):parametric_cmd(name) {}
-
- char const * get_usage() const override { return "+"; }
-
- char const * get_main_descr() const override {
- return "get interpolant for formulas";
- }
-
- void init_pdescrs(cmd_context & ctx, param_descrs & p) override {
- }
-
- void prepare(cmd_context & ctx) override {
- parametric_cmd::prepare(ctx);
- m_targets.resize(0);
- }
-
- cmd_arg_kind next_arg_kind(cmd_context & ctx) const override {
- return CPK_EXPR;
- }
-
- void set_next_arg(cmd_context & ctx, expr * arg) override {
- m_targets.push_back(arg);
- }
-
- void execute(cmd_context & ctx) override {
- get_interpolant(ctx,m_targets,m_params);
- }
-};
-
-class compute_interpolant_cmd : public get_interpolant_cmd {
-public:
- compute_interpolant_cmd(char const * name = "compute-interpolant"):get_interpolant_cmd(name) {}
-
- void execute(cmd_context & ctx) override {
- compute_interpolant(ctx,m_targets,m_params);
- }
-
-};
-
-void install_interpolant_cmds(cmd_context & ctx) {
- ctx.insert(alloc(get_interpolant_cmd));
- ctx.insert(alloc(compute_interpolant_cmd));
- // ctx.insert(alloc(get_and_check_interpolant_cmd));
-}
diff --git a/src/cmd_context/interpolant_cmds.h b/src/cmd_context/interpolant_cmds.h
deleted file mode 100644
index daef70926..000000000
--- a/src/cmd_context/interpolant_cmds.h
+++ /dev/null
@@ -1,24 +0,0 @@
-/*++
- Copyright (c) 2011 Microsoft Corporation
-
- Module Name:
-
- interpolant_cmds.h
-
- Abstract:
- Commands for interpolation.
-
- Author:
-
- Leonardo (leonardo) 2011-12-23
-
- Notes:
-
- --*/
-#ifndef INTERPOLANT_CMDS_H_
-#define INTERPOLANT_CMDS_H_
-
-class cmd_context;
-void install_interpolant_cmds(cmd_context & ctx);
-
-#endif
diff --git a/src/duality/CMakeLists.txt b/src/duality/CMakeLists.txt
deleted file mode 100644
index eb2d5c4f2..000000000
--- a/src/duality/CMakeLists.txt
+++ /dev/null
@@ -1,11 +0,0 @@
-z3_add_component(duality
- SOURCES
- duality_profiling.cpp
- duality_rpfp.cpp
- duality_solver.cpp
- duality_wrapper.cpp
- COMPONENT_DEPENDENCIES
- interp
- qe
- smt
-)
diff --git a/src/duality/duality.h b/src/duality/duality.h
deleted file mode 100644
index 9bf323d8b..000000000
--- a/src/duality/duality.h
+++ /dev/null
@@ -1,1365 +0,0 @@
-/*++
- Copyright (c) 2012 Microsoft Corporation
-
- Module Name:
-
- duality.h
-
- Abstract:
-
- main header for duality
-
- Author:
-
- Ken McMillan (kenmcmil)
-
- Revision History:
-
-
- --*/
-
-#pragma once
-
-#include "duality/duality_wrapper.h"
-#include
-#include
-#include