Initializing BVMinisat Solver::notify to nullptr. (#1132)

diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 0213ef7e37fa18aa57dadb177c08b4b078e356ec..0ca4b637bff60406391fdde69198f45089807f85 100644 (file)
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -91,7 +91,8 @@ Solver::Solver(CVC4::context::Context* c) :
 
     // Parameters (user settable):
     //
-    c(c)
+    d_notify(nullptr)
+  , c(c)
   , verbosity        (0)
   , var_decay        (opt_var_decay)
   , clause_decay     (opt_clause_decay)
@@ -712,9 +713,10 @@ void Solver::uncheckedEnqueue(Lit p, CRef from)
     vardata[var(p)] = mkVarData(from, decisionLevel());
     trail.push_(p);
     if (decisionLevel() <= assumptions.size() && marker[var(p)] == 1) {
-      if (notify) {
-        Debug("bvminisat::explain") << OUTPUT_TAG << "propagating " << p << std::endl;
-        notify->notify(p);
+      if (d_notify) {
+        Debug("bvminisat::explain")
+            << OUTPUT_TAG << "propagating " << p << std::endl;
+        d_notify->notify(p);
       }
     }
 }
@@ -1466,5 +1468,18 @@ void ClauseAllocator::reloc(CRef& cr, ClauseAllocator& to, CVC4::BVProofProxy* p
   else if (to[cr].has_extra()) to[cr].calcAbstraction();
 }
 
+void Solver::setNotify(Notify* toNotify) { d_notify = toNotify; }
+
+bool Solver::withinBudget(uint64_t ammount) const {
+  AlwaysAssert(d_notify);
+  d_notify->spendResource(ammount);
+  d_notify->safePoint(0);
+
+  return !asynch_interrupt &&
+         (conflict_budget < 0 || conflicts < (uint64_t)conflict_budget) &&
+         (propagation_budget < 0 ||
+          propagations < (uint64_t)propagation_budget);
+}
+
 } /* CVC4::BVMinisat namespace */
 } /* CVC4 namespace */

diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h
index 485eb85355168c2a6366257ce83a89a5f66bd198..b3b792ef595dcc2c64abddf5f9ac535e62bd9736 100644 (file)
--- a/src/prop/bvminisat/core/Solver.h
+++ b/src/prop/bvminisat/core/Solver.h
@@ -80,7 +80,7 @@ public:
     static CRef TCRef_Lazy;
 private:
     /** To notify */
-    Notify* notify;
+    Notify* d_notify;
 
     /** Cvc4 context */
     CVC4::context::Context* c;
@@ -98,7 +98,7 @@ public:
     Solver(CVC4::context::Context* c);
     virtual ~Solver();
 
-    void setNotify(Notify* toNotify) { notify = toNotify; }
+    void setNotify(Notify* toNotify);
 
     // Problem specification:
     //
@@ -461,14 +461,6 @@ inline void     Solver::setPropBudget(int64_t x){ propagation_budget = propagati
 inline void     Solver::interrupt(){ asynch_interrupt = true; }
 inline void     Solver::clearInterrupt(){ asynch_interrupt = false; }
 inline void     Solver::budgetOff(){ conflict_budget = propagation_budget = -1; }
-inline bool     Solver::withinBudget(uint64_t ammount) const {
-    Assert (notify);
-    notify->spendResource(ammount);
-    notify->safePoint(0);
-
-    return !asynch_interrupt &&
-           (conflict_budget    < 0 || conflicts < (uint64_t)conflict_budget) &&
-           (propagation_budget < 0 || propagations < (uint64_t)propagation_budget); }
 
 inline lbool     Solver::solve         ()                    { budgetOff(); return solve_(); }
 inline lbool     Solver::solve         (Lit p)               { budgetOff(); assumptions.push(p); return solve_(); }