Remove ProofProxy (#1965)

diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 047c32e8382145b43b2bec4dda8da956276a268a..d1833fd076094b3cc04b13afb2f9fa6ae0733cca 100644 (file)
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -80,10 +80,6 @@ class LFSCUFProof;
 class LFSCBitVectorProof;
 class LFSCRewriterProof;
 
-template <class Solver> class ProofProxy;
-typedef ProofProxy< CVC4::Minisat::Solver> CoreProofProxy;
-typedef ProofProxy< CVC4::BVMinisat::Solver> BVProofProxy;
-
 namespace prop {
   typedef uint64_t SatVariable;
   class SatLiteral;

diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index 19a8d30cf0bf353afff4fc65abb36afc4c69e996..57e3a9bc1b39b5e1cbf63887676aa5146b805f99 100644 (file)
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -38,8 +38,6 @@
 // Forward declarations.
 namespace CVC4 {
 class CnfProof;
-template <class Solver>
-class ProofProxy;
 } /* namespace CVC4 */
 
 namespace CVC4 {
@@ -192,7 +190,6 @@ class TSatProof {
    */
   void storeUnitResolution(typename Solver::TLit lit);
 
-  ProofProxy<Solver>* getProxy() { return d_proxy; }
   /**
    * Constructs the SAT proof for the given clause,
    * by collecting the needed clauses in the d_seen
@@ -341,8 +338,6 @@ class TSatProof {
 
   const ClauseId d_emptyClauseId;
   const ClauseId d_nullId;
-  // proxy class to break circular dependencies
-  ProofProxy<Solver>* d_proxy;
 
   // temporary map for updating CRefs
   ClauseIdMap d_temp_clauseId;
@@ -379,16 +374,6 @@ class TSatProof {
   Statistics d_statistics;
 }; /* class TSatProof */
 
-template <class S>
-class ProofProxy {
- private:
-  TSatProof<S>* d_proof;
-
- public:
-  ProofProxy(TSatProof<S>* pf);
-  void updateCRef(typename S::TCRef oldref, typename S::TCRef newref);
-}; /* class ProofProxy */
-
 template <class SatSolver>
 class LFSCSatProof : public TSatProof<SatSolver> {
  private:

diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h
index daf98ceea07fbdc7c45ac52f9efcff92abee8e2c..e3cbae361e6839a03c640d506fb5ad30e7d0cabe 100644 (file)
--- a/src/proof/sat_proof_implementation.h
+++ b/src/proof/sat_proof_implementation.h
@@ -184,16 +184,6 @@ void ResChain<Solver>::addRedundantLit(typename Solver::TLit lit) {
   }
 }
 
-/// ProxyProof
-template <class Solver>
-ProofProxy<Solver>::ProofProxy(TSatProof<Solver>* proof) : d_proof(proof) {}
-
-template <class Solver>
-void ProofProxy<Solver>::updateCRef(typename Solver::TCRef oldref,
-                                    typename Solver::TCRef newref) {
-  d_proof->updateCRef(oldref, newref);
-}
-
 /// SatProof
 template <class Solver>
 TSatProof<Solver>::TSatProof(Solver* solver, context::Context* context,
@@ -227,13 +217,10 @@ TSatProof<Solver>::TSatProof(Solver* solver, context::Context* context,
       d_seenLemmas(),
       d_satProofConstructed(false),
       d_statistics(name) {
-  d_proxy = new ProofProxy<Solver>(this);
 }
 
 template <class Solver>
 TSatProof<Solver>::~TSatProof() {
-  delete d_proxy;
-
   // FIXME: double free if deleted clause also appears in d_seenLemmas?
   IdToSatClause::const_iterator it = d_deletedTheoryLemmas.begin();
   IdToSatClause::const_iterator end = d_deletedTheoryLemmas.end();

diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 885e429f007ecae9e79a1b1d69d3f9ad7e7ec501..8d71e2f65a964f39472d204af899ab83e7b4e3c9 100644 (file)
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -1412,7 +1412,7 @@ void Solver::relocAll(ClauseAllocator& to)
             // printf(" >>> RELOCING: %s%d\n", sign(p)?"-":"", var(p)+1);
             vec<Watcher>& ws = watches[p];
             for (int j = 0; j < ws.size(); j++)
-              ca.reloc(ws[j].cref, to, d_bvp ?  d_bvp->getSatProof()->getProxy() : NULL);
+              ca.reloc(ws[j].cref, to, d_bvp ? d_bvp->getSatProof() : NULL);
         }
 
     // All reasons:
@@ -1421,19 +1421,19 @@ void Solver::relocAll(ClauseAllocator& to)
         Var v = var(trail[i]);
 
         if (reason(v) != CRef_Undef && (ca[reason(v)].reloced() || locked(ca[reason(v)])))
-            ca.reloc(vardata[v].reason, to, d_bvp ?  d_bvp->getSatProof()->getProxy() : NULL);
+          ca.reloc(vardata[v].reason, to, d_bvp ? d_bvp->getSatProof() : NULL);
     }
 
     // All learnt:
     //
     for (int i = 0; i < learnts.size(); i++)
-        ca.reloc(learnts[i], to, d_bvp ?  d_bvp->getSatProof()->getProxy() : NULL);
+      ca.reloc(learnts[i], to, d_bvp ? d_bvp->getSatProof() : NULL);
 
     // All original:
     //
     for (int i = 0; i < clauses.size(); i++)
-        ca.reloc(clauses[i], to, d_bvp ?  d_bvp->getSatProof()->getProxy() : NULL);
-       
+      ca.reloc(clauses[i], to, d_bvp ? d_bvp->getSatProof() : NULL);
+
     if(d_bvp){ d_bvp->getSatProof()->finishUpdateCRef(); }
 }
 
@@ -1451,7 +1451,9 @@ void Solver::garbageCollect()
     to.moveTo(ca);
 }
 
-void ClauseAllocator::reloc(CRef& cr, ClauseAllocator& to, CVC4::BVProofProxy* proxy)
+void ClauseAllocator::reloc(CRef& cr,
+                            ClauseAllocator& to,
+                            CVC4::TSatProof<Solver>* proof)
 {
   CRef old = cr;  // save the old reference
 
@@ -1460,8 +1462,9 @@ void ClauseAllocator::reloc(CRef& cr, ClauseAllocator& to, CVC4::BVProofProxy* p
   
   cr = to.alloc(c, c.learnt());
   c.relocate(cr);
-  if (proxy) {
-    proxy->updateCRef(old, cr); 
+  if (proof)
+  {
+    proof->updateCRef(old, cr);
   }
   
   // Copy extra data-fields: 

diff --git a/src/prop/bvminisat/core/SolverTypes.h b/src/prop/bvminisat/core/SolverTypes.h
index 1fd7ac5a7c21aad7958e0d079192f35c1cb794c1..302db104f511373ccd6b85ffcfe492de38e55336 100644 (file)
--- a/src/prop/bvminisat/core/SolverTypes.h
+++ b/src/prop/bvminisat/core/SolverTypes.h
@@ -33,8 +33,8 @@ namespace CVC4 {
 namespace BVMinisat {
 class Solver;
 }
-template <class Solver> class ProofProxy;
-typedef ProofProxy<BVMinisat::Solver> BVProofProxy;
+template <class Solver>
+class TSatProof;
 }
 
 namespace CVC4 {
@@ -256,7 +256,9 @@ class ClauseAllocator : public RegionAllocator<uint32_t>
         RegionAllocator<uint32_t>::free(clauseWord32Size(c.size(), c.has_extra()));
     }
 
-  void reloc(CRef& cr, ClauseAllocator& to, CVC4::BVProofProxy* proxy = NULL);
+    void reloc(CRef& cr,
+               ClauseAllocator& to,
+               CVC4::TSatProof<Solver>* proof = NULL);
 };
 
 

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index b034f846071a4bef2afcc475d195e3c8bf5a7df1..0967f434ccf62629d5e1b06239f60bb67d79b7d3 100644 (file)
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -29,8 +29,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "options/prop_options.h"
 #include "proof/clause_id.h"
 #include "proof/proof_manager.h"
-#include "proof/sat_proof_implementation.h"
 #include "proof/sat_proof.h"
+#include "proof/sat_proof_implementation.h"
 #include "prop/minisat/minisat.h"
 #include "prop/minisat/mtl/Sort.h"
 #include "prop/theory_proxy.h"
@@ -1528,7 +1528,7 @@ void Solver::relocAll(ClauseAllocator& to)
             // printf(" >>> RELOCING: %s%d\n", sign(p)?"-":"", var(p)+1);
             vec<Watcher>& ws = watches[p];
             for (int j = 0; j < ws.size(); j++)
-              ca.reloc(ws[j].cref, to,   NULLPROOF( ProofManager::getSatProof()->getProxy() ));
+              ca.reloc(ws[j].cref, to, NULLPROOF(ProofManager::getSatProof()));
         }
 
     // All reasons:
@@ -1537,19 +1537,22 @@ void Solver::relocAll(ClauseAllocator& to)
         Var v = var(trail[i]);
 
         if (hasReasonClause(v) && (ca[reason(v)].reloced() || locked(ca[reason(v)])))
-          ca.reloc(vardata[v].reason, to, NULLPROOF( ProofManager::getSatProof()->getProxy() ));
+          ca.reloc(
+              vardata[v].reason, to, NULLPROOF(ProofManager::getSatProof()));
     }
     // All learnt:
     //
     for (int i = 0; i < clauses_removable.size(); i++)
-      ca.reloc(clauses_removable[i], to,  NULLPROOF( ProofManager::getSatProof()->getProxy() ));
+      ca.reloc(
+          clauses_removable[i], to, NULLPROOF(ProofManager::getSatProof()));
 
     // All original:
     //
     for (int i = 0; i < clauses_persistent.size(); i++)
-      ca.reloc(clauses_persistent[i], to,  NULLPROOF( ProofManager::getSatProof()->getProxy() ));
+      ca.reloc(
+          clauses_persistent[i], to, NULLPROOF(ProofManager::getSatProof()));
 
-      PROOF( ProofManager::getSatProof()->finishUpdateCRef(); )
+    PROOF(ProofManager::getSatProof()->finishUpdateCRef();)
 }
 
 
@@ -1811,7 +1814,9 @@ CRef Solver::updateLemmas() {
   return conflict;
 }
 
-void ClauseAllocator::reloc(CRef& cr, ClauseAllocator& to, CVC4::CoreProofProxy* proxy)
+void ClauseAllocator::reloc(CRef& cr,
+                            ClauseAllocator& to,
+                            CVC4::TSatProof<Solver>* proof)
 {
 
   // FIXME what is this CRef_lazy
@@ -1823,8 +1828,9 @@ void ClauseAllocator::reloc(CRef& cr, ClauseAllocator& to, CVC4::CoreProofProxy*
 
   cr = to.alloc(c.level(), c, c.removable());
   c.relocate(cr);
-  if (proxy) {
-    proxy->updateCRef(old, cr);
+  if (proof)
+  {
+    proof->updateCRef(old, cr);
   }
   // Copy extra data-fields:
   // (This could be cleaned-up. Generalize Clause-constructor to be applicable here instead?)

diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h
index 116a39a49debdb4c829048c47c063af7a9fcc4e6..bbd6e17a2ac7edd0d491a684aea39c3d5d2a3b3c 100644 (file)
--- a/src/prop/minisat/core/SolverTypes.h
+++ b/src/prop/minisat/core/SolverTypes.h
@@ -31,6 +31,14 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/minisat/mtl/Map.h"
 #include "prop/minisat/mtl/Alloc.h"
 
+namespace CVC4 {
+namespace Minisat {
+class Solver;
+}
+template <class Solver>
+class TSatProof;
+}  // namespace CVC4
+
 namespace CVC4 {
 namespace Minisat {
 
@@ -168,24 +176,10 @@ inline std::ostream& operator <<(std::ostream& out, Minisat::lbool val) {
   return out;
 }
 
-
-class Solver;
-
-class ProofProxyAbstract {
-public:
-  virtual ~ProofProxyAbstract() {}
-  virtual void updateCRef(Minisat::CRef oldref, Minisat::CRef newref) = 0; 
-};
-
 } /* namespace CVC4::Minisat */
 } /* namespace CVC4 */
 
 
-namespace CVC4 {
-template <class Solver> class ProofProxy;
-typedef ProofProxy<CVC4::Minisat::Solver> CoreProofProxy;
-} 
-
 namespace CVC4 {
 namespace Minisat{
 
@@ -307,8 +301,10 @@ class ClauseAllocator : public RegionAllocator<uint32_t>
         RegionAllocator<uint32_t>::free(clauseWord32Size(c.size(), c.has_extra()));
     }
 
-  void reloc(CRef& cr, ClauseAllocator& to, CVC4::CoreProofProxy* proxy = NULL);
-  // Implementation moved to Solver.cc.
+    void reloc(CRef& cr,
+               ClauseAllocator& to,
+               CVC4::TSatProof<Solver>* proof = NULL);
+    // Implementation moved to Solver.cc.
 };