diff options
author | Finn Haedicke <finn@informatik.uni-bremen.de> | 2015-04-17 10:46:07 +0200 |
---|---|---|
committer | Finn Haedicke <finn@informatik.uni-bremen.de> | 2015-04-17 10:46:07 +0200 |
commit | ca31b5f9de8575b9d6878c7ad7a674e48ae3c6df (patch) | |
tree | 1de4d4cfb4fe2ab95f6dc7b731056389677f13ca /src/proof/sat_proof.h | |
parent | 1c95df5efa3727a8b709049ef26ebb3fe6f0c6eb (diff) |
moved Minisat namespace into CVC4
This avoids conflicts when CVC4 is linked to an application that
also uses plain Minisat.
Diffstat (limited to 'src/proof/sat_proof.h')
-rw-r--r-- | src/proof/sat_proof.h | 80 |
1 files changed, 41 insertions, 39 deletions
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index 7c195c83d..a9793e784 100644 --- a/src/proof/sat_proof.h +++ b/src/proof/sat_proof.h @@ -29,10 +29,12 @@ #include "expr/expr.h" #include "proof/proof_manager.h" +namespace CVC4 { namespace Minisat { class Solver; typedef uint32_t CRef; }/* Minisat namespace */ +} #include "prop/minisat/core/SolverTypes.h" #include "util/proof.h" @@ -46,14 +48,14 @@ namespace CVC4 { /** * Helper debugging functions */ -void printDebug(::Minisat::Lit l); -void printDebug(::Minisat::Clause& c); +void printDebug(Minisat::Lit l); +void printDebug(Minisat::Clause& c); struct ResStep { - ::Minisat::Lit lit; + Minisat::Lit lit; ClauseId id; bool sign; - ResStep(::Minisat::Lit l, ClauseId i, bool s) : + ResStep(Minisat::Lit l, ClauseId i, bool s) : lit(l), id(i), sign(s) @@ -61,7 +63,7 @@ struct ResStep { };/* struct ResStep */ typedef std::vector< ResStep > ResSteps; -typedef std::set < ::Minisat::Lit> LitSet; +typedef std::set < Minisat::Lit> LitSet; class ResChain { private: @@ -70,9 +72,9 @@ private: LitSet* d_redundantLits; public: ResChain(ClauseId start); - void addStep(::Minisat::Lit, ClauseId, bool); + void addStep(Minisat::Lit, ClauseId, bool); bool redundantRemoved() { return (d_redundantLits == NULL || d_redundantLits->empty()); } - void addRedundantLit(::Minisat::Lit lit); + void addRedundantLit(Minisat::Lit lit); ~ResChain(); // accessor methods ClauseId getStart() { return d_start; } @@ -80,9 +82,9 @@ public: LitSet* getRedundant() { return d_redundantLits; } };/* class ResChain */ -typedef std::hash_map < ClauseId, ::Minisat::CRef > IdCRefMap; -typedef std::hash_map < ::Minisat::CRef, ClauseId > ClauseIdMap; -typedef std::hash_map < ClauseId, ::Minisat::Lit> IdUnitMap; +typedef std::hash_map < ClauseId, Minisat::CRef > IdCRefMap; +typedef std::hash_map < Minisat::CRef, ClauseId > ClauseIdMap; +typedef std::hash_map < ClauseId, Minisat::Lit> IdUnitMap; typedef std::hash_map < int, ClauseId> UnitIdMap; //FIXME typedef std::hash_map < ClauseId, ResChain*> IdResMap; typedef std::hash_set < ClauseId > IdHashSet; @@ -90,8 +92,8 @@ typedef std::hash_map < ClauseId, uint64_t > IdProofRuleMap; typedef std::vector < ResChain* > ResStack; typedef std::hash_map <ClauseId, prop::SatClause* > IdToSatClause; typedef std::set < ClauseId > IdSet; -typedef std::vector < ::Minisat::Lit > LitVector; -typedef __gnu_cxx::hash_map<ClauseId, ::Minisat::Clause& > IdToMinisatClause; +typedef std::vector < Minisat::Lit > LitVector; +typedef __gnu_cxx::hash_map<ClauseId, Minisat::Clause& > IdToMinisatClause; class SatProof; @@ -100,7 +102,7 @@ private: SatProof* d_proof; public: ProofProxy(SatProof* pf); - void updateCRef(::Minisat::CRef oldref, ::Minisat::CRef newref); + void updateCRef(Minisat::CRef oldref, Minisat::CRef newref); };/* class ProofProxy */ @@ -108,7 +110,7 @@ class CnfProof; class SatProof { protected: - ::Minisat::Solver* d_solver; + Minisat::Solver* d_solver; // clauses IdCRefMap d_idClause; ClauseIdMap d_clauseId; @@ -138,7 +140,7 @@ protected: ClauseId d_unitConflictId; bool d_storedUnitConflict; public: - SatProof(::Minisat::Solver* solver, bool checkRes = false); + SatProof(Minisat::Solver* solver, bool checkRes = false); virtual ~SatProof(); protected: void print(ClauseId id); @@ -149,17 +151,17 @@ protected: bool isTheoryConflict(ClauseId id); bool isLemmaClause(ClauseId id); bool isUnit(ClauseId id); - bool isUnit(::Minisat::Lit lit); + bool isUnit(Minisat::Lit lit); bool hasResolution(ClauseId id); void createLitSet(ClauseId id, LitSet& set); void registerResolution(ClauseId id, ResChain* res); - ClauseId getClauseId(::Minisat::CRef clause); - ClauseId getClauseId(::Minisat::Lit lit); - ::Minisat::CRef getClauseRef(ClauseId id); - ::Minisat::Lit getUnit(ClauseId id); - ClauseId getUnitId(::Minisat::Lit lit); - ::Minisat::Clause& getClause(::Minisat::CRef ref); + ClauseId getClauseId(Minisat::CRef clause); + ClauseId getClauseId(Minisat::Lit lit); + Minisat::CRef getClauseRef(ClauseId id); + Minisat::Lit getUnit(ClauseId id); + ClauseId getUnitId(Minisat::Lit lit); + Minisat::Clause& getClause(Minisat::CRef ref); virtual void toStream(std::ostream& out); bool checkResolution(ClauseId id); @@ -170,7 +172,7 @@ protected: * * @return */ - ClauseId resolveUnit(::Minisat::Lit lit); + ClauseId resolveUnit(Minisat::Lit lit); /** * Does a depth first search on removed literals and adds the literals * to be removed in the proper order to the stack. @@ -179,27 +181,27 @@ protected: * @param removedSet the previously computed set of redundant literals * @param removeStack the stack of literals in reverse order of resolution */ - void removedDfs(::Minisat::Lit lit, LitSet* removedSet, LitVector& removeStack, LitSet& inClause, LitSet& seen); + void removedDfs(Minisat::Lit lit, LitSet* removedSet, LitVector& removeStack, LitSet& inClause, LitSet& seen); void removeRedundantFromRes(ResChain* res, ClauseId id); public: - void startResChain(::Minisat::CRef start); - void addResolutionStep(::Minisat::Lit lit, ::Minisat::CRef clause, bool sign); + void startResChain(Minisat::CRef start); + void addResolutionStep(Minisat::Lit lit, Minisat::CRef clause, bool sign); /** * Pops the current resolution of the stack and stores it * in the resolution map. Also registers the 'clause' parameter * @param clause the clause the resolution is proving */ - void endResChain(::Minisat::CRef clause); - void endResChain(::Minisat::Lit lit); + void endResChain(Minisat::CRef clause); + void endResChain(Minisat::Lit lit); /** * Stores in the current derivation the redundant literals that were * eliminated from the conflict clause during conflict clause minimization. * @param lit the eliminated literal */ - void storeLitRedundant(::Minisat::Lit lit); + void storeLitRedundant(Minisat::Lit lit); /// update the CRef Id maps when Minisat does memory reallocation x - void updateCRef(::Minisat::CRef old_ref, ::Minisat::CRef new_ref); + void updateCRef(Minisat::CRef old_ref, Minisat::CRef new_ref); void finishUpdateCRef(); /** @@ -207,33 +209,33 @@ public: * * @param conflict */ - void finalizeProof(::Minisat::CRef conflict); + void finalizeProof(Minisat::CRef conflict); /// clause registration methods - ClauseId registerClause(const ::Minisat::CRef clause, ClauseKind kind, uint64_t proof_id); - ClauseId registerUnitClause(const ::Minisat::Lit lit, ClauseKind kind, uint64_t proof_id); + ClauseId registerClause(const Minisat::CRef clause, ClauseKind kind, uint64_t proof_id); + ClauseId registerUnitClause(const Minisat::Lit lit, ClauseKind kind, uint64_t proof_id); - void storeUnitConflict(::Minisat::Lit lit, ClauseKind kind, uint64_t proof_id); + void storeUnitConflict(Minisat::Lit lit, ClauseKind kind, uint64_t proof_id); /** * Marks the deleted clauses as deleted. Note we may still use them in the final * resolution. * @param clause */ - void markDeleted(::Minisat::CRef clause); + void markDeleted(Minisat::CRef clause); bool isDeleted(ClauseId id) { return d_deleted.find(id) != d_deleted.end(); } /** * Constructs the resolution of ~q and resolves it with the current * resolution thus eliminating q from the current clause * @param q the literal to be resolved out */ - void resolveOutUnit(::Minisat::Lit q); + void resolveOutUnit(Minisat::Lit q); /** * Constructs the resolution of the literal lit. Called when a clause * containing lit becomes satisfied and is removed. * @param lit */ - void storeUnitResolution(::Minisat::Lit lit); + void storeUnitResolution(Minisat::Lit lit); ProofProxy* getProxy() {return d_proxy; } @@ -248,7 +250,7 @@ protected: IdHashSet d_seenTheoryConflicts; IdHashSet d_seenLemmas; - inline std::string varName(::Minisat::Lit lit); + inline std::string varName(Minisat::Lit lit); inline std::string clauseName(ClauseId id); void collectClauses(ClauseId id); @@ -261,7 +263,7 @@ class LFSCSatProof : public SatProof { private: void printResolution(ClauseId id, std::ostream& out, std::ostream& paren); public: - LFSCSatProof(::Minisat::Solver* solver, bool checkRes = false) + LFSCSatProof(Minisat::Solver* solver, bool checkRes = false) : SatProof(solver, checkRes) {} virtual void printResolutions(std::ostream& out, std::ostream& paren); |