From 55863b4bb5097c4da60c5db9f34ec089d13b697f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 23 Apr 2014 14:05:59 +0200
Subject: [PATCH] fix build problems, fix scoping

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/python/z3printer.py         |  2 +-
 src/opt/opt_sls_solver.h            |  6 ++----
 src/opt/weighted_maxsat.cpp         | 33 ++++++++++++++++++++---------
 src/tactic/arith/card2bv_tactic.cpp |  3 ++-
 4 files changed, 28 insertions(+), 16 deletions(-)

diff --git a/src/api/python/z3printer.py b/src/api/python/z3printer.py
index d3dc43d3e..d1d85d30e 100644
--- a/src/api/python/z3printer.py
+++ b/src/api/python/z3printer.py
@@ -386,7 +386,7 @@ def seq3(args, lp='(', rp=')'):
     else:
         return group(indent(len(lp), compose(to_format(lp), seq(args), to_format(rp))))
 
-class StopPPException:
+class StopPPException(Exception):
     def __str__(self):
         return 'pp-interrupted'
 
diff --git a/src/opt/opt_sls_solver.h b/src/opt/opt_sls_solver.h
index cd634e728..7578502b0 100644
--- a/src/opt/opt_sls_solver.h
+++ b/src/opt/opt_sls_solver.h
@@ -204,10 +204,8 @@ namespace opt {
             for (unsigned i = 0; i < m_soft.size(); ++i) {
                 m_pbsls->add(m_soft[i].get(), m_weights[i]);
             }
-            lbool is_sat = (*m_pbsls.get())();
-            if (is_sat == l_true) {
-                m_pbsls->get_model(m_model);
-            }
+            (*m_pbsls.get())();
+            m_pbsls->get_model(m_model);            
         }
 
         void bvsls_opt() {
diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp
index 774147b91..593e87e7f 100644
--- a/src/opt/weighted_maxsat.cpp
+++ b/src/opt/weighted_maxsat.cpp
@@ -156,6 +156,8 @@ namespace opt {
                 for (unsigned i = 0; i < sz; ++i) {
                     sat_solver->assert_expr(s().get_assertion(i));
                 }   
+                unsigned lvl = m_s->get_scope_level();
+                while (lvl > 0) { sat_solver->push(); --lvl; }
                 m_s = sat_solver;
             }
         }
@@ -163,7 +165,9 @@ namespace opt {
         void enable_sls() {
             if (m_enable_sls && probe_bv()) {
                 m_params.set_uint("restarts", 20);
+                unsigned lvl = m_s->get_scope_level();
                 m_s = alloc(sls_solver, m, m_s.get(), m_soft, m_weights, m_params);
+                while (lvl > 0) { m_s->push(); --lvl; }
             }
         }
         
@@ -247,6 +251,7 @@ namespace opt {
             m_soft_constraints(m),
             m_enable_lazy(false) {
             m_enable_lazy = true;
+            enable_sls();
         }
 
         virtual ~bcd2() {}
@@ -257,7 +262,6 @@ namespace opt {
             lbool is_sat = l_undef;
             expr_ref_vector asms(m);
             bool first = true;
-            enable_sls();
             solver::scoped_push _scope1(s());
             init();
             init_bcd();
@@ -551,13 +555,14 @@ namespace opt {
         bool m_use_aux;
     public:
         pbmax(solver* s, ast_manager& m, bool use_aux): 
-            maxsmt_solver_base(s, m), m_use_aux(use_aux) {}
+            maxsmt_solver_base(s, m), m_use_aux(use_aux) {
+            enable_bvsat();
+            enable_sls();
+        }
         
         virtual ~pbmax() {}
 
         lbool operator()() {
-            enable_bvsat();
-            enable_sls();
             TRACE("opt", s().display(tout); tout << "\n";
                   for (unsigned i = 0; i < m_soft.size(); ++i) {
                       tout << mk_pp(m_soft[i].get(), m) << " " << m_weights[i] << "\n";
@@ -628,14 +633,15 @@ namespace opt {
     class wpm2 : public maxsmt_solver_base {
         scoped_ptr<maxsmt_solver_base> maxs;
     public:
-        wpm2(solver* s, ast_manager& m, maxsmt_solver_base* maxs): 
-            maxsmt_solver_base(s, m), maxs(maxs) {}
+        wpm2(solver* s, ast_manager& m, maxsmt_solver_base* _maxs): 
+            maxsmt_solver_base(s, m), maxs(_maxs) {
+            enable_sls();
+        }
 
         virtual ~wpm2() {}
 
         lbool operator()() {
             IF_VERBOSE(1, verbose_stream() << "(wmaxsat.wpm2 solve)\n";);
-            enable_sls();
             solver::scoped_push _s(s());
             pb_util u(m);
             app_ref fml(m), a(m), b(m), c(m);
@@ -778,6 +784,12 @@ namespace opt {
                 amk.push_back(k);
             }            
         }
+
+        virtual void set_cancel(bool f) { 
+            maxsmt_solver_base::set_cancel(f); 
+            maxs->set_cancel(f); 
+        }
+
     private:
         lbool new_bound(expr_ref_vector const& al, 
                         vector<rational> const& ws, 
@@ -825,12 +837,13 @@ namespace opt {
     class sls : public maxsmt_solver_base {
     public:
         sls(solver* s, ast_manager& m): 
-            maxsmt_solver_base(s, m) {}
+            maxsmt_solver_base(s, m) {
+            enable_bvsat();
+            enable_sls();
+        }
         virtual ~sls() {}
         lbool operator()() {
             IF_VERBOSE(1, verbose_stream() << "(sls solve)\n";);
-            enable_bvsat();
-            enable_sls();
             init();
             lbool is_sat = s().check_sat(0, 0);
             if (is_sat == l_true) {
diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp
index ca40d8a47..bba8705e0 100644
--- a/src/tactic/arith/card2bv_tactic.cpp
+++ b/src/tactic/arith/card2bv_tactic.cpp
@@ -137,9 +137,10 @@ namespace pb {
             return BR_FAILED;
     }
 
-    template class rewriter_tpl<card2bv_rewriter_cfg>;
 };
 
+template class rewriter_tpl<pb::card2bv_rewriter_cfg>;
+
 class card2bv_tactic : public tactic {
     ast_manager &              m;
     params_ref                 m_params;