add MUS/MCS plan

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

src/muz/rel/product_set.h

@@ -122,10 +122,9 @@ namespace datalog {
             UNREACHABLE();
             return t; 
         }
-
-
     };
 
+
     typedef ptr_hashtable<product_set, product_set::hash, product_set::eq> product_sets;
 
     class product_set_relation : public relation_base {
@@ -215,6 +214,72 @@ namespace datalog {
             ptr_vector<relation_mutator_fn>& mutators);
     };
 
+    class product_set_factory;
+
+
+    class product_set2 {
+        friend class product_set_factory;
+        unsigned char m_data[0];
+    public:
+        enum initial_t {
+            EMPTY_t,
+            FULL_t
+        };
+        product_set2(product_set_factory& fac, initial_t init);
+        ~product_set2();
+        unsigned get_hash(product_set_factory& fac) const;
+        bool equals(product_set_factory& fac, product_set2 const& other) const;
+        void add_fact(product_set_factory& fac, const relation_fact & f);
+        bool contains_fact(product_set_factory& fac, const relation_fact & f) const;
+        relation_base * clone(product_set_factory& fac) const;
+        void reset(product_set_factory& fac);
+        void mk_join(product_set_factory& fac, product_set2 const& r1, product_set2 const& r2, 
+                     unsigned num_cols, unsigned const* cols1, unsigned const* cols2);
+        void mk_project(product_set_factory& fac, 
+                        product_set2 const& r, unsigned col_cnt, unsigned const* removed_cols);
+        void mk_rename(product_set_factory& fac, 
+                       product_set2 const& r, unsigned col_cnt, unsigned const* cycle);
+        void mk_union(product_set_factory& fac, 
+                      product_set2 const& src, product_set2* delta, bool is_widen);
+        unsigned find(product_set_factory& fac, unsigned i);
+        void merge(product_set_factory& fac, unsigned i, unsigned j);
+        void display(product_set_factory& fac, std::ostream& out) const;        
+    };
+
+
+    class product_set_factory {
+        friend class product_set_factory;
+        unsigned char m_data[0];
+    public:
+        enum initial_t {
+            EMPTY_t,
+            FULL_t
+        };
+        product_set_factory(product_set_plugin& p, relation_signature const& sig);
+        ~product_set_factory();
+        product_set2* create();
+        void          retire(product_set2*);
+
+        unsigned get_hash(product_set2& ps) const;
+        bool equals(product_set2 const& p1, product_set2 const& p2);
+        void add_fact(product_set2& p, const relation_fact & f);
+        bool contains_fact(product_set2& p, const relation_fact & f) const;
+        relation_base * clone(product_set2& p) const;
+        void reset(product_set2& p);
+        void mk_join(product_set2& p, product_set2 const& r1, product_set2 const& r2, 
+                     unsigned num_cols, unsigned const* cols1, unsigned const* cols2);
+        void mk_project(product_set2& p, 
+                        product_set2 const& r, unsigned col_cnt, unsigned const* removed_cols);
+        void mk_rename(product_set2& p, 
+                       product_set2 const& r, unsigned col_cnt, unsigned const* cycle);
+        void mk_union(product_set2& p, 
+                      product_set2 const& src, product_set2* delta, bool is_widen);
+        unsigned find(product_set2& p, unsigned i);
+        void merge(product_set2& p, unsigned i, unsigned j);
+        void display(product_set2& p, std::ostream& out) const;        
+    };
+
+
 };
 
 #endif

src/opt/maxres.cpp

@@ -70,6 +70,7 @@ public:
     enum strategy_t {
         s_mus,
         s_mus_mss,
+        s_mus_mss2,
         s_mss
     };
 private:
@@ -267,12 +268,54 @@ public:
         return l_true;
     }
 
+    /**
+       Plan:
+       - Get maximal set of disjoint cores.
+       - Update the lower bound using the cores.
+       - As a side-effect find a satisfying assignment that
+         has maximal weight.
+         (during core minimization several queries are bound to be SAT,
+         those can be used to boot-strap the MCS search).
+       - Use the best satisfying assignment to find an MCS of least weight.
+       - Update the upper bound using the MCS.
+       - Update the soft constraints using first the cores.
+       - Then update the resulting soft constraints using the evaluation of the MCS/MSS 
+       - Add a cardinality constraint to force new satisfying assignments to improve 
+         the new upper bound.
+       - In every iteration, the lower bound is improved using the cores.
+       - In every iteration, the upper bound is improved using the MCS
+    */
+    lbool mus_mss2_solver() {
+        init();
+        init_local();
+        sls();
+        NOT_IMPLEMENTED_YET();
+        ptr_vector<expr> mcs;
+        vector<ptr_vector<expr> > cores;
+        return l_undef;
+#if 0
+        while (m_lower < m_upper) {            
+            TRACE("opt", 
+                  display_vec(tout, m_asms.size(), m_asms.c_ptr());
+                  s().display(tout);
+                  tout << "\n";
+                  display(tout);
+                  );
+        }
+        m_lower = m_upper;
+        return l_true;
+#endif
+    }
+
+
     lbool operator()() {
         switch(m_st) {
         case s_mus:
             return mus_solver();
         case s_mus_mss:
             return mus_mss_solver();
+        case s_mus_mss2:
+            return mus_mss2_solver();
         case s_mss:
             return mss_solver();
         }