working on core-maxsat

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

src/opt/core_maxsat.cpp

@@ -18,6 +18,7 @@ Notes:
 --*/
 #include "core_maxsat.h"
 #include "card_decl_plugin.h"
+#include "ast_pp.h"
 
 namespace opt {
 
@@ -36,9 +37,9 @@ namespace opt {
         solver::scoped_push _sp(s);
         for (unsigned i = 0; i < m_soft.size(); ++i) {
             expr* a = m.mk_fresh_const("p", m.mk_bool_sort());
-            aux.push_back(a);
+            aux.push_back(m.mk_not(a));
-            s.assert_expr(m.mk_implies(a, m_soft[i].get()));
+            s.assert_expr(m.mk_or(a, m_soft[i].get()));
-            block_vars.insert(a);
+            block_vars.insert(aux.back());
         }            
         while (m_answer.size() < m_upper) {
             ptr_vector<expr> vars;
@@ -60,20 +61,30 @@ namespace opt {
                         ans.push_back(m_soft[i].get());
                     }
                 }
+                TRACE("opt", tout << "sat\n";
+                      for (unsigned i = 0; i < ans.size(); ++i) {
+                          tout << mk_pp(ans[i].get(), m) << "\n";
+                      });
                 if (ans.size() > m_answer.size()) {
                     m_answer.reset();
                     m_answer.append(ans);
                 }
-                unsigned k = m_soft.size()-m_answer.size()-1; // TBD: fix this
+                unsigned k = m_soft.size()-m_answer.size()-1;
                 expr_ref fml = mk_at_most(core_vars, k);
+                TRACE("opt", tout << "add: " << fml << "\n";);
                 s.assert_expr(fml);
                 break;                    
             }
             case l_false: {
                 ptr_vector<expr> core;
                 s.get_unsat_core(core);
+                TRACE("opt", tout << "core";
                       for (unsigned i = 0; i < core.size(); ++i) {
-                    core_vars.insert(core[i]);
+                          tout << mk_pp(core[i], m) << " ";
+                      }
+                      tout << "\n";);
+                for (unsigned i = 0; i < core.size(); ++i) {
+                    core_vars.insert(get_not(core[i]));
                     block_vars.remove(core[i]);
                 }
                 if (core.empty()) {
@@ -84,6 +95,7 @@ namespace opt {
                     // at least one core variable is True
                     expr_ref fml = mk_at_most(core_vars, 0);
                     fml = m.mk_not(fml);
+                    TRACE("opt", tout << "add: " << fml << "\n";);
                     s.assert_expr(fml);
                 }
                 --m_upper;                
@@ -108,6 +120,12 @@ namespace opt {
         return expr_ref(card.mk_at_most_k(es.size(), es.c_ptr(), k), m);
     }
 
+    expr* core_maxsat::get_not(expr* e) const {
+        expr* result = 0;
+        VERIFY(m.is_not(e, result));
+        return result;
+    }
+    
     rational core_maxsat::get_lower() const {
         return rational(m_answer.size());
     }

src/opt/core_maxsat.h

@@ -44,6 +44,7 @@ namespace opt {
     private:
         void set2vector(expr_set const& set, ptr_vector<expr>& es) const;
         expr_ref mk_at_most(expr_set const& set, unsigned k);
+        expr* get_not(expr* e) const;
     };
     
 };

src/opt/fu_malik.h

@@ -6,6 +6,7 @@ Module Name:
     fu_malik.h
 
 Abstract:
+
     Fu&Malik built-in optimization method.
     Adapted from sample code in C.
 
@@ -15,6 +16,10 @@ Author:
 
 Notes:
 
+    Takes solver with hard constraints added.
+    Returns a maximal satisfying subset of soft_constraints
+    that are still consistent with the solver state.
+
 --*/
 #ifndef _OPT_FU_MALIK_H_
 #define _OPT_FU_MALIK_H_
@@ -23,11 +28,6 @@ Notes:
 #include "maxsmt.h"
 
 namespace opt {
-    /**
-       Takes solver with hard constraints added.
-       Returns a maximal satisfying subset of soft_constraints
-       that are still consistent with the solver state.
-    */
 
     class fu_malik : public maxsmt_solver {
         struct imp;

src/opt/maxsmt.cpp

@@ -3,7 +3,7 @@ Copyright (c) 2013 Microsoft Corporation
 
 Module Name:
 
-    opt_maxsmt.cpp
+    maxsmt.cpp
 
 Abstract:
    
@@ -19,8 +19,10 @@ Notes:
 
 #include "maxsmt.h"
 #include "fu_malik.h"
+#include "core_maxsat.h"
 #include "weighted_maxsat.h"
 #include "ast_pp.h"
+#include "opt_params.hpp"
 
 namespace opt {
 
@@ -35,8 +37,13 @@ namespace opt {
             m_answer.append(m_soft_constraints);
         }
         else if (is_maxsat_problem(m_weights)) {
+            if (m_maxsat_engine == symbol("core_maxsat")) {
+                m_msolver = alloc(core_maxsat, m, s, m_soft_constraints);
+            }
+            else {
                 m_msolver = alloc(fu_malik, m, s, m_soft_constraints);
             }
+        }
         else {
             m_msolver = alloc(wmaxsmt, m, opt_solver::to_opt(s), m_soft_constraints, m_weights);
         }
@@ -110,6 +117,8 @@ namespace opt {
     }
 
     void maxsmt::updt_params(params_ref& p) {
+        opt_params _p(p);
+        m_maxsat_engine = _p.maxsat_engine();        
     }
 
 

src/opt/maxsmt.h

@@ -3,7 +3,7 @@ Copyright (c) 2013 Microsoft Corporation
 
 Module Name:
 
-    opt_maxsmt.h
+    maxsmt.h
 
 Abstract:
    
@@ -47,6 +47,7 @@ namespace opt {
         expr_ref_vector  m_answer;
         vector<rational> m_weights;
         scoped_ptr<maxsmt_solver> m_msolver;
+        symbol           m_maxsat_engine;
     public:
         maxsmt(ast_manager& m): m(m), m_s(0), m_cancel(false), m_soft_constraints(m), m_answer(m) {}
 

src/opt/opt_params.pyg

@@ -3,6 +3,7 @@ def_module_params('opt',
                   export=True,
                   params=(('timeout', UINT, UINT_MAX, 'set timeout'),
                           ('engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'farkas', 'symba'"),
+	                  ('maxsat_engine', SYMBOL, 'fu_malik', "select engine for non-weighted maxsat: 'fu_malik', 'core_maxsat'"),
                           ('pareto', BOOL, False, 'return a Pareto front (as opposed to a bounding box)'),
                           ))
 

src/smt/theory_card.cpp

@@ -453,19 +453,19 @@ namespace smt {
 
     void theory_card::pop_scope_eh(unsigned num_scopes) {
         unsigned sz = m_watch_lim[m_watch_lim.size()-num_scopes];
-        for (unsigned i = m_watch_trail.size(); i > sz; ) {
+        while (m_watch_trail.size() > sz) {
-            --i;
             ptr_vector<card>* cards = 0;
-            VERIFY(m_watch.find(m_watch_trail[i], cards));
+            VERIFY(m_watch.find(m_watch_trail.back(), cards));
             SASSERT(cards && !cards->empty());
             cards->pop_back();
+            m_watch_trail.pop_back();
         }
         m_watch_lim.resize(m_watch_lim.size()-num_scopes);
         sz = m_cards_lim[m_cards_lim.size()-num_scopes];
-        for (unsigned i = m_cards_trail.size(); i > sz; ) {
+        while (m_cards_trail.size() > sz) {
-            --i;
+            SASSERT(m_cards.contains(m_cards_trail.back()));
-            SASSERT(m_cards.contains(m_cards_trail[i]));
+            m_cards.remove(m_cards_trail.back());
-            m_cards.remove(m_cards_trail[i]);
+            m_cards_trail.pop_back();
         }
         m_cards_lim.resize(m_cards_lim.size()-num_scopes);
     }
@@ -482,7 +482,7 @@ namespace smt {
         TRACE("card", ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); tout << "\n";);
         justification* js = 0;
         ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0);
-        IF_VERBOSE(0, 
+        IF_VERBOSE(1, 
                    for (unsigned i = 0; i < lits.size(); ++i) {
                        verbose_stream() << lits[i] << " ";
                    }