From 689c5b4e123cae99426941a99d06efdea5b030bd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Sep 2021 16:46:30 +0100 Subject: [PATCH] generalize level Signed-off-by: Nikolaj Bjorner --- src/math/polysat/conflict_core.cpp | 8 +++++--- src/math/polysat/constraint.cpp | 12 ++++++++++-- src/math/polysat/constraint.h | 5 ++++- src/math/polysat/solver.cpp | 11 +++++++++-- src/math/polysat/ule_constraint.cpp | 5 +++-- src/test/polysat.cpp | 17 +++++++++-------- 6 files changed, 40 insertions(+), 18 deletions(-) diff --git a/src/math/polysat/conflict_core.cpp b/src/math/polysat/conflict_core.cpp index eb919d336..65de89a05 100644 --- a/src/math/polysat/conflict_core.cpp +++ b/src/math/polysat/conflict_core.cpp @@ -186,11 +186,13 @@ namespace polysat { auto& premises = it->m_value; clause_builder c_lemma(s()); for (auto premise : premises) { + LOG_H3("premise: " << premise); keep(premise); - SASSERT(premise->has_bvar()); - SASSERT(premise.bvalue(s()) == l_true); // otherwise the propagation doesn't make sense + SASSERT(premise->has_bvar()); + SASSERT(premise.is_currently_true(s()) || premise.bvalue(s()) == l_true); + // otherwise the propagation doesn't make sense c_lemma.push(~premise.blit()); - active_level = std::max(active_level, s().m_bvars.level(premise.blit())); + active_level = std::max(active_level, premise.level(s())); } c_lemma.push(c.blit()); clause* cl = cm().store(c_lemma.build()); diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp index 85721bd18..cbd53ce6c 100644 --- a/src/math/polysat/constraint.cpp +++ b/src/math/polysat/constraint.cpp @@ -219,11 +219,10 @@ namespace polysat { return *dynamic_cast(this); } - std::ostream& constraint::display_extra(std::ostream& out, lbool status) const { + std::ostream& constraint::display_extra(std::ostream& out) const { out << " (b"; if (has_bvar()) { out << bvar(); } else { out << "_"; } out << ")"; - (void)status; return out; } @@ -261,6 +260,15 @@ namespace polysat { m_unit_clause = cl; } + unsigned constraint::level(solver& s) const { + if (s.m_bvars.value(sat::literal(bvar())) != l_undef) + return s.m_bvars.level(bvar()); + unsigned level = 0; + for (auto v : vars()) + level = std::max(level, s.get_level(v)); + return level; + } + lbool signed_constraint::bvalue(solver& s) const { return s.m_bvars.value(blit()); } diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h index fae03b839..1451fe7e1 100644 --- a/src/math/polysat/constraint.h +++ b/src/math/polysat/constraint.h @@ -148,7 +148,7 @@ namespace polysat { constraint(constraint_manager& m, ckind_t k): m_kind(k) {} protected: - std::ostream& display_extra(std::ostream& out, lbool status) const; + std::ostream& display_extra(std::ostream& out) const; public: virtual ~constraint() {} @@ -179,6 +179,7 @@ namespace polysat { bool contains_var(pvar v) const { return m_vars.contains(v); } bool has_bvar() const { return m_bvar != sat::null_bool_var; } sat::bool_var bvar() const { return m_bvar; } + unsigned level(solver& s) const; clause* unit_clause() const { return m_unit_clause; } void set_unit_clause(clause* cl); @@ -231,12 +232,14 @@ namespace polysat { bool is_currently_false(solver& s) const { return get()->is_currently_false(s, is_positive()); } bool is_currently_true(solver& s) const { return get()->is_currently_true(s, is_positive()); } lbool bvalue(solver& s) const; + unsigned level(solver& s) const { return get()->level(s); } void narrow(solver& s) { get()->narrow(s, is_positive()); } inequality as_inequality() const { return get()->as_inequality(is_positive()); } sat::bool_var bvar() const { return m_constraint->bvar(); } sat::literal blit() const { return sat::literal(bvar(), is_negative()); } constraint* get() const { return m_constraint; } + explicit operator bool() const { return !!m_constraint; } bool operator!() const { return !m_constraint; } diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index 2278eeb9f..0966ae8cc 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -744,15 +744,22 @@ namespace polysat { void solver::add_lemma(clause_ref lemma) { if (!lemma) return; + bool non_propagated_literal = false; LOG("Lemma: " << show_deref(lemma)); for (sat::literal lit : *lemma) { LOG(" Literal " << lit << " is: " << m_constraints.lookup(lit)); signed_constraint c = m_constraints.lookup(lit); // Check that fully evaluated constraints are on the stack - SASSERT(m_bvars.is_assigned(lit) || !c.is_currently_false(*this)); - SASSERT(m_bvars.is_assigned(lit) || !c.is_currently_true(*this)); + SASSERT(!c.is_currently_true(*this)); + // literals that are added from m_conflict.m_vars have not been assigned. + // they are false in the current model. + if (!m_bvars.is_assigned(lit) && c.is_currently_false(*this)) { + non_propagated_literal = true; + } + // SASSERT(m_bvars.is_assigned(lit) || !c.is_currently_false(*this)); // TODO: work out invariant for the lemma. It should be impossible to extend the model in a way that makes the lemma true. } + // SASSERT(!non_propagated_literal); SASSERT(lemma->size() > 0); clause* cl = m_constraints.store(std::move(lemma)); if (cl->size() == 1) { diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp index eab319365..05620739b 100644 --- a/src/math/polysat/ule_constraint.cpp +++ b/src/math/polysat/ule_constraint.cpp @@ -39,7 +39,7 @@ namespace polysat { else if (status == l_false) out << " > "; else out << " <=/> "; out << m_rhs; - return display_extra(out, status); + return display_extra(out); } std::ostream& ule_constraint::display(std::ostream& out) const { @@ -48,7 +48,8 @@ namespace polysat { out << " == "; else out << " <= "; - return out << m_rhs; + out << m_rhs; + return display_extra(out); } void ule_constraint::narrow(solver& s, bool is_positive) { diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp index cea7a999d..94a1ab33a 100644 --- a/src/test/polysat.cpp +++ b/src/test/polysat.cpp @@ -869,17 +869,13 @@ namespace polysat { void tst_polysat() { // not working // polysat::test_fixed_point_arith_div_mul_inverse(); - // polysat::test_cjust(); - polysat::test_ineq_basic5(); - // polysat::test_ineq_basic6(); - // polysat::test_monot_bounds_full(); - // polysat::test_monot_bounds_simple(8); - // working + polysat::test_cjust(); + //polysat::test_monot_bounds_simple(8); return; + + // working polysat::test_fixed_point_arith_mul_div_inverse(); - - polysat::test_subst(); polysat::test_monot_bounds(8); @@ -898,8 +894,13 @@ void tst_polysat() { polysat::test_ineq_basic2(); polysat::test_ineq_basic3(); polysat::test_ineq_basic4(); + polysat::test_ineq_basic5(); + polysat::test_ineq_basic6(); polysat::test_monot_bounds(2); + // inefficient conflicts: + // Takes time: polysat::test_monot_bounds_full(); + #if 0 // worry about this later polysat::test_ineq1();