From be1cceba3427f262cbedbd3b02acc7528350f007 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 15 Aug 2014 11:29:08 -0700
Subject: [PATCH] fix scope and mus with user-scopes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/maxres.cpp     |  5 +----
 src/sat/sat_mus.cpp    | 11 ++++++++++-
 src/sat/sat_solver.cpp |  4 ++++
 3 files changed, 15 insertions(+), 5 deletions(-)

diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index a4ccf567f..f31c9e048 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -134,7 +134,6 @@ public:
     }
 
     lbool mus_solver() {
-        solver::scoped_push _sc(m_s);
         init();
         init_local();
         while (true) {
@@ -178,10 +177,9 @@ public:
     }
 
     lbool mus_mss_solver() {
-        solver::scoped_push _sc(s());
         init();
         init_local();
-        enable_sls(m_asms);
+        //enable_sls(m_asms);
         ptr_vector<expr> mcs;
         vector<ptr_vector<expr> > cores;
         while (m_lower < m_upper) {            
@@ -222,7 +220,6 @@ public:
 
     lbool mss_solver() {
         NOT_IMPLEMENTED_YET();
-        solver::scoped_push _sc(s());
         init();
         init_local();
         ptr_vector<expr> mcs;
diff --git a/src/sat/sat_mus.cpp b/src/sat/sat_mus.cpp
index 11d0fc15d..6295513a9 100644
--- a/src/sat/sat_mus.cpp
+++ b/src/sat/sat_mus.cpp
@@ -48,6 +48,13 @@ namespace sat {
         literal_vector& core = m_core;
         literal_vector& mus = m_mus;
         core.append(s.get_core());        
+        for (unsigned i = 0; i < core.size(); ++i) {
+            s.m_user_scope_literals.contains(core[i]);
+            mus.push_back(core[i]);
+            core[i] = core.back();
+            core.pop_back();
+            --i;
+        }
 
         while (!core.empty()) {
             TRACE("sat", 
@@ -61,9 +68,10 @@ namespace sat {
             literal lit = core.back();
             core.pop_back();
             unsigned sz = mus.size();
-            mus.push_back(~lit); // TBD: measure
+            // mus.push_back(~lit); // TBD: measure
             mus.append(core);
             lbool is_sat = s.check(mus.size(), mus.c_ptr());
+            TRACE("sat", tout << "mus: " << mus << "\n";);
             mus.resize(sz);
             switch (is_sat) {
             case l_undef:
@@ -83,6 +91,7 @@ namespace sat {
                 if (new_core.contains(~lit)) {
                     break;
                 }
+                TRACE("sat", tout << "new core: " << new_core << "\n";);
                 core.reset();
                 for (unsigned i = 0; i < new_core.size(); ++i) {
                     literal lit = new_core[i];
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index e4e34b8a3..e779c9495 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -896,6 +896,9 @@ namespace sat {
               for (unsigned i = 0; i < num_lits; ++i) 
                   tout << lits[i] << " ";
               tout << "\n";
+              if (!m_user_scope_literals.empty()) {
+                  tout << "user literals: " << m_user_scope_literals << "\n";
+              }
               m_mc.display(tout);
               );
 #define _INSERT_LIT(_l_)                     \
@@ -2237,6 +2240,7 @@ namespace sat {
             lit = m_user_scope_literal_pool.back();
             m_user_scope_literal_pool.pop_back();
         }
+        TRACE("sat", tout << "user_push: " << lit << "\n";);
         m_user_scope_literals.push_back(lit);
     }