From c41abf2241deb5e1d4d23429d9b0b35a420e5cf7 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 13 Aug 2020 08:36:16 -0700
Subject: [PATCH] fix #4624 #4633 #4632 #4631
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/math/dd/dd_bdd.cpp | 4 ++--
src/opt/maxres.cpp | 4 +---
src/sat/sat_config.cpp | 2 +-
src/smt/theory_pb.cpp | 51 +++++++++++++++++++++---------------------
4 files changed, 29 insertions(+), 32 deletions(-)
diff --git a/src/math/dd/dd_bdd.cpp b/src/math/dd/dd_bdd.cpp
index ccc5b67d2..86f2b9408 100644
--- a/src/math/dd/dd_bdd.cpp
+++ b/src/math/dd/dd_bdd.cpp
@@ -318,7 +318,7 @@ namespace dd {
goto go_down;
}
else {
- while (current_cost() != best_cost) {
+ while (current_cost() > best_cost) {
sift_up(--lvl);
}
return;
@@ -339,7 +339,7 @@ namespace dd {
goto go_up;
}
else {
- while (current_cost() != best_cost) {
+ while (current_cost() > best_cost) {
sift_up(lvl++);
}
return;
diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index 3fc5f80e6..49a73b269 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -289,10 +289,8 @@ public:
Give preference to cores that have large minimal values.
*/
sort_assumptions(asms);
- m_last_index = std::min(m_last_index, asms.size()-1);
- m_last_index = 0;
- unsigned index = m_last_index>0?m_last_index-1:0;
m_last_index = 0;
+ unsigned index = 0;
bool first = index > 0;
SASSERT(index < asms.size() || asms.empty());
IF_VERBOSE(10, verbose_stream() << "start hill climb " << index << " asms: " << asms.size() << "\n";);
diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index f8186e446..fd961d94b 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -99,7 +99,7 @@ namespace sat {
else
m_local_search_mode = local_search_mode::wsat;
m_local_search_dbg_flips = p.local_search_dbg_flips();
- m_binspr = p.binspr();
+ //m_binspr = p.binspr();
m_binspr = false; // prevent adventurous users from trying feature that isn't ready
m_anf_simplify = p.anf();
m_anf_delay = p.anf_delay();
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index 097451035..ec5d953bf 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -1325,37 +1325,37 @@ namespace smt {
bool theory_pb::gc() {
-
unsigned z = 0, nz = 0;
m_occs.reset();
for (unsigned i = 0; i < m_card_trail.size(); ++i) {
bool_var v = m_card_trail[i];
- if (v == null_bool_var) continue;
+ if (v == null_bool_var)
+ continue;
card* c = m_var_infos[v].m_card;
- if (c) {
- c->reset_propagations();
- literal lit = c->lit();
- if (c->is_aux() && ctx.get_assign_level(lit) > ctx.get_search_level()) {
- double activity = ctx.get_activity(v);
- if (activity <= 0) {
- nz++;
- }
- else {
- z++;
- clear_watch(*c);
- m_var_infos[v].m_card = nullptr;
- dealloc(c);
- m_card_trail[i] = null_bool_var;
- ctx.remove_watch(v);
- // TBD: maybe v was used in a clause for propagation.
- m_occs.insert(v);
- }
+ if (!c)
+ continue;
+ c->reset_propagations();
+ literal lit = c->lit();
+ if (c->is_aux() && ctx.get_assign_level(lit) > ctx.get_search_level()) {
+ double activity = ctx.get_activity(v);
+ if (activity <= 0) {
+ nz++;
+ }
+ else {
+ z++;
+ clear_watch(*c);
+ m_var_infos[v].m_card = nullptr;
+ dealloc(c);
+ m_card_trail[i] = null_bool_var;
+ ctx.remove_watch(v);
+ // TBD: maybe v was used in a clause for propagation.
+ m_occs.insert(v);
}
}
}
- clause_vector const& lemmas = ctx.get_lemmas();
- for (unsigned i = 0; i < lemmas.size(); ++i) {
- clause* cl = lemmas[i];
+
+#if 0
+ for (clause* cl : ctx.get_lemmas()) {
if (!cl->deleted()) {
for (literal lit : *cl) {
if (m_occs.contains(lit.var())) {
@@ -1365,9 +1365,6 @@ namespace smt {
}
}
- //std::cout << "zs: " << z << " nzs: " << nz << " lemmas: " << ctx.get_lemmas().size() << " trail: " << m_card_trail.size() << "\n";
- return z*10 >= nz;
-
m_occs.reset();
for (unsigned i = 0; i < lemmas.size(); ++i) {
clause* cl = lemmas[i];
@@ -1377,6 +1374,8 @@ namespace smt {
m_occs.insert(idx);
}
}
+#endif
+ return z*10 >= nz;
}