v2 of dual maxres engine

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

src/opt/inc_sat_solver.cpp

@@ -89,7 +89,7 @@ public:
         m_solver.pop_to_base_level();
         dep2asm_t dep2asm;
 
-        m_model.reset();
+        m_model = 0;
         lbool r = internalize_formulas();
         if (r != l_true) return r;
         r = internalize_assumptions(num_assumptions, assumptions, dep2asm);
@@ -161,7 +161,7 @@ public:
         r.append(m_core.size(), m_core.c_ptr());
     }
     virtual void get_model(model_ref & m) {
-        if (!m_model) {
+        if (!m_model.get()) {
             extract_model();
         }
         m = m_model;
@@ -275,6 +275,7 @@ private:
     // bit-blasting model converter.
 
     void extract_model() {
+        TRACE("sat", tout << "retrieve model\n";);
         model_ref md = alloc(model, m);
         sat::model const & ll_m = m_solver.get_model();
         atom2bool_var::iterator it  = m_map.begin();
@@ -300,6 +301,7 @@ private:
         if (m_mc) {
             (*m_mc)(m_model);
         }
+        SASSERT(m_model);
         // IF_VERBOSE(0, model_smt2_pp(verbose_stream(), m, *(m_model.get()), 0););
 
     }

src/opt/maxres.cpp

@@ -58,10 +58,10 @@ Notes:
 #include "maxres.h"
 #include "ast_pp.h"
 #include "mus.h"
+#include "mss.h"
 
 using namespace opt;
 
-
 class maxres : public maxsmt_solver_base {
 public:
     enum strategy_t {
@@ -75,8 +75,10 @@ private:
     obj_map<expr, rational> m_asm2weight;
     ptr_vector<expr> m_new_core;
     mus              m_mus;
+    mss              m_mss;
     expr_ref_vector  m_trail;
     strategy_t       m_st;
+    rational         m_max_upper;
 
 public:
     maxres(ast_manager& m, opt_solver* s, params_ref& p, 
@@ -85,6 +87,7 @@ public:
         maxsmt_solver_base(s, m, p, ws, soft),
         m_B(m), m_asms(m),
         m_mus(m_s, m),
+        m_mss(m_s, m),
         m_trail(m),
         m_st(st)
     {
@@ -168,7 +171,6 @@ public:
             default:
                 break;
             }
-            IF_VERBOSE(1, verbose_stream() << "(opt.max_res [" << m_lower << ":" << m_upper << "])\n";);
         }
         return l_true;
     }
@@ -179,8 +181,7 @@ public:
         init_local();
         enable_bvsat();
         enable_sls();
-        lbool was_sat = l_false;
+        ptr_vector<expr> mcs;
-        ptr_vector<expr> soft_compl;
         vector<ptr_vector<expr> > cores;
         while (m_lower < m_upper) {            
             TRACE("opt", 
@@ -189,37 +190,38 @@ public:
                   tout << "\n";
                   display(tout);
                   );
-            lbool is_sat = m_s->check_sat(0, 0);
+            lbool is_sat = try_improve_bound(cores, mcs);
             if (m_cancel) {
                 return l_undef;
             }
-            if (is_sat == l_true) {
-                was_sat = l_true;
-                is_sat = extend_model(soft_compl);
-                switch (is_sat) {
-                case l_undef:
-                    break;
-                case l_false:
-                    is_sat = process_unsat();
-                    break;
-                case l_true:
-                    is_sat = process_sat(soft_compl);
-                    break;
-                }
-            }
             switch (is_sat) {
             case l_undef:
                 return l_undef;
             case l_false:
+                SASSERT(cores.empty() && mcs.empty());
                 m_lower = m_upper;
-                return was_sat;
+                return l_true;
             case l_true:
+                SASSERT(cores.empty() || mcs.empty());
+                SASSERT(!cores.empty() || !mcs.empty());
+                for (unsigned i = 0; is_sat == l_true && i < cores.size(); ++i) {
+                    is_sat = process_unsat(cores[i]);
+                }
+                if (is_sat == l_true && !mcs.empty()) {
+                    is_sat = process_sat(mcs);
+                }
+                if (is_sat != l_true) {
+                    return is_sat;
+                }
                 break;
             }
         }
-        return was_sat;
+        m_lower = m_lower;        
+        return l_true;
     }
 
+
+
     lbool mss_solver() {
         NOT_IMPLEMENTED_YET();
         return l_undef;
@@ -314,6 +316,7 @@ public:
         fml = m.mk_not(m.mk_and(m_B.size(), m_B.c_ptr()));
         m_s->assert_expr(fml);
         m_lower += w;
+        IF_VERBOSE(1, verbose_stream() << "(opt.maxres [" << m_lower << ":" << m_upper << "])\n";);
         return l_true;
     }
 
@@ -422,6 +425,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) {
+        TRACE("opt", display_vec(tout << "correction set: ", cs.size(), cs.c_ptr()););
         SASSERT(!cs.empty());
         expr_ref fml(m), asum(m);
         app_ref cls(m), d(m), dd(m);
@@ -437,6 +441,7 @@ public:
         // asm => b_i
         // asm => d_{i-1} or b_{i-1}
         // d_i => d_{i-1} or b_{i-1}
+        //
         for (unsigned i = 1; i < cs.size(); ++i) {
             expr* b_i = m_B[i-1].get();
             expr* b_i1 = m_B[i].get();
@@ -460,82 +465,89 @@ public:
         m_s->assert_expr(fml);
     }
 
-    //
+    lbool try_improve_bound(vector<ptr_vector<expr> >& cores, ptr_vector<expr>& mcs) {
-    // The hard constraints are satisfiable.
+        cores.reset();
-    // Extend the current model to satisfy as many
+        mcs.reset();
-    // soft constraints as possible until either
+        ptr_vector<expr> core;
-    // hitting an unsatisfiable subset of size < 1/2*#assumptions,
+        expr_ref_vector asms(m_asms);
-    // or producing a maximal satisfying assignment exceeding 
+        while (true) {
-    // number of soft constraints >= 1/2*#assumptions.
+            rational upper = m_max_upper;
-    // In both cases, soft constraints that are not satisfied 
+            unsigned sz = 0;
-    // is <= 1/2*#assumptions. In this way, the new modified assumptions
+            for (unsigned i = 0; m_upper <= upper && i < asms.size(); ++i, ++sz) {
-    // account for at most 1/2 of the current assumptions.
+                upper -= get_weight(asms[i].get());
-    // The core reduction algorithms also need to take into account
+            }
-    // at most 1/2 of the assumptions for minimization.
+            lbool is_sat = m_s->check_sat(sz, asms.c_ptr());
-    // 
-
-    lbool extend_model(ptr_vector<expr>& soft_compl) {
-        ptr_vector<expr> asms;
-        model_ref mdl;
-        expr_ref tmp(m);
-        m_s->get_model(mdl);
-        unsigned num_true = update_model(mdl, asms, soft_compl);
-        for (unsigned j = 0; j < m_asms.size(); ++j) {
-            expr* fml = m_asms[j].get();
-            VERIFY(mdl->eval(fml, tmp));
-            if (m.is_false(tmp)) {
-                asms.push_back(fml);
-                lbool is_sat = m_s->check_sat(asms.size(), asms.c_ptr());
-                asms.pop_back();
             switch (is_sat) {
-                case l_false:
+            case l_true: {
-                    if (num_true*2 < m_asms.size()) {
+                ptr_vector<expr> lits;
-                        return l_false;
+                lits.append(asms.size(), asms.c_ptr());
-                    }
+                set_mus(false);
-                    break;
+                is_sat = m_mss(cores, lits);
-                case l_true:
+                set_mus(true);
-                    m_s->get_model(mdl);
+                if (is_sat != l_true) {
-                    num_true = update_model(mdl, asms, soft_compl);
+                    return is_sat;
-                    break;
-                case l_undef:
-                    return l_undef;
-                }
                 }
+                m_mss.get_model(m_model); // last model is best way to reduce search space.
+                update_assignment();
+                if (cores.empty() || asms.size() < cores.back().size()) {
+                    cores.reset();
+                    mcs.append(asms.size(), asms.c_ptr());                    
                 }
                 return l_true;
             }
+            case l_undef:
+                return l_undef;
+            case l_false:
+                core.reset();
+                m_s->get_unsat_core(core);
+                is_sat = minimize_core(core);
+                if (is_sat != l_true) {
+                    break;
+                }
+                if (core.empty()) {
+                    cores.reset();
+                    mcs.reset();
+                    return l_false;
+                }
+                cores.push_back(core);
+                if (core.size() >= 3) {
+                    return l_true;
+                }
+                //
+                // check arithmetic: cannot improve upper bound
+                //
+                if (m_upper <= upper) {
+                    return l_true;
+                }
                 
-    unsigned update_model(model_ref& mdl, ptr_vector<expr>& asms, ptr_vector<expr>& soft_compl) {
+                remove_soft(core, asms);
-        expr_ref tmp(m);
+                break;
-        asms.reset();
-        soft_compl.reset();
-        rational weight = m_lower;
-        unsigned num_true = 0;
-        for (unsigned i = 0; i < m_asms.size(); ++i) {
-            expr* fml = m_asms[i].get();
-            VERIFY(mdl->eval(fml, tmp));
-            SASSERT(m.is_false(tmp) || m.is_true(tmp));            
-            if (m.is_false(tmp)) {
-                weight += get_weight(fml);
-                soft_compl.push_back(fml);
-            }
-            else {
-                ++num_true;
-                asms.push_back(fml);
             }
         }
-        if (weight < m_upper) {
+        
-            m_upper = weight;
+        return l_undef;
-            m_model = mdl;
+    }
+
+
+    void update_assignment() {
+        rational upper(0);
         for (unsigned i = 0; i < m_soft.size(); ++i) {
             expr_ref tmp(m);
-                VERIFY(m_model->eval(m_soft[i].get(), tmp));
+            expr* n = m_soft[i].get();
+            VERIFY(m_model->eval(n, tmp));
+            CTRACE("opt", !m.is_true(tmp) && !m.is_false(tmp), 
+                   tout << mk_pp(n, m) << " |-> " << mk_pp(tmp, m) << "\n";);
+
             m_assignment[i] = m.is_true(tmp);
+            if (!m_assignment[i]) {
+                upper += m_weights[i];
             }
+        }
+        SASSERT(upper <= m_upper);
+        m_upper = upper;
         IF_VERBOSE(1, verbose_stream() << 
-                       "(opt.mus-mss_max_res [" << m_lower << ":" << m_upper << "])\n";);
+                   "(opt.maxres [" << m_lower << ":" << m_upper << "])\n";);
-        }
+
-        return num_true;
     }
 
     void remove_soft(ptr_vector<expr> const& core, expr_ref_vector& asms) {
@@ -564,6 +576,7 @@ public:
         for (unsigned i = 0; i < m_soft.size(); ++i) {
             add_soft(m_soft[i].get(), m_weights[i]);
         }
+        m_max_upper = m_upper;
     }
 
 };

src/opt/maxsmt.cpp

@@ -138,8 +138,6 @@ namespace opt {
         m_s = sat_solver;
     }
 
-
-
     void maxsmt_solver_base::enable_bvsat()  {
         if (m_enable_sat && !m_sat_enabled && probe_bv()) {
             enable_inc_bvsat();
@@ -159,6 +157,12 @@ namespace opt {
         }
     }       
 
+    void maxsmt_solver_base::set_mus(bool f) {
+        params_ref p;
+        p.set_bool("minimize_core", f);
+        m_s->updt_params(p);
+    }
+
     app* maxsmt_solver_base::mk_fresh_bool(char const* name) {
         app* result = m.mk_fresh_const(name, m.mk_bool_sort());
         m_mc->insert(result->get_decl());

src/opt/maxsmt.h

@@ -94,6 +94,7 @@ namespace opt {
         void init();
         expr* mk_not(expr* e);
         bool probe_bv();
+        void set_mus(bool f);
         void enable_bvsat();
         void enable_sls();
         app* mk_fresh_bool(char const* name);

src/opt/mss.cpp

@@ -27,35 +27,74 @@ Notes:
 namespace opt {
 
 
-    mss::mss(solver& s, ast_manager& m): s(s), m(m), m_cancel(false) {
+    mss::mss(ref<solver>& s, ast_manager& m): m_s(s), m(m), m_cancel(false) {
     }
     
     mss::~mss() {
     }    
 
+    bool mss::check_result() {
+        lbool is_sat = m_s->check_sat(m_mss.size(), m_mss.c_ptr());
+        if (is_sat == l_undef) return true;
+        SASSERT(is_sat == l_true);
+        if (is_sat == l_false) return false;
+        expr_set::iterator it = m_mcs.begin(), end = m_mcs.end();
+        for (; it != end; ++it) {
+            m_mss.push_back(*it);
+            is_sat = m_s->check_sat(m_mss.size(), m_mss.c_ptr());
+            m_mss.pop_back();
+            if (is_sat == l_undef) return true;
+            SASSERT(is_sat == l_false);
+            if (is_sat == l_true) return false;
+        }
+        return true;
+    }
 
-    void mss::check_parameters(vector<exprs > const& cores, exprs& literals) {
+    void mss::initialize(vector<exprs>& cores, exprs& literals) {
         expr* n;
+        expr_set lits, core_lits;
         for (unsigned i = 0; i < literals.size(); ++i) {
             n = literals[i];
+            lits.insert(n);
             m.is_not(n, n);
             if (!is_uninterp_const(n)) {
                 throw default_exception("arguments have to be uninterpreted literals");
             }
         }
-        // cores are disjoint
+        exprs rest_core;
-        // cores are a subset of literals
-        // literals not in cores evaluate to true in current model
-    }
-
-    /**
-       \brief Move literals satisfied in todo into mss.
-       Precondition: the solver state is satisfiable.
-    */
-    void mss::update_model() {
         expr_ref tmp(m);
-        s.get_model(m_model);
+        //
-        update_set(m_todo);
+        // the last core is a dummy core. It contains literals that
+        // did not occur in previous cores and did not evaluate to true
+        // in the current model.
+        //
+        for (unsigned i = 0; i < cores.size(); ++i) {
+            exprs const& core = cores[i];
+            for (unsigned j = 0; j < core.size(); ++j) {
+                expr* n = core[j];
+                if (!core_lits.contains(n)) {
+                    core_lits.insert(n);
+                    VERIFY(m_model->eval(n, tmp));
+                    if (m.is_true(tmp)) {
+                        m_mss.push_back(n);
+                    }
+                }
+            }
+        }
+        for (unsigned i = 0; i < literals.size(); ++i) {
+            expr* n = literals[i];
+            if (!core_lits.contains(n)) {
+                VERIFY(m_model->eval(n, tmp));
+                if (m.is_true(tmp)) {
+                    m_mss.push_back(n);
+                }
+                else {
+                    rest_core.push_back(n);
+                    core_lits.insert(n);
+                }
+            }
+        }
+        cores.push_back(rest_core);
     }
     
     void mss::update_set(exprs& lits) {
@@ -69,7 +108,7 @@ namespace opt {
                 continue;
             }
             VERIFY(m_model->eval(n, tmp));
-            if (m.is_false(tmp)) {
+            if (!m.is_true(tmp)) {
                 if (j != i) {
                     lits[j] = lits[i];
                 }
@@ -83,33 +122,44 @@ namespace opt {
     }
     
     
-    lbool mss::operator()(vector<exprs> const& cores, exprs& literals) {
+    lbool mss::operator()(vector<exprs> const& _cores, exprs& literals) {
         m_mss.reset();
         m_mcs.reset();
-        m_todo.reset();
+        m_s->get_model(m_model);
-        m_todo.append(literals);
+        SASSERT(m_model);
-        check_parameters(cores, literals);
+        vector<exprs> cores(_cores);
-        update_model();
+        TRACE("opt", 
+              for (unsigned i = 0; i < cores.size(); ++i) {
+                  display_vec(tout << "core: ", cores[i].size(), cores[i].c_ptr());
+              }
+              display_vec(tout << "lits: ", literals.size(), literals.c_ptr());
+              );
+        initialize(cores, literals);
+        TRACE("opt", display(tout););
         lbool is_sat = l_true;
         for (unsigned i = 0; is_sat == l_true && i < cores.size(); ++i) {
-            is_sat = process_core(cores[i]);
+            bool has_mcs = false;
+            bool is_last = i + 1 < cores.size();
+            SASSERT(check_invariant());
+            update_set(cores[i]);
+            is_sat = process_core(1, cores[i], has_mcs, is_last);
         }    
         if (is_sat == l_true) {
+            SASSERT(check_invariant());
+            TRACE("opt", display(tout););
             literals.reset();
             literals.append(m_mss);
+            SASSERT(check_result());
         }
         return is_sat;
     }
 
-    lbool mss::process_core(exprs const& _core) {
+    
+    //
     // at least one literal in core is false in current model.
     // pick literals in core that are not yet in mss.
-        exprs core(_core);
+    //    
-        update_set(core);
+    lbool mss::process_core(unsigned sz, exprs& core, bool& has_mcs, bool is_last) {
-        return process_core(1, core);    
-    }
-    
-    lbool mss::process_core(unsigned sz, exprs& core) {
         TRACE("opt", tout << "process: " << sz << " out of " << core.size() << " literals\n";);
         SASSERT(sz > 0);
         if (core.empty()) {
@@ -118,18 +168,25 @@ namespace opt {
         if (m_cancel) {
             return l_undef;
         }
+        if (sz == 1 && is_last && !has_mcs) {
+            // there has to be at least one false 
+            // literal in the core. 
+            m_mcs.insert(core[0]);
+            return l_true;
+        }
         sz = std::min(sz, core.size());
         unsigned sz_save = m_mss.size();
         m_mss.append(sz, core.c_ptr());
-        lbool is_sat = s.check_sat(m_mss.size(), m_mss.c_ptr());
+        lbool is_sat = m_s->check_sat(m_mss.size(), m_mss.c_ptr());
         m_mss.resize(sz_save);
         switch (is_sat) {
         case l_true:
-            update_model();
+            m_s->get_model(m_model);
             update_set(core);
-            return process_core(2*sz, core);
+            return process_core(2*sz, core, has_mcs, is_last);
         case l_false:
             if (sz == 1) {
+                has_mcs = true;
                 m_mcs.insert(core[0]);
                 core[0] = core.back();
                 core.pop_back();
@@ -138,12 +195,12 @@ namespace opt {
                 exprs core2;            
                 core2.append(core.size()-sz, core.c_ptr()+sz);
                 core.resize(sz);
-                is_sat = process_core(sz, core2);
+                is_sat = process_core(sz, core2, has_mcs, false);
                 if (is_sat != l_true) {
                     return is_sat;
                 }
             }
-            return process_core(1, core);
+            return process_core(1, core, has_mcs, is_last);
         case l_undef:
             return l_undef;
         }
@@ -151,8 +208,41 @@ namespace opt {
         return l_true;
     }
 
+    void mss::display_vec(std::ostream& out, unsigned sz, expr* const* args) const {
+        for (unsigned i = 0; i < sz; ++i) {
+            out << mk_pp(args[i], m) << " ";
+        }
+        out << "\n";
+    }
+
     void mss::display(std::ostream& out) const {
+        expr_set::iterator it = m_mcs.begin(), end = m_mcs.end();
+        out << "mcs:\n";
+        for (; it != end; ++it) {
+            out << mk_pp(*it, m) << "\n";
+        }
+        out << "\n";
+        out << "mss:\n";
+        for (unsigned i = 0; i < m_mss.size(); ++i) {
+            out << mk_pp(m_mss[i], m) << "\n";
+        }
+        out << "\n";
+        if (m_model) {
+            model_smt2_pp(out, m, *(m_model.get()), 0);
+        }
+    }
 
+    bool mss::check_invariant() const {
+        if (!m_model) return true;
+        expr_ref tmp(m);
+        for (unsigned i = 0; i < m_mss.size(); ++i) {
+            expr* n = m_mss[i];
+            VERIFY(m_model->eval(n, tmp));
+            CTRACE("opt", !m.is_true(tmp), tout << mk_pp(n, m) << " |-> " << mk_pp(tmp, m) << "\n";);
+            SASSERT(!m.is_false(tmp));
+        }
+
+        return true;
     }
 }
 

src/opt/mss.h

@@ -21,30 +21,34 @@ Notes:
 
 namespace opt {
     class mss {
-        solver&       s;
+        ref<solver>&  m_s;
         ast_manager&  m;
         volatile bool m_cancel;
         typedef ptr_vector<expr> exprs;
         typedef obj_hashtable<expr>  expr_set;
         exprs         m_mss;
         expr_set      m_mcs;
-        exprs         m_todo;
         model_ref     m_model;
     public:
-        mss(solver& s, ast_manager& m);
+        mss(ref<solver>& s, ast_manager& m);
         ~mss();
         
-        lbool operator()(vector<ptr_vector<expr> > const& cores, ptr_vector<expr>& literals);
+        lbool operator()(vector<exprs> const& cores, exprs& literals);
                 
         void set_cancel(bool f) { m_cancel = f; }
 
+        void get_model(model_ref& mdl) { mdl = m_model; }
+
     private:
-        void  check_parameters(vector<exprs > const& cores, exprs& literals);
+        void  initialize(vector<exprs>& cores, exprs& literals);
+        bool  check_result();
         void  update_model();
         void  update_set(exprs& lits);
         lbool process_core(exprs const& _core);
-        lbool process_core(unsigned sz, exprs& core);
+        lbool process_core(unsigned sz, exprs& core, bool& has_mcs, bool is_last);
         void display(std::ostream& out) const;
+        void display_vec(std::ostream& out, unsigned sz, expr* const* args) const;
+        bool check_invariant() const;
     };
 
 };