Some formatting and better tracing in prop engine (#6022)

Miscellaneous changes from proof-new.

2 files changed, 36 insertions, 14 deletions

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index dbf734a3c..d597ac934 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -278,13 +278,16 @@ Var Solver::newVar(bool sign, bool dvar, bool isTheoryAtom, bool preRegister, bo
 
     setDecisionVar(v, dvar);
 
+    Debug("minisat") << "new var " << v << std::endl;
+
     // If the variable is introduced at non-zero level, we need to reintroduce it on backtracks
-    if (preRegister) {
+    if (preRegister)
+    {
+      Debug("minisat") << "  To register at level " << decisionLevel()
+                       << std::endl;
       variables_to_register.push(VarIntroInfo(v, decisionLevel()));
     }
 
-    Debug("minisat") << "new var " << v << std::endl;
-
     return v;
 }
 
@@ -981,19 +984,22 @@ Lit Solver::pickBranchLit()
 |________________________________________________________________________________________________@*/
 int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
 {
-    int pathC = 0;
-    Lit p     = lit_Undef;
+  Trace("pf::sat") << "Solver::analyze: starting with " << confl
+                   << " with decision level " << decisionLevel() << "\n";
 
-    // Generate conflict clause:
-    //
-    out_learnt.push();      // (leave room for the asserting literal)
-    int index   = trail.size() - 1;
+  int pathC = 0;
+  Lit p = lit_Undef;
 
-    int max_resolution_level = 0; // Maximal level of the resolved clauses
+  // Generate conflict clause:
+  //
+  out_learnt.push();  // (leave room for the asserting literal)
+  int index = trail.size() - 1;
 
-    if (options::unsatCores() && !isProofEnabled())
-    {
-      ProofManager::getSatProof()->startResChain(confl);
+  int max_resolution_level = 0;  // Maximal level of the resolved clauses
+
+  if (options::unsatCores() && !isProofEnabled())
+  {
+    ProofManager::getSatProof()->startResChain(confl);
     }
     if (isProofEnabled())
     {
@@ -1013,12 +1019,26 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
           if (c.removable()) claBumpActivity(c);
         }
 
+        if (Trace.isOn("pf::sat"))
+        {
+          Trace("pf::sat") << "Solver::analyze: conflict clause ";
+          for (unsigned i = 0, size = ca[confl].size(); i < size; ++i)
+          {
+            Trace("pf::sat") << ca[confl][i] << " ";
+          }
+          Trace("pf::sat") << "\n";
+        }
+
+        Trace("pf::sat") << CVC4::push;
         for (int j = (p == lit_Undef) ? 0 : 1, size = ca[confl].size();
              j < size;
              j++)
         {
           Lit q = ca[confl][j];
 
+          Trace("pf::sat") << "Lit " << q
+                           << " seen/level: " << (seen[var(q)] ? 1 : 0) << " / "
+                           << level(var(q)) << "\n";
           if (!seen[var(q)] && level(var(q)) > 0)
           {
             varBumpActivity(var(q));
@@ -1052,6 +1072,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
             }
           }
         }
+        Trace("pf::sat") << CVC4::pop;
 
         // Select next clause to look at:
         while (!seen[var(trail[index--])]);
@@ -2274,6 +2295,7 @@ CRef Solver::updateLemmas() {
           }
         } else {
           Debug("minisat::lemmas") << "lemma size is " << lemma.size() << std::endl;
+          Debug("minisat::lemmas") << "lemma ref is " << lemma_ref << std::endl;
           uncheckedEnqueue(lemma[0], lemma_ref);
         }
       }
diff --git a/src/prop/sat_solver_types.h b/src/prop/sat_solver_types.h
index 717b1ffaa..e2d7f93d5 100644
--- a/src/prop/sat_solver_types.h
+++ b/src/prop/sat_solver_types.h
@@ -136,7 +136,7 @@ public:
    */
   std::string toString() const {
     std::ostringstream os;
-    os << (isNegated()? "~" : "") << getSatVariable() << " ";
+    os << (isNegated() ? "~" : "") << getSatVariable();
     return os.str();
   }