From 0e8969ce6079bb370de13fffd5e433c451ca0f75 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 24 Jan 2025 09:40:33 -0800
Subject: [PATCH] deal with compiler warnings and include value exchange prior
to final check.
---
src/ast/sls/sat_ddfw.cpp | 2 +
src/ast/sls/sls_arith_base.cpp | 56 ++++++++-----
src/ast/sls/sls_arith_base.h | 4 +
src/ast/sls/sls_arith_clausal.cpp | 127 ++++++++++--------------------
src/ast/sls/sls_arith_clausal.h | 2 -
src/ast/sls/sls_basic_plugin.cpp | 2 +-
src/ast/sls/sls_bv_engine.cpp | 4 +-
src/ast/sls/sls_bv_eval.cpp | 4 +-
src/ast/sls/sls_bv_lookahead.cpp | 2 -
src/ast/sls/sls_euf_plugin.cpp | 4 +-
src/ast/sls/sls_seq_plugin.cpp | 36 ++++-----
src/ast/sls/sls_smt_plugin.cpp | 2 +-
src/sat/dimacs.cpp | 4 +-
src/smt/theory_sls.cpp | 25 ++++--
src/smt/theory_sls.h | 4 +
15 files changed, 132 insertions(+), 146 deletions(-)
diff --git a/src/ast/sls/sat_ddfw.cpp b/src/ast/sls/sat_ddfw.cpp
index a70f455f7..bc89ca28b 100644
--- a/src/ast/sls/sat_ddfw.cpp
+++ b/src/ast/sls/sat_ddfw.cpp
@@ -428,6 +428,8 @@ namespace sat {
for (unsigned i = 0; i < num_vars(); ++i)
m_model[i] = to_lbool(value(i));
save_priorities();
+ if (m_plugin && !m_in_external_flip && m_restart_count == 0)
+ m_plugin->on_restart(); // import values if there are any updated ones.
if (m_plugin && !m_in_external_flip)
m_last_result = m_plugin->on_save_model();
}
diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp
index 4bd6c1176..ab9e581f5 100644
--- a/src/ast/sls/sls_arith_base.cpp
+++ b/src/ast/sls/sls_arith_base.cpp
@@ -13,31 +13,13 @@ Author:
Nikolaj Bjorner (nbjorner) 2023-02-07
+Notes:
+
Uses quadratic solver method from nia_ls in hybrid-smt
(with a bug fix for when order of roots are swapped)
Other features from nia_ls are also used as a starting point,
such as tabu and fallbacks.
-Todo:
-
-- add fairness for which variable to flip and direction (by age fifo).
- - maintain age per variable, per sign
-
-- include more general tabu measure
- -
-
-- random walk when there is no applicable update
- - repair_down can fail repeatedely. Then allow a mode to reset arguments similar to
- repair of literals.
-
-- avoid overflow for nested products
-
-Done:
-- add tabu for flipping variable back to the same value.
- - remember last variable/delta and block -delta = last_delta && last_variable = current_variable
-- include measures for bounded updates
- - per variable maintain increasing range
-
--*/
#include "ast/sls/sls_arith_base.h"
@@ -1439,6 +1421,20 @@ namespace sls {
}
for (auto bv : m_tmp_set)
vi.m_bool_vars_of.push_back(bv);
+
+ m_tmp_nat_set.reset();
+ m_tmp_nat_set.assure_domain(ctx.clauses().size() + 1);
+
+ for (auto bv : vi.m_bool_vars_of) {
+ for (auto lit : { sat::literal(bv, false), sat::literal(bv, true) }) {
+ for (auto ci : ctx.get_use_list(lit)) {
+ if (m_tmp_nat_set.contains(ci))
+ continue;
+ m_tmp_nat_set.insert(ci);
+ vi.m_clauses_of.push_back(ci);
+ }
+ }
+ }
}
template<typename num_t>
@@ -2435,6 +2431,7 @@ namespace sls {
template<typename num_t>
void arith_base<num_t>::collect_statistics(statistics& st) const {
st.update("sls-arith-steps", m_stats.m_steps);
+ st.update("sls-arith-propagations", m_stats.m_propagations);
}
template<typename num_t>
@@ -2838,6 +2835,24 @@ namespace sls {
m_fixed_atoms.insert(bv);
}
+ template<typename num_t>
+ void arith_base<num_t>::add_lookahead(sat::bool_var bv) {
+ auto* ineq = get_ineq(bv);
+ if (!ineq)
+ return;
+ num_t na, nb;
+ for (auto const& [x, nl] : ineq->m_nonlinear) {
+ if (is_fixed(x))
+ continue;
+ if (is_linear(x, nl, nb))
+ find_linear_moves(*ineq, x, nb);
+ else if (is_quadratic(x, nl, na, nb))
+ find_quadratic_moves(*ineq, x, na, nb, ineq->m_args_value);
+ else
+ ;
+ }
+ }
+
// for every variable e, for every atom containing e
// add lookahead for e.
// m_fixable_atoms contains atoms that can be fixed.
@@ -3254,6 +3269,7 @@ namespace sls {
template<typename num_t>
void arith_base<num_t>::start_propagation() {
+ ++m_stats.m_propagations;
updt_params();
if (m_config.use_clausal_lookahead)
m_clausal_sls.search();
diff --git a/src/ast/sls/sls_arith_base.h b/src/ast/sls/sls_arith_base.h
index d801e60da..9956572ba 100644
--- a/src/ast/sls/sls_arith_base.h
+++ b/src/ast/sls/sls_arith_base.h
@@ -77,6 +77,7 @@ namespace sls {
struct stats {
unsigned m_steps = 0;
unsigned m_restarts = 0;
+ unsigned m_propagations = 0;
};
public:
@@ -120,6 +121,7 @@ namespace sls {
unsigned m_def_idx = UINT_MAX;
vector<std::pair<num_t, sat::bool_var>> m_linear_occurs;
sat::bool_var_vector m_bool_vars_of;
+ unsigned_vector m_clauses_of;
unsigned_vector m_muls;
unsigned_vector m_adds;
optional<bound> m_lo, m_hi;
@@ -216,6 +218,7 @@ namespace sls {
svector<double> m_prob_break;
indexed_uint_set m_bool_var_atoms;
indexed_uint_set m_tmp_set;
+ nat_set m_tmp_nat_set;
void invariant();
void invariant(ineq const& i);
@@ -381,6 +384,7 @@ namespace sls {
double lookahead(expr* e, bool update_score);
void add_lookahead(bool_info& i, expr* e);
void add_lookahead(bool_info& i, sat::bool_var bv);
+ void add_lookahead(sat::bool_var bv);
ptr_vector<expr> const& get_fixable_exprs(expr* e);
bool apply_move(expr* f, ptr_vector<expr> const& vars, arith_move_type t);
expr* get_candidate_unsat();
diff --git a/src/ast/sls/sls_arith_clausal.cpp b/src/ast/sls/sls_arith_clausal.cpp
index 1337baa34..322ca2320 100644
--- a/src/ast/sls/sls_arith_clausal.cpp
+++ b/src/ast/sls/sls_arith_clausal.cpp
@@ -121,22 +121,14 @@ namespace sls {
template<typename num_t>
void arith_clausal<num_t>::add_lookahead_on_unsat_vars() {
a.m_updates.reset();
- a.m_fixed_atoms.reset();
TRACE("arith_verbose", tout << "unsat-vars ";
for (auto v : ctx.unsat_vars())
if (a.get_ineq(v)) tout << mk_bounded_pp(ctx.atom(v), a.m) << " ";
tout << "\n";);
- for (auto v : ctx.unsat_vars()) {
- auto* ineq = a.get_ineq(v);
- if (!ineq)
- continue;
- auto e = ctx.atom(v);
- auto& i = a.get_bool_info(e);
- auto const& vars = a.get_fixable_exprs(e);
- for (auto v : vars)
- a.add_lookahead(i, v);
- }
+ for (auto v : ctx.unsat_vars())
+ a.add_lookahead(v);
+
}
/**
@@ -146,7 +138,6 @@ namespace sls {
template<typename num_t>
void arith_clausal<num_t>::add_lookahead_on_false_literals() {
a.m_updates.reset();
- a.m_fixed_atoms.reset();
unsigned sz = a.m_bool_var_atoms.size();
bool is_big = sz > 45u;
@@ -164,47 +155,25 @@ namespace sls {
};
unsigned idx = 0;
- //unsigned num_sampled = 0;
- for (unsigned i = std::min(sz, 45u); i-- > 0;) {
- if (is_big) {
+ if (is_big) {
+ for (unsigned i = 45, j = 90; j-- > 0 && i-- > 0 && sz > 0;) {
idx = ctx.rand(sz);
bv = a.m_bool_var_atoms[idx];
- }
- else
- bv = a.m_bool_var_atoms[i];
-
- if (occurs_negative(bv)) {
- auto e = ctx.atom(bv);
- auto& i = a.get_bool_info(e);
- a.add_lookahead(i, bv);
- //++num_sampled;
- }
-
- if (is_big) {
--sz;
a.m_bool_var_atoms.swap_elems(idx, sz);
+ if (occurs_negative(bv))
+ a.add_lookahead(bv);
+ else
+ ++i;
}
}
-
-#if 0
- for (auto bv : a.m_bool_var_atoms) {
- if (ctx.unsat_vars().contains(bv))
- continue;
- auto* ineq = a.get_ineq(bv);
- if (!ineq)
- continue;
- sat::literal lit(bv, !ineq->is_true());
- auto const& ul = ctx.get_use_list(~lit);
- if (ul.begin() == ul.end())
- continue;
- // literal is false in some clause but none of the clauses where it occurs false are unsat.
-
- auto e = ctx.atom(bv);
- auto& i = a.get_bool_info(e);
-
- a.add_lookahead(i, bv);
+ else {
+ for (unsigned i = 0; i < sz; ++i) {
+ bv = a.m_bool_var_atoms[i];
+ if (occurs_negative(bv))
+ a.add_lookahead(bv);
+ }
}
-#endif
}
template<typename num_t>
@@ -300,50 +269,38 @@ namespace sls {
if (!a.update_num(v, delta))
return -1;
double score = 0;
- m_tmp_nat_set.reset();
- m_tmp_nat_set.assure_domain(ctx.clauses().size() + 1);
- for (auto bv : vi.m_bool_vars_of) {
- for (auto lit : { sat::literal(bv, false), sat::literal(bv, true) }) {
- for (auto ci : ctx.get_use_list(lit)) {
- if (m_tmp_nat_set.contains(ci)) {
- continue;
- }
- m_tmp_nat_set.insert(ci);
-
- auto const& c = ctx.get_clause(ci);
- unsigned num_true = 0;
- for (auto lit : c) {
- auto bv = lit.var();
- auto ineq = a.get_ineq(bv);
- if (ineq) {
- if (ineq->is_true() != lit.sign())
- ++num_true;
- }
- else if (ctx.is_true(lit))
- ++num_true;
- }
-
- CTRACE("arith_verbose", c.m_num_trues != num_true && (c.m_num_trues == 0 || num_true == 0),
- tout << "clause: " << c
- << " v" << v << " += " << delta
- << " new-true lits: " << num_true
- << " old-true lits: " << c.m_num_trues
- << " w: " << c.m_weight << "\n";
- for (auto lit : c)
- if (a.get_ineq(lit.var()))
- tout << lit << " " << *a.get_ineq(lit.var()) << "\n";);
- if (c.m_num_trues > 0 && num_true == 0)
- score -= c.m_weight;
- else if (c.m_num_trues == 0 && num_true > 0)
- score += c.m_weight;
+ for (auto ci : vi.m_clauses_of) {
+ auto const& c = ctx.get_clause(ci);
+ unsigned num_true = 0;
+ for (auto lit : c) {
+ auto bv = lit.var();
+ auto ineq = a.get_ineq(bv);
+ if (ineq) {
+ if (ineq->is_true() != lit.sign())
+ ++num_true;
}
+ else if (ctx.is_true(lit))
+ ++num_true;
}
-
+
+ CTRACE("arith_verbose", c.m_num_trues != num_true && (c.m_num_trues == 0 || num_true == 0),
+ tout << "clause: " << c
+ << " v" << v << " += " << delta
+ << " new-true lits: " << num_true
+ << " old-true lits: " << c.m_num_trues
+ << " w: " << c.m_weight << "\n";
+ for (auto lit : c)
+ if (a.get_ineq(lit.var()))
+ tout << lit << " " << *a.get_ineq(lit.var()) << "\n";);
+ if (c.m_num_trues > 0 && num_true == 0)
+ score -= c.m_weight;
+ else if (c.m_num_trues == 0 && num_true > 0)
+ score += c.m_weight;
}
+ // verbose_stream() << num_clauses << " " << num_dup << "\n";
// revert the update
- a.update_args_value(v, vi.value() - delta);
-
+ a.update_args_value(v, vi.value() - delta);
return score;
}
diff --git a/src/ast/sls/sls_arith_clausal.h b/src/ast/sls/sls_arith_clausal.h
index 78897ba27..ba9109b9a 100644
--- a/src/ast/sls/sls_arith_clausal.h
+++ b/src/ast/sls/sls_arith_clausal.h
@@ -80,8 +80,6 @@ namespace sls {
unsigned m_best_last_step = 0;
unsigned m_num_lookaheads = 0;
- nat_set m_tmp_nat_set;
-
// avoid checking the same updates twice
var_t m_last_var = UINT_MAX;
num_t m_last_delta;
diff --git a/src/ast/sls/sls_basic_plugin.cpp b/src/ast/sls/sls_basic_plugin.cpp
index aca1e646b..1a836a511 100644
--- a/src/ast/sls/sls_basic_plugin.cpp
+++ b/src/ast/sls/sls_basic_plugin.cpp
@@ -81,7 +81,7 @@ namespace sls {
}
expr_ref basic_plugin::eval_ite(app* e) {
- expr* c, * th, * el;
+ expr* c = nullptr, * th = nullptr, * el = nullptr;
VERIFY(m.is_ite(e, c, th, el));
if (bval0(c))
return ctx.get_value(th);
diff --git a/src/ast/sls/sls_bv_engine.cpp b/src/ast/sls/sls_bv_engine.cpp
index 8d009b500..96e355c2d 100644
--- a/src/ast/sls/sls_bv_engine.cpp
+++ b/src/ast/sls/sls_bv_engine.cpp
@@ -396,13 +396,12 @@ double sls_engine::find_best_move_mc(ptr_vector<func_decl> & to_evaluate, double
// main search loop
lbool sls_engine::search() {
lbool res = l_undef;
- double score = 0.0, old_score = 0.0;
+ double score = 0.0;
unsigned new_const = (unsigned)-1, new_bit;
mpz new_value;
move_type move;
score = rescore();
- unsigned sz = m_assertions.size();
while (check_restart(m_stats.m_moves)) {
if (!m_manager.inc())
@@ -435,7 +434,6 @@ lbool sls_engine::search() {
continue;
}
- old_score = score;
new_const = (unsigned)-1;
// find best increasing move
diff --git a/src/ast/sls/sls_bv_eval.cpp b/src/ast/sls/sls_bv_eval.cpp
index afaf71a89..a68a3a633 100644
--- a/src/ast/sls/sls_bv_eval.cpp
+++ b/src/ast/sls/sls_bv_eval.cpp
@@ -986,7 +986,7 @@ namespace sls {
}
void bv_eval::fold_oper(bvect& out, app* t, unsigned i, std::function<void(bvect&, bvval const&)> const& f) {
- auto i2 = i == 0 ? 1 : 0;
+ unsigned i2 = i == 0 ? 1 : 0;
auto const& c = wval(t->get_arg(i2));
for (unsigned j = 0; j < c.nw; ++j)
out[j] = c.bits()[j];
@@ -1242,8 +1242,6 @@ namespace sls {
bool bv_eval::try_repair_sdiv(bvect const& e, bvval& a, bvval& b, unsigned i) {
bool sign_a = a.sign();
- bool sign_b = b.sign();
- bool sign_e = e.get(a.bw - 1);
// y = 0, x >= 0 -> -1
if (i == 0 && b.is_zero() && a.is_ones(e) && a.try_set(m_zero))
diff --git a/src/ast/sls/sls_bv_lookahead.cpp b/src/ast/sls/sls_bv_lookahead.cpp
index 0d342287c..ba06e1d7c 100644
--- a/src/ast/sls/sls_bv_lookahead.cpp
+++ b/src/ast/sls/sls_bv_lookahead.cpp
@@ -676,7 +676,6 @@ namespace sls {
for (unsigned i = 0; i < m_update_stack[depth].size(); ++i) {
auto [e, is_bv] = m_update_stack[depth][i];
TRACE("bv_verbose", tout << "update " << mk_bounded_pp(e, m) << "\n";);
- bool old_truth = false;
if (t == e)
;
else if (is_bv) {
@@ -684,7 +683,6 @@ namespace sls {
wval(e).commit_eval_ignore_tabu();
}
else {
- old_truth = m_ev.get_bool_value(e);
SASSERT(m.is_bool(e));
auto v1 = m_ev.bval1(e);
diff --git a/src/ast/sls/sls_euf_plugin.cpp b/src/ast/sls/sls_euf_plugin.cpp
index 3bb90aa0a..d3d120cd0 100644
--- a/src/ast/sls/sls_euf_plugin.cpp
+++ b/src/ast/sls/sls_euf_plugin.cpp
@@ -197,8 +197,6 @@ namespace sls {
g.mk(m.mk_true(), 0, 0, nullptr);
if (!g.find(m.mk_false()))
g.mk(m.mk_false(), 0, 0, nullptr);
-
- // merge all equalities
// check for conflict with disequalities during propagation
if (merge_eqs) {
TRACE("euf", tout << "root literals " << ctx.root_literals() << "\n");
@@ -279,7 +277,7 @@ namespace sls {
void euf_plugin::validate_model() {
auto& g = *m_g;
for (auto lit : ctx.root_literals()) {
- euf::enode* a, * b;
+ euf::enode* a = nullptr, * b = nullptr;
if (!ctx.is_true(lit))
continue;
auto e = ctx.atom(lit.var());
diff --git a/src/ast/sls/sls_seq_plugin.cpp b/src/ast/sls/sls_seq_plugin.cpp
index 2c7e7f8d9..5abe91e6c 100644
--- a/src/ast/sls/sls_seq_plugin.cpp
+++ b/src/ast/sls/sls_seq_plugin.cpp
@@ -276,7 +276,7 @@ namespace sls {
ptr_vector<expr> const& seq_plugin::lhs(expr* eq) {
auto& ev = get_eval(eq);
if (ev.lhs.empty()) {
- expr* x, * y;
+ expr* x = nullptr, * y = nullptr;
VERIFY(m.is_eq(eq, x, y));
seq.str.get_concat(x, ev.lhs);
seq.str.get_concat(y, ev.rhs);
@@ -332,7 +332,7 @@ namespace sls {
}
bool seq_plugin::bval1_seq(app* e) {
- expr* a, *b;
+ expr* a = nullptr, *b = nullptr;
SASSERT(e->get_family_id() == seq.get_family_id());
switch (e->get_decl_kind()) {
case OP_SEQ_CONTAINS:
@@ -433,7 +433,7 @@ namespace sls {
}
}
case OP_SEQ_AT: {
- expr* x, * offset;
+ expr* x = nullptr, * offset = nullptr;
VERIFY(seq.str.is_at(e, x, offset));
zstring r = strval0(x);
expr_ref offset_e = ctx.get_value(offset);
@@ -613,14 +613,14 @@ namespace sls {
}
void seq_plugin::repair_up_str_length(app* e) {
- expr* x;
+ expr* x = nullptr;
VERIFY(seq.str.is_length(e, x));
zstring val_x = strval0(x);
update(e, rational(val_x.length()));
}
void seq_plugin::repair_up_str_indexof(app* e) {
- expr* x, * y, * z = nullptr;
+ expr* x = nullptr, * y = nullptr, * z = nullptr;
VERIFY(seq.str.is_index(e, x, y, z) || seq.str.is_index(e, x, y));
zstring val_x = strval0(x);
zstring val_y = strval0(y);
@@ -801,6 +801,7 @@ namespace sls {
index -= len_x;
}
}
+#if 0
unsigned last_diff = 0;
for (unsigned i = 1; i <= val.length() && i <= val_other.length(); ++i) {
if (val[val.length() - i] != val_other[val_other.length() - i]) {
@@ -809,7 +810,7 @@ namespace sls {
}
}
-#if 0
+
if (last_diff != 0) {
unsigned index = last_diff;
for (auto x : w) {
@@ -1273,7 +1274,7 @@ namespace sls {
}
bool seq_plugin::repair_down_str_replace(app* e) {
- expr* x, * y, * z;
+ expr* x = nullptr, * y = nullptr, * z = nullptr;
VERIFY(seq.str.is_replace(e, x, y, z));
zstring r = strval0(e);
if (r == strval1(e))
@@ -1293,7 +1294,7 @@ namespace sls {
}
bool seq_plugin::repair_down_str_itos(app* e) {
- expr* x;
+ expr* x = nullptr;
VERIFY(seq.str.is_itos(e, x));
zstring se = strval0(e);
rational r(se.encode().c_str());
@@ -1305,7 +1306,7 @@ namespace sls {
}
bool seq_plugin::repair_down_str_stoi(app* e) {
- expr* x;
+ expr* x = nullptr;
rational r;
VERIFY(seq.str.is_stoi(e, x));
VERIFY(a.is_numeral(ctx.get_value(e), r) && r.is_int());
@@ -1330,7 +1331,7 @@ namespace sls {
}
bool seq_plugin::repair_down_str_at(app* e) {
- expr* x, * y;
+ expr* x = nullptr, * y = nullptr;
VERIFY(seq.str.is_at(e, x, y));
zstring se = strval0(e);
// std::cout << "repair-str-at: " << mk_pp(e, m) << ": \"" << se << "\"" << std::endl;
@@ -1387,7 +1388,7 @@ namespace sls {
}
bool seq_plugin::repair_down_str_indexof(app* e) {
- expr* x, * y, * offset = nullptr;
+ expr* x = nullptr, * y = nullptr, * offset = nullptr;
VERIFY(seq.str.is_index(e, x, y, offset) || seq.str.is_index(e, x, y));
rational value;
VERIFY(a.is_numeral(ctx.get_value(e), value) && value.is_int());
@@ -1437,7 +1438,7 @@ namespace sls {
}
bool seq_plugin::repair_down_str_prefixof(app* e) {
- expr* a, * b;
+ expr* a = nullptr, * b = nullptr;
VERIFY(seq.str.is_prefix(e, a, b));
zstring sa = strval0(a);
zstring sb = strval0(b);
@@ -1475,7 +1476,7 @@ namespace sls {
}
bool seq_plugin::repair_down_str_suffixof(app* e) {
- expr* a, * b;
+ expr* a = nullptr, * b = nullptr;
VERIFY(seq.str.is_suffix(e, a, b));
zstring sa = strval0(a);
zstring sb = strval0(b);
@@ -1513,7 +1514,7 @@ namespace sls {
}
bool seq_plugin::repair_down_str_contains(expr* e) {
- expr* a, *b;
+ expr* a = nullptr, *b = nullptr;
VERIFY(seq.str.is_contains(e, a, b));
zstring sa = strval0(a);
zstring sb = strval0(b);
@@ -1568,7 +1569,7 @@ namespace sls {
}
bool seq_plugin::repair_down_str_extract(app* e) {
- expr* x, * offset, * len;
+ expr* x = nullptr, * offset = nullptr, * len = nullptr;
VERIFY(seq.str.is_extract(e, x, offset, len));
SASSERT(strval0(e) != strval1(e));
zstring v = strval0(e);
@@ -1832,7 +1833,7 @@ namespace sls {
auto& ev = get_eval(t);
ev.max_length = 1;
}
- expr* x, * offset, * len;
+ expr* x = nullptr, * offset = nullptr, * len = nullptr;
rational len_r;
if (seq.str.is_extract(t, x, offset, len) && a.is_numeral(len, len_r)) {
auto& ev = get_eval(t);
@@ -1855,7 +1856,6 @@ namespace sls {
auto e = ctx.atom(lit.var());
if (!is_seq_predicate(e))
return;
- auto a = to_app(e);
if (bval1(e) == lit.sign())
ctx.flip(lit.var());
}
@@ -1890,7 +1890,7 @@ namespace sls {
}
bool seq_plugin::repair_down_in_re(app* e) {
- expr* x, * y;
+ expr* x = nullptr, * y = nullptr;
VERIFY(seq.str.is_in_re(e, x, y));
auto info = seq.re.get_info(y);
if (!info.interpreted)
diff --git a/src/ast/sls/sls_smt_plugin.cpp b/src/ast/sls/sls_smt_plugin.cpp
index 67049d781..952515264 100644
--- a/src/ast/sls/sls_smt_plugin.cpp
+++ b/src/ast/sls/sls_smt_plugin.cpp
@@ -212,7 +212,7 @@ namespace sls {
m_sat_phase[v] = ctx.get_best_phase(v);
}
- bool smt_plugin::export_to_sls() {
+ bool smt_plugin::export_to_sls() {
bool updated = false;
if (m_has_units) {
std::lock_guard<std::mutex> lock(m_mutex);
diff --git a/src/sat/dimacs.cpp b/src/sat/dimacs.cpp
index 1d19a60c7..f81eb3aa4 100644
--- a/src/sat/dimacs.cpp
+++ b/src/sat/dimacs.cpp
@@ -132,7 +132,7 @@ static bool parse_dimacs_core(Buffer & in, std::ostream& err, sat::solver & solv
}
}
}
- catch (dimacs::lex_error) {
+ catch (dimacs::lex_error& ) {
return false;
}
return true;
@@ -280,7 +280,7 @@ namespace dimacs {
}
return true;
}
- catch (lex_error) {
+ catch (dimacs::lex_error&) {
return false;
}
}
diff --git a/src/smt/theory_sls.cpp b/src/smt/theory_sls.cpp
index da2207e56..0ce329046 100644
--- a/src/smt/theory_sls.cpp
+++ b/src/smt/theory_sls.cpp
@@ -103,13 +103,14 @@ namespace smt {
m_smt_plugin->check(fmls, clauses);
m_smt_plugin->get_shared_clauses(m_shared_clauses);
}
- else if (!m_parallel_mode)
- propagate_local_search();
- else if (m_smt_plugin->completed()) {
+ else if (m_parallel_mode && m_smt_plugin->completed()) {
m_smt_plugin->finalize(m_model, m_st);
m_smt_plugin = nullptr;
m_init_search = false;
}
+ else
+ propagate_local_search();
+
}
void theory_sls::pop_scope_eh(unsigned n) {
@@ -152,17 +153,29 @@ namespace smt {
}
}
+ void theory_sls::update_propagation_scope() {
+ if (m_propagation_scope > ctx.get_scope_level() && m_propagation_scope == m_max_propagation_scope) {
+ m_smt_plugin->smt_values_to_sls();
+ }
+ m_propagation_scope = ctx.get_scope_level();
+ m_max_propagation_scope = std::max(m_max_propagation_scope, m_propagation_scope);
+ }
+
void theory_sls::propagate_local_search() {
if (!m_has_unassigned_clause_after_resolve)
return;
- if (m_parallel_mode || !m_smt_plugin)
+ if (!m_smt_plugin)
return;
++m_after_resolve_decide_count;
- if (100 + m_after_resolve_decide_gap > m_after_resolve_decide_count)
+ if (100 + m_after_resolve_decide_gap > m_after_resolve_decide_count) {
+ //update_propagation_scope();
return;
+ }
m_after_resolve_decide_gap *= 2;
- if (!shared_clauses_are_true())
+ if (!shared_clauses_are_true()) {
+ update_propagation_scope();
return;
+ }
m_resolve_count = 0;
m_has_unassigned_clause_after_resolve = false;
run_guided_sls();
diff --git a/src/smt/theory_sls.h b/src/smt/theory_sls.h
index 40f73b52e..b0407cbdb 100644
--- a/src/smt/theory_sls.h
+++ b/src/smt/theory_sls.h
@@ -73,6 +73,8 @@ namespace smt {
unsigned m_after_resolve_decide_count = 0;
unsigned m_resolve_count = 0;
unsigned m_resolve_gap = 0;
+ unsigned m_max_propagation_scope = 0;
+ unsigned m_propagation_scope = 0;
mutable bool m_init_search = false;
mutable ::statistics m_st;
vector<sat::literal_vector> m_shared_clauses;
@@ -95,6 +97,8 @@ namespace smt {
void run_guided_sls();
void finalize() const;
+ void update_propagation_scope();
+
public:
theory_sls(context& ctx);
~theory_sls() override;