diff --git a/scripts/mk_nuget_task.py b/scripts/mk_nuget_task.py
index dd81349df..e22057a0f 100644
--- a/scripts/mk_nuget_task.py
+++ b/scripts/mk_nuget_task.py
@@ -25,9 +25,11 @@ os_info = { 'ubuntu-latest' : ('so', 'linux-x64'),
'ubuntu-18' : ('so', 'linux-x64'),
'ubuntu-20' : ('so', 'linux-x64'),
'glibc-2.31' : ('so', 'linux-x64'),
+ 'glibc' : ('so', 'linux-x64'),
'x64-win' : ('dll', 'win-x64'),
'x86-win' : ('dll', 'win-x86'),
- 'osx' : ('dylib', 'osx-x64'),
+ 'x64-osx' : ('dylib', 'osx-x64'),
+ 'arm64-osx' : ('dylib', 'osx-arm64'),
'debian' : ('so', 'linux-x64') }
diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index 0a3b35aed..ca39329bb 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -233,16 +233,38 @@ extern "C" {
Z3_CATCH_RETURN(nullptr);
}
+ /**
+ * attach a simplifier to solver.
+ * This is legal when the solver is fresh, does not already have assertions (and scopes).
+ * To allow recycling the argument solver, we create a fresh copy of it and pass it to
+ * mk_simplifier_solver.
+ */
Z3_solver Z3_API Z3_solver_add_simplifier(Z3_context c, Z3_solver solver, Z3_simplifier simplifier) {
Z3_TRY;
LOG_Z3_solver_add_simplifier(c, solver, simplifier);
- init_solver(c, solver);
+ solver_ref s_fresh;
+ if (to_solver(solver)->m_solver) {
+ s_fresh = to_solver_ref(solver)->translate(mk_c(c)->m(), to_solver(solver)->m_params);
+ }
+ else {
+ // create the solver, but hijack it for internal uses.
+ init_solver(c, solver);
+ s_fresh = to_solver(solver)->m_solver;
+ to_solver(solver)->m_solver = nullptr;
+ }
+ if (!s_fresh) {
+ SET_ERROR_CODE(Z3_INVALID_ARG, "unexpected empty solver state");
+ RETURN_Z3(nullptr);
+ }
+ if (s_fresh->get_num_assertions() > 0) {
+ SET_ERROR_CODE(Z3_INVALID_ARG, "adding a simplifier to a solver with assertions is not allowed.");
+ RETURN_Z3(nullptr);
+ }
auto simp = to_simplifier_ref(simplifier);
- auto* slv = mk_simplifier_solver(to_solver_ref(solver), simp);
- Z3_solver_ref* sr = alloc(Z3_solver_ref, *mk_c(c), slv);
- mk_c(c)->save_object(sr);
- // ?? init_solver_log(c, sr)
- RETURN_Z3(of_solver(sr));
+ auto* simplifier_solver = mk_simplifier_solver(s_fresh.get(), simp);
+ Z3_solver_ref* result = alloc(Z3_solver_ref, *mk_c(c), simplifier_solver);
+ mk_c(c)->save_object(result);
+ RETURN_Z3(of_solver(result));
Z3_CATCH_RETURN(nullptr);
}
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/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 0f7ef8999..92bb2aa24 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -8214,8 +8214,6 @@ class Simplifier:
def add(self, solver):
"""Return a solver that applies the simplification pre-processing specified by the simplifier"""
- print(solver.solver)
- print(self.simplifier)
return Solver(Z3_solver_add_simplifier(self.ctx.ref(), solver.solver, self.simplifier), self.ctx)
def help(self):
@@ -9074,7 +9072,7 @@ def PbGe(args, k):
def PbEq(args, k, ctx=None):
- """Create a Pseudo-Boolean inequality k constraint.
+ """Create a Pseudo-Boolean equality k constraint.
>>> a, b, c = Bools('a b c')
>>> f = PbEq(((a,1),(b,3),(c,2)), 3)
diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h
index e2d480664..66544bec7 100644
--- a/src/ast/recfun_decl_plugin.h
+++ b/src/ast/recfun_decl_plugin.h
@@ -60,7 +60,7 @@ namespace recfun {
func_decl_ref m_pred; //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/simplifiers/eliminate_predicates.cpp b/src/ast/simplifiers/eliminate_predicates.cpp
index 2166913da..6c1eccea0 100644
--- a/src/ast/simplifiers/eliminate_predicates.cpp
+++ b/src/ast/simplifiers/eliminate_predicates.cpp
@@ -567,9 +567,9 @@ void eliminate_predicates::try_find_macro(clause& cl) {
return false;
app* x = to_app(_x);
return
- can_be_quasi_macro_head(x, cl.m_bound.size()) &&
- is_macro_safe(y) &&
- !occurs(x->get_decl(), y);
+ can_be_quasi_macro_head(x, cl.m_bound.size()) &&
+ is_macro_safe(y) &&
+ !occurs(x->get_decl(), y);
};
if (cl.is_unit() && m.is_eq(cl.atom(0), x, y)) {
@@ -592,7 +592,8 @@ void eliminate_predicates::try_find_macro(clause& cl) {
}
if (cl.is_unit()) {
expr* body = cl.sign(0) ? m.mk_false() : m.mk_true();
- if (can_be_qdef(cl.atom(0), body)) {
+ expr* x = cl.atom(0);
+ if (can_be_qdef(x, body)) {
insert_quasi_macro(to_app(x), body, cl);
return;
}
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/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp
index 4559586f3..a0805110b 100644
--- a/src/cmd_context/tactic_cmds.cpp
+++ b/src/cmd_context/tactic_cmds.cpp
@@ -296,9 +296,10 @@ public:
}
void execute(cmd_context & ctx) override {
- if (!m_tactic) {
+ if (!m_tactic)
throw cmd_exception("apply needs a tactic argument");
- }
+ if (ctx.ignore_check())
+ return;
params_ref p = ctx.params().merge_default_params(ps());
tactic_ref tref = using_params(sexpr2tactic(ctx, m_tactic), p);
{
diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp
index dc362c7e3..291af3b5c 100644
--- a/src/math/dd/dd_pdd.cpp
+++ b/src/math/dd/dd_pdd.cpp
@@ -190,7 +190,7 @@ namespace dd {
while (p2 != 0 && !m_todo.empty()) {
PDD r = m_todo.back();
m_todo.pop_back();
- if (is_marked(r))
+ if (is_marked(r))
continue;
set_mark(r);
if (!is_val(r)) {
@@ -203,7 +203,7 @@ namespace dd {
p2 = val(r).trailing_zeros();
}
m_todo.reset();
- return p2;
+ return p2;
}
pdd pdd_manager::subst_val(pdd const& p, pdd const& s) {
@@ -1816,9 +1816,8 @@ namespace dd {
pdd p = *this;
while (!p.is_val())
p = p.lo();
- return p.val();
+ return p.val();
}
-
pdd pdd::shl(unsigned n) const {
return (*this) * rational::power_of_two(n);
diff --git a/src/math/lp/lar_core_solver.h b/src/math/lp/lar_core_solver.h
index 0043ed23d..bcd33966f 100644
--- a/src/math/lp/lar_core_solver.h
+++ b/src/math/lp/lar_core_solver.h
@@ -222,7 +222,7 @@ public:
m_d_x.resize(m_d_A.column_count());
pop_basis(k);
m_stacked_simplex_strategy.pop(k);
- settings().simplex_strategy() = m_stacked_simplex_strategy;
+ settings().set_simplex_strategy(m_stacked_simplex_strategy);
lp_assert(m_r_solver.basis_heading_is_correct());
lp_assert(!need_to_presolve_with_double_solver() || m_d_solver.basis_heading_is_correct());
}
diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index f78dab119..46ed0b5a9 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -300,7 +300,7 @@ namespace lp {
m_term_register.shrink(m_term_count);
m_terms.resize(m_term_count);
m_simplex_strategy.pop(k);
- m_settings.simplex_strategy() = m_simplex_strategy;
+ m_settings.set_simplex_strategy(m_simplex_strategy);
lp_assert(sizes_are_correct());
lp_assert((!m_settings.use_tableau()) || m_mpq_lar_core_solver.m_r_solver.reduced_costs_are_correct_tableau());
m_usage_in_terms.pop(k);
@@ -465,10 +465,10 @@ namespace lp {
switch (settings().simplex_strategy()) {
case simplex_strategy_enum::tableau_rows:
- settings().simplex_strategy() = simplex_strategy_enum::tableau_costs;
+ settings().set_simplex_strategy(simplex_strategy_enum::tableau_costs);
prepare_costs_for_r_solver(term);
ret = maximize_term_on_tableau(term, term_max);
- settings().simplex_strategy() = simplex_strategy_enum::tableau_rows;
+ settings().set_simplex_strategy(simplex_strategy_enum::tableau_rows);
set_costs_to_zero(term);
m_mpq_lar_core_solver.m_r_solver.set_status(lp_status::OPTIMAL);
return ret;
@@ -2006,10 +2006,10 @@ namespace lp {
void lar_solver::decide_on_strategy_and_adjust_initial_state() {
lp_assert(strategy_is_undecided());
if (m_columns_to_ul_pairs.size() > m_settings.column_number_threshold_for_using_lu_in_lar_solver) {
- m_settings.simplex_strategy() = simplex_strategy_enum::lu;
+ m_settings.set_simplex_strategy(simplex_strategy_enum::lu);
}
else {
- m_settings.simplex_strategy() = simplex_strategy_enum::tableau_rows; // todo: when to switch to tableau_costs?
+ m_settings.set_simplex_strategy(simplex_strategy_enum::tableau_rows); // todo: when to switch to tableau_costs?
}
adjust_initial_state();
}
diff --git a/src/math/lp/lp_core_solver_base.h b/src/math/lp/lp_core_solver_base.h
index 673ef2404..5cde4485d 100644
--- a/src/math/lp/lp_core_solver_base.h
+++ b/src/math/lp/lp_core_solver_base.h
@@ -74,9 +74,9 @@ public:
vector & m_x; // a feasible solution, the fist time set in the constructor
vector & m_costs;
lp_settings & m_settings;
+ lu> * m_factorization = nullptr;
vector m_y; // the buffer for yB = cb
// a device that is able to solve Bx=c, xB=d, and change the basis
- lu> * m_factorization;
const column_namer & m_column_names;
indexed_vector m_w; // the vector featuring in 24.3 of the Chvatal book
vector m_d; // the vector of reduced costs
diff --git a/src/math/lp/lp_core_solver_base_def.h b/src/math/lp/lp_core_solver_base_def.h
index c1b64492b..f85de1111 100644
--- a/src/math/lp/lp_core_solver_base_def.h
+++ b/src/math/lp/lp_core_solver_base_def.h
@@ -55,7 +55,6 @@ lp_core_solver_base(static_matrix & A,
m_costs(costs),
m_settings(settings),
m_y(m_m()),
- m_factorization(nullptr),
m_column_names(column_names),
m_w(m_m()),
m_d(m_n()),
diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h
index aa06cb263..2245f6f4e 100644
--- a/src/math/lp/lp_settings.h
+++ b/src/math/lp/lp_settings.h
@@ -336,8 +336,8 @@ public:
return m_simplex_strategy;
}
- simplex_strategy_enum & simplex_strategy() {
- return m_simplex_strategy;
+ void set_simplex_strategy(simplex_strategy_enum s) {
+ m_simplex_strategy = s;
}
bool use_lu() const {
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/qe/qe.cpp b/src/qe/qe.cpp
index f4ebce594..12365b204 100644
--- a/src/qe/qe.cpp
+++ b/src/qe/qe.cpp
@@ -1513,10 +1513,11 @@ namespace qe {
propagate_assignment(*model_eval);
VERIFY(CHOOSE_VAR == update_current(*model_eval, true));
SASSERT(m_current->fml());
- if (l_true != m_solver.check()) {
- return l_true;
- }
+ if (l_true != m_solver.check())
+ return l_true;
m_solver.get_model(model);
+ if (!model)
+ return l_undef;
model_eval = alloc(model_evaluator, *model);
search_tree* st = m_current;
update_current(*model_eval, false);
diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index eb2d0071d..0a9e803a9 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -65,6 +65,8 @@ namespace sat {
m_phase = PS_RANDOM;
else if (s == symbol("frozen"))
m_phase = PS_FROZEN;
+ else if (s == symbol("local_search"))
+ m_phase = PS_LOCAL_SEARCH;
else
throw sat_param_exception("invalid phase selection strategy: always_false, always_true, basic_caching, caching, random");
diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h
index 8adfc13ed..f8c0775b1 100644
--- a/src/sat/sat_config.h
+++ b/src/sat/sat_config.h
@@ -28,6 +28,7 @@ namespace sat {
PS_ALWAYS_FALSE,
PS_BASIC_CACHING,
PS_SAT_CACHING,
+ PS_LOCAL_SEARCH,
PS_FROZEN,
PS_RANDOM
};
diff --git a/src/sat/sat_ddfw.cpp b/src/sat/sat_ddfw.cpp
index ecfc13aa6..f1493232c 100644
--- a/src/sat/sat_ddfw.cpp
+++ b/src/sat/sat_ddfw.cpp
@@ -49,6 +49,7 @@ namespace sat {
else if (should_parallel_sync()) do_parallel_sync();
else shift_weights();
}
+ log();
return m_min_sz == 0 ? l_true : l_undef;
}
@@ -66,9 +67,9 @@ namespace sat {
<< std::setw(10) << kflips_per_sec
<< std::setw(10) << m_flips
<< std::setw(10) << m_restart_count
- << std::setw(10) << m_reinit_count
- << std::setw(10) << m_unsat_vars.size()
- << std::setw(10) << m_shifts;
+ << std::setw(11) << m_reinit_count
+ << std::setw(13) << m_unsat_vars.size()
+ << std::setw(9) << m_shifts;
if (m_par) verbose_stream() << std::setw(10) << m_parsync_count;
verbose_stream() << ")\n");
m_stopwatch.start();
@@ -90,18 +91,18 @@ namespace sat {
unsigned n = 1;
bool_var v0 = null_bool_var;
for (bool_var v : m_unsat_vars) {
- int r = reward(v);
- if (r > 0) {
+ double r = reward(v);
+ if (r > 0.0) {
sum_pos += score(r);
}
- else if (r == 0 && sum_pos == 0 && (m_rand() % (n++)) == 0) {
+ else if (r == 0.0 && sum_pos == 0 && (m_rand() % (n++)) == 0) {
v0 = v;
}
}
if (sum_pos > 0) {
double lim_pos = ((double) m_rand() / (1.0 + m_rand.max_value())) * sum_pos;
for (bool_var v : m_unsat_vars) {
- int r = reward(v);
+ double r = reward(v);
if (r > 0) {
lim_pos -= score(r);
if (lim_pos <= 0) {
@@ -121,7 +122,7 @@ namespace sat {
* TBD: map reward value to a score, possibly through an exponential function, such as
* exp(-tau/r), where tau > 0
*/
- double ddfw::mk_score(unsigned r) {
+ double ddfw::mk_score(double r) {
return r;
}
@@ -201,7 +202,7 @@ namespace sat {
m_shifts = 0;
m_stopwatch.start();
}
-
+
void ddfw::reinit(solver& s) {
add(s);
add_assumptions();
@@ -235,7 +236,7 @@ namespace sat {
for (unsigned cls_idx : use_list(*this, lit)) {
clause_info& ci = m_clauses[cls_idx];
ci.del(lit);
- unsigned w = ci.m_weight;
+ double w = ci.m_weight;
// cls becomes false: flip any variable in clause to receive reward w
switch (ci.m_num_trues) {
case 0: {
@@ -257,7 +258,7 @@ namespace sat {
}
for (unsigned cls_idx : use_list(*this, nlit)) {
clause_info& ci = m_clauses[cls_idx];
- unsigned w = ci.m_weight;
+ double w = ci.m_weight;
// the clause used to have a single true (pivot) literal, now it has two.
// Then the previous pivot is no longer penalized for flipping.
switch (ci.m_num_trues) {
@@ -406,9 +407,8 @@ namespace sat {
void ddfw::save_best_values() {
if (m_unsat.empty()) {
m_model.reserve(num_vars());
- for (unsigned i = 0; i < num_vars(); ++i) {
+ for (unsigned i = 0; i < num_vars(); ++i)
m_model[i] = to_lbool(value(i));
- }
}
if (m_unsat.size() < m_min_sz) {
m_models.reset();
@@ -422,13 +422,11 @@ namespace sat {
}
unsigned h = value_hash();
if (!m_models.contains(h)) {
- for (unsigned v = 0; v < num_vars(); ++v) {
+ for (unsigned v = 0; v < num_vars(); ++v)
bias(v) += value(v) ? 1 : -1;
- }
m_models.insert(h);
- if (m_models.size() > m_config.m_max_num_models) {
+ if (m_models.size() > m_config.m_max_num_models)
m_models.erase(*m_models.begin());
- }
}
m_min_sz = m_unsat.size();
}
@@ -450,10 +448,9 @@ namespace sat {
3. select multiple clauses instead of just one per clause in unsat.
*/
- bool ddfw::select_clause(unsigned max_weight, unsigned max_trues, clause_info const& cn, unsigned& n) {
- if (cn.m_num_trues == 0 || cn.m_weight < max_weight) {
+ bool ddfw::select_clause(double max_weight, clause_info const& cn, unsigned& n) {
+ if (cn.m_num_trues == 0 || cn.m_weight + 1e-5 < max_weight)
return false;
- }
if (cn.m_weight > max_weight) {
n = 2;
return true;
@@ -462,51 +459,72 @@ namespace sat {
}
unsigned ddfw::select_max_same_sign(unsigned cf_idx) {
- clause const& c = get_clause(cf_idx);
- unsigned max_weight = 2;
- unsigned max_trues = 0;
+ auto& ci = m_clauses[cf_idx];
unsigned cl = UINT_MAX; // clause pointer to same sign, max weight satisfied clause.
+ clause const& c = *ci.m_clause;
+ double max_weight = m_init_weight;
unsigned n = 1;
for (literal lit : c) {
for (unsigned cn_idx : use_list(*this, lit)) {
auto& cn = m_clauses[cn_idx];
- if (select_clause(max_weight, max_trues, cn, n)) {
+ if (select_clause(max_weight, cn, n)) {
cl = cn_idx;
max_weight = cn.m_weight;
- max_trues = cn.m_num_trues;
}
}
}
return cl;
}
+ void ddfw::transfer_weight(unsigned from, unsigned to, double w) {
+ auto& cf = m_clauses[to];
+ auto& cn = m_clauses[from];
+ if (cn.m_weight < w)
+ return;
+ cf.m_weight += w;
+ cn.m_weight -= w;
+
+ for (literal lit : get_clause(to))
+ inc_reward(lit, w);
+ if (cn.m_num_trues == 1)
+ inc_reward(to_literal(cn.m_trues), w);
+ }
+
+ unsigned ddfw::select_random_true_clause() {
+ unsigned num_clauses = m_clauses.size();
+ unsigned rounds = 100 * num_clauses;
+ for (unsigned i = 0; i < rounds; ++i) {
+ unsigned idx = (m_rand() * m_rand()) % num_clauses;
+ auto & cn = m_clauses[idx];
+ if (cn.is_true() && cn.m_weight >= m_init_weight)
+ return idx;
+ }
+ return UINT_MAX;
+ }
+
+ // 1% chance to disregard neighbor
+ inline bool ddfw::disregard_neighbor() {
+ return false; // rand() % 1000 == 0;
+ }
+
+ double ddfw::calculate_transfer_weight(double w) {
+ return (w > m_init_weight) ? m_init_weight : 1;
+ }
+
void ddfw::shift_weights() {
++m_shifts;
- for (unsigned cf_idx : m_unsat) {
- auto& cf = m_clauses[cf_idx];
+ for (unsigned to_idx : m_unsat) {
+ auto& cf = m_clauses[to_idx];
SASSERT(!cf.is_true());
- unsigned cn_idx = select_max_same_sign(cf_idx);
- while (cn_idx == UINT_MAX) {
- unsigned idx = (m_rand() * m_rand()) % m_clauses.size();
- auto & cn = m_clauses[idx];
- if (cn.is_true() && cn.m_weight >= 2) {
- cn_idx = idx;
- }
- }
- auto & cn = m_clauses[cn_idx];
+ unsigned from_idx = select_max_same_sign(to_idx);
+ if (from_idx == UINT_MAX || disregard_neighbor())
+ from_idx = select_random_true_clause();
+ if (from_idx == UINT_MAX)
+ continue;
+ auto & cn = m_clauses[from_idx];
SASSERT(cn.is_true());
- unsigned wn = cn.m_weight;
- SASSERT(wn >= 2);
- unsigned inc = (wn > 2) ? 2 : 1;
- SASSERT(wn - inc >= 1);
- cf.m_weight += inc;
- cn.m_weight -= inc;
- for (literal lit : get_clause(cf_idx)) {
- inc_reward(lit, inc);
- }
- if (cn.m_num_trues == 1) {
- inc_reward(to_literal(cn.m_trues), inc);
- }
+ double w = calculate_transfer_weight(cn.m_weight);
+ transfer_weight(from_idx, to_idx, w);
}
// DEBUG_CODE(invariant(););
}
@@ -543,7 +561,7 @@ namespace sat {
VERIFY(found);
}
for (unsigned v = 0; v < num_vars(); ++v) {
- int v_reward = 0;
+ double v_reward = 0;
literal lit(v, !value(v));
for (unsigned j : m_use_list[lit.index()]) {
clause_info const& ci = m_clauses[j];
@@ -559,7 +577,7 @@ namespace sat {
}
}
IF_VERBOSE(0, if (v_reward != reward(v)) verbose_stream() << v << " " << v_reward << " " << reward(v) << "\n");
- SASSERT(reward(v) == v_reward);
+ // SASSERT(reward(v) == v_reward);
}
DEBUG_CODE(
for (auto const& ci : m_clauses) {
diff --git a/src/sat/sat_ddfw.h b/src/sat/sat_ddfw.h
index 1cad87363..ed9936f0a 100644
--- a/src/sat/sat_ddfw.h
+++ b/src/sat/sat_ddfw.h
@@ -34,10 +34,10 @@ namespace sat {
class ddfw : public i_local_search {
struct clause_info {
- clause_info(clause* cl, unsigned init_weight): m_weight(init_weight), m_trues(0), m_num_trues(0), m_clause(cl) {}
- unsigned m_weight; // weight of clause
- unsigned m_trues; // set of literals that are true
- unsigned m_num_trues; // size of true set
+ clause_info(clause* cl, double init_weight): m_weight(init_weight), m_clause(cl) {}
+ double m_weight; // weight of clause
+ unsigned m_trues = 0; // set of literals that are true
+ unsigned m_num_trues = 0; // size of true set
clause* m_clause;
bool is_true() const { return m_num_trues > 0; }
void add(literal lit) { ++m_num_trues; m_trues += lit.index(); }
@@ -65,23 +65,24 @@ namespace sat {
};
struct var_info {
- var_info(): m_value(false), m_reward(0), m_make_count(0), m_bias(0), m_reward_avg(1e-5) {}
- bool m_value;
- int m_reward;
- unsigned m_make_count;
- int m_bias;
- ema m_reward_avg;
+ var_info() {}
+ bool m_value = false;
+ double m_reward = 0;
+ unsigned m_make_count = 0;
+ int m_bias = 0;
+ ema m_reward_avg = 1e-5;
};
- config m_config;
- reslimit m_limit;
- clause_allocator m_alloc;
+ config m_config;
+ reslimit m_limit;
+ clause_allocator m_alloc;
svector m_clauses;
literal_vector m_assumptions;
svector m_vars; // var -> info
svector m_probs; // var -> probability of flipping
svector m_scores; // reward -> score
model m_model; // var -> best assignment
+ unsigned m_init_weight = 2;
vector m_use_list;
unsigned_vector m_flat_use_list;
@@ -90,11 +91,11 @@ namespace sat {
indexed_uint_set m_unsat;
indexed_uint_set m_unsat_vars; // set of variables that are in unsat clauses
random_gen m_rand;
- unsigned m_num_non_binary_clauses{ 0 };
- unsigned m_restart_count{ 0 }, m_reinit_count{ 0 }, m_parsync_count{ 0 };
- uint64_t m_restart_next{ 0 }, m_reinit_next{ 0 }, m_parsync_next{ 0 };
- uint64_t m_flips{ 0 }, m_last_flips{ 0 }, m_shifts{ 0 };
- unsigned m_min_sz{ 0 };
+ unsigned m_num_non_binary_clauses = 0;
+ unsigned m_restart_count = 0, m_reinit_count = 0, m_parsync_count = 0;
+ uint64_t m_restart_next = 0, m_reinit_next = 0, m_parsync_next = 0;
+ uint64_t m_flips = 0, m_last_flips = 0, m_shifts = 0;
+ unsigned m_min_sz = 0;
hashtable> m_models;
stopwatch m_stopwatch;
@@ -112,9 +113,9 @@ namespace sat {
void flatten_use_list();
- double mk_score(unsigned r);
+ double mk_score(double r);
- inline double score(unsigned r) { return r; } // TBD: { for (unsigned sz = m_scores.size(); sz <= r; ++sz) m_scores.push_back(mk_score(sz)); return m_scores[r]; }
+ inline double score(double r) { return r; } // TBD: { for (unsigned sz = m_scores.size(); sz <= r; ++sz) m_scores.push_back(mk_score(sz)); return m_scores[r]; }
inline unsigned num_vars() const { return m_vars.size(); }
@@ -124,9 +125,9 @@ namespace sat {
inline bool value(bool_var v) const { return m_vars[v].m_value; }
- inline int& reward(bool_var v) { return m_vars[v].m_reward; }
+ inline double& reward(bool_var v) { return m_vars[v].m_reward; }
- inline int reward(bool_var v) const { return m_vars[v].m_reward; }
+ inline double reward(bool_var v) const { return m_vars[v].m_reward; }
inline int& bias(bool_var v) { return m_vars[v].m_bias; }
@@ -136,7 +137,7 @@ namespace sat {
inline clause const& get_clause(unsigned idx) const { return *m_clauses[idx].m_clause; }
- inline unsigned get_weight(unsigned idx) const { return m_clauses[idx].m_weight; }
+ inline double get_weight(unsigned idx) const { return m_clauses[idx].m_weight; }
inline bool is_true(unsigned idx) const { return m_clauses[idx].is_true(); }
@@ -154,9 +155,9 @@ namespace sat {
if (--make_count(v) == 0) m_unsat_vars.remove(v);
}
- inline void inc_reward(literal lit, int inc) { reward(lit.var()) += inc; }
+ inline void inc_reward(literal lit, double w) { reward(lit.var()) += w; }
- inline void dec_reward(literal lit, int inc) { reward(lit.var()) -= inc; }
+ inline void dec_reward(literal lit, double w) { reward(lit.var()) -= w; }
// flip activity
bool do_flip();
@@ -166,17 +167,20 @@ namespace sat {
// shift activity
void shift_weights();
+ inline double calculate_transfer_weight(double w);
// reinitialize weights activity
bool should_reinit_weights();
void do_reinit_weights();
- inline bool select_clause(unsigned max_weight, unsigned max_trues, clause_info const& cn, unsigned& n);
+ inline bool select_clause(double max_weight, clause_info const& cn, unsigned& n);
// restart activity
bool should_restart();
void do_restart();
void reinit_values();
+ unsigned select_random_true_clause();
+
// parallel integration
bool should_parallel_sync();
void do_parallel_sync();
@@ -193,6 +197,10 @@ namespace sat {
void add_assumptions();
+ inline void transfer_weight(unsigned from, unsigned to, double w);
+
+ inline bool disregard_neighbor();
+
public:
ddfw(): m_par(nullptr) {}
@@ -210,6 +218,8 @@ namespace sat {
void set_seed(unsigned n) override { m_rand.set_seed(n); }
void add(solver const& s) override;
+
+ bool get_value(bool_var v) const override { return value(v); }
std::ostream& display(std::ostream& out) const;
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index bf4c85987..f9edbe928 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1331,17 +1331,37 @@ namespace sat {
ERROR_EX
};
+ struct solver::scoped_ls {
+ solver& s;
+ scoped_ls(solver& s): s(s) {}
+ ~scoped_ls() {
+ dealloc(s.m_local_search);
+ s.m_local_search = nullptr;
+ }
+ };
+
+ void solver::bounded_local_search() {
+ literal_vector _lits;
+ scoped_limits scoped_rl(rlimit());
+ m_local_search = alloc(ddfw);
+ scoped_ls _ls(*this);
+ SASSERT(m_local_search);
+ m_local_search->add(*this);
+ m_local_search->updt_params(m_params);
+ m_local_search->set_seed(m_rand());
+ scoped_rl.push_child(&(m_local_search->rlimit()));
+ m_local_search->rlimit().push(500000);
+ m_local_search->reinit(*this);
+ m_local_search->check(_lits.size(), _lits.data(), nullptr);
+ for (unsigned i = 0; i < m_phase.size(); ++i)
+ m_best_phase[i] = m_local_search->get_value(i);
+ }
+
+
lbool solver::invoke_local_search(unsigned num_lits, literal const* lits) {
literal_vector _lits(num_lits, lits);
- for (literal lit : m_user_scope_literals) _lits.push_back(~lit);
- struct scoped_ls {
- solver& s;
- scoped_ls(solver& s): s(s) {}
- ~scoped_ls() {
- dealloc(s.m_local_search);
- s.m_local_search = nullptr;
- }
- };
+ for (literal lit : m_user_scope_literals)
+ _lits.push_back(~lit);
scoped_ls _ls(*this);
if (inconsistent())
return l_false;
@@ -1611,27 +1631,28 @@ namespace sat {
bool solver::guess(bool_var next) {
lbool lphase = m_ext ? m_ext->get_phase(next) : l_undef;
-
+
if (lphase != l_undef)
return lphase == l_true;
switch (m_config.m_phase) {
- case PS_ALWAYS_TRUE:
- return true;
- case PS_ALWAYS_FALSE:
- return false;
- case PS_BASIC_CACHING:
+ case PS_ALWAYS_TRUE:
+ return true;
+ case PS_ALWAYS_FALSE:
+ return false;
+ case PS_BASIC_CACHING:
+ return m_phase[next];
+ case PS_FROZEN:
+ return m_best_phase[next];
+ case PS_SAT_CACHING:
+ case PS_LOCAL_SEARCH:
+ if (m_search_state == s_unsat)
return m_phase[next];
- case PS_FROZEN:
- return m_best_phase[next];
- case PS_SAT_CACHING:
- if (m_search_state == s_unsat)
- return m_phase[next];
- return m_best_phase[next];
- case PS_RANDOM:
- return (m_rand() % 2) == 0;
- default:
- UNREACHABLE();
- return false;
+ return m_best_phase[next];
+ case PS_RANDOM:
+ return (m_rand() % 2) == 0;
+ default:
+ UNREACHABLE();
+ return false;
}
}
@@ -2823,7 +2844,7 @@ namespace sat {
}
bool solver::is_two_phase() const {
- return m_config.m_phase == PS_SAT_CACHING;
+ return m_config.m_phase == PS_SAT_CACHING || m_config.m_phase == PS_LOCAL_SEARCH;
}
bool solver::is_sat_phase() const {
@@ -2923,6 +2944,10 @@ namespace sat {
case PS_RANDOM:
for (auto& p : m_phase) p = (m_rand() % 2) == 0;
break;
+ case PS_LOCAL_SEARCH:
+ if (m_search_state == s_sat)
+ bounded_local_search();
+ break;
default:
UNREACHABLE();
break;
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 227568f3d..524f6b06d 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -589,7 +589,9 @@ namespace sat {
lbool do_ddfw_search(unsigned num_lits, literal const* lits);
lbool do_prob_search(unsigned num_lits, literal const* lits);
lbool invoke_local_search(unsigned num_lits, literal const* lits);
+ void bounded_local_search();
lbool do_unit_walk();
+ struct scoped_ls;
// -----------------------
//
diff --git a/src/sat/sat_types.h b/src/sat/sat_types.h
index 4e119a2ae..c92a8bbeb 100644
--- a/src/sat/sat_types.h
+++ b/src/sat/sat_types.h
@@ -91,7 +91,7 @@ namespace sat {
virtual model const& get_model() const = 0;
virtual void collect_statistics(statistics& st) const = 0;
virtual double get_priority(bool_var v) const { return 0; }
-
+ virtual bool get_value(bool_var v) const { return true; }
};
class proof_hint {
diff --git a/src/shell/lp_frontend.cpp b/src/shell/lp_frontend.cpp
index 70d2cffb1..8d6425533 100644
--- a/src/shell/lp_frontend.cpp
+++ b/src/shell/lp_frontend.cpp
@@ -80,7 +80,7 @@ void run_solver(smt_params_helper & params, char const * mps_file_name) {
solver->settings().set_message_ostream(&std::cout);
solver->settings().report_frequency = params.arith_rep_freq();
solver->settings().print_statistics = params.arith_print_stats();
- solver->settings().simplex_strategy() = lp:: simplex_strategy_enum::lu;
+ solver->settings().set_simplex_strategy(lp:: simplex_strategy_enum::lu);
solver->find_maximal_solution();
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 219b2c46b..a717c4932 100644
--- a/src/solver/simplifier_solver.cpp
+++ b/src/solver/simplifier_solver.cpp
@@ -95,18 +95,30 @@ class simplifier_solver : public solver {
expr_ref_vector m_assumptions;
model_converter_ref m_mc;
bool m_inconsistent = false;
+ expr_safe_replace m_core_replace;
+
+ void replace(expr_ref_vector& r) {
+ expr_ref tmp(m);
+ for (unsigned i = 0; i < r.size(); ++i) {
+ m_core_replace(r.get(i), tmp);
+ r[i] = tmp;
+ }
+ }
void flush(expr_ref_vector& assumptions) {
unsigned qhead = m_preprocess_state.qhead();
- if (qhead < m_fmls.size()) {
- for (expr* a : assumptions)
- m_preprocess_state.freeze(a);
+ expr_ref_vector orig_assumptions(assumptions);
+ m_core_replace.reset();
+ if (qhead < m_fmls.size() || !assumptions.empty()) {
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;
m_preprocess_state.advance_qhead();
+ for (unsigned i = 0; i < assumptions.size(); ++i)
+ m_core_replace.insert(assumptions.get(i), orig_assumptions.get(i));
}
m_mc = m_preprocess_state.model_trail().get_model_converter();
m_cached_mc = nullptr;
@@ -148,6 +160,7 @@ public:
m_preprocess_state(*this),
m_preprocess(m, s->get_params(), m_preprocess_state),
m_assumptions(m),
+ m_core_replace(m),
m_proof(m)
{
if (fac)
@@ -189,7 +202,7 @@ public:
lbool check_sat_core(unsigned num_assumptions, expr* const* assumptions) override {
expr_ref_vector _assumptions(m, num_assumptions, assumptions);
flush(_assumptions);
- return s->check_sat_core(num_assumptions, assumptions);
+ return s->check_sat_core(num_assumptions, _assumptions.data());
}
void collect_statistics(statistics& st) const override {
@@ -211,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) {
@@ -258,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); }
+ 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(); }
@@ -273,15 +286,59 @@ public:
unsigned get_num_assumptions() const override { return s->get_num_assumptions(); }
expr* get_assumption(unsigned idx) const override { return s->get_assumption(idx); }
unsigned get_scope_level() const override { return s->get_scope_level(); }
- lbool check_sat_cc(expr_ref_vector const& cube, vector const& clauses) override { return check_sat_cc(cube, clauses); }
void set_progress_callback(progress_callback* callback) override { s->set_progress_callback(callback); }
+
lbool get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) override {
- return s->get_consequences(asms, vars, consequences);
+ expr_ref_vector es(m);
+ es.append(asms);
+ es.append(vars);
+ flush(es);
+ expr_ref_vector asms1(m, asms.size(), es.data());
+ expr_ref_vector vars1(m, vars.size(), es.data() + asms.size());
+ lbool r = s->get_consequences(asms1, vars1, consequences);
+ replace(consequences);
+ return r;
+ }
+
+ lbool check_sat_cc(expr_ref_vector const& cube, vector const& clauses) override {
+ expr_ref_vector es(m);
+ es.append(cube);
+ for (auto const& c : clauses)
+ es.append(c);
+ flush(es);
+ expr_ref_vector cube1(m, cube.size(), es.data());
+ vector clauses1;
+ unsigned offset = cube.size();
+ for (auto const& c : clauses) {
+ clauses1.push_back(expr_ref_vector(m, c.size(), es.data() + offset));
+ offset += c.size();
+ }
+ return s->check_sat_cc(cube1, clauses1);
+ }
+
+ lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) override {
+ expr_ref_vector vars1(vars);
+ flush(vars1);
+ lbool r = s->find_mutexes(vars1, mutexes);
+ for (auto& mux : mutexes)
+ replace(mux);
+ return r;
+ }
+
+ lbool preferred_sat(expr_ref_vector const& asms, vector& cores) override {
+ expr_ref_vector asms1(asms);
+ flush(asms1);
+ lbool r = s->preferred_sat(asms1, cores);
+ for (auto& c : cores)
+ replace(c);
+ return r;
}
- lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) override { return s->find_mutexes(vars, mutexes); }
- lbool preferred_sat(expr_ref_vector const& asms, vector& cores) override { return s->preferred_sat(asms, cores); }
- expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) override { return s->cube(vars, backtrack_level); }
+ // todo flush?
+ expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) override {
+ return s->cube(vars, backtrack_level);
+ }
+
expr* congruence_root(expr* e) override { return s->congruence_root(e); }
expr* congruence_next(expr* e) override { return s->congruence_next(e); }
std::ostream& display(std::ostream& out, unsigned n, expr* const* assumptions) const override {
diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp
index 547985f26..c82cdd0a4 100644
--- a/src/test/lp/lp.cpp
+++ b/src/test/lp/lp.cpp
@@ -1391,7 +1391,7 @@ void update_settings(argument_parser & args_parser, lp_settings& settings) {
settings.set_random_seed(n);
}
if (get_int_from_args_parser("--simplex_strategy", args_parser, n)) {
- settings.simplex_strategy() = static_cast(n);
+ settings.set_simplex_strategy(static_cast(n));
}
}
diff --git a/src/util/tbv.h b/src/util/tbv.h
index b010dc388..a023ea2b0 100644
--- a/src/util/tbv.h
+++ b/src/util/tbv.h
@@ -30,7 +30,7 @@ enum tbit {
BIT_z = 0x0, // unknown
BIT_0 = 0x1, // for sure 0
BIT_1 = 0x2, // for sure 1
- BIT_x = 0x3 // don't care
+ BIT_x = 0x3 // don't care
};
inline tbit neg(tbit t) {
@@ -43,7 +43,7 @@ class tbv_manager {
ptr_vector allocated_tbvs;
public:
tbv_manager(unsigned n): m(2*n) {}
- tbv_manager(const tbv_manager& m) = delete;
+ tbv_manager(tbv_manager const& m) = delete;
~tbv_manager();
void reset();
tbv* allocate();
@@ -154,11 +154,9 @@ public:
};
inline std::ostream& operator<<(std::ostream& out, tbv_ref const& c) {
- const char* names[] = { "z", "0", "1", "x" };
- for (unsigned i = c.num_tbits(); i > 0; i--) {
- out << names[(unsigned)c[i - 1]];
+ char const* names[] = { "z", "0", "1", "x" };
+ for (unsigned i = c.num_tbits(); i-- > 0; ) {
+ out << names[static_cast(c[i])];
}
return out;
}
-
-
diff --git a/src/util/util.h b/src/util/util.h
index 783ec50a4..6d4efb671 100644
--- a/src/util/util.h
+++ b/src/util/util.h
@@ -413,22 +413,6 @@ inline size_t megabytes_to_bytes(unsigned mb) {
return r;
}
-/** Compact version of std::all_of */
-template
-bool all_of(Container const& c, Predicate p)
-{
- using std::begin, std::end; // allows begin(c) to also find c.begin()
- return std::all_of(begin(c), end(c), std::forward(p));
-}
-
-/** Compact version of std::any_of */
-template
-bool any_of(Container const& c, Predicate p)
-{
- using std::begin, std::end; // allows begin(c) to also find c.begin()
- return std::any_of(begin(c), end(c), std::forward(p));
-}
-
/** Compact version of std::count */
template
std::size_t count(Container const& c, Item x)