From cad1e5cab39992b5c0d30da7fcc45a91a69e5b72 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 11 May 2014 18:39:36 -0700
Subject: [PATCH] move to scoped state, change default parameter for sls until
 bv is debugged

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/opt_context.cpp     | 16 ++++++++--------
 src/opt/opt_params.pyg      |  2 +-
 src/opt/weighted_maxsat.cpp | 31 ++++++-------------------------
 3 files changed, 15 insertions(+), 34 deletions(-)

diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 5d0632c1c..3a88ff904 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -991,11 +991,11 @@ namespace opt {
         free_func_visitor visitor(m);
         std::ostringstream out;
 #define PP(_e_) ast_smt2_pp(out, _e_, env);
-        for (unsigned i = 0; i < m_hard_constraints.size(); ++i) {
-            visitor.collect(m_hard_constraints[i]);
+        for (unsigned i = 0; i < m_scoped_state.m_hard.size(); ++i) {
+            visitor.collect(m_scoped_state.m_hard[i]);
         }
-        for (unsigned i = 0; i < m_objectives.size(); ++i) {
-            objective const& obj = m_objectives[i];
+        for (unsigned i = 0; i < m_scoped_state.m_objectives.size(); ++i) {
+            objective const& obj = m_scoped_state.m_objectives[i];
             switch(obj.m_type) {
             case O_MAXIMIZE: 
             case O_MINIMIZE:
@@ -1023,13 +1023,13 @@ namespace opt {
             PP(*it);
             out << "\n";
         }
-        for (unsigned i = 0; i < m_hard_constraints.size(); ++i) {
+        for (unsigned i = 0; i < m_scoped_state.m_hard.size(); ++i) {
             out << "(assert ";
-            PP(m_hard_constraints[i]);
+            PP(m_scoped_state.m_hard[i]);
             out << ")\n";
         }
-        for (unsigned i = 0; i < m_objectives.size(); ++i) {
-            objective const& obj = m_objectives[i];
+        for (unsigned i = 0; i < m_scoped_state.m_objectives.size(); ++i) {
+            objective const& obj = m_scoped_state.m_objectives[i];
             switch(obj.m_type) {
             case O_MAXIMIZE: 
                 out << "(maximize ";
diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg
index 201a1601b..2e6f67219 100644
--- a/src/opt/opt_params.pyg
+++ b/src/opt/opt_params.pyg
@@ -12,7 +12,7 @@ def_module_params('opt',
                           ('wmaxsat_engine', SYMBOL, 'wmax', "weighted maxsat engine: 'wmax', 'pbmax', 'bcd2', 'wpm2', 'bvsls', 'sls'"),
                           ('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsast'),
                           ('enable_sat', BOOL, False, 'enable the new SAT core for propositional constraints'),
-                          ('sls_engine', SYMBOL, 'bv', "SLS engine. Either 'bv' or 'pb'"),
+                          ('sls_engine', SYMBOL, 'pb', "SLS engine. Either 'bv' or 'pb'"),
                           ('elim_01', BOOL, True, 'eliminate 01 variables'),
                           ('pb.compile_equality', BOOL, False, 'compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalites)')
 
diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp
index f19c5c77e..075b89a76 100644
--- a/src/opt/weighted_maxsat.cpp
+++ b/src/opt/weighted_maxsat.cpp
@@ -576,10 +576,9 @@ namespace opt {
     // lower bounds.
 
     class pbmax : public maxsmt_solver_base {
-        bool m_use_aux;
     public:
-        pbmax(solver* s, ast_manager& m, bool use_aux): 
-            maxsmt_solver_base(s, m), m_use_aux(use_aux) {
+        pbmax(solver* s, ast_manager& m): 
+            maxsmt_solver_base(s, m) {
         }
         
         virtual ~pbmax() {}
@@ -598,20 +597,8 @@ namespace opt {
             app_ref b(m);
             expr_ref_vector nsoft(m);
             init();            
-            if (m_use_aux) {
-                s().push();
-            }
             for (unsigned i = 0; i < m_soft.size(); ++i) {
-                if (m_use_aux) {
-                    b = m.mk_fresh_const("b", m.mk_bool_sort());
-                    m_mc->insert(b->get_decl());
-                    fml = m.mk_or(m_soft[i].get(), b);
-                    s().assert_expr(fml);
-                    nsoft.push_back(b);
-                }
-                else {
-                    nsoft.push_back(mk_not(m_soft[i].get()));
-                }
+                nsoft.push_back(mk_not(m_soft[i].get()));
             }
             lbool is_sat = l_true;
             while (l_true == is_sat) {
@@ -643,9 +630,6 @@ namespace opt {
                 is_sat = l_true;
                 m_lower = m_upper;
             }
-            if (m_use_aux) {
-                s().pop(1);
-            }
             TRACE("opt", tout << "lower: " << m_lower << "\n";);
             return is_sat;
         }
@@ -1008,14 +992,11 @@ namespace opt {
             if (m_maxsmt) {
                 return *m_maxsmt;
             }
-            if (m_engine == symbol("pwmax")) {
-                m_maxsmt = alloc(pbmax, s.get(), m, true);
-            }
-            else if (m_engine == symbol("pbmax")) {
-                m_maxsmt = alloc(pbmax, s.get(), m, false);
+            if (m_engine == symbol("pbmax")) {
+                m_maxsmt = alloc(pbmax, s.get(), m);
             }
             else if (m_engine == symbol("wpm2")) {
-                maxsmt_solver_base* s2 = alloc(pbmax, s.get(), m, false);
+                maxsmt_solver_base* s2 = alloc(pbmax, s.get(), m);
                 m_maxsmt = alloc(wpm2, s.get(), m, s2);
             }
             else if (m_engine == symbol("bcd2")) {