diff options
author | guykatzz <katz911@gmail.com> | 2017-03-23 14:13:46 -0700 |
---|---|---|
committer | guykatzz <katz911@gmail.com> | 2017-03-23 14:13:46 -0700 |
commit | 16c0d86ae359fc16064e29ed7545db5896366c9b (patch) | |
tree | 71706cd01f2adde9fb94cfacab67ef284ef2c200 /src/proof/sat_proof.h | |
parent | 99ea8403a0f41387fef1a42abe45817fb191aa12 (diff) |
support incremental unsat cores
Diffstat (limited to 'src/proof/sat_proof.h')
-rw-r--r-- | src/proof/sat_proof.h | 19 |
1 files changed, 12 insertions, 7 deletions
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index 52e059e95..5691d1bd2 100644 --- a/src/proof/sat_proof.h +++ b/src/proof/sat_proof.h @@ -28,6 +28,7 @@ #include <sstream> #include <vector> +#include "context/cdhashmap.h" #include "expr/expr.h" #include "proof/clause_id.h" #include "proof/proof_manager.h" @@ -101,9 +102,9 @@ class TSatProof { typedef std::set<typename Solver::TVar> VarSet; typedef std::hash_map<ClauseId, typename Solver::TCRef> IdCRefMap; typedef std::hash_map<typename Solver::TCRef, ClauseId> ClauseIdMap; - typedef std::hash_map<ClauseId, typename Solver::TLit> IdUnitMap; - typedef std::hash_map<int, ClauseId> UnitIdMap; - typedef std::hash_map<ClauseId, ResolutionChain*> IdResMap; + typedef context::CDHashMap<ClauseId, typename Solver::TLit> IdUnitMap; + typedef context::CDHashMap<int, ClauseId> UnitIdMap; + typedef context::CDHashMap<ClauseId, ResolutionChain*> IdResMap; typedef std::hash_map<ClauseId, uint64_t> IdProofRuleMap; typedef std::vector<ResolutionChain*> ResStack; typedef std::set<ClauseId> IdSet; @@ -113,7 +114,8 @@ class TSatProof { typedef __gnu_cxx::hash_map<ClauseId, LitVector*> IdToConflicts; public: - TSatProof(Solver* solver, const std::string& name, bool checkRes = false); + TSatProof(Solver* solver, context::Context* context, + const std::string& name, bool checkRes = false); virtual ~TSatProof(); void setCnfProof(CnfProof* cnf_proof); @@ -198,6 +200,8 @@ class TSatProof { */ void constructProof(ClauseId id); void constructProof() { constructProof(d_emptyClauseId); } + void refreshProof(ClauseId id); + void refreshProof() { refreshProof(d_emptyClauseId); } bool proofConstructed() const; void collectClauses(ClauseId id); bool derivedEmptyClause() const; @@ -298,6 +302,7 @@ class TSatProof { // Internal data. typename Solver::Solver* d_solver; + context::Context* d_context; CnfProof* d_cnfProof; // clauses @@ -389,9 +394,9 @@ template <class SatSolver> class LFSCSatProof : public TSatProof<SatSolver> { private: public: - LFSCSatProof(SatSolver* solver, const std::string& name, - bool checkRes = false) - : TSatProof<SatSolver>(solver, name, checkRes) {} + LFSCSatProof(SatSolver* solver, context::Context* context, + const std::string& name, bool checkRes = false) + : TSatProof<SatSolver>(solver, context, name, checkRes) {} virtual void printResolution(ClauseId id, std::ostream& out, std::ostream& paren); virtual void printResolutions(std::ostream& out, std::ostream& paren); |