debug mutex

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Jul 24, 2019 · c2264c7 · c2264c7
1 parent df04d7f
commit c2264c7
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 14 deletions.
diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
@@ -171,8 +171,8 @@ namespace opt {
         if (is_sat != l_true) {
             return is_sat;
         }
-        for (unsigned i = 0; i < mutexes.size(); ++i) {
-            process_mutex(mutexes[i], new_soft);
+        for (auto& mux : mutexes) {
+            process_mutex(mux, new_soft);
         }
         return l_true;
     }
@@ -187,8 +187,8 @@ namespace opt {
 
     void maxsmt_solver_base::process_mutex(expr_ref_vector& mutex, obj_map<expr, rational>& new_soft) {
         TRACE("opt", 
-              for (unsigned i = 0; i < mutex.size(); ++i) {
-                  tout << mk_pp(mutex[i].get(), m) << " |-> " << new_soft.find(mutex[i].get()) << "\n";
+              for (expr* e : mutex) {
+                  tout << mk_pp(e, m) << " |-> " << new_soft.find(e) << "\n";
               });
         if (mutex.size() <= 1) {
             return;
@@ -201,14 +201,13 @@ namespace opt {
 
         rational weight(0), sum1(0), sum2(0);
         vector<rational> weights;
-        for (unsigned i = 0; i < mutex.size(); ++i) {
-            rational w = new_soft.find(mutex[i].get());
+        for (expr* e : mutex) {
+            rational w = new_soft.find(e);
             weights.push_back(w);
             sum1 += w;
-            new_soft.remove(mutex[i].get());
+            new_soft.remove(e);
         }
-        for (unsigned i = mutex.size(); i > 0; ) {
-            --i;
+        for (unsigned i = mutex.size(); i-- > 0; ) {
             expr_ref soft(m.mk_or(i+1, mutex.c_ptr()), m);
             m_trail.push_back(soft);
             rational w = weights[i];

diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp
@@ -68,6 +68,7 @@ namespace sat {
 
     void model_converter::operator()(model & m) const {
         bool first =  false; 
+        TRACE("sat", display(tout););
         literal_vector clause;
         for (unsigned i = m_entries.size(); i-- > m_exposed_lim; ) {
             entry const& e = m_entries[i];
@@ -124,6 +125,7 @@ namespace sat {
                 for (literal const& l : e.m_clauses) {
                     if (l == null_literal) {
                         CTRACE("sat", !sat, 
+                               tout << "exposed: " << m_exposed_lim << "\n";
                                if (m_solver) m_solver->display(tout);
                                display(tout);
                                for (unsigned v = 0; v < m.size(); ++v) tout << v << ": " << m[v] << "\n";

diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -888,6 +888,7 @@ class inc_sat_solver : public solver {
             }
         }
 
+        TRACE("sat", m_solver.display(tout););
         if (m_sat_mc) {
             (*m_sat_mc)(mdl);
         }
@@ -919,16 +920,11 @@ class inc_sat_solver : public solver {
         }
         if (!all_true) {
             IF_VERBOSE(0, verbose_stream() << m_params << "\n");
-            // IF_VERBOSE(0, m_sat_mc->display(verbose_stream() << "sat mc\n"));
             IF_VERBOSE(0, if (m_mcs.back()) m_mcs.back()->display(verbose_stream() << "mc0\n"));
-            //IF_VERBOSE(0, m_solver.display(verbose_stream()));
             IF_VERBOSE(0, for (auto const& kv : m_map) verbose_stream() << mk_pp(kv.m_key, m) << " |-> " << kv.m_value << "\n");
         }
         else {
             IF_VERBOSE(1, verbose_stream() << "solution verified\n");
-//            IF_VERBOSE(0, if (m_mcs.back()) m_mcs.back()->display(verbose_stream() << "mcs\n"));
-//            IF_VERBOSE(0, if (m_sat_mc) m_sat_mc->display(verbose_stream() << "sat_mc\n"));
-//            IF_VERBOSE(0, model_smt2_pp(verbose_stream() << "after\n", m, *mdl, 0););
         }
     }
 };