local changes

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

src/smt/theory_pb.cpp

@@ -227,7 +227,43 @@ namespace smt {
         SASSERT(sum >= k());
         return true;
     }
-    
+
+    // cardinality
+
+    //
+    // 
+    lbool theory_pb::cardinality::assign_at_least(theory_pb& th, literal lit) {
+        // literal is assigned to false.
+        context& ctx = th.get_context();
+        SASSERT(m_type == le_t);
+        SASSERT(m_bound > 0);
+        SASSERT(m_args.size() >= 2*m_bound);
+        SASSERT(m_watch_sum < m_bound);
+        unsigned index = m_bound + 1;
+        bool all_false = true;
+        for (unsigned i = 0; i <= m_bound; ++i) {
+            if (m_args[i] == lit) {
+                index = i;
+                break;
+            }
+            all_false &= (value(args[i]) == l_false);
+        }
+        
+        for (unsigned i = m_bound + 1; i < m_args.size(); ++i) {
+            if (value(m_args[i]) != l_false) {
+                std::swap(m_args[index], m_args[i]);
+                // watch m_args[index] now
+                // end-clause-case
+            }
+        }
+
+        if (all_false) {
+            
+        }        
+
+        return l_undef;
+    }
+
     theory_pb::theory_pb(ast_manager& m, theory_pb_params& p):
         theory(m.mk_family_id("pb")),
         m_params(p),

src/smt/theory_pb.h

@@ -181,6 +181,55 @@ namespace smt {
 
         };
 
+        enum card_t {
+            eq_t,
+            le_t,
+            ge_t
+        };
+
+        struct cardinality {
+            literal         m_lit;      // literal repesenting predicate
+            card_t          m_type;
+            literal_vector  m_args;
+            unsigned        m_bound;
+            unsigned        m_watch_sum;
+            unsigned        m_num_propagations;
+            unsigned        m_compilation_threshold;
+            lbool           m_compiled;
+            
+            cardinality(literal l, card_t t, unsigned bound):
+                m_lit(l),
+                m_type(t),
+                m_bound(bound),
+                m_watch_sum(0),
+                m_num_propagations(0),
+                m_compilation_threshold(0),
+                m_compiled(0)
+            {}            
+
+            std::ostream& display(std::ostream& out) const;
+
+            app_ref to_expr(context& ctx);
+
+            lbool assign_at_least(literal lit);
+            //
+            // lit occurs within m_bound positions
+            // m_bound <= m_args.size()/2
+            // m_lit is pos
+            // type at least: m_args >= m_bound
+            //   lit occurs with opposite sign in m_args
+            // type at most: m_args <= m_bound
+            //   lit occurs with same sign in m_args
+            // search for literal above m_bound, such that 
+            // either lit' is positive, type = ge_t
+            //        lit' is negative, type = le_t
+            //        lit' is unassigned
+            // swap lit and lit' in watch list
+            // If there is a single unassigned lit', and no other to swap, perform unit propagation
+            // If there are no literals to swap with, then create conflict clause
+            // 
+        };
+
         struct row_info {
             unsigned     m_slack;   // slack variable in simplex tableau
             numeral      m_bound;   // bound
@@ -216,9 +265,6 @@ namespace smt {
         theory_pb_params         m_params;        
 
         svector<var_info>        m_var_infos; 
-//        u_map<watch_list*>       m_lwatch;      // per literal.
-//        u_map<watch_list*>       m_vwatch;      // per variable.
-//        u_map<ineq*>             m_ineqs;       // per inequality.
         arg_map                  m_ineq_rep;       // Simplex: representative inequality
         u_map<row_info>          m_ineq_row_info;  // Simplex: row information per variable
         uint_set                 m_vars;           // Simplex: 0-1 variables.