summaryrefslogtreecommitdiff
path: root/src/proof/sat_proof.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/sat_proof.h')
-rw-r--r--src/proof/sat_proof.h134
1 files changed, 67 insertions, 67 deletions
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index a4178f518..477eeeb99 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -9,7 +9,7 @@
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief Resolution proof
+ ** \brief Resolution proof
**
** Resolution proof
**/
@@ -43,11 +43,11 @@ namespace std {
namespace CVC4 {
-/**
+/**
* Helper debugging functions
*/
void printDebug(::Minisat::Lit l);
-void printDebug(::Minisat::Clause& c);
+void printDebug(::Minisat::Clause& c);
struct ResStep {
::Minisat::Lit lit;
@@ -60,8 +60,8 @@ struct ResStep {
{}
};/* struct ResStep */
-typedef std::vector< ResStep > ResSteps;
-typedef std::set < ::Minisat::Lit> LitSet;
+typedef std::vector< ResStep > ResSteps;
+typedef std::set < ::Minisat::Lit> LitSet;
class ResChain {
private:
@@ -72,7 +72,7 @@ public:
ResChain(ClauseId start);
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; }
@@ -83,16 +83,16 @@ public:
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_map < int, ClauseId> UnitIdMap; //FIXME
+typedef std::hash_map < ClauseId, ResChain*> IdResMap;
typedef std::hash_set < ClauseId > IdHashSet;
-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 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;
-class SatProof;
+class SatProof;
class ProofProxy : public ProofProxyAbstract {
private:
@@ -103,31 +103,31 @@ public:
};/* class ProofProxy */
-class CnfProof;
+class CnfProof;
class SatProof {
protected:
::Minisat::Solver* d_solver;
- // clauses
+ // clauses
IdCRefMap d_idClause;
ClauseIdMap d_clauseId;
IdUnitMap d_idUnit;
UnitIdMap d_unitId;
IdHashSet d_deleted;
- IdToSatClause d_deletedTheoryLemmas;
- IdHashSet d_inputClauses;
- IdHashSet d_lemmaClauses;
- // resolutions
+ IdToSatClause d_deletedTheoryLemmas;
+ IdHashSet d_inputClauses;
+ IdHashSet d_lemmaClauses;
+ // resolutions
IdResMap d_resChains;
- ResStack d_resStack;
+ ResStack d_resStack;
bool d_checkRes;
-
- static ClauseId d_idCounter;
+
+ static ClauseId d_idCounter;
const ClauseId d_emptyClauseId;
const ClauseId d_nullId;
- // proxy class to break circular dependencies
+ // proxy class to break circular dependencies
ProofProxy* d_proxy;
-
+
// temporary map for updating CRefs
ClauseIdMap d_temp_clauseId;
IdCRefMap d_temp_idClause;
@@ -135,43 +135,43 @@ protected:
// unit conflict
ClauseId d_unitConflictId;
bool d_storedUnitConflict;
-public:
+public:
SatProof(::Minisat::Solver* solver, bool checkRes = false);
virtual ~SatProof() {}
protected:
- void print(ClauseId id);
+ void print(ClauseId id);
void printRes(ClauseId id);
- void printRes(ResChain* res);
-
+ void printRes(ResChain* res);
+
bool isInputClause(ClauseId id);
bool isLemmaClause(ClauseId id);
bool isUnit(ClauseId id);
- bool isUnit(::Minisat::Lit lit);
- bool hasResolution(ClauseId id);
- void createLitSet(ClauseId id, LitSet& set);
+ 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);
+ ClauseId getClauseId(::Minisat::Lit lit);
::Minisat::CRef getClauseRef(ClauseId id);
::Minisat::Lit getUnit(ClauseId id);
- ClauseId getUnitId(::Minisat::Lit lit);
+ ClauseId getUnitId(::Minisat::Lit lit);
::Minisat::Clause& getClause(::Minisat::CRef ref);
virtual void toStream(std::ostream& out);
bool checkResolution(ClauseId id);
- /**
+ /**
* Constructs a resolution tree that proves lit
* and returns the ClauseId for the unit clause lit
* @param lit the literal we are proving
- *
- * @return
+ *
+ * @return
*/
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.
- *
+ * to be removed in the proper order to the stack.
+ *
* @param lit the literal we are recursing on
* @param removedSet the previously computed set of redundant literals
* @param removeStack the stack of literals in reverse order of resolution
@@ -181,71 +181,71 @@ protected:
public:
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
+ * @param clause the clause the resolution is proving
*/
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
+ /**
+ * 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);
/// update the CRef Id maps when Minisat does memory reallocation x
void updateCRef(::Minisat::CRef old_ref, ::Minisat::CRef new_ref);
void finishUpdateCRef();
-
- /**
+
+ /**
* Constructs the empty clause resolution from the final conflict
- *
- * @param conflict
+ *
+ * @param conflict
*/
void finalizeProof(::Minisat::CRef conflict);
- /// clause registration methods
+ /// clause registration methods
ClauseId registerClause(const ::Minisat::CRef clause, ClauseKind kind = LEARNT);
ClauseId registerUnitClause(const ::Minisat::Lit lit, ClauseKind kind = LEARNT);
- void storeUnitConflict(::Minisat::Lit lit);
-
- /**
+ void storeUnitConflict(::Minisat::Lit lit, ClauseKind kind = LEARNT);
+
+ /**
* Marks the deleted clauses as deleted. Note we may still use them in the final
- * resolution.
- * @param clause
+ * resolution.
+ * @param 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);
- /**
+ /**
* Constructs the resolution of the literal lit. Called when a clause
- * containing lit becomes satisfied and is removed.
- * @param lit
+ * containing lit becomes satisfied and is removed.
+ * @param lit
*/
- void storeUnitResolution(::Minisat::Lit lit);
-
+ void storeUnitResolution(::Minisat::Lit lit);
+
ProofProxy* getProxy() {return d_proxy; }
/**
- Constructs the SAT proof identifying the needed lemmas
+ Constructs the SAT proof identifying the needed lemmas
*/
void constructProof();
-
+
protected:
IdSet d_seenLearnt;
IdHashSet d_seenInput;
- IdHashSet d_seenLemmas;
-
+ IdHashSet d_seenLemmas;
+
inline std::string varName(::Minisat::Lit lit);
- inline std::string clauseName(ClauseId id);
+ inline std::string clauseName(ClauseId id);
void collectClauses(ClauseId id);
void addToProofManager(ClauseId id, ClauseKind kind);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback