From 978bd9e560efad8ce65a2ea59091d37a81b20404 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 31 Aug 2021 08:55:48 -0700 Subject: [PATCH] remove scoped Signed-off-by: Nikolaj Bjorner --- src/math/polysat/clause_builder.cpp | 4 +- src/math/polysat/clause_builder.h | 2 +- src/math/polysat/constraint.cpp | 14 +-- src/math/polysat/constraint.h | 104 ++++------------------- src/math/polysat/eq_constraint.cpp | 2 +- src/math/polysat/eq_constraint.h | 2 +- src/math/polysat/explain.h | 1 + src/math/polysat/forbidden_intervals.cpp | 8 +- src/math/polysat/solver.cpp | 18 ++-- src/math/polysat/solver.h | 14 +-- src/math/polysat/ule_constraint.cpp | 2 +- src/math/polysat/ule_constraint.h | 2 +- 12 files changed, 52 insertions(+), 121 deletions(-) diff --git a/src/math/polysat/clause_builder.cpp b/src/math/polysat/clause_builder.cpp index 9f05296ef..1c26e7573 100644 --- a/src/math/polysat/clause_builder.cpp +++ b/src/math/polysat/clause_builder.cpp @@ -52,13 +52,13 @@ namespace polysat { m_literals.push_back(lit); } - void clause_builder::push_new_constraint(scoped_signed_constraint c) { + void clause_builder::push_new_constraint(signed_constraint c) { SASSERT(c); if (c.is_always_false()) return; m_level = std::max(m_level, c->level()); m_literals.push_back(c.blit()); - m_new_constraints.push_back(c.detach()); + m_new_constraints.push_back(c.get()); } } diff --git a/src/math/polysat/clause_builder.h b/src/math/polysat/clause_builder.h index ba1de674d..40c358caa 100644 --- a/src/math/polysat/clause_builder.h +++ b/src/math/polysat/clause_builder.h @@ -47,7 +47,7 @@ namespace polysat { void push_literal(sat::literal lit); /// Add a constraint to the clause that does not yet exist in the solver so far. - void push_new_constraint(scoped_signed_constraint c); + void push_new_constraint(signed_constraint c); }; } diff --git a/src/math/polysat/constraint.cpp b/src/math/polysat/constraint.cpp index 0abd66507..500ec0af5 100644 --- a/src/math/polysat/constraint.cpp +++ b/src/math/polysat/constraint.cpp @@ -21,8 +21,8 @@ Author: namespace polysat { - static_assert(!std::is_copy_assignable_v); - static_assert(!std::is_copy_constructible_v); + //static_assert(!std::is_copy_assignable_v); + //static_assert(!std::is_copy_constructible_v); void constraint_manager::assign_bv2c(sat::bool_var bv, constraint* c) { SASSERT_EQ(get_bv2c(bv), nullptr); @@ -185,15 +185,15 @@ namespace polysat { return true; } - scoped_signed_constraint constraint_manager::eq(unsigned lvl, pdd const& p) { + signed_constraint constraint_manager::eq(unsigned lvl, pdd const& p) { return {dedup(alloc(eq_constraint, *this, lvl, p)), true}; } - scoped_signed_constraint constraint_manager::ule(unsigned lvl, pdd const& a, pdd const& b) { + signed_constraint constraint_manager::ule(unsigned lvl, pdd const& a, pdd const& b) { return {dedup(alloc(ule_constraint, *this, lvl, a, b)), true}; } - scoped_signed_constraint constraint_manager::ult(unsigned lvl, pdd const& a, pdd const& b) { + signed_constraint constraint_manager::ult(unsigned lvl, pdd const& a, pdd const& b) { // a < b <=> !(b <= a) return ~ule(lvl, b, a); } @@ -214,12 +214,12 @@ namespace polysat { // // Argument: flipping the msb swaps the negative and non-negative blocks // - scoped_signed_constraint constraint_manager::sle(unsigned lvl, pdd const& a, pdd const& b) { + signed_constraint constraint_manager::sle(unsigned lvl, pdd const& a, pdd const& b) { auto shift = rational::power_of_two(a.power_of_2() - 1); return ule(lvl, a + shift, b + shift); } - scoped_signed_constraint constraint_manager::slt(unsigned lvl, pdd const& a, pdd const& b) { + signed_constraint constraint_manager::slt(unsigned lvl, pdd const& a, pdd const& b) { auto shift = rational::power_of_two(a.power_of_2() - 1); return ult(lvl, a + shift, b + shift); } diff --git a/src/math/polysat/constraint.h b/src/math/polysat/constraint.h index 252636a41..3cbbc6cf9 100644 --- a/src/math/polysat/constraint.h +++ b/src/math/polysat/constraint.h @@ -28,13 +28,8 @@ namespace polysat { class constraint; class eq_constraint; class ule_constraint; + class signed_constraint; - class scoped_constraint_ptr; - - template - class signed_constraint_base; - using signed_constraint = signed_constraint_base; - using scoped_signed_constraint = signed_constraint_base; class clause; using clause_ref = ref; @@ -96,11 +91,11 @@ namespace polysat { signed_constraint lookup(sat::literal lit) const; constraint* lookup_external(unsigned dep) const { return m_external_constraints.get(dep, nullptr); } - scoped_signed_constraint eq(unsigned lvl, pdd const& p); - scoped_signed_constraint ule(unsigned lvl, pdd const& a, pdd const& b); - scoped_signed_constraint ult(unsigned lvl, pdd const& a, pdd const& b); - scoped_signed_constraint sle(unsigned lvl, pdd const& a, pdd const& b); - scoped_signed_constraint slt(unsigned lvl, pdd const& a, pdd const& b); + signed_constraint eq(unsigned lvl, pdd const& p); + signed_constraint ule(unsigned lvl, pdd const& a, pdd const& b); + signed_constraint ult(unsigned lvl, pdd const& a, pdd const& b); + signed_constraint sle(unsigned lvl, pdd const& a, pdd const& b); + signed_constraint slt(unsigned lvl, pdd const& a, pdd const& b); }; @@ -183,82 +178,25 @@ namespace polysat { * \returns True iff a forbidden interval exists and the output parameters were set. */ // TODO: we can probably remove this and unify the implementations for both cases by relying on as_inequality(). - virtual bool forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, scoped_signed_constraint& out_neg_cond) { return false; } + virtual bool forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, signed_constraint& out_neg_cond) { return false; } }; inline std::ostream& operator<<(std::ostream& out, constraint const& c) { return c.display(out); } - - // Like scoped_ptr, but only deallocates the constraint if it is temporary (i.e., does not have a boolean variable). - // This is needed because when a constraint is created, due to deduplication, we might get either a new constraint or an existing one. - // (We want early deduplication because otherwise we might overlook possible boolean resolutions during conflict resolution.) - // (TODO: we could replace this class by std::unique_ptr with a custom deleter) - class scoped_constraint_ptr { - constraint* m_ptr; - - void dealloc_ptr() const { - if (m_ptr && !m_ptr->has_bvar()) - dealloc(m_ptr); - } - + class signed_constraint final { public: - scoped_constraint_ptr(constraint* ptr = nullptr): m_ptr(ptr) {} - - scoped_constraint_ptr(scoped_constraint_ptr &&other) noexcept : m_ptr(nullptr) { - std::swap(m_ptr, other.m_ptr); - } - - ~scoped_constraint_ptr() { - dealloc_ptr(); - } - - scoped_constraint_ptr& operator=(scoped_constraint_ptr&& other) { - *this = other.detach(); - return *this; - }; - - scoped_constraint_ptr& operator=(constraint* n) { - if (m_ptr != n) { - dealloc_ptr(); - m_ptr = n; - } - return *this; - } - - void swap(scoped_constraint_ptr& p) { - std::swap(m_ptr, p.m_ptr); - } - - constraint* detach() { - constraint* tmp = m_ptr; - m_ptr = nullptr; - return tmp; - } - - explicit operator bool() const { return !!m_ptr; } - bool operator!() const { return !m_ptr; } - constraint* get() const { return m_ptr; } - constraint* operator->() const { return m_ptr; } - const constraint& operator*() const { return *m_ptr; } - constraint &operator*() { return *m_ptr; } - }; - - - template - class signed_constraint_base final { - public: - using ptr_t = std::conditional_t; + using ptr_t = constraint*; private: ptr_t m_constraint = nullptr; bool m_positive = true; public: - signed_constraint_base() {} - signed_constraint_base(constraint* c, bool is_positive): + signed_constraint() {} + signed_constraint(constraint* c, bool is_positive): m_constraint(c), m_positive(is_positive) {} - signed_constraint_base(constraint* c, sat::literal lit): - signed_constraint_base(c, !lit.sign()) { + signed_constraint(constraint* c, sat::literal lit): + signed_constraint(c, !lit.sign()) { SASSERT_EQ(blit(), lit); } @@ -279,10 +217,8 @@ namespace polysat { sat::bool_var bvar() const { return m_constraint->bvar(); } sat::literal blit() const { return sat::literal(bvar(), is_negative()); } - constraint* get() const { if constexpr (is_owned) return m_constraint.get(); else return m_constraint; } - signed_constraint get_signed() const { return {get(), m_positive}; } - template - std::enable_if_t detach() { return m_constraint.detach(); } + constraint* get() const { return m_constraint; } + explicit operator bool() const { return !!m_constraint; } bool operator!() const { return !m_constraint; } @@ -290,9 +226,9 @@ namespace polysat { constraint& operator*() { return *m_constraint; } constraint const& operator*() const { return *m_constraint; } - signed_constraint_base& operator=(std::nullptr_t) { m_constraint = nullptr; return *this; } + signed_constraint& operator=(std::nullptr_t) { m_constraint = nullptr; return *this; } - bool operator==(signed_constraint_base const& other) const { + bool operator==(signed_constraint const& other) const { return get() == other.get() && is_positive() == other.is_positive(); } @@ -304,8 +240,7 @@ namespace polysat { } }; - template - inline std::ostream& operator<<(std::ostream& out, signed_constraint_base const& c) { + inline std::ostream& operator<<(std::ostream& out, signed_constraint const& c) { return c.display(out); } @@ -313,9 +248,6 @@ namespace polysat { return {c.get(), !c.is_positive()}; } - inline scoped_signed_constraint operator~(scoped_signed_constraint&& c) { - return {c.detach(), !c.is_positive()}; - } /// Disjunction of constraints represented by boolean literals // NB code review: diff --git a/src/math/polysat/eq_constraint.cpp b/src/math/polysat/eq_constraint.cpp index a5fa4b103..687dbb592 100644 --- a/src/math/polysat/eq_constraint.cpp +++ b/src/math/polysat/eq_constraint.cpp @@ -121,7 +121,7 @@ namespace polysat { /// Compute forbidden interval for equality constraint by considering it as p <=u 0 (or p >u 0 for disequality) - bool eq_constraint::forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, scoped_signed_constraint& out_neg_cond) + bool eq_constraint::forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, signed_constraint& out_neg_cond) { // Current only works when degree(v) is at most one unsigned const deg = p().degree(v); diff --git a/src/math/polysat/eq_constraint.h b/src/math/polysat/eq_constraint.h index dd05aec74..859d782ec 100644 --- a/src/math/polysat/eq_constraint.h +++ b/src/math/polysat/eq_constraint.h @@ -31,7 +31,7 @@ namespace polysat { bool is_currently_false(solver& s, bool is_positive) override; bool is_currently_true(solver& s, bool is_positive) override; void narrow(solver& s, bool is_positive) override; - bool forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, scoped_signed_constraint& out_neg_cond) override; + bool forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, signed_constraint& out_neg_cond) override; inequality as_inequality(bool is_positive) const override; unsigned hash() const override; bool operator==(constraint const& other) const override; diff --git a/src/math/polysat/explain.h b/src/math/polysat/explain.h index 714d2c579..0ae629f1e 100644 --- a/src/math/polysat/explain.h +++ b/src/math/polysat/explain.h @@ -20,6 +20,7 @@ Author: namespace polysat { class solver; + class conflict_explainer; class inference_engine { public: diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp index b68083158..e1d409ffe 100644 --- a/src/math/polysat/forbidden_intervals.cpp +++ b/src/math/polysat/forbidden_intervals.cpp @@ -22,7 +22,7 @@ namespace polysat { struct fi_record { eval_interval interval; - scoped_signed_constraint neg_cond; // could be multiple constraints later + signed_constraint neg_cond; // could be multiple constraints later signed_constraint src; }; @@ -74,7 +74,7 @@ namespace polysat { for (signed_constraint c : conflict) { LOG_H3("Computing forbidden interval for: " << c); eval_interval interval = eval_interval::full(); - scoped_signed_constraint neg_cond; + signed_constraint neg_cond; if (c->forbidden_interval(s, c.is_positive(), v, interval, neg_cond)) { LOG("interval: " << interval); LOG("neg_cond: " << neg_cond); @@ -160,12 +160,12 @@ namespace polysat { auto const& next_hi = records[next_i].interval.hi(); auto const& lhs = hi - next_lo; auto const& rhs = next_hi - next_lo; - scoped_signed_constraint c = ~s.m_constraints.ult(lemma_lvl, lhs, rhs); + signed_constraint c = ~s.m_constraints.ult(lemma_lvl, lhs, rhs); LOG("constraint: " << c); clause.push_new_constraint(std::move(c)); // Side conditions // TODO: check whether the condition is subsumed by c? maybe at the end do a "lemma reduction" step, to try and reduce branching? - scoped_signed_constraint& neg_cond = records[i].neg_cond; + signed_constraint& neg_cond = records[i].neg_cond; if (neg_cond) clause.push_new_constraint(std::move(neg_cond)); } diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index cfcab64eb..9ea6b9abe 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -114,36 +114,34 @@ namespace polysat { m_free_vars.del_var_eh(v); } - scoped_signed_constraint solver::mk_eq(pdd const& p) { + signed_constraint solver::mk_eq(pdd const& p) { return m_constraints.eq(m_level, p); } - scoped_signed_constraint solver::mk_diseq(pdd const& p) { + signed_constraint solver::mk_diseq(pdd const& p) { return ~m_constraints.eq(m_level, p); } - scoped_signed_constraint solver::mk_ule(pdd const& p, pdd const& q) { + signed_constraint solver::mk_ule(pdd const& p, pdd const& q) { return m_constraints.ule(m_level, p, q); } - scoped_signed_constraint solver::mk_ult(pdd const& p, pdd const& q) { + signed_constraint solver::mk_ult(pdd const& p, pdd const& q) { return m_constraints.ult(m_level, p, q); } - scoped_signed_constraint solver::mk_sle(pdd const& p, pdd const& q) { + signed_constraint solver::mk_sle(pdd const& p, pdd const& q) { return m_constraints.sle(m_level, p, q); } - scoped_signed_constraint solver::mk_slt(pdd const& p, pdd const& q) { + signed_constraint solver::mk_slt(pdd const& p, pdd const& q) { return m_constraints.slt(m_level, p, q); } - void solver::new_constraint(scoped_signed_constraint sc, unsigned dep, bool activate) { + void solver::new_constraint(signed_constraint c, unsigned dep, bool activate) { VERIFY(at_base_level()); - SASSERT(sc); + SASSERT(c); SASSERT(activate || dep != null_dependency); // if we don't activate the constraint, we need the dependency to access it again later. - signed_constraint c = sc.get_signed(); - sc.detach(); clause* unit = m_constraints.store(clause::from_unit(c, mk_dep_ref(dep))); c->set_unit_clause(unit); if (dep != null_dependency) diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 5a4e1fe80..4d34faf53 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -219,13 +219,13 @@ namespace polysat { void backjump(unsigned new_level); void add_lemma(clause_ref lemma); - scoped_signed_constraint mk_eq(pdd const& p); - scoped_signed_constraint mk_diseq(pdd const& p); - scoped_signed_constraint mk_ule(pdd const& p, pdd const& q); - scoped_signed_constraint mk_ult(pdd const& p, pdd const& q); - scoped_signed_constraint mk_sle(pdd const& p, pdd const& q); - scoped_signed_constraint mk_slt(pdd const& p, pdd const& q); - void new_constraint(scoped_signed_constraint c, unsigned dep, bool activate); + signed_constraint mk_eq(pdd const& p); + signed_constraint mk_diseq(pdd const& p); + signed_constraint mk_ule(pdd const& p, pdd const& q); + signed_constraint mk_ult(pdd const& p, pdd const& q); + signed_constraint mk_sle(pdd const& p, pdd const& q); + signed_constraint mk_slt(pdd const& p, pdd const& q); + void new_constraint(signed_constraint c, unsigned dep, bool activate); static void insert_constraint(signed_constraints& cs, signed_constraint c); bool invariant(); diff --git a/src/math/polysat/ule_constraint.cpp b/src/math/polysat/ule_constraint.cpp index b0c8f88d6..1475be0e7 100644 --- a/src/math/polysat/ule_constraint.cpp +++ b/src/math/polysat/ule_constraint.cpp @@ -113,7 +113,7 @@ namespace polysat { return p.is_val() && q.is_val() && p.val() > q.val(); } - bool ule_constraint::forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, scoped_signed_constraint& out_neg_cond) + bool ule_constraint::forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, signed_constraint& out_neg_cond) { // Current only works when degree(v) is at most one on both sides unsigned const deg1 = lhs().degree(v); diff --git a/src/math/polysat/ule_constraint.h b/src/math/polysat/ule_constraint.h index 4a1a6372a..1872d3c17 100644 --- a/src/math/polysat/ule_constraint.h +++ b/src/math/polysat/ule_constraint.h @@ -37,7 +37,7 @@ namespace polysat { bool is_currently_false(solver& s, bool is_positive) override; bool is_currently_true(solver& s, bool is_positive) override; void narrow(solver& s, bool is_positive) override; - bool forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, scoped_signed_constraint& out_neg_cond) override; + bool forbidden_interval(solver& s, bool is_positive, pvar v, eval_interval& out_interval, signed_constraint& out_neg_cond) override; inequality as_inequality(bool is_positive) const override; unsigned hash() const override; bool operator==(constraint const& other) const override;