Merge branch 'opt' of https://git01.codeplex.com/z3 into opt

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:
@@ -83,6 +84,7 @@ private:
     strategy_t       m_st;
     rational         m_max_upper;
     bool             m_hill_climb;
+    bool             m_all_cores;
 
 public:
     maxres(context& c,
@@ -94,7 +96,8 @@ public:
         m_mss(m_s, m),
         m_trail(m),
         m_st(st),
-        m_hill_climb(true)
+        m_hill_climb(true),
+        m_all_cores(false)
     {
     }
 
@@ -150,21 +153,9 @@ public:
                 return l_undef;
             }
             switch (is_sat) {
-            case l_true: {
-                s().get_model(m_model);
-                expr_ref tmp(m);
-                DEBUG_CODE(
-                    for (unsigned i = 0; i < m_asms.size(); ++i) {
-                        VERIFY(m_model->eval(m_asms[i].get(), tmp));                        
-                        SASSERT(m.is_true(tmp));
-                    });
-                for (unsigned i = 0; i < m_soft.size(); ++i) {
-                    VERIFY(m_model->eval(m_soft[i].get(), tmp));
-                    m_assignment[i] = m.is_true(tmp);
-                }
-                m_upper = m_lower;
+            case l_true: 
+                found_optimum();
                 return l_true;
-            }
             case l_false:
                 is_sat = process_unsat();
                 if (is_sat != l_true) return is_sat;
@@ -267,12 +258,104 @@ 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 from the MUS search 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.
+       - Optionally: add a cardinality constraint to prune the upper bound.
+       
+       What are the corner cases:
+       - suppose that cost of cores adds up to current upper bound.
+         -> it means that each core is a unit (?)
+       
+    */
+    lbool mus_mss2_solver() {
+        init();
+        init_local();
+        sls();
+        m_all_cores = true;
+        NOT_IMPLEMENTED_YET();
+        vector<ptr_vector<expr> > cores;
+        return l_undef;
+        lbool is_sat = l_true;
+        while (m_lower < m_upper && is_sat == l_true) {            
+            TRACE("opt", 
+                  display_vec(tout, m_asms.size(), m_asms.c_ptr());
+                  s().display(tout);
+                  tout << "\n";
+                  display(tout);
+                  );
+            lbool is_sat = s().check_sat(m_asms.size(), m_asms.c_ptr());
+            if (m_cancel) {
+                return l_undef;
+            }
+            switch (is_sat) {
+            case l_true: 
+                found_optimum();
+                return l_true;
+            case l_false:
+                is_sat = process_unsat(cores);
+                break;
+            default:
+                break;
+            }
+            if (is_sat == l_undef) {
+                return l_undef;
+            }
+            if (cores.empty()) {
+                SASSERT(is_sat == l_false);
+                break;
+            }
+            SASSERT(is_sat == l_true);
+            // there is some best model, 
+            // extend it to a maximal assignment
+            // extracting the mss and mcs.
+            set_mus(false);
+            ptr_vector<expr> mss, mcs;
+            is_sat = m_mss(cores, mss, mcs);
+            set_mus(true);
+            if (is_sat != l_true) return is_sat;
+            // 
+        }
+        m_lower = m_upper;
+        return l_true;
+    }
+
+    void found_optimum() {
+        s().get_model(m_model);
+        expr_ref tmp(m);
+        DEBUG_CODE(
+            for (unsigned i = 0; i < m_asms.size(); ++i) {
+                VERIFY(m_model->eval(m_asms[i].get(), tmp));                        
+                SASSERT(m.is_true(tmp));
+            });
+        for (unsigned i = 0; i < m_soft.size(); ++i) {
+            VERIFY(m_model->eval(m_soft[i].get(), tmp));
+            m_assignment[i] = m.is_true(tmp);
+        }
+        m_upper = m_lower;
+    }
+
+
     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();
         }
@@ -293,8 +376,7 @@ public:
                 break;
             }
             cores.push_back(core);
-            // TBD: ad hoc to avoid searching for large cores..
-            if (core.size() >= 3) {
+            if (!m_all_cores && core.size() >= 3) {
                 break;
             }
             remove_soft(core, asms);
@@ -361,7 +443,7 @@ public:
         return index;
     }
 
