From 2e068e3f563a04a0ddf085b55fd249ccb226b92d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Feb 2023 17:41:00 -0800 Subject: [PATCH 1/7] add simplifiers to .net API --- src/api/dotnet/CMakeLists.txt | 1 + src/api/dotnet/Context.cs | 116 +++++++++++++++++++++ src/api/dotnet/Simplifiers.cs | 78 ++++++++++++++ src/ast/simplifiers/dependent_expr_state.h | 3 +- src/solver/simplifier_solver.cpp | 5 +- 5 files changed, 199 insertions(+), 4 deletions(-) create mode 100644 src/api/dotnet/Simplifiers.cs 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..a7fbe185f --- /dev/null +++ b/src/api/dotnet/Simplifiers.cs @@ -0,0 +1,78 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + Tactic.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/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/solver/simplifier_solver.cpp b/src/solver/simplifier_solver.cpp index 0c41d4f7e..3ac84ea36 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; From 4143c542571948368a6a36334a21392ed50ddb3f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Feb 2023 19:06:26 -0800 Subject: [PATCH 2/7] add simplifier to java API --- src/api/dotnet/Simplifiers.cs | 2 +- src/api/java/CMakeLists.txt | 2 + src/api/java/Context.java | 115 ++++++++++++++++++++++++ src/api/java/Simplifier.java | 58 ++++++++++++ src/api/java/SimplifierDecRefQueue.java | 31 +++++++ 5 files changed, 207 insertions(+), 1 deletion(-) create mode 100644 src/api/java/Simplifier.java create mode 100644 src/api/java/SimplifierDecRefQueue.java diff --git a/src/api/dotnet/Simplifiers.cs b/src/api/dotnet/Simplifiers.cs index a7fbe185f..28469c1e5 100644 --- a/src/api/dotnet/Simplifiers.cs +++ b/src/api/dotnet/Simplifiers.cs @@ -3,7 +3,7 @@ Copyright (c) 2012 Microsoft Corporation Module Name: - Tactic.cs + Simplifiers.cs Abstract: 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); + } +} From ed4a84e5d3637d3a0e4088dd1613055a7972cf07 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Feb 2023 19:21:34 -0800 Subject: [PATCH 3/7] compiler warning Signed-off-by: Nikolaj Bjorner --- src/muz/spacer/spacer_cluster.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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; From efbecb19b162a767afe3ee62291018a757413791 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Feb 2023 19:23:30 -0800 Subject: [PATCH 4/7] compiler warning Signed-off-by: Nikolaj Bjorner --- src/smt/theory_fpa.cpp | 1 - 1 file changed, 1 deletion(-) 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"; } From 741634b7032a9c449c19d571f8e8622e0df61176 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Feb 2023 19:26:51 -0800 Subject: [PATCH 5/7] compiler warning fix Signed-off-by: Nikolaj Bjorner --- src/math/lp/nla_powers.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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()); From 0d05104d8c68eaa15ce2659eb8b7c1f3de277af0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Feb 2023 19:33:23 -0800 Subject: [PATCH 6/7] remove unused field Signed-off-by: Nikolaj Bjorner --- src/ast/simplifiers/dominator_simplifier.cpp | 14 +++++++------- src/ast/simplifiers/dominator_simplifier.h | 2 +- src/ast/substitution/demodulator_rewriter.cpp | 1 - src/ast/substitution/demodulator_rewriter.h | 1 - 4 files changed, 8 insertions(+), 10 deletions(-) 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; From 39d28189235aba92da2f50a36ad864e7cf7fd66e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Feb 2023 19:36:22 -0800 Subject: [PATCH 7/7] compiler warnings/bugs Signed-off-by: Nikolaj Bjorner --- src/solver/simplifier_solver.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/solver/simplifier_solver.cpp b/src/solver/simplifier_solver.cpp index 3ac84ea36..a717c4932 100644 --- a/src/solver/simplifier_solver.cpp +++ b/src/solver/simplifier_solver.cpp @@ -224,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) { @@ -271,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(); } @@ -313,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 {