From 79183b6339fd48cf6e984edd6f2938defde64ec7 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 31 Mar 2020 20:10:51 -0700
Subject: [PATCH 01/14] say no to local search + parallel #3636
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/sat/sat_solver.cpp | 1 +
1 file changed, 1 insertion(+)
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 8b542097f..0d6edd3ab 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1154,6 +1154,7 @@ namespace sat {
if (mdl[v] != l_true) l.neg();
push();
assign_core(l, justification(scope_lvl()));
+ propagate(false);
}
mk_model();
break;
From fe267803d198f31e80bfcb401213cef8e169b295 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 31 Mar 2020 20:33:42 -0700
Subject: [PATCH 02/14] fix #3634
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/smt_context.cpp | 26 ++++++++++++++++----------
src/smt/smt_context.h | 2 ++
src/smt/tactic/smt_tactic.cpp | 1 +
3 files changed, 19 insertions(+), 10 deletions(-)
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index d9219fcb6..cf77877a2 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -2950,7 +2950,7 @@ namespace smt {
void context::assert_expr_core(expr * e, proof * pr) {
if (get_cancel_flag()) return;
SASSERT(is_well_sorted(m, e));
- TRACE("begin_assert_expr", tout << this << " " << mk_pp(e, m) << "\n";);
+ TRACE("begin_assert_expr", tout << mk_pp(e, m) << " " << mk_pp(pr, m) << "\n";);
TRACE("begin_assert_expr_ll", tout << mk_ll_pp(e, m) << "\n";);
pop_to_base_lvl();
if (pr == nullptr)
@@ -3141,20 +3141,24 @@ namespace smt {
m_asserted_formulas.commit();
}
if (m_asserted_formulas.inconsistent() && !inconsistent()) {
- proof * pr = m_asserted_formulas.get_inconsistency_proof();
- if (pr == nullptr) {
- set_conflict(b_justification::mk_axiom());
- }
- else {
- set_conflict(mk_justification(justification_proof_wrapper(*this, pr)));
- m_unsat_proof = pr;
- }
+ asserted_inconsistent();
}
TRACE("internalize_assertions", tout << "after internalize_assertions()...\n";
tout << "inconsistent: " << inconsistent() << "\n";);
TRACE("after_internalize_assertions", display(tout););
}
+ void context::asserted_inconsistent() {
+ proof * pr = m_asserted_formulas.get_inconsistency_proof();
+ m_unsat_proof = pr;
+ if (!pr) {
+ set_conflict(b_justification::mk_axiom());
+ }
+ else {
+ set_conflict(mk_justification(justification_proof_wrapper(*this, pr)));
+ }
+ }
+
/**
\brief Assumptions must be uninterpreted boolean constants (aka propositional variables).
*/
@@ -3626,8 +3630,10 @@ namespace smt {
lbool context::search() {
- if (m_asserted_formulas.inconsistent())
+ if (m_asserted_formulas.inconsistent()) {
+ asserted_inconsistent();
return l_false;
+ }
if (inconsistent()) {
VERIFY(!resolve_conflict());
return l_false;
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index b52590c90..b790b6f9e 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -1138,6 +1138,8 @@ namespace smt {
void internalize_assertions();
+ void asserted_inconsistent();
+
bool validate_assumptions(expr_ref_vector const& asms);
void init_assumptions(expr_ref_vector const& asms);
diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp
index 855023f18..9b0f8d617 100644
--- a/src/smt/tactic/smt_tactic.cpp
+++ b/src/smt/tactic/smt_tactic.cpp
@@ -249,6 +249,7 @@ public:
lcore = m.mk_join(lcore, m.mk_leaf(d));
}
}
+ if (!pr && m.proofs_enabled()) pr = m.mk_asserted(m.mk_false()); // bail out
in->assert_expr(m.mk_false(), pr, lcore);
result.push_back(in.get());
return;
From ddc77b11005b6e924229638a88ea0fdaf2f113ed Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 31 Mar 2020 20:53:10 -0700
Subject: [PATCH 03/14] fix #3632
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/sat/sat_local_search.cpp | 16 +++++++++++++---
src/sat/sat_solver.cpp | 5 ++++-
2 files changed, 17 insertions(+), 4 deletions(-)
diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp
index dc2193168..b3ce9c6c1 100644
--- a/src/sat/sat_local_search.cpp
+++ b/src/sat/sat_local_search.cpp
@@ -31,7 +31,9 @@ namespace sat {
for (unsigned i = 0; i < m_assumptions.size(); ++i) {
add_clause(1, m_assumptions.c_ptr() + i);
}
-
+ if (m_is_unsat)
+ return;
+
// add sentinel variable.
m_vars.push_back(var_info());
@@ -334,7 +336,12 @@ namespace sat {
void local_search::add_unit(literal lit, literal exp) {
bool_var v = lit.var();
- if (is_unit(lit)) return;
+ if (is_unit(lit)) {
+ if (m_vars[v].m_value == lit.sign()) {
+ m_is_unsat = true;
+ }
+ return;
+ }
SASSERT(!m_units.contains(v));
if (m_vars[v].m_value == lit.sign() && !m_initializing) {
flip_walksat(v);
@@ -575,8 +582,11 @@ namespace sat {
m_assumptions.append(sz, assumptions);
unsigned num_units = m_units.size();
init();
+ if (m_is_unsat)
+ return l_false;
walksat();
-
+
+ TRACE("sat", tout << m_units << "\n";);
// remove unit clauses
for (unsigned i = m_units.size(); i-- > num_units; ) {
m_vars[m_units[i]].m_unit = false;
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 0d6edd3ab..fc7ce0837 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1282,7 +1282,10 @@ namespace sat {
struct scoped_ls {
solver& s;
scoped_ls(solver& s): s(s) {}
- ~scoped_ls() { dealloc(s.m_local_search); s.m_local_search = nullptr; }
+ ~scoped_ls() {
+ dealloc(s.m_local_search);
+ s.m_local_search = nullptr;
+ }
};
scoped_ls _ls(*this);
if (inconsistent()) return l_false;
From 1d6fb6352fb5def39a2ca30ef9602246b34bc979 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 31 Mar 2020 21:00:52 -0700
Subject: [PATCH 04/14] fix #3631
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/sat/ba_solver.cpp | 16 ++++++++++++----
1 file changed, 12 insertions(+), 4 deletions(-)
diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index 7f4e290c0..f1bd9c749 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -2076,12 +2076,20 @@ namespace sat {
else
polarity = polarity ^ sign;
}
- if (lits.empty()) {
- throw default_exception("empty xor is TBD");
- }
- if (polarity) {
+ if (polarity && !lits.empty()) {
lits[0].neg();
}
+ switch (lits.size()) {
+ case 0:
+ if (polarity)
+ s().set_conflict(justification(0));
+ return nullptr;
+ case 1:
+ s().assign_scoped(lits[0]);
+ return nullptr;
+ default:
+ break;
+ }
void * mem = m_allocator.allocate(xr::get_obj_size(lits.size()));
xr* x = new (mem) xr(next_id(), lits);
x->set_learned(learned);
From b92d8aa00edfaa3b3a923a3c30416ab0e86a3cb4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 31 Mar 2020 22:59:31 -0700
Subject: [PATCH 05/14] finish fix for #3631
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/sat/ba_solver.cpp | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index f1bd9c749..c1fc6a9e1 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -2057,8 +2057,8 @@ namespace sat {
// {false, true}, p => {true, false}
// {false, true}, !p => {true, false}
void add(literal l) {
+ sign = lit == (sign == l.sign());
lit = !lit;
- sign = sign != l.sign();
}
};
literal_vector lits;
From d9032890e44759bcfe26f4c7c9d172dac7d5d2dc Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 31 Mar 2020 23:03:45 -0700
Subject: [PATCH 06/14] finish fix for #3631
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/sat/ba_solver.cpp | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index c1fc6a9e1..e3a8a7ea2 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -3246,7 +3246,8 @@ namespace sat {
recompile(c.to_pb());
break;
case xr_t:
- //NOT_IMPLEMENTED_YET();
+ add_xr(c.to_xr().literals(), c.learned());
+ remove_constraint(c, "recompile xor");
break;
default:
UNREACHABLE();
From c20b321e574bfe15cc423d6d78c5206a47767bd2 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 31 Mar 2020 23:29:08 -0700
Subject: [PATCH 07/14] fix #3641
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/theory_lra.cpp | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 2555fc2d8..8d26562fd 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1038,8 +1038,6 @@ public:
bool internalize_atom(app * atom, bool gate_ctx) {
SASSERT(!ctx().b_internalized(atom));
- bool_var bv = ctx().mk_bool_var(atom);
- ctx().set_var_theory(bv, get_id());
expr* n1, *n2;
rational r;
lp_api::bound_kind k;
@@ -1059,8 +1057,10 @@ public:
else {
TRACE("arith", tout << "Could not internalize " << mk_pp(atom, m) << "\n";);
found_unsupported(atom);
- return true;
+ return false;
}
+ bool_var bv = ctx().mk_bool_var(atom);
+ ctx().set_var_theory(bv, get_id());
if (is_int(v) && !r.is_int()) {
r = (k == lp_api::upper_t) ? floor(r) : ceil(r);
}
@@ -1069,7 +1069,7 @@ public:
updt_unassigned_bounds(v, +1);
m_bounds_trail.push_back(v);
m_bool_var2bound.insert(bv, b);
- TRACE("arith_verbose", tout << "Internalized " << mk_pp(atom, m) << "\n";);
+ TRACE("arith_verbose", tout << "Internalized " << bv << ": " << mk_pp(atom, m) << "\n";);
mk_bound_axioms(*b);
//add_use_lists(b);
return true;
From e9bc8e2433bade3d0f0f985dc2a9f28d45367bfc Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 31 Mar 2020 23:38:07 -0700
Subject: [PATCH 08/14] fix #3642
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/ast/ast.cpp | 4 ++--
src/smt/asserted_formulas.cpp | 2 +-
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 444274270..1890acaae 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1800,7 +1800,7 @@ static void track_id(ast* n, unsigned id) {
if (n->get_id() != id) return;
++s_count;
std::cout << s_count << "\n";
- SASSERT(s_count != 1);
+ //SASSERT(s_count != 1);
}
#endif
@@ -1834,7 +1834,7 @@ ast * ast_manager::register_node_core(ast * n) {
n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk();
- // track_id(n, 2147483792);
+ // track_id(n, 70);
TRACE("ast", tout << "Object " << n->m_id << " was created.\n";);
TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";);
diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp
index e535633cd..c76c61ed9 100644
--- a/src/smt/asserted_formulas.cpp
+++ b/src/smt/asserted_formulas.cpp
@@ -421,7 +421,7 @@ void asserted_formulas::nnf_cnf() {
for (; i < sz; i++) {
expr * n = m_formulas[i].get_fml();
TRACE("nnf_bug", tout << "processing:\n" << mk_pp(n, m) << "\n";);
- proof * pr = m_formulas[i].get_proof();
+ proof_ref pr(m_formulas[i].get_proof(), m);
expr_ref r1(m);
proof_ref pr1(m);
push_todo.reset();
From 9d759a187e4163b2f9702ae456e5a89cd9038b65 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 1 Apr 2020 00:19:05 -0700
Subject: [PATCH 09/14] fix #3643
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/sat/ba_solver.cpp | 38 ++++++++++++++------------------------
1 file changed, 14 insertions(+), 24 deletions(-)
diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index e3a8a7ea2..6819da579 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -2048,40 +2048,30 @@ namespace sat {
return lit;
}
+
ba_solver::constraint* ba_solver::add_xr(literal_vector const& _lits, bool learned) {
- struct parity {
- bool sign; bool lit;
- parity(): sign(false), lit(false) {}
- // {false, false}, p => {false, true}
- // {false, false}, !p => {true, true}
- // {false, true}, p => {true, false}
- // {false, true}, !p => {true, false}
- void add(literal l) {
- sign = lit == (sign == l.sign());
- lit = !lit;
- }
- };
literal_vector lits;
- u_map<parity> var2parity;
+ u_map<bool> var2sign;
+ bool sign = false, odd = false;
for (literal lit : _lits) {
- var2parity.insert_if_not_there2(lit.var(), parity())->get_data().m_value.add(lit);
+ if (var2sign.find(lit.var(), sign)) {
+ var2sign.erase(lit.var());
+ odd ^= (sign ^ lit.sign());
+ }
+ else {
+ var2sign.insert(lit.var(), lit.sign());
+ }
}
- bool polarity = false;
- for (auto const& kv : var2parity) {
- bool lit = kv.m_value.lit;
- bool sign = kv.m_value.sign;
- if (lit)
- lits.push_back(literal(kv.m_key, sign));
- else
- polarity = polarity ^ sign;
+ for (auto const& kv : var2sign) {
+ lits.push_back(literal(kv.m_key, kv.m_value));
}
- if (polarity && !lits.empty()) {
+ if (odd && !lits.empty()) {
lits[0].neg();
}
switch (lits.size()) {
case 0:
- if (polarity)
+ if (!odd)
s().set_conflict(justification(0));
return nullptr;
case 1:
From d8e00bc02e989172b167fdbd27a5a31c07c5069d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 1 Apr 2020 00:26:02 -0700
Subject: [PATCH 10/14] fix #3644 regression introduced in #3641
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/theory_lra.cpp | 30 +++++++++++++++++-------------
1 file changed, 17 insertions(+), 13 deletions(-)
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 8d26562fd..f1754177f 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1042,6 +1042,8 @@ public:
rational r;
lp_api::bound_kind k;
theory_var v = null_theory_var;
+ bool_var bv = ctx().mk_bool_var(atom);
+ ctx().set_var_theory(bv, get_id());
if (a.is_le(atom, n1, n2) && is_numeral(n2, r) && is_app(n1)) {
v = internalize_def(to_app(n1));
k = lp_api::upper_t;
@@ -1057,10 +1059,9 @@ public:
else {
TRACE("arith", tout << "Could not internalize " << mk_pp(atom, m) << "\n";);
found_unsupported(atom);
- return false;
+ return true;
}
- bool_var bv = ctx().mk_bool_var(atom);
- ctx().set_var_theory(bv, get_id());
+
if (is_int(v) && !r.is_int()) {
r = (k == lp_api::upper_t) ? floor(r) : ceil(r);
}
@@ -2241,12 +2242,14 @@ public:
return;
}
while (m_asserted_qhead < m_asserted_atoms.size() && !ctx().inconsistent()) {
- bool_var bv = m_asserted_atoms[m_asserted_qhead].m_bv;
- bool is_true = m_asserted_atoms[m_asserted_qhead].m_is_true;
+ bool_var bv = m_asserted_atoms[m_asserted_qhead].m_bv;
+ bool is_true = m_asserted_atoms[m_asserted_qhead].m_is_true;
m_to_check.push_back(bv);
- lp_api::bound& b = *m_bool_var2bound.find(bv);
- assert_bound(bv, is_true, b);
- ++m_asserted_qhead;
+ lp_api::bound* b = nullptr;
+ if (m_bool_var2bound.find(bv, b)) {
+ assert_bound(bv, is_true, *b);
+ ++m_asserted_qhead;
+ }
}
if (ctx().inconsistent()) {
m_to_check.reset();
@@ -2691,11 +2694,12 @@ public:
}
void propagate_basic_bounds() {
- for (auto const& bv : m_to_check) {
- lp_api::bound& b = *m_bool_var2bound.find(bv);
- propagate_bound(bv, ctx().get_assignment(bv) == l_true, b);
- if (ctx().inconsistent()) break;
-
+ for (auto const& bv : m_to_check) {
+ lp_api::bound* b = nullptr;
+ if (m_bool_var2bound.find(bv, b)) {
+ propagate_bound(bv, ctx().get_assignment(bv) == l_true, *b);
+ if (ctx().inconsistent()) break;
+ }
}
m_to_check.reset();
}
From cc394f0fe9d6bb259dd55e925b655dad5c82b657 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 1 Apr 2020 03:42:13 -0700
Subject: [PATCH 11/14] na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/math/lp/lar_solver.cpp | 11 +++++------
src/math/lp/nla_core.cpp | 19 +++++++++----------
src/math/lp/u_set.h | 8 +++++++-
src/model/model_evaluator.cpp | 4 ++--
src/smt/theory_lra.cpp | 4 ++--
5 files changed, 25 insertions(+), 21 deletions(-)
diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 5772888e4..6b81d6faa 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -2395,9 +2395,7 @@ bool lar_solver::inside_bounds(lpvar j, const impq& val) const {
bool lar_solver::try_to_patch(lpvar j, const mpq& val, const std::function<bool (lpvar)>& blocker, const std::function<void (lpvar)>& report_change) {
if (is_base(j)) {
- bool r = remove_from_basis(j);
- SASSERT(r);
- (void)r;
+ VERIFY(remove_from_basis(j));
}
impq ival(val);
if (!inside_bounds(j, ival))
@@ -2409,10 +2407,10 @@ bool lar_solver::try_to_patch(lpvar j, const mpq& val, const std::function<bool
const mpq & a = c.coeff();
unsigned rj = m_mpq_lar_core_solver.m_r_basis[row_index];
impq rj_new_val = a * delta + get_column_value(rj);
- if (column_is_int(rj) && ! rj_new_val.is_int())
- return false;
+ if (column_is_int(rj) && !rj_new_val.is_int())
+ return false;
if (!inside_bounds(rj, rj_new_val) || blocker(rj))
- return false;
+ return false;
}
set_column_value(j, ival);
@@ -2423,6 +2421,7 @@ bool lar_solver::try_to_patch(lpvar j, const mpq& val, const std::function<bool
m_mpq_lar_core_solver.m_r_solver.add_delta_to_x(rj, a * delta);
report_change(rj);
}
+
return true;
}
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 28d3d2277..b42906425 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1342,18 +1342,17 @@ bool core::var_is_used_in_a_correct_monic(lpvar j) const {
void core::update_to_refine_of_var(lpvar j) {
for (const monic & m : emons().get_use_list(j)) {
- if (val(var(m)) == mul_val(m))
+ if (var_val(m) == mul_val(m))
m_to_refine.erase(var(m));
else
m_to_refine.insert(var(m));
}
if (is_monic_var(j)) {
const monic& m = emons()[j];
- if (val(var(m)) == mul_val(m))
+ if (var_val(m) == mul_val(m))
m_to_refine.erase(j);
else
- m_to_refine.insert(j);
-
+ m_to_refine.insert(j);
}
}
@@ -1373,15 +1372,15 @@ void core::patch_monomial_with_real_var(lpvar j) {
return;
if (!var_is_int(j) &&
!var_is_used_in_a_correct_monic(j)
- && try_to_patch(j, v)) {
+ && try_to_patch(j, v)
+ ) {
m_to_refine.erase(j);
} else {
rational r = val(j) / v;
for (lpvar k: m.vars()) {
- if (var_is_int(k)) continue;
- if (var_is_used_in_a_correct_monic(k))
- continue;
- if (try_to_patch(k, r * val(k))) { // r * val(k) gives the right value of k
+ if (!var_is_int(k) &&
+ !var_is_used_in_a_correct_monic(k) &&
+ try_to_patch(k, r * val(k))) { // r * val(k) gives the right value of k
m_to_refine.erase(j);
break;
}
@@ -1394,7 +1393,7 @@ void core::patch_monomial_with_real_var(lpvar j) {
void core::patch_monomials_with_real_vars() {
auto to_refine = m_to_refine.index();
- // the rest of the function might change m_to_refine, so have to copy
+ // the rest of the function might change m_to_refine, so have to copy
for (lpvar j : to_refine) {
patch_monomial_with_real_var(j);
}
diff --git a/src/math/lp/u_set.h b/src/math/lp/u_set.h
index 589ef9232..8b7cd0a5e 100644
--- a/src/math/lp/u_set.h
+++ b/src/math/lp/u_set.h
@@ -94,7 +94,7 @@ public:
m_index.resize(0);
}
- std::ostream& operator<<(std::ostream& out) const {
+ std::ostream& display(std::ostream& out) const {
for (unsigned j : m_index) {
out << j << " ";
}
@@ -105,4 +105,10 @@ public:
const unsigned * end() const { return m_index.end(); }
const unsigned_vector& index() { return m_index; }
};
+
+
+}
+
+inline std::ostream& operator<<(std::ostream& out, lp::u_set const& s) {
+ return s.display(out);
}
diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 132af4204..66ee46b86 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -160,7 +160,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
family_id fid = f->get_family_id();
bool is_uninterp = fid != null_family_id && m.get_plugin(fid)->is_considered_uninterpreted(f);
br_status st = BR_FAILED;
- if (num == 0 && (fid == null_family_id || is_uninterp)) { // || m_ar.is_as_array(f)
+ if (num == 0 && (fid == null_family_id || is_uninterp)) { // || m_ar.is_as_array(f)) {
expr * val = m_model.get_const_interp(f);
if (val != nullptr) {
result = val;
@@ -168,7 +168,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
TRACE("model_evaluator", tout << result << "\n";);
return st;
}
- else if (m_model_completion) {
+ else if (m_model_completion && !m_ar.is_as_array(f)) {
sort * s = f->get_range();
expr * val = m_model.get_some_value(s);
m_model.register_decl(f, val);
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index f1754177f..1e6e69e3a 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1561,8 +1561,8 @@ public:
void init_variable_values() {
reset_variable_values();
- if (!m.canceled() && m_solver.get() && th.get_num_vars() > 0) {
- TRACE("arith", tout << "update variable values\n";);
+ if (!m.canceled() && m_solver.get() && th.get_num_vars() > 0) {
+ TRACE("arith", display(tout << "update variable values\n"););
lp().get_model(m_variable_values);
}
}
From f98e6a62fe62490f74d8abd77f3a51d541bf0207 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 1 Apr 2020 03:49:48 -0700
Subject: [PATCH 12/14] fix #3648
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/tactic/smt_tactic.cpp | 1 +
1 file changed, 1 insertion(+)
diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp
index 9b0f8d617..a2a7f2a32 100644
--- a/src/smt/tactic/smt_tactic.cpp
+++ b/src/smt/tactic/smt_tactic.cpp
@@ -269,6 +269,7 @@ public:
if (pr) {
in->reset();
in->assert_expr(m.get_fact(pr), pr, nullptr);
+ in->updt_prec(goal::UNDER_OVER);
}
if (m_candidate_models) {
switch (m_ctx->last_failure()) {
From 3574a95e501c75bbec47a4cb054454e389f8e9b1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 1 Apr 2020 03:52:59 -0700
Subject: [PATCH 13/14] fix #3647
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/sat/sat_solver.cpp | 1 +
1 file changed, 1 insertion(+)
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index fc7ce0837..6446c9c56 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1317,6 +1317,7 @@ namespace sat {
lbool solver::do_prob_search(unsigned num_lits, literal const* lits) {
if (m_ext) return l_undef;
+ if (num_lits > 0 || !m_user_scope_literals.empty()) return l_undef;
SASSERT(!m_local_search);
m_local_search = alloc(prob);
return invoke_local_search(num_lits, lits);
From 65b2037ba271ea119cc6439baf29981a9203abcd Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 1 Apr 2020 04:07:59 -0700
Subject: [PATCH 14/14] add code review comments, add assertions (disabled for
now)
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/math/lp/nla_core.cpp | 38 ++++++++++++++++++++++----------------
1 file changed, 22 insertions(+), 16 deletions(-)
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index b42906425..787ff3f91 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1368,25 +1368,31 @@ bool core::try_to_patch(lpvar k, const rational& v) {
void core::patch_monomial_with_real_var(lpvar j) {
const monic& m = emons()[j];
rational v = mul_val(m);
- if (val(j) == v || val(j).is_zero() || v.is_zero()) // correct or a lemma will catch it
- return;
- if (!var_is_int(j) &&
- !var_is_used_in_a_correct_monic(j)
- && try_to_patch(j, v)
- ) {
+ SASSERT(j == var(m));
+ if (var_val(m) == v) {
m_to_refine.erase(j);
- } else {
- rational r = val(j) / v;
- for (lpvar k: m.vars()) {
- if (!var_is_int(k) &&
- !var_is_used_in_a_correct_monic(k) &&
- try_to_patch(k, r * val(k))) { // r * val(k) gives the right value of k
- m_to_refine.erase(j);
- break;
- }
+ return;
+ }
+ if (val(j).is_zero() || v.is_zero()) // a lemma will catch it
+ return;
+
+ if (!var_is_int(j) && !var_is_used_in_a_correct_monic(j) && try_to_patch(j, v)) {
+ // SASSERT(mul_val(m) == var_val(m));
+ m_to_refine.erase(j);
+ return;
+ }
+
+ // nsb code review: k could occur multiple times in m
+ rational r = val(j) / v;
+ for (lpvar k: m.vars()) {
+ if (!var_is_int(k) &&
+ !var_is_used_in_a_correct_monic(k) &&
+ try_to_patch(k, r * val(k))) { // r * val(k) gives the right value of k
+ // SASSERT(mul_val(m) == var_val(m));
+ m_to_refine.erase(j);
+ break;
}
}
-
}