From 8040eddf6580be69ea02880fbf918978211ab40f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 18 Jun 2018 16:41:04 -0700
Subject: [PATCH] fix #1658 fix #1689
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/nlsat/nlsat_explain.cpp | 47 ++++++++-----
src/nlsat/nlsat_scoped_literal_vector.h | 7 +-
src/nlsat/nlsat_solver.cpp | 87 ++++++++++++++-----------
src/nlsat/nlsat_solver.h | 10 +--
src/qe/nlqsat.cpp | 37 +++++------
5 files changed, 105 insertions(+), 83 deletions(-)
diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index 2278e53dd..420174506 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -574,7 +574,7 @@ namespace nlsat {
if (is_const(p))
return;
if (m_factor) {
- TRACE("nlsat_explain", tout << "adding factors of\n"; display(tout, p); tout << "\n";);
+ TRACE("nlsat_explain", display(tout << "adding factors of\n", p); tout << "\n";);
factor(p, m_factors);
polynomial_ref f(m_pm);
for (unsigned i = 0; i < m_factors.size(); i++) {
@@ -1457,7 +1457,7 @@ namespace nlsat {
process(num, ls);
reset_already_added();
m_result = nullptr;
- TRACE("nlsat_explain", tout << "[explain] result\n"; display(tout, result););
+ TRACE("nlsat_explain", display(tout << "[explain] result\n", result););
CASSERT("nlsat", check_already_added());
}
@@ -1466,7 +1466,12 @@ namespace nlsat {
m_result = &result;
svector<literal> lits;
- TRACE("nlsat", tout << "project x" << x << "\n"; m_solver.display(tout););
+ TRACE("nlsat", tout << "project x" << x << "\n";
+ for (unsigned i = 0; i < num; ++i) {
+ m_solver.display(tout, ls[i]) << " ";
+ }
+ tout << "\n";
+ m_solver.display(tout););
DEBUG_CODE(
for (unsigned i = 0; i < num; ++i) {
@@ -1509,8 +1514,15 @@ namespace nlsat {
result.set(i, ~result[i]);
}
DEBUG_CODE(
- for (unsigned i = 0; i < result.size(); ++i) {
- SASSERT(l_true == m_solver.value(result[i]));
+ TRACE("nlsat",
+ for (literal l : result) {
+ m_solver.display(tout << " ", l);
+ }
+ tout << "\n";
+ );
+ for (literal l : result) {
+ CTRACE("nlsat", l_true != m_solver.value(l), m_solver.display(tout, l) << " " << m_solver.value(l) << "\n";);
+ SASSERT(l_true == m_solver.value(l));
});
}
@@ -1621,21 +1633,21 @@ namespace nlsat {
roots.reset();
m_am.isolate_roots(p, undef_var_assignment(m_assignment, x), roots);
bool glb_valid = false, lub_valid = false;
- for (unsigned j = 0; j < roots.size(); ++j) {
- int s = m_am.compare(x_val, roots[j]);
+ for (auto const& r : roots) {
+ int s = m_am.compare(x_val, r);
SASSERT(s != 0);
+
+ if (s < 0 && (!lub_valid || m_am.lt(r, lub))) {
+ lub_index = i;
+ m_am.set(lub, r);
+ }
+
+ if (s > 0 && (!glb_valid || m_am.lt(glb, r))) {
+ glb_index = i;
+ m_am.set(glb, r);
+ }
lub_valid |= s < 0;
glb_valid |= s > 0;
-
- if (s < 0 && m_am.lt(roots[j], lub)) {
- lub_index = i;
- m_am.set(lub, roots[j]);
- }
-
- if (s > 0 && m_am.lt(glb, roots[j])) {
- glb_index = i;
- m_am.set(glb, roots[j]);
- }
}
if (glb_valid) {
++num_glb;
@@ -1701,6 +1713,7 @@ namespace nlsat {
}
void project_pairs(var x, unsigned idx, polynomial_ref_vector const& ps) {
+ TRACE("nlsat_explain", tout << "project pairs\n";);
polynomial_ref p(m_pm);
p = ps.get(idx);
for (unsigned i = 0; i < ps.size(); ++i) {
diff --git a/src/nlsat/nlsat_scoped_literal_vector.h b/src/nlsat/nlsat_scoped_literal_vector.h
index 61760f06d..dffaa169f 100644
--- a/src/nlsat/nlsat_scoped_literal_vector.h
+++ b/src/nlsat/nlsat_scoped_literal_vector.h
@@ -34,9 +34,8 @@ namespace nlsat {
bool empty() const { return m_lits.empty(); }
literal operator[](unsigned i) const { return m_lits[i]; }
void reset() {
- unsigned sz = m_lits.size();
- for (unsigned i = 0; i < sz; i++) {
- m_solver.dec_ref(m_lits[i]);
+ for (literal l : m_lits) {
+ m_solver.dec_ref(l);
}
m_lits.reset();
}
@@ -50,6 +49,8 @@ namespace nlsat {
m_lits[i] = l;
}
literal const * c_ptr() const { return m_lits.c_ptr(); }
+ literal const * begin() const { return m_lits.begin(); }
+ literal const * end() const { return m_lits.end(); }
void shrink(unsigned new_sz) {
SASSERT(new_sz <= m_lits.size());
unsigned sz = m_lits.size();
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index 9767448b1..f430f3a0c 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -270,7 +270,7 @@ namespace nlsat {
TRACE("ref", tout << "inc: " << b << "\n";);
if (b == null_bool_var)
return;
- if (m_atoms[b] == 0)
+ if (m_atoms[b] == nullptr)
return;
m_atoms[b]->inc_ref();
}
@@ -395,7 +395,7 @@ namespace nlsat {
bool_var mk_bool_var_core() {
bool_var b = m_bid_gen.mk();
m_num_bool_vars++;
- m_atoms .setx(b, 0, 0);
+ m_atoms .setx(b, nullptr, nullptr);
m_bvalues .setx(b, l_undef, l_undef);
m_levels .setx(b, UINT_MAX, UINT_MAX);
m_justifications.setx(b, null_justification, null_justification);
@@ -469,7 +469,7 @@ namespace nlsat {
//SASSERT(m_bvalues[b] == l_undef);
m_num_bool_vars--;
m_dead[b] = true;
- m_atoms[b] = 0;
+ m_atoms[b] = nullptr;
m_bid_gen.recycle(b);
}
@@ -494,6 +494,7 @@ namespace nlsat {
void del(atom * a) {
if (a == nullptr)
return ;
+ TRACE("nlsat", display(tout << "del: b" << a->m_bool_var << " ", *a) << "\n";);
if (a->is_ineq_atom())
del(to_ineq_atom(a));
else
@@ -555,6 +556,7 @@ namespace nlsat {
bool_var b = mk_bool_var_core();
m_atoms[b] = atom;
atom->m_bool_var = b;
+ TRACE("nlsat", display(tout << "create: b" << atom->m_bool_var << " ", *atom) << "\n";);
return b;
}
}
@@ -749,7 +751,7 @@ namespace nlsat {
m_levels[b] = UINT_MAX;
del_jst(m_allocator, m_justifications[b]);
m_justifications[b] = null_justification;
- if (m_atoms[b] == 0 && b < m_bk)
+ if (m_atoms[b] == nullptr && b < m_bk)
m_bk = b;
}
@@ -895,7 +897,7 @@ namespace nlsat {
\brief Assign literal using the given justification
*/
void assign(literal l, justification j) {
- TRACE("nlsat", tout << "assigning literal:\n"; display(tout, l);
+ TRACE("nlsat", tout << "assigning literal: "; display(tout, l);
tout << "\njustification kind: " << j.get_kind() << "\n";);
SASSERT(assigned_value(l) == l_undef);
SASSERT(j != null_justification);
@@ -926,6 +928,7 @@ namespace nlsat {
*/
lbool value(literal l) {
lbool val = assigned_value(l);
+ TRACE("nlsat_verbose", display(tout << " assigned value " << val << " for ", l) << "\n";);
if (val != l_undef) {
return val;
}
@@ -941,7 +944,7 @@ namespace nlsat {
val = to_lbool(m_evaluator.eval(a, l.sign()));
TRACE("value_bug", tout << "value of: "; display(tout, l); tout << " := " << val << "\n";
tout << "xk: " << m_xk << ", a->max_var(): " << a->max_var() << "\n";
- display_assignment(tout););
+ display_assignment(tout););
return val;
}
@@ -2011,9 +2014,9 @@ namespace nlsat {
}
bool can_reorder() const {
- for (unsigned i = 0; i < m_atoms.size(); ++i) {
- if (m_atoms[i]) {
- if (m_atoms[i]->is_root_atom()) return false;
+ for (atom * a : m_atoms) {
+ if (a) {
+ if (a->is_root_atom()) return false;
}
}
return true;
@@ -2100,16 +2103,13 @@ namespace nlsat {
\brief After variable reordering some lemmas containing root atoms may be ill-formed.
*/
void del_ill_formed_lemmas() {
- unsigned sz = m_learned.size();
unsigned j = 0;
- for (unsigned i = 0; i < sz; i++) {
- clause * c = m_learned[i];
+ for (clause* c : m_learned) {
if (ill_formed(*c)) {
del_clause(c);
}
else {
- m_learned[j] = c;
- j++;
+ m_learned[j++] = c;
}
}
m_learned.shrink(j);
@@ -2119,9 +2119,8 @@ namespace nlsat {
\brief Return true if the clause contains an ill formed root atom
*/
bool ill_formed(clause const & c) {
- unsigned sz = c.size();
- for (unsigned i = 0; i < sz; i++) {
- bool_var b = c[i].var();
+ for (literal lit : c) {
+ bool_var b = lit.var();
atom * a = m_atoms[b];
if (a == nullptr)
continue;
@@ -2139,19 +2138,16 @@ namespace nlsat {
void reinit_cache() {
reinit_cache(m_clauses);
reinit_cache(m_learned);
- for (unsigned i = 0; i < m_atoms.size(); ++i) {
- reinit_cache(m_atoms[i]);
- }
+ for (atom* a : m_atoms)
+ reinit_cache(a);
}
void reinit_cache(clause_vector const & cs) {
- unsigned sz = cs.size();
- for (unsigned i = 0; i < sz; i++)
- reinit_cache(*(cs[i]));
+ for (clause* c : cs)
+ reinit_cache(*c);
}
void reinit_cache(clause const & c) {
- unsigned sz = c.size();
- for (unsigned i = 0; i < sz; i++)
- reinit_cache(c[i]);
+ for (literal l : c)
+ reinit_cache(l);
}
void reinit_cache(literal l) {
bool_var b = l.var();
@@ -2566,9 +2562,12 @@ namespace nlsat {
std::ostream& display_bool_assignment(std::ostream & out) const {
unsigned sz = m_atoms.size();
for (bool_var b = 0; b < sz; b++) {
- if (m_atoms[b] == 0 && m_bvalues[b] != l_undef) {
+ if (m_atoms[b] == nullptr && m_bvalues[b] != l_undef) {
out << "b" << b << " -> " << (m_bvalues[b] == l_true ? "true" : "false") << "\n";
}
+ else if (m_atoms[b] != nullptr && m_bvalues[b] != l_undef) {
+ display(out << "b" << b << " ", *m_atoms[b]) << " -> " << (m_bvalues[b] == l_true ? "true" : "false") << "\n";
+ }
}
TRACE("nlsat_bool_assignment",
for (bool_var b = 0; b < sz; b++) {
@@ -3035,7 +3034,7 @@ namespace nlsat {
std::ostream& display_smt2_bool_decls(std::ostream & out) const {
unsigned sz = m_atoms.size();
for (unsigned i = 0; i < sz; i++) {
- if (m_atoms[i] == 0)
+ if (m_atoms[i] == nullptr)
out << "(declare-fun b" << i << " () Bool)\n";
}
return out;
@@ -3162,13 +3161,24 @@ namespace nlsat {
void solver::get_bvalues(svector<lbool>& vs) {
vs.reset();
- vs.append(m_imp->m_bvalues);
+ unsigned sz = m_imp->m_bvalues.size();
+ for (bool_var b = 0; b < sz; ++b) {
+ if (m_imp->m_atoms[b] == nullptr) {
+ vs.push_back(m_imp->m_bvalues[b]);
+ }
+ else {
+ vs.push_back(l_undef); // don't save values from atoms.
+ }
+ }
+ TRACE("nlsat", display(tout););
}
void solver::set_bvalues(svector<lbool> const& vs) {
+ TRACE("nlsat", display(tout););
m_imp->m_bvalues.reset();
m_imp->m_bvalues.append(vs);
m_imp->m_bvalues.resize(m_imp->m_atoms.size(), l_undef);
+ TRACE("nlsat", display(tout););
}
var solver::mk_var(bool is_int) {
@@ -3199,27 +3209,28 @@ namespace nlsat {
return m_imp->mk_clause(num_lits, lits, a);
}
- void solver::display(std::ostream & out) const {
- m_imp->display(out);
+ std::ostream& solver::display(std::ostream & out) const {
+ return m_imp->display(out);
}
- void solver::display(std::ostream & out, literal l) const {
- m_imp->display(out, l);
+ std::ostream& solver::display(std::ostream & out, literal l) const {
+ return m_imp->display(out, l);
}
- void solver::display(std::ostream & out, unsigned n, literal const* ls) const {
+ std::ostream& solver::display(std::ostream & out, unsigned n, literal const* ls) const {
for (unsigned i = 0; i < n; ++i) {
display(out, ls[i]);
out << "; ";
}
+ return out;
}
- void solver::display(std::ostream & out, var x) const {
- m_imp->m_display_var(out, x);
+ std::ostream& solver::display(std::ostream & out, var x) const {
+ return m_imp->m_display_var(out, x);
}
- void solver::display(std::ostream & out, atom const& a) const {
- m_imp->display(out, a, m_imp->m_display_var);
+ std::ostream& solver::display(std::ostream & out, atom const& a) const {
+ return m_imp->display(out, a, m_imp->m_display_var);
}
display_var_proc const & solver::display_proc() const {
diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h
index e7b250f64..4ba1225bd 100644
--- a/src/nlsat/nlsat_solver.h
+++ b/src/nlsat/nlsat_solver.h
@@ -225,21 +225,21 @@ namespace nlsat {
/**
\brief Display solver's state.
*/
- void display(std::ostream & out) const;
+ std::ostream& display(std::ostream & out) const;
/**
\brief Display literal
*/
- void display(std::ostream & out, literal l) const;
+ std::ostream& display(std::ostream & out, literal l) const;
- void display(std::ostream & out, unsigned n, literal const* ls) const;
+ std::ostream& display(std::ostream & out, unsigned n, literal const* ls) const;
- void display(std::ostream & out, atom const& a) const;
+ std::ostream& display(std::ostream & out, atom const& a) const;
/**
\brief Display variable
*/
- void display(std::ostream & out, var x) const;
+ std::ostream& display(std::ostream & out, var x) const;
display_var_proc const & display_proc() const;
};
diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp
index d8d6705fe..95f6b9b21 100644
--- a/src/qe/nlqsat.cpp
+++ b/src/qe/nlqsat.cpp
@@ -205,8 +205,7 @@ namespace qe {
nlsat::scoped_literal_vector new_result(m_solver);
result.reset();
// project quantified Boolean variables.
- for (unsigned i = 0; i < m_asms.size(); ++i) {
- nlsat::literal lit = m_asms[i];
+ for (nlsat::literal lit : m_asms) {
if (!m_b2a.contains(lit.var()) || fvars.contains(lit.var())) {
result.push_back(lit);
}
@@ -215,12 +214,13 @@ namespace qe {
// project quantified real variables.
// They are sorted by size, so we project the largest variables first to avoid
// renaming variables.
- for (unsigned i = vars.size(); i > 0;) {
- --i;
+ for (unsigned i = vars.size(); i-- > 0;) {
new_result.reset();
+ TRACE("qe", m_solver.display(tout << "project: ", vars[i]) << "\n";);
ex.project(vars[i], result.size(), result.c_ptr(), new_result);
result.swap(new_result);
- TRACE("qe", m_solver.display(tout, result.size(), result.c_ptr()); tout << "\n";);
+ TRACE("qe", m_solver.display(tout, vars[i]) << ": ";
+ m_solver.display(tout, result.size(), result.c_ptr()); tout << "\n";);
}
negate_clause(result);
}
@@ -596,6 +596,7 @@ namespace qe {
}
void display(std::ostream& out) {
+ out << "level " << level() << "\n";
display_preds(out);
display_assumptions(out);
m_solver.display(out << "solver:\n");
@@ -682,7 +683,7 @@ namespace qe {
}
else if (m_t2x.is_var(v)) {
nlsat::var w = m_t2x.to_var(v);
- TRACE("qe", tout << mk_pp(v, m) << " |-> " << w << "\n";);
+ TRACE("qe", tout << mk_pp(v, m) << " |-> x" << w << "\n";);
m_bound_rvars.back().push_back(w);
m_rvar2level.setx(w, lvl, max_level());
}
@@ -724,13 +725,11 @@ namespace qe {
}
void init_var2expr() {
- expr2var::iterator it = m_t2x.begin(), end = m_t2x.end();
- for (; it != end; ++it) {
- m_x2t.insert(it->m_value, it->m_key);
+ for (auto const& kv : m_t2x) {
+ m_x2t.insert(kv.m_value, kv.m_key);
}
- it = m_a2b.begin(), end = m_a2b.end();
- for (; it != end; ++it) {
- m_b2a.insert(it->m_value, it->m_key);
+ for (auto const& kv : m_a2b) {
+ m_b2a.insert(kv.m_value, kv.m_key);
}
}
@@ -741,10 +740,9 @@ namespace qe {
bool ok = true;
model_ref md = alloc(model, m);
arith_util util(m);
- expr2var::iterator it = m_t2x.begin(), end = m_t2x.end();
- for (; it != end; ++it) {
- nlsat::var x = it->m_value;
- expr * t = it->m_key;
+ for (auto const& kv : m_t2x) {
+ nlsat::var x = kv.m_value;
+ expr * t = kv.m_key;
if (!is_uninterp_const(t) || !m_free_vars.contains(t) || m_aux_vars.contains(t))
continue;
expr * v;
@@ -760,10 +758,9 @@ namespace qe {
}
md->register_decl(to_app(t)->get_decl(), v);
}
- it = m_a2b.begin(), end = m_a2b.end();
- for (; it != end; ++it) {
- expr * a = it->m_key;
- nlsat::bool_var b = it->m_value;
+ for (auto const& kv : m_a2b) {
+ expr * a = kv.m_key;
+ nlsat::bool_var b = kv.m_value;
if (a == nullptr || !is_uninterp_const(a) || b == m_is_true.var() || !m_free_vars.contains(a) || m_aux_vars.contains(a))
continue;
lbool val = m_bmodel0.get(b, l_undef);