add code review to constraint

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

src/math/polysat/constraint.cpp

@@ -259,7 +259,7 @@ namespace polysat {
             if (lit.var() != var)
                 m_literals[j++] = lit;
         m_literals.shrink(j);
-        for (sat::literal lit : other.literals())
+        for (sat::literal lit : other)
             if (lit.var() != var)
                 m_literals.push_back(lit);
         return true;
@@ -267,7 +267,7 @@ namespace polysat {
 
     std::ostream& clause::display(std::ostream& out) const {
         bool first = true;
-        for (auto lit : literals()) {
+        for (auto lit : *this) {
             if (first)
                 first = false;
             else

src/math/polysat/constraint.h

@@ -24,7 +24,6 @@ Author:
 namespace polysat {
 
     enum ckind_t { eq_t, ule_t };
-    enum csign_t : bool { neg_t = false, pos_t = true };
 
     class constraint;
     class eq_constraint;
@@ -55,9 +54,19 @@ namespace polysat {
         constraint_table m_constraint_table;
 
         // Constraint storage per level
+
         vector<scoped_ptr_vector<constraint>> m_constraints;
         vector<vector<clause_ref>> m_clauses;
 
+        // NB code review: Elsewhere we use flat arrays for m_constraints, m_clauses and then
+        //         unsigned_vector m_constraints_lim;
+        //         unsigned        m_clauses_lim;
+        // The code for 'release_level' would require rewriting and the assumptions about how many
+        // scopes are released have to be revisited then. ~constraint_manager calls release_level
+        // to gc remaining constraints and ensure destruction. It's possible this call is not
+        // needed since memory management is scoped.
+
+        
         // Association to external dependency values (i.e., external names for constraints)
         u_map<constraint*> m_external_constraints;
 
@@ -126,6 +135,8 @@ namespace polysat {
          *  If this is not null_bool_var, then the constraint corresponds to a literal on the assignment stack.
          *  Convention: the plain constraint corresponds the positive sat::literal.
          */
+        // NB code review: the convention would make sense. Unfortunately, elsewhere in z3 we use "true" for negative literals
+        // and "false" for positive literals. It is called the "sign" bit.
         sat::bool_var       m_bvar = sat::null_bool_var;
 
         constraint(constraint_manager& m, unsigned lvl, ckind_t k):
@@ -137,8 +148,8 @@ namespace polysat {
     public:
         virtual ~constraint() {}
 
-	    virtual unsigned hash() const = 0;
+        virtual unsigned hash() const = 0;
-	    virtual bool operator==(constraint const& other) const = 0;
+        virtual bool operator==(constraint const& other) const = 0;
 
         bool is_eq() const { return m_kind == ckind_t::eq_t; }
         bool is_ule() const { return m_kind == ckind_t::ule_t; }
@@ -296,7 +307,9 @@ namespace polysat {
     };
 
     template <bool is_owned>
-    inline std::ostream& operator<<(std::ostream& out, signed_constraint_base<is_owned> const& c) { return c.display(out); }
+    inline std::ostream& operator<<(std::ostream& out, signed_constraint_base<is_owned> const& c) {
+        return c.display(out);
+    }
 
     inline signed_constraint operator~(signed_constraint const& c) {
         return {c.get(), !c.is_positive()};
@@ -306,8 +319,12 @@ namespace polysat {
         return {c.detach(), !c.is_positive()};
     }
 
-
     /// Disjunction of constraints represented by boolean literals
+    // NB code review:
+    // right, ref-count is unlikely the right mechanism.
+    // In the SAT solver all clauses are managed in one arena (auxiliarary and redundant)
+    // and deleted when they exist the arena.
+    //
     class clause {
         friend class constraint_manager;
 
@@ -327,8 +344,7 @@ namespace polysat {
         */
 
         clause(unsigned lvl, p_dependency_ref d, sat::literal_vector literals):
-            m_level(lvl), m_dep(std::move(d)), m_literals(std::move(literals))
+            m_level(lvl), m_dep(std::move(d)), m_literals(std::move(literals)) {
-        {
             SASSERT(std::count(m_literals.begin(), m_literals.end(), sat::null_literal) == 0);
         }
 
@@ -342,7 +358,6 @@ namespace polysat {
         // Resolve with 'other' upon 'var'.
         bool resolve(sat::bool_var var, clause const& other);
 
-        sat::literal_vector const& literals() const { return m_literals; }
         p_dependency* dep() const { return m_dep; }
         unsigned level() const { return m_level; }
 
@@ -358,7 +373,7 @@ namespace polysat {
         bool is_currently_false(solver& s) const;
 
         unsigned next_guess() {
-            SASSERT(m_next_guess < m_literals.size());
+            SASSERT(m_next_guess < size());
             return m_next_guess++;
         }
 

src/math/polysat/solver.cpp

@@ -699,8 +699,8 @@ namespace polysat {
         clause* cl = lemma.get();
         add_lemma(std::move(lemma));
         if (cl->size() == 1) {
-            sat::literal lit = cl->literals()[0];
+	    sat::literal lit = (*cl)[0];
-            signed_constraint c = m_constraints.lookup(lit);
+	    signed_constraint c = m_constraints.lookup(lit);
             c->set_unit_clause(cl);
             push_cjust(v, c);
             activate_constraint_base(c);
@@ -904,8 +904,8 @@ namespace polysat {
     void solver::propagate_bool(sat::literal lit, clause* reason) {
         LOG("Propagate boolean literal " << lit << " @ " << m_level << " by " << show_deref(reason));
         SASSERT(reason);
-        if (reason->literals().size() == 1) {
+        if (reason->size() == 1) {
-            SASSERT(reason->literals()[0] == lit);
+            SASSERT((*reason)[0] == lit);
             signed_constraint c = m_constraints.lookup(lit);
             // m_redundant.push_back(c);
             activate_constraint_base(c);
@@ -989,7 +989,7 @@ namespace polysat {
         clause* cl = m_constraints.store(std::move(lemma));
         m_redundant_clauses.push_back(cl);
         if (cl->size() == 1) {
-            signed_constraint c = m_constraints.lookup(cl->literals()[0]);
+            signed_constraint c = m_constraints.lookup((*cl)[0]);
             insert_constraint(m_redundant, c);
         }
     }

src/util/scoped_ptr_vector.h

@@ -81,6 +81,7 @@ public:
         m_vector[m_vector.size()-1] = tmp;
     }
 
+
     ptr_vector<T> detach() {
         ptr_vector<T> tmp(std::move(m_vector));
         SASSERT(m_vector.empty());