-    lbool process_sat(ptr_vector<expr>& corr_set) {
+    lbool process_sat(ptr_vector<expr> const& corr_set) {
         expr_ref fml(m), tmp(m);
         TRACE("opt", display_vec(tout << "corr_set: ", corr_set.size(), corr_set.c_ptr()););
         if (corr_set.empty()) {
@@ -377,6 +459,10 @@ public:
 
     lbool process_unsat() {
         vector<ptr_vector<expr> > cores;
+        return process_unsat(cores);
+    }
+
+    lbool process_unsat(vector<ptr_vector<expr> >& cores) {
         lbool is_sat = get_cores(cores);
         if (is_sat != l_true) {
             return is_sat;
@@ -390,7 +476,7 @@ public:
         return is_sat;
     }
     
-    lbool process_unsat(ptr_vector<expr>& core) {
+    lbool process_unsat(ptr_vector<expr> const& core) {
         expr_ref fml(m);
         remove_core(core);
         rational w = split_core(core);
@@ -404,7 +490,7 @@ public:
     }
 
     lbool minimize_core(ptr_vector<expr>& core) {
-        if (m_c.sat_enabled()) {
+        if (m_c.sat_enabled() || core.empty()) {
             return l_true;
         }
         m_mus.reset();
@@ -473,7 +559,7 @@ public:
         }
     }
 
-    void max_resolve(ptr_vector<expr>& core, rational const& w) {
+    void max_resolve(ptr_vector<expr> const& core, rational const& w) {
         SASSERT(!core.empty());
         expr_ref fml(m), asum(m);
         app_ref cls(m), d(m), dd(m);
@@ -515,7 +601,7 @@ public:
     }
 
     // cs is a correction set (a complement of a (maximal) satisfying assignment).
-    void cs_max_resolve(ptr_vector<expr>& cs, rational const& w) {
+    void cs_max_resolve(ptr_vector<expr> const& cs, rational const& w) {
         TRACE("opt", display_vec(tout << "correction set: ", cs.size(), cs.c_ptr()););
         SASSERT(!cs.empty());
         expr_ref fml(m), asum(m);

src/opt/maxsmt.cpp

@@ -41,7 +41,7 @@ namespace opt {
         m_c(c),
         m_cancel(false), m_soft(m),
         m_assertions(m) {
-        m_s.get_model(m_model);
+        c.get_base_model(m_model);
         SASSERT(m_model);
         updt_params(c.params());
         init_soft(ws, soft);

src/opt/opt_context.cpp

@@ -215,7 +215,7 @@ namespace opt {
         case 0:
             return is_sat;
         case 1:
-            return execute(m_objectives[0], true);
+            return execute(m_objectives[0], true, false);
         default: {
             opt_params optp(m_params);
             symbol pri = optp.priority();
@@ -232,6 +232,10 @@ namespace opt {
         }
     }
 
+    void context::get_base_model(model_ref& mdl) {
+        mdl = m_model;
+    }
+
     void context::get_model(model_ref& mdl) {
         mdl = m_model;
         if (mdl) {
@@ -242,27 +246,31 @@ namespace opt {
         }
     }
 
-    lbool context::execute_min_max(unsigned index, bool committed) {
+    lbool context::execute_min_max(unsigned index, bool committed, bool scoped) {
+        if (scoped) get_solver().push();            
         lbool result = m_optsmt.lex(index);
-        if (result == l_true && committed) m_optsmt.commit_assignment(index);
         if (result == l_true) m_optsmt.get_model(m_model);
+        if (scoped) get_solver().pop(1);        
+        if (result == l_true && committed) m_optsmt.commit_assignment(index);
         return result;
     }
     
-    lbool context::execute_maxsat(symbol const& id, bool committed) {
+    lbool context::execute_maxsat(symbol const& id, bool committed, bool scoped) {
         model_ref tmp;
         maxsmt& ms = *m_maxsmts.find(id);
+        if (scoped) get_solver().push();            
         lbool result = ms(m_solver.get());
-        if (result == l_true && committed) ms.commit_assignment();
         if (result != l_false && (ms.get_model(tmp), tmp.get())) ms.get_model(m_model);
+        if (scoped) get_solver().pop(1);
+        if (result == l_true && committed) ms.commit_assignment();
         return result;
     }
 
-    lbool context::execute(objective const& obj, bool committed) {
+    lbool context::execute(objective const& obj, bool committed, bool scoped) {
         switch(obj.m_type) {
-        case O_MAXIMIZE: return execute_min_max(obj.m_index, committed);
-        case O_MINIMIZE: return execute_min_max(obj.m_index, committed);
-        case O_MAXSMT: return execute_maxsat(obj.m_id, committed);
+        case O_MAXIMIZE: return execute_min_max(obj.m_index, committed, scoped);
+        case O_MINIMIZE: return execute_min_max(obj.m_index, committed, scoped);
+        case O_MAXSMT: return execute_maxsat(obj.m_id, committed, scoped);
         default: UNREACHABLE(); return l_undef;
         }
     }
@@ -271,9 +279,7 @@ namespace opt {
         lbool r = l_true;
         for (unsigned i = 0; r == l_true && i < m_objectives.size(); ++i) {
             bool is_last = i + 1 == m_objectives.size();
-            if (!is_last) get_solver().push();            
-            r = execute(m_objectives[i], i + 1 < m_objectives.size());
-            if (!is_last) get_solver().pop(1);
+            r = execute(m_objectives[i], i + 1 < m_objectives.size(), !is_last);
             if (r == l_true && !get_lower_as_num(i).is_finite()) {
                 return r;
             }
@@ -291,7 +297,7 @@ namespace opt {
             objective const& obj = m_objectives[i];
             if (obj.m_type == O_MAXSMT) {
                 solver::scoped_push _sp(get_solver());
-                r = execute(obj, false);
+                r = execute(obj, false, false);
             }
         }
         return r;
@@ -399,9 +405,6 @@ namespace opt {
         if (is_sat == l_true) {
             yield();
         }
-        else {
-            m_solver->pop(1);
-        }
         return is_sat;
     }
 

src/opt/opt_context.h

@@ -179,14 +179,15 @@ namespace opt {
         void enable_sls(expr_ref_vector const& soft, weights_t& weights);
         void set_enable_sls(bool f) { m_enable_sls = f; }
         symbol const& maxsat_engine() const { return m_maxsat_engine; }
+        void get_base_model(model_ref& m);
 
 
     private:
         void validate_feasibility(maxsmt& ms);
 
-        lbool execute(objective const& obj, bool committed);
-        lbool execute_min_max(unsigned index, bool committed);
-        lbool execute_maxsat(symbol const& s, bool committed);
+        lbool execute(objective const& obj, bool committed, bool scoped);
+        lbool execute_min_max(unsigned index, bool committed, bool scoped);
+        lbool execute_maxsat(symbol const& s, bool committed, bool scoped);
         lbool execute_lex();
         lbool execute_box();
         lbool execute_pareto();