From 04f94d818fdd2e5a5718b48114417719b5703c32 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 11 Jun 2022 11:56:32 -0700 Subject: [PATCH] fix #6091 --- src/sat/sat_drat.cpp | 22 +++++++++++----------- src/sat/sat_drat.h | 4 ++-- src/smt/theory_arith.h | 2 +- src/smt/theory_arith_nl.h | 17 +++++++++++++---- 4 files changed, 27 insertions(+), 18 deletions(-) diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp index 7557a885e..073110077 100644 --- a/src/sat/sat_drat.cpp +++ b/src/sat/sat_drat.cpp @@ -217,7 +217,7 @@ namespace sat { return; if (m_check_unsat) { - assign_propagate(l); + assign_propagate(l, nullptr); m_units.push_back({l, nullptr}); } } @@ -249,9 +249,9 @@ namespace sat { if (value(l1) == l_false && value(l2) == l_false) m_inconsistent = true; else if (value(l1) == l_false) - assign_propagate(l2); + assign_propagate(l2, &c); else if (value(l2) == l_false) - assign_propagate(l1); + assign_propagate(l1, &c); } } @@ -319,7 +319,7 @@ namespace sat { m_inconsistent = true; break; case 1: - assign_propagate(l1); + assign_propagate(l1, &c); break; default: { SASSERT(num_watch == 2); @@ -363,7 +363,7 @@ namespace sat { unsigned num_units = m_units.size(); for (unsigned i = 0; !m_inconsistent && i < n; ++i) { declare(c[i]); - assign_propagate(~c[i]); + assign_propagate(~c[i], nullptr); } for (unsigned i = num_units; i < m_units.size(); ++i) @@ -384,7 +384,7 @@ namespace sat { return false; unsigned num_units = m_units.size(); for (unsigned i = 0; !m_inconsistent && i < n; ++i) - assign_propagate(~c[i]); + assign_propagate(~c[i], nullptr); DEBUG_CODE(if (!m_inconsistent) validate_propagation();); DEBUG_CODE( @@ -595,7 +595,7 @@ namespace sat { return val == l_undef || !l.sign() ? val : ~val; } - void drat::assign(literal l) { + void drat::assign(literal l, clause* c) { lbool new_value = l.sign() ? l_false : l_true; lbool old_value = value(l); // TRACE("sat_drat", tout << "assign " << l << " := " << new_value << " from " << old_value << "\n";); @@ -607,16 +607,16 @@ namespace sat { break; case l_undef: m_assignment.setx(l.var(), new_value, l_undef); - m_units.push_back({l, nullptr}); + m_units.push_back({l, c}); break; } } - void drat::assign_propagate(literal l) { + void drat::assign_propagate(literal l, clause* c) { if (!m_check_unsat) return; unsigned num_units = m_units.size(); - assign(l); + assign(l, c); for (unsigned i = num_units; !m_inconsistent && i < m_units.size(); ++i) propagate(m_units[i].first); } @@ -661,7 +661,7 @@ namespace sat { else { *it2 = *it; it2++; - assign(wc.m_l1); + assign(wc.m_l1, &c); } } } diff --git a/src/sat/sat_drat.h b/src/sat/sat_drat.h index 2408e5d8e..18ca7b7b8 100644 --- a/src/sat/sat_drat.h +++ b/src/sat/sat_drat.h @@ -105,9 +105,9 @@ namespace sat { status get_status(bool learned) const; void declare(literal l); - void assign(literal l); + void assign(literal l, clause* c); void propagate(literal l); - void assign_propagate(literal l); + void assign_propagate(literal l, clause* c); void del_watch(clause& c, literal l); bool is_drup(unsigned n, literal const* c); bool is_drat(unsigned n, literal const* c); diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 6e1d77dd4..a1054423a 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -974,7 +974,7 @@ namespace smt { /** \brief A monomial is 'pure' if does not have a numeric coefficient. */ - bool is_pure_monomial(expr * m) const { return m_util.is_mul(m) && (to_app(m)->get_num_args() > 2 || !m_util.is_numeral(to_app(m)->get_arg(0))); } + bool is_pure_monomial(expr * m) const; bool is_pure_monomial(theory_var v) const { return is_pure_monomial(get_enode(v)->get_expr()); } void mark_var(theory_var v, svector & vars, var_set & already_found); void mark_dependents(theory_var v, svector & vars, var_set & already_found, row_set & already_visited_rows); diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index d73f604c1..044a42e7e 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -624,11 +624,9 @@ template bool theory_arith::check_monomial_assignments() { bool computed_epsilon = false; for (theory_var v : m_nl_monomials) { - TRACE("non_linear", tout << "v" << v << " is relevant: " << ctx.is_relevant(get_enode(v)) << "\n"; - tout << "check_monomial_assignments result: " << check_monomial_assignment(v, computed_epsilon) << "\n"; - tout << "computed_epsilon: " << computed_epsilon << "\n";); + TRACE("non_linear", tout << "v" << v << " is relevant: " << ctx.is_relevant(get_enode(v)) << "\n"); if (ctx.is_relevant(get_enode(v)) && !check_monomial_assignment(v, computed_epsilon)) { - TRACE("non_linear_failed", tout << "check_monomial_assignment failed for:\n" << mk_ismt2_pp(var2expr(v), get_manager()) << "\n"; + TRACE("non_linear", tout << "check_monomial_assignment failed for:\n" << mk_ismt2_pp(var2expr(v), get_manager()) << "\n"; display_var(tout, v);); return false; } @@ -1254,6 +1252,17 @@ bool theory_arith::in_monovariate_monomials(buffer & p, expr * } +template +bool theory_arith::is_pure_monomial(expr* mon) const { + if (!m_util.is_mul(mon)) + return false; + app* p = to_app(mon); + for (expr* arg : *p) + if (m_util.is_numeral(arg) || m_util.is_mul(arg)) + return false; + return true; +} + /** \brief Display a nested form expression */