summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2018-05-23 06:53:06 -0700
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>2018-05-23 08:53:06 -0500
commit4c2138a14c4abba2431bc8ba51359d3a565baf05 (patch)
tree4bf45363b8b76895138669cd8097c2be49f02f80
parent8de9510b8aa818f555294ebe88d9733cc10ff8b9 (diff)
Remove ProofProxy (#1965)
-rw-r--r--src/proof/proof_manager.h4
-rw-r--r--src/proof/sat_proof.h15
-rw-r--r--src/proof/sat_proof_implementation.h13
-rw-r--r--src/prop/bvminisat/core/Solver.cc19
-rw-r--r--src/prop/bvminisat/core/SolverTypes.h8
-rw-r--r--src/prop/minisat/core/Solver.cc24
-rw-r--r--src/prop/minisat/core/SolverTypes.h28
7 files changed, 43 insertions, 68 deletions
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 047c32e83..d1833fd07 100644
--- 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 19a8d30cf..57e3a9bc1 100644
--- 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 daf98ceea..e3cbae361 100644
--- 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 885e429f0..8d71e2f65 100644
--- 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 1fd7ac5a7..302db104f 100644
--- 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 b034f8460..0967f434c 100644
--- 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 116a39a49..bbd6e17a2 100644
--- a/src/prop/minisat/core/SolverTypes.h
+++ b/src/prop/minisat/core/SolverTypes.h
@@ -33,6 +33,14 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
namespace CVC4 {
namespace Minisat {
+class Solver;
+}
+template <class Solver>
+class TSatProof;
+} // namespace CVC4
+
+namespace CVC4 {
+namespace Minisat {
//=================================================================================================
// Variables, literals, lifted booleans, clauses:
@@ -168,25 +176,11 @@ 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.
};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback