remove scoped

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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());
     }
 
 }

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);
     };
 
 }

src/math/polysat/constraint.cpp

@@ -21,8 +21,8 @@ Author:
 
 namespace polysat {
 
-    static_assert(!std::is_copy_assignable_v<scoped_signed_constraint>);
+    //static_assert(!std::is_copy_assignable_v<scoped_signed_constraint>);
-    static_assert(!std::is_copy_constructible_v<scoped_signed_constraint>);
+    //static_assert(!std::is_copy_constructible_v<scoped_signed_constraint>);
 
     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);
     }

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 <bool is_owned>
-    class signed_constraint_base;
-    using signed_constraint = signed_constraint_base<false>;
-    using scoped_signed_constraint = signed_constraint_base<true>;
 
     class clause;
     using clause_ref = ref<clause>;
@@ -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);
+        signed_constraint eq(unsigned lvl, pdd const& p);
-        scoped_signed_constraint ule(unsigned lvl, pdd const& a, pdd const& b);
+        signed_constraint ule(unsigned lvl, pdd const& a, pdd const& b);
-        scoped_signed_constraint ult(unsigned lvl, pdd const& a, pdd const& b);
+        signed_constraint ult(unsigned lvl, pdd const& a, pdd const& b);
-        scoped_signed_constraint sle(unsigned lvl, pdd const& a, pdd const& b);
+        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 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); }
 
-
+    class signed_constraint final {
-    // Like scoped_ptr<constraint>, 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);
-        }
-
     public:
-        scoped_constraint_ptr(constraint* ptr = nullptr): m_ptr(ptr) {}
+        using ptr_t = constraint*;
-
-        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 <bool is_owned>
-    class signed_constraint_base final {
-    public:
-        using ptr_t = std::conditional_t<is_owned, scoped_constraint_ptr, constraint*>;
 
     private:
         ptr_t m_constraint = nullptr;
         bool m_positive = true;
 
     public:
-        signed_constraint_base() {}
+        signed_constraint() {}
-        signed_constraint_base(constraint* c, bool is_positive):
+        signed_constraint(constraint* c, bool is_positive):
             m_constraint(c), m_positive(is_positive) {}
-        signed_constraint_base(constraint* c, sat::literal lit):
+        signed_constraint(constraint* c, sat::literal lit):
-            signed_constraint_base(c, !lit.sign()) {
+            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; }
+        constraint* get() const { return m_constraint; }
-        signed_constraint get_signed() const { return {get(), m_positive}; }
+
-        template <bool Owned = is_owned>
-        std::enable_if_t<Owned, constraint*> detach() { return m_constraint.detach(); }
 
         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<is_owned>& 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<is_owned> 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 <bool is_owned>
+    inline std::ostream& operator<<(std::ostream& out, signed_constraint const& c) {
-    inline std::ostream& operator<<(std::ostream& out, signed_constraint_base<is_owned> 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:

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);

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;

src/math/polysat/explain.h

@@ -20,6 +20,7 @@ Author:
 namespace polysat {
 
     class solver;
+    class conflict_explainer;
 
     class inference_engine {
     public:

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));
         }

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)

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);
+        signed_constraint mk_eq(pdd const& p);
-        scoped_signed_constraint mk_diseq(pdd const& p);
+        signed_constraint mk_diseq(pdd const& p);
-        scoped_signed_constraint mk_ule(pdd const& p, pdd const& q);
+        signed_constraint mk_ule(pdd const& p, pdd const& q);
-        scoped_signed_constraint mk_ult(pdd const& p, pdd const& q);
+        signed_constraint mk_ult(pdd const& p, pdd const& q);
-        scoped_signed_constraint mk_sle(pdd const& p, pdd const& q);
+        signed_constraint mk_sle(pdd const& p, pdd const& q);
-        scoped_signed_constraint mk_slt(pdd const& p, pdd const& q);
+        signed_constraint mk_slt(pdd const& p, pdd const& q);
-        void new_constraint(scoped_signed_constraint c, unsigned dep, bool activate);
+        void new_constraint(signed_constraint c, unsigned dep, bool activate);
         static void insert_constraint(signed_constraints& cs, signed_constraint c);
 
         bool invariant();

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);

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;