diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt
index a9344aa86..fcd7b0d85 100644
--- a/src/api/dotnet/CMakeLists.txt
+++ b/src/api/dotnet/CMakeLists.txt
@@ -103,6 +103,7 @@ set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE
SeqExpr.cs
SeqSort.cs
SetSort.cs
+ Simplifiers.cs
Solver.cs
Sort.cs
Statistics.cs
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 80b5a95f1..6365852a6 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -3726,6 +3726,110 @@ namespace Microsoft.Z3
}
#endregion
+ #region Simplifiers
+ ///
+ /// The number of supported simplifiers.
+ ///
+ public uint NumSimplifiers
+ {
+ get { return Native.Z3_get_num_simplifiers(nCtx); }
+ }
+
+ ///
+ /// The names of all supported tactics.
+ ///
+ public string[] SimplifierNames
+ {
+ get
+ {
+
+ uint n = NumSimplifiers;
+ string[] res = new string[n];
+ for (uint i = 0; i < n; i++)
+ res[i] = Native.Z3_get_simplifier_name(nCtx, i);
+ return res;
+ }
+ }
+
+ ///
+ /// Returns a string containing a description of the simplifier with the given name.
+ ///
+ public string SimplifierDescription(string name)
+ {
+
+ return Native.Z3_simplifier_get_descr(nCtx, name);
+ }
+
+ ///
+ /// Creates a new Tactic.
+ ///
+ public Simplifier MkSimplifier(string name)
+ {
+
+ return new Simplifier(this, name);
+ }
+
+ ///
+ /// Create a simplifie that applies and
+ /// then .
+ ///
+ public Simplifier AndThen(Simplifier t1, Simplifier t2, params Simplifier[] ts)
+ {
+ Debug.Assert(t1 != null);
+ Debug.Assert(t2 != null);
+ // Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
+
+
+ CheckContextMatch(t1);
+ CheckContextMatch(t2);
+ CheckContextMatch(ts);
+
+ IntPtr last = IntPtr.Zero;
+ if (ts != null && ts.Length > 0)
+ {
+ last = ts[ts.Length - 1].NativeObject;
+ for (int i = ts.Length - 2; i >= 0; i--)
+ last = Native.Z3_simplifier_and_then(nCtx, ts[i].NativeObject, last);
+ }
+ if (last != IntPtr.Zero)
+ {
+ last = Native.Z3_simplifier_and_then(nCtx, t2.NativeObject, last);
+ return new Simplifier(this, Native.Z3_simplifier_and_then(nCtx, t1.NativeObject, last));
+ }
+ else
+ return new Simplifier(this, Native.Z3_simplifier_and_then(nCtx, t1.NativeObject, t2.NativeObject));
+ }
+
+ ///
+ /// Create a simplifier that applies and then
+ /// then .
+ ///
+ ///
+ /// Shorthand for AndThen.
+ ///
+ public Simplifier Then(Simplifier t1, Simplifier t2, params Simplifier[] ts)
+ {
+ Debug.Assert(t1 != null);
+ Debug.Assert(t2 != null);
+ // Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
+
+ return AndThen(t1, t2, ts);
+ }
+
+ ///
+ /// Create a tactic that applies using the given set of parameters .
+ ///
+ public Simplifier UsingParams(Simplifier t, Params p)
+ {
+ Debug.Assert(t != null);
+ Debug.Assert(p != null);
+
+ CheckContextMatch(t);
+ CheckContextMatch(p);
+ return new Simplifier(this, Native.Z3_simplifier_using_params(nCtx, t.NativeObject, p.NativeObject));
+ }
+ #endregion
+
#region Probes
///
/// The number of supported Probes.
@@ -3926,6 +4030,16 @@ namespace Microsoft.Z3
return new Solver(this, Native.Z3_mk_simple_solver(nCtx));
}
+ ///
+ /// Creates a solver that uses an incremental simplifier.
+ ///
+ public Solver MkSolver(Solver s, Simplifier t)
+ {
+ Debug.Assert(t != null);
+ Debug.Assert(s != null);
+ return new Solver(this, Native.Z3_solver_add_simplifier(nCtx, s.NativeObject, t.NativeObject));
+ }
+
///
/// Creates a solver that is implemented using the given tactic.
///
@@ -3939,6 +4053,8 @@ namespace Microsoft.Z3
return new Solver(this, Native.Z3_mk_solver_from_tactic(nCtx, t.NativeObject));
}
+
+
#endregion
#region Fixedpoints
diff --git a/src/api/dotnet/Simplifiers.cs b/src/api/dotnet/Simplifiers.cs
new file mode 100644
index 000000000..28469c1e5
--- /dev/null
+++ b/src/api/dotnet/Simplifiers.cs
@@ -0,0 +1,78 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+ Simplifiers.cs
+
+Abstract:
+
+ Z3 Managed API: Simplifiers
+
+Author:
+
+ Christoph Wintersteiger (cwinter) 2012-03-21
+
+--*/
+
+using System;
+using System.Diagnostics;
+
+namespace Microsoft.Z3
+{
+ ///
+ /// Simplifiers are the basic building block for creating custom solvers with incremental pre-processing.
+ /// The complete list of simplifiers may be obtained using Context.NumSimplifiers
+ /// and Context.SimplifierNames.
+ /// It may also be obtained using the command (help-simplifier) in the SMT 2.0 front-end.
+ ///
+ public class Simplifier : Z3Object
+ {
+ ///
+ /// A string containing a description of parameters accepted by the tactic.
+ ///
+ public string Help
+ {
+ get
+ {
+
+ return Native.Z3_simplifier_get_help(Context.nCtx, NativeObject);
+ }
+ }
+
+ ///
+ /// Retrieves parameter descriptions for Simplifiers.
+ ///
+ public ParamDescrs ParameterDescriptions
+ {
+ get { return new ParamDescrs(Context, Native.Z3_simplifier_get_param_descrs(Context.nCtx, NativeObject)); }
+ }
+
+ #region Internal
+ internal Simplifier(Context ctx, IntPtr obj)
+ : base(ctx, obj)
+ {
+ Debug.Assert(ctx != null);
+ }
+ internal Simplifier(Context ctx, string name)
+ : base(ctx, Native.Z3_mk_simplifier(ctx.nCtx, name))
+ {
+ Debug.Assert(ctx != null);
+ }
+
+ internal override void IncRef(IntPtr o)
+ {
+ Native.Z3_simplifier_inc_ref(Context.nCtx, o);
+ }
+
+ internal override void DecRef(IntPtr o)
+ {
+ lock (Context)
+ {
+ if (Context.nCtx != IntPtr.Zero)
+ Native.Z3_simplifier_dec_ref(Context.nCtx, o);
+ }
+ }
+ #endregion
+ }
+}
diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt
index e0d6bd0a0..4b13a25b1 100644
--- a/src/api/java/CMakeLists.txt
+++ b/src/api/java/CMakeLists.txt
@@ -165,6 +165,8 @@ set(Z3_JAVA_JAR_SOURCE_FILES
SeqExpr.java
SeqSort.java
SetSort.java
+ Simplifier.java
+ SimplifierDecRefQueue.java
SolverDecRefQueue.java
Solver.java
Sort.java
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index d48101235..0f15d9411 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -3081,6 +3081,106 @@ public class Context implements AutoCloseable {
Native.interrupt(nCtx());
}
+ /**
+ * The number of supported simplifiers.
+ **/
+ public int getNumSimplifiers()
+ {
+ return Native.getNumSimplifiers(nCtx());
+ }
+
+ /**
+ * The names of all supported simplifiers.
+ **/
+ public String[] getSimplifierNames()
+ {
+
+ int n = getNumSimplifiers();
+ String[] res = new String[n];
+ for (int i = 0; i < n; i++)
+ res[i] = Native.getSimplifierName(nCtx(), i);
+ return res;
+ }
+
+ /**
+ * Returns a string containing a description of the simplifier with the given
+ * name.
+ **/
+ public String getSimplifierDescription(String name)
+ {
+ return Native.simplifierGetDescr(nCtx(), name);
+ }
+
+ /**
+ * Creates a new Simplifier.
+ **/
+ public Simplifier mkSimplifier(String name)
+ {
+ return new Simplifier(this, name);
+ }
+
+ /**
+ * Create a simplifier that applies {@code t1} and then {@code t1}
+ **/
+ public Simplifier andThen(Simplifier t1, Simplifier t2, Simplifier... ts)
+
+ {
+ checkContextMatch(t1);
+ checkContextMatch(t2);
+ checkContextMatch(ts);
+
+ long last = 0;
+ if (ts != null && ts.length > 0)
+ {
+ last = ts[ts.length - 1].getNativeObject();
+ for (int i = ts.length - 2; i >= 0; i--) {
+ last = Native.simplifierAndThen(nCtx(), ts[i].getNativeObject(),
+ last);
+ }
+ }
+ if (last != 0)
+ {
+ last = Native.simplifierAndThen(nCtx(), t2.getNativeObject(), last);
+ return new Simplifier(this, Native.simplifierAndThen(nCtx(),
+ t1.getNativeObject(), last));
+ } else
+ return new Simplifier(this, Native.simplifierAndThen(nCtx(),
+ t1.getNativeObject(), t2.getNativeObject()));
+ }
+
+ /**
+ * Create a simplifier that applies {@code t1} and then {@code t2}
+ *
+ * Remarks: Shorthand for {@code AndThen}.
+ **/
+ public Simplifier then(Simplifier t1, Simplifier t2, Simplifier... ts)
+ {
+ return andThen(t1, t2, ts);
+ }
+
+ /**
+ * Create a simplifier that applies {@code t} using the given set of
+ * parameters {@code p}.
+ **/
+ public Simplifier usingParams(Simplifier t, Params p)
+ {
+ checkContextMatch(t);
+ checkContextMatch(p);
+ return new Simplifier(this, Native.simplifierUsingParams(nCtx(),
+ t.getNativeObject(), p.getNativeObject()));
+ }
+
+ /**
+ * Create a simplifier that applies {@code t} using the given set of
+ * parameters {@code p}.
+ * Remarks: Alias for
+ * {@code UsingParams}
+ **/
+ public Simplifier with(Simplifier t, Params p)
+ {
+ return usingParams(t, p);
+ }
+
/**
* The number of supported Probes.
**/
@@ -3279,6 +3379,14 @@ public class Context implements AutoCloseable {
t.getNativeObject()));
}
+ /**
+ * Creates a solver that is uses the simplifier pre-processing.
+ **/
+ public Solver mkSolver(Solver s, Simplifier simp)
+ {
+ return new Solver(this, Native.solverAddSimplifier(nCtx(), s.getNativeObject(), simp.getNativeObject()));
+ }
+
/**
* Create a Fixedpoint context.
**/
@@ -4209,6 +4317,7 @@ public class Context implements AutoCloseable {
private SolverDecRefQueue m_Solver_DRQ = new SolverDecRefQueue();
private StatisticsDecRefQueue m_Statistics_DRQ = new StatisticsDecRefQueue();
private TacticDecRefQueue m_Tactic_DRQ = new TacticDecRefQueue();
+ private SimplifierDecRefQueue m_Simplifier_DRQ = new SimplifierDecRefQueue();
private FixedpointDecRefQueue m_Fixedpoint_DRQ = new FixedpointDecRefQueue();
private OptimizeDecRefQueue m_Optimize_DRQ = new OptimizeDecRefQueue();
private ConstructorDecRefQueue m_Constructor_DRQ = new ConstructorDecRefQueue();
@@ -4293,6 +4402,11 @@ public class Context implements AutoCloseable {
return m_Tactic_DRQ;
}
+ public IDecRefQueue getSimplifierDRQ()
+ {
+ return m_Simplifier_DRQ;
+ }
+
public IDecRefQueue getFixedpointDRQ()
{
return m_Fixedpoint_DRQ;
@@ -4323,6 +4437,7 @@ public class Context implements AutoCloseable {
m_Optimize_DRQ.forceClear(this);
m_Statistics_DRQ.forceClear(this);
m_Tactic_DRQ.forceClear(this);
+ m_Simplifier_DRQ.forceClear(this);
m_Fixedpoint_DRQ.forceClear(this);
m_boolSort = null;
diff --git a/src/api/java/Simplifier.java b/src/api/java/Simplifier.java
new file mode 100644
index 000000000..b3fc89ccf
--- /dev/null
+++ b/src/api/java/Simplifier.java
@@ -0,0 +1,58 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+ Simplifiers.cs
+
+Abstract:
+
+ Z3 Managed API: Simplifiers
+
+Author:
+
+ Christoph Wintersteiger (cwinter) 2012-03-21
+
+--*/
+
+package com.microsoft.z3;
+
+
+public class Simplifier extends Z3Object {
+ /*
+ * A string containing a description of parameters accepted by the simplifier.
+ */
+
+ public String getHelp()
+ {
+ return Native.simplifierGetHelp(getContext().nCtx(), getNativeObject());
+ }
+
+ /*
+ * Retrieves parameter descriptions for Simplifiers.
+ */
+ public ParamDescrs getParameterDescriptions() {
+ return new ParamDescrs(getContext(), Native.simplifierGetParamDescrs(getContext().nCtx(), getNativeObject()));
+ }
+
+ Simplifier(Context ctx, long obj)
+ {
+ super(ctx, obj);
+ }
+
+ Simplifier(Context ctx, String name)
+ {
+ super(ctx, Native.mkSimplifier(ctx.nCtx(), name));
+ }
+
+ @Override
+ void incRef()
+ {
+ Native.simplifierIncRef(getContext().nCtx(), getNativeObject());
+ }
+
+ @Override
+ void addToReferenceQueue() {
+ getContext().getSimplifierDRQ().storeReference(getContext(), this);
+ }
+}
\ No newline at end of file
diff --git a/src/api/java/SimplifierDecRefQueue.java b/src/api/java/SimplifierDecRefQueue.java
new file mode 100644
index 000000000..ba15dd5be
--- /dev/null
+++ b/src/api/java/SimplifierDecRefQueue.java
@@ -0,0 +1,31 @@
+/**
+Copyright (c) 2012-2014 Microsoft Corporation
+
+Module Name:
+
+ SimplifierDecRefQueue.java
+
+Abstract:
+
+Author:
+
+ @author Christoph Wintersteiger (cwinter) 2012-03-15
+
+Notes:
+
+**/
+
+package com.microsoft.z3;
+
+class SimplifierDecRefQueue extends IDecRefQueue {
+ public SimplifierDecRefQueue()
+ {
+ super();
+ }
+
+ @Override
+ protected void decRef(Context ctx, long obj)
+ {
+ Native.simplifierDecRef(ctx.nCtx(), obj);
+ }
+}
diff --git a/src/ast/simplifiers/dependent_expr_state.h b/src/ast/simplifiers/dependent_expr_state.h
index d4d449cf8..b4fe4e9d4 100644
--- a/src/ast/simplifiers/dependent_expr_state.h
+++ b/src/ast/simplifiers/dependent_expr_state.h
@@ -90,7 +90,8 @@ public:
* Freeze internal functions
*/
void freeze(expr* term);
- bool frozen(func_decl* f) const { return m_frozen.is_marked(f); }
+ void freeze(expr_ref_vector const& terms) { for (expr* t : terms) freeze(t); }
+ bool frozen(func_decl* f) const { return m_frozen.is_marked(f); }
bool frozen(expr* f) const { return is_app(f) && m_frozen.is_marked(to_app(f)->get_decl()); }
void freeze_suffix();
diff --git a/src/ast/simplifiers/dominator_simplifier.cpp b/src/ast/simplifiers/dominator_simplifier.cpp
index 12f2e2941..2ef4528ab 100644
--- a/src/ast/simplifiers/dominator_simplifier.cpp
+++ b/src/ast/simplifiers/dominator_simplifier.cpp
@@ -41,7 +41,7 @@ expr_ref dominator_simplifier::simplify_ite(app * ite) {
if (is_subexpr(child, t) && !is_subexpr(child, e))
simplify_rec(child);
- pop(scope_level() - old_lvl);
+ local_pop(scope_level() - old_lvl);
expr_ref new_t = simplify_arg(t);
reset_cache();
if (!assert_expr(new_c, true)) {
@@ -50,7 +50,7 @@ expr_ref dominator_simplifier::simplify_ite(app * ite) {
for (expr * child : tree(ite))
if (is_subexpr(child, e) && !is_subexpr(child, t))
simplify_rec(child);
- pop(scope_level() - old_lvl);
+ local_pop(scope_level() - old_lvl);
expr_ref new_e = simplify_arg(e);
if (c == new_c && t == new_t && e == new_e) {
@@ -159,7 +159,7 @@ expr_ref dominator_simplifier::simplify_and_or(bool is_and, app * e) {
r = simplify_arg(arg);
args.push_back(r);
if (!assert_expr(r, !is_and)) {
- pop(scope_level() - old_lvl);
+ local_pop(scope_level() - old_lvl);
r = is_and ? m.mk_false() : m.mk_true();
reset_cache();
return true;
@@ -181,7 +181,7 @@ expr_ref dominator_simplifier::simplify_and_or(bool is_and, app * e) {
args.reverse();
}
- pop(scope_level() - old_lvl);
+ local_pop(scope_level() - old_lvl);
reset_cache();
return { is_and ? mk_and(args) : mk_or(args), m };
}
@@ -191,7 +191,7 @@ expr_ref dominator_simplifier::simplify_not(app * e) {
ENSURE(m.is_not(e, ee));
unsigned old_lvl = scope_level();
expr_ref t = simplify_rec(ee);
- pop(scope_level() - old_lvl);
+ local_pop(scope_level() - old_lvl);
reset_cache();
return mk_not(t);
}
@@ -245,7 +245,7 @@ void dominator_simplifier::reduce() {
}
m_fmls.update(i, dependent_expr(m, r, new_pr, d));
}
- pop(scope_level());
+ local_pop(scope_level());
// go backwards
m_forward = false;
@@ -268,7 +268,7 @@ void dominator_simplifier::reduce() {
}
m_fmls.update(i, dependent_expr(m, r, new_pr, d));
}
- pop(scope_level());
+ local_pop(scope_level());
}
SASSERT(scope_level() == 0);
}
diff --git a/src/ast/simplifiers/dominator_simplifier.h b/src/ast/simplifiers/dominator_simplifier.h
index 562aeace1..b412f6db0 100644
--- a/src/ast/simplifiers/dominator_simplifier.h
+++ b/src/ast/simplifiers/dominator_simplifier.h
@@ -48,7 +48,7 @@ class dominator_simplifier : public dependent_expr_simplifier {
expr* idom(expr *e) const { return m_dominators.idom(e); }
unsigned scope_level() { return m_simplifier->scope_level(); }
- void pop(unsigned n) { SASSERT(n <= m_simplifier->scope_level()); m_simplifier->pop(n); }
+ void local_pop(unsigned n) { SASSERT(n <= m_simplifier->scope_level()); m_simplifier->pop(n); }
bool assert_expr(expr* f, bool sign) { return m_simplifier->assert_expr(f, sign); }
diff --git a/src/ast/substitution/demodulator_rewriter.cpp b/src/ast/substitution/demodulator_rewriter.cpp
index c25647c01..f174b1491 100644
--- a/src/ast/substitution/demodulator_rewriter.cpp
+++ b/src/ast/substitution/demodulator_rewriter.cpp
@@ -780,7 +780,6 @@ void demodulator_rewriter::operator()(expr_ref_vector const& exprs,
demodulator_match_subst::demodulator_match_subst(ast_manager & m):
- m(m),
m_subst(m) {
}
diff --git a/src/ast/substitution/demodulator_rewriter.h b/src/ast/substitution/demodulator_rewriter.h
index 3a1e442d5..8a1e6feb5 100644
--- a/src/ast/substitution/demodulator_rewriter.h
+++ b/src/ast/substitution/demodulator_rewriter.h
@@ -111,7 +111,6 @@ class demodulator_match_subst {
typedef std::pair expr_pair;
typedef obj_pair_hashtable cache;
- ast_manager & m;
substitution m_subst;
cache m_cache;
svector m_todo;
diff --git a/src/math/lp/nla_powers.cpp b/src/math/lp/nla_powers.cpp
index 4054dd7c1..3af31a488 100644
--- a/src/math/lp/nla_powers.cpp
+++ b/src/math/lp/nla_powers.cpp
@@ -131,7 +131,7 @@ namespace nla {
return l_false;
}
- if (xval >= 3 && yval != 0 & rval <= yval + 1) {
+ if (xval >= 3 && yval != 0 && rval <= yval + 1) {
new_lemma lemma(c, "x >= 3, y != 0 => x^y > ln(x)y + 1");
lemma |= ineq(x, llc::LT, rational(3));
lemma |= ineq(y, llc::EQ, rational::zero());
diff --git a/src/muz/spacer/spacer_cluster.cpp b/src/muz/spacer/spacer_cluster.cpp
index b03562b12..fac3a920f 100644
--- a/src/muz/spacer/spacer_cluster.cpp
+++ b/src/muz/spacer/spacer_cluster.cpp
@@ -378,7 +378,7 @@ void lemma_cluster_finder::cluster(lemma_ref &lemma) {
<< pattern << "\n"
<< " and lemma cube: " << lcube << "\n";);
- for (const lemma_ref &l : neighbours) {
+ for (auto l : neighbours) {
SASSERT(cluster->can_contain(l));
bool added = cluster->add_lemma(l, false);
(void)added;
diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index d63ff93cd..2ecc17c45 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -671,7 +671,6 @@ namespace smt {
out << "equivalence classes:\n";
for (enode * n : ctx.enodes()) {
- expr * e = n->get_expr();
expr * r = n->get_root()->get_expr();
out << r->get_id() << " --> " << enode_pp(n, ctx) << "\n";
}
diff --git a/src/solver/simplifier_solver.cpp b/src/solver/simplifier_solver.cpp
index 0c41d4f7e..a717c4932 100644
--- a/src/solver/simplifier_solver.cpp
+++ b/src/solver/simplifier_solver.cpp
@@ -110,10 +110,9 @@ class simplifier_solver : public solver {
expr_ref_vector orig_assumptions(assumptions);
m_core_replace.reset();
if (qhead < m_fmls.size() || !assumptions.empty()) {
- for (expr* a : assumptions)
- m_preprocess_state.freeze(a);
TRACE("solver", tout << "qhead " << qhead << "\n");
- m_preprocess_state.replay(qhead, assumptions);
+ m_preprocess_state.replay(qhead, assumptions);
+ m_preprocess_state.freeze(assumptions);
m_preprocess.reduce();
if (!m.inc())
return;
@@ -225,7 +224,7 @@ public:
}
proof_ref m_proof;
- proof* get_proof_core() {
+ proof* get_proof_core() override {
proof* p = s->get_proof();
m_proof = p;
if (p) {
@@ -272,7 +271,7 @@ public:
std::string reason_unknown() const override { return s->reason_unknown(); }
void set_reason_unknown(char const* msg) override { s->set_reason_unknown(msg); }
void get_labels(svector& r) override { s->get_labels(r); }
- void get_unsat_core(expr_ref_vector& r) { s->get_unsat_core(r); replace(r); }
+ void get_unsat_core(expr_ref_vector& r) override { s->get_unsat_core(r); replace(r); }
ast_manager& get_manager() const override { return s->get_manager(); }
void reset_params(params_ref const& p) override { s->reset_params(p); }
params_ref const& get_params() const override { return s->get_params(); }
@@ -314,7 +313,7 @@ public:
clauses1.push_back(expr_ref_vector(m, c.size(), es.data() + offset));
offset += c.size();
}
- return check_sat_cc(cube1, clauses1);
+ return s->check_sat_cc(cube1, clauses1);
}
lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) override {