mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix #1658 fix #1689

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-06-18 16:41:04 -07:00
parent c3b27903f8
commit 8040eddf65
5 changed files with 105 additions and 83 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

47
src/nlsat/nlsat_explain.cpp
View file

@ -574,7 +574,7 @@ namespace nlsat {
if (is_const(p)) if (is_const(p))
return; return;
if (m_factor) { 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); factor(p, m_factors);
polynomial_ref f(m_pm); polynomial_ref f(m_pm);
for (unsigned i = 0; i < m_factors.size(); i++) { for (unsigned i = 0; i < m_factors.size(); i++) {
@ -1457,7 +1457,7 @@ namespace nlsat {
process(num, ls); process(num, ls);
reset_already_added(); reset_already_added();
m_result = nullptr; 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()); CASSERT("nlsat", check_already_added());
} }
@ -1466,7 +1466,12 @@ namespace nlsat {
m_result = &result; m_result = &result;
svector<literal> lits; 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( DEBUG_CODE(
for (unsigned i = 0; i < num; ++i) { for (unsigned i = 0; i < num; ++i) {
@ -1509,8 +1514,15 @@ namespace nlsat {
result.set(i, ~result[i]); result.set(i, ~result[i]);
} }
DEBUG_CODE( DEBUG_CODE(
for (unsigned i = 0; i < result.size(); ++i) { TRACE("nlsat",
SASSERT(l_true == m_solver.value(result[i])); 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(); roots.reset();
m_am.isolate_roots(p, undef_var_assignment(m_assignment, x), roots); m_am.isolate_roots(p, undef_var_assignment(m_assignment, x), roots);
bool glb_valid = false, lub_valid = false; bool glb_valid = false, lub_valid = false;
for (unsigned j = 0; j < roots.size(); ++j) { for (auto const& r : roots) {
int s = m_am.compare(x_val, roots[j]); int s = m_am.compare(x_val, r);
SASSERT(s != 0); 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; lub_valid |= s < 0;
glb_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) { if (glb_valid) {
++num_glb; ++num_glb;
@ -1701,6 +1713,7 @@ namespace nlsat {
} }
void project_pairs(var x, unsigned idx, polynomial_ref_vector const& ps) { void project_pairs(var x, unsigned idx, polynomial_ref_vector const& ps) {
TRACE("nlsat_explain", tout << "project pairs\n";);
polynomial_ref p(m_pm); polynomial_ref p(m_pm);
p = ps.get(idx); p = ps.get(idx);
for (unsigned i = 0; i < ps.size(); ++i) { for (unsigned i = 0; i < ps.size(); ++i) {

7
src/nlsat/nlsat_scoped_literal_vector.h
View file

@ -34,9 +34,8 @@ namespace nlsat {
bool empty() const { return m_lits.empty(); } bool empty() const { return m_lits.empty(); }
literal operator[](unsigned i) const { return m_lits[i]; } literal operator[](unsigned i) const { return m_lits[i]; }
void reset() { void reset() {
unsigned sz = m_lits.size(); for (literal l : m_lits) {
for (unsigned i = 0; i < sz; i++) { m_solver.dec_ref(l);
m_solver.dec_ref(m_lits[i]);
} }
m_lits.reset(); m_lits.reset();
} }
@ -50,6 +49,8 @@ namespace nlsat {
m_lits[i] = l; m_lits[i] = l;
} }
literal const * c_ptr() const { return m_lits.c_ptr(); } 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) { void shrink(unsigned new_sz) {
SASSERT(new_sz <= m_lits.size()); SASSERT(new_sz <= m_lits.size());
unsigned sz = m_lits.size(); unsigned sz = m_lits.size();

87
src/nlsat/nlsat_solver.cpp
View file

@ -270,7 +270,7 @@ namespace nlsat {
TRACE("ref", tout << "inc: " << b << "\n";); TRACE("ref", tout << "inc: " << b << "\n";);
if (b == null_bool_var) if (b == null_bool_var)
return; return;
if (m_atoms[b] == 0) if (m_atoms[b] == nullptr)
return; return;
m_atoms[b]->inc_ref(); m_atoms[b]->inc_ref();
} }
@ -395,7 +395,7 @@ namespace nlsat {
bool_var mk_bool_var_core() { bool_var mk_bool_var_core() {
bool_var b = m_bid_gen.mk(); bool_var b = m_bid_gen.mk();
m_num_bool_vars++; 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_bvalues .setx(b, l_undef, l_undef);
m_levels .setx(b, UINT_MAX, UINT_MAX); m_levels .setx(b, UINT_MAX, UINT_MAX);
m_justifications.setx(b, null_justification, null_justification); m_justifications.setx(b, null_justification, null_justification);
@ -469,7 +469,7 @@ namespace nlsat {
//SASSERT(m_bvalues[b] == l_undef); //SASSERT(m_bvalues[b] == l_undef);
m_num_bool_vars--; m_num_bool_vars--;
m_dead[b] = true; m_dead[b] = true;
m_atoms[b] = 0; m_atoms[b] = nullptr;
m_bid_gen.recycle(b); m_bid_gen.recycle(b);
} }
@ -494,6 +494,7 @@ namespace nlsat {
void del(atom * a) { void del(atom * a) {
if (a == nullptr) if (a == nullptr)
return ; return ;
TRACE("nlsat", display(tout << "del: b" << a->m_bool_var << " ", *a) << "\n";);
if (a->is_ineq_atom()) if (a->is_ineq_atom())
del(to_ineq_atom(a)); del(to_ineq_atom(a));
else else
@ -555,6 +556,7 @@ namespace nlsat {
bool_var b = mk_bool_var_core(); bool_var b = mk_bool_var_core();
m_atoms[b] = atom; m_atoms[b] = atom;
atom->m_bool_var = b; atom->m_bool_var = b;
TRACE("nlsat", display(tout << "create: b" << atom->m_bool_var << " ", *atom) << "\n";);
return b; return b;
} }
} }
@ -749,7 +751,7 @@ namespace nlsat {
m_levels[b] = UINT_MAX; m_levels[b] = UINT_MAX;
del_jst(m_allocator, m_justifications[b]); del_jst(m_allocator, m_justifications[b]);
m_justifications[b] = null_justification; m_justifications[b] = null_justification;
if (m_atoms[b] == 0 && b < m_bk) if (m_atoms[b] == nullptr && b < m_bk)
m_bk = b; m_bk = b;
} }
@ -895,7 +897,7 @@ namespace nlsat {
\brief Assign literal using the given justification \brief Assign literal using the given justification
*/ */
void assign(literal l, justification j) { 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";); tout << "\njustification kind: " << j.get_kind() << "\n";);
SASSERT(assigned_value(l) == l_undef); SASSERT(assigned_value(l) == l_undef);
SASSERT(j != null_justification); SASSERT(j != null_justification);
@ -926,6 +928,7 @@ namespace nlsat {
*/ */
lbool value(literal l) { lbool value(literal l) {
lbool val = assigned_value(l); lbool val = assigned_value(l);
TRACE("nlsat_verbose", display(tout << " assigned value " << val << " for ", l) << "\n";);
if (val != l_undef) { if (val != l_undef) {
return val; return val;
} }
@ -941,7 +944,7 @@ namespace nlsat {
val = to_lbool(m_evaluator.eval(a, l.sign())); val = to_lbool(m_evaluator.eval(a, l.sign()));
TRACE("value_bug", tout << "value of: "; display(tout, l); tout << " := " << val << "\n"; TRACE("value_bug", tout << "value of: "; display(tout, l); tout << " := " << val << "\n";
tout << "xk: " << m_xk << ", a->max_var(): " << a->max_var() << "\n"; tout << "xk: " << m_xk << ", a->max_var(): " << a->max_var() << "\n";
display_assignment(tout);); display_assignment(tout););
return val; return val;
} }
@ -2011,9 +2014,9 @@ namespace nlsat {
} }
bool can_reorder() const { bool can_reorder() const {
for (unsigned i = 0; i < m_atoms.size(); ++i) { for (atom * a : m_atoms) {
if (m_atoms[i]) { if (a) {
if (m_atoms[i]->is_root_atom()) return false; if (a->is_root_atom()) return false;
} }
} }
return true; return true;
@ -2100,16 +2103,13 @@ namespace nlsat {
\brief After variable reordering some lemmas containing root atoms may be ill-formed. \brief After variable reordering some lemmas containing root atoms may be ill-formed.
*/ */
void del_ill_formed_lemmas() { void del_ill_formed_lemmas() {
unsigned sz = m_learned.size();
unsigned j = 0; unsigned j = 0;
for (unsigned i = 0; i < sz; i++) { for (clause* c : m_learned) {
clause * c = m_learned[i];
if (ill_formed(*c)) { if (ill_formed(*c)) {
del_clause(c); del_clause(c);
} }
else { else {
m_learned[j] = c; m_learned[j++] = c;
j++;
} }
} }
m_learned.shrink(j); m_learned.shrink(j);
@ -2119,9 +2119,8 @@ namespace nlsat {
\brief Return true if the clause contains an ill formed root atom \brief Return true if the clause contains an ill formed root atom
*/ */
bool ill_formed(clause const & c) { bool ill_formed(clause const & c) {
unsigned sz = c.size(); for (literal lit : c) {
for (unsigned i = 0; i < sz; i++) { bool_var b = lit.var();
bool_var b = c[i].var();
atom * a = m_atoms[b]; atom * a = m_atoms[b];
if (a == nullptr) if (a == nullptr)
continue; continue;
@ -2139,19 +2138,16 @@ namespace nlsat {
void reinit_cache() { void reinit_cache() {
reinit_cache(m_clauses); reinit_cache(m_clauses);
reinit_cache(m_learned); reinit_cache(m_learned);
for (unsigned i = 0; i < m_atoms.size(); ++i) { for (atom* a : m_atoms)
reinit_cache(m_atoms[i]); reinit_cache(a);
}
} }
void reinit_cache(clause_vector const & cs) { void reinit_cache(clause_vector const & cs) {
unsigned sz = cs.size(); for (clause* c : cs)
for (unsigned i = 0; i < sz; i++) reinit_cache(*c);
reinit_cache(*(cs[i]));
} }
void reinit_cache(clause const & c) { void reinit_cache(clause const & c) {
unsigned sz = c.size(); for (literal l : c)
for (unsigned i = 0; i < sz; i++) reinit_cache(l);
reinit_cache(c[i]);
} }
void reinit_cache(literal l) { void reinit_cache(literal l) {
bool_var b = l.var(); bool_var b = l.var();
@ -2566,9 +2562,12 @@ namespace nlsat {
std::ostream& display_bool_assignment(std::ostream & out) const { std::ostream& display_bool_assignment(std::ostream & out) const {
unsigned sz = m_atoms.size(); unsigned sz = m_atoms.size();
for (bool_var b = 0; b < sz; b++) { 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"; 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", TRACE("nlsat_bool_assignment",
for (bool_var b = 0; b < sz; b++) { for (bool_var b = 0; b < sz; b++) {
@ -3035,7 +3034,7 @@ namespace nlsat {
std::ostream& display_smt2_bool_decls(std::ostream & out) const { std::ostream& display_smt2_bool_decls(std::ostream & out) const {
unsigned sz = m_atoms.size(); unsigned sz = m_atoms.size();
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; i < sz; i++) {
if (m_atoms[i] == 0) if (m_atoms[i] == nullptr)
out << "(declare-fun b" << i << " () Bool)\n"; out << "(declare-fun b" << i << " () Bool)\n";
} }
return out; return out;
@ -3162,13 +3161,24 @@ namespace nlsat {
void solver::get_bvalues(svector<lbool>& vs) { void solver::get_bvalues(svector<lbool>& vs) {
vs.reset(); 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) { void solver::set_bvalues(svector<lbool> const& vs) {
TRACE("nlsat", display(tout););
m_imp->m_bvalues.reset(); m_imp->m_bvalues.reset();
m_imp->m_bvalues.append(vs); m_imp->m_bvalues.append(vs);
m_imp->m_bvalues.resize(m_imp->m_atoms.size(), l_undef); m_imp->m_bvalues.resize(m_imp->m_atoms.size(), l_undef);
TRACE("nlsat", display(tout););
} }
var solver::mk_var(bool is_int) { var solver::mk_var(bool is_int) {
@ -3199,27 +3209,28 @@ namespace nlsat {
return m_imp->mk_clause(num_lits, lits, a); return m_imp->mk_clause(num_lits, lits, a);
} }
void solver::display(std::ostream & out) const { std::ostream& solver::display(std::ostream & out) const {
m_imp->display(out); return m_imp->display(out);
} }
void solver::display(std::ostream & out, literal l) const { std::ostream& solver::display(std::ostream & out, literal l) const {
m_imp->display(out, l); 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) { for (unsigned i = 0; i < n; ++i) {
display(out, ls[i]); display(out, ls[i]);
out << "; "; out << "; ";
} }
return out;
} }
void solver::display(std::ostream & out, var x) const { std::ostream& solver::display(std::ostream & out, var x) const {
m_imp->m_display_var(out, x); return m_imp->m_display_var(out, x);
} }
void solver::display(std::ostream & out, atom const& a) const { std::ostream& solver::display(std::ostream & out, atom const& a) const {
m_imp->display(out, a, m_imp->m_display_var); return m_imp->display(out, a, m_imp->m_display_var);
} }
display_var_proc const & solver::display_proc() const { display_var_proc const & solver::display_proc() const {

10
src/nlsat/nlsat_solver.h
View file

@ -225,21 +225,21 @@ namespace nlsat {
/** /**
\brief Display solver's state. \brief Display solver's state.
*/ */
void display(std::ostream & out) const; std::ostream& display(std::ostream & out) const;
/** /**
\brief Display literal \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 \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; display_var_proc const & display_proc() const;
}; };

37
src/qe/nlqsat.cpp
View file

@ -205,8 +205,7 @@ namespace qe {
nlsat::scoped_literal_vector new_result(m_solver); nlsat::scoped_literal_vector new_result(m_solver);
result.reset(); result.reset();
// project quantified Boolean variables. // project quantified Boolean variables.
for (unsigned i = 0; i < m_asms.size(); ++i) { for (nlsat::literal lit : m_asms) {
nlsat::literal lit = m_asms[i];
if (!m_b2a.contains(lit.var()) || fvars.contains(lit.var())) { if (!m_b2a.contains(lit.var()) || fvars.contains(lit.var())) {
result.push_back(lit); result.push_back(lit);
} }
@ -215,12 +214,13 @@ namespace qe {
// project quantified real variables. // project quantified real variables.
// They are sorted by size, so we project the largest variables first to avoid // They are sorted by size, so we project the largest variables first to avoid
// renaming variables. // renaming variables.
for (unsigned i = vars.size(); i > 0;) { for (unsigned i = vars.size(); i-- > 0;) {
--i;
new_result.reset(); new_result.reset();
TRACE("qe", m_solver.display(tout << "project: ", vars[i]) << "\n";);
ex.project(vars[i], result.size(), result.c_ptr(), new_result); ex.project(vars[i], result.size(), result.c_ptr(), new_result);
result.swap(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); negate_clause(result);
} }
@ -596,6 +596,7 @@ namespace qe {
} }
void display(std::ostream& out) { void display(std::ostream& out) {
out << "level " << level() << "\n";
display_preds(out); display_preds(out);
display_assumptions(out); display_assumptions(out);
m_solver.display(out << "solver:\n"); m_solver.display(out << "solver:\n");
@ -682,7 +683,7 @@ namespace qe {
} }
else if (m_t2x.is_var(v)) { else if (m_t2x.is_var(v)) {
nlsat::var w = m_t2x.to_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_bound_rvars.back().push_back(w);
m_rvar2level.setx(w, lvl, max_level()); m_rvar2level.setx(w, lvl, max_level());
} }
@ -724,13 +725,11 @@ namespace qe {
} }
void init_var2expr() { void init_var2expr() {
expr2var::iterator it = m_t2x.begin(), end = m_t2x.end(); for (auto const& kv : m_t2x) {
for (; it != end; ++it) { m_x2t.insert(kv.m_value, kv.m_key);
m_x2t.insert(it->m_value, it->m_key);
} }
it = m_a2b.begin(), end = m_a2b.end(); for (auto const& kv : m_a2b) {
for (; it != end; ++it) { m_b2a.insert(kv.m_value, kv.m_key);
m_b2a.insert(it->m_value, it->m_key);
} }
} }
@ -741,10 +740,9 @@ namespace qe {
bool ok = true; bool ok = true;
model_ref md = alloc(model, m); model_ref md = alloc(model, m);
arith_util util(m); arith_util util(m);
expr2var::iterator it = m_t2x.begin(), end = m_t2x.end(); for (auto const& kv : m_t2x) {
for (; it != end; ++it) { nlsat::var x = kv.m_value;
nlsat::var x = it->m_value; expr * t = kv.m_key;
expr * t = it->m_key;
if (!is_uninterp_const(t) || !m_free_vars.contains(t) || m_aux_vars.contains(t)) if (!is_uninterp_const(t) || !m_free_vars.contains(t) || m_aux_vars.contains(t))
continue; continue;
expr * v; expr * v;
@ -760,10 +758,9 @@ namespace qe {
} }
md->register_decl(to_app(t)->get_decl(), v); md->register_decl(to_app(t)->get_decl(), v);
} }
it = m_a2b.begin(), end = m_a2b.end(); for (auto const& kv : m_a2b) {
for (; it != end; ++it) { expr * a = kv.m_key;
expr * a = it->m_key; nlsat::bool_var b = kv.m_value;
nlsat::bool_var b = it->m_value;
if (a == nullptr || !is_uninterp_const(a) || b == m_is_true.var() || !m_free_vars.contains(a) || m_aux_vars.contains(a)) if (a == nullptr || !is_uninterp_const(a) || b == m_is_true.var() || !m_free_vars.contains(a) || m_aux_vars.contains(a))
continue; continue;
lbool val = m_bmodel0.get(b, l_undef); lbool val = m_bmodel0.get(b, l_undef);