diff options
| author | lianah <lianahady@gmail.com> | 2013-05-10 15:52:37 -0400 |
|---|---|---|
| committer | lianah <lianahady@gmail.com> | 2013-05-10 15:52:45 -0400 |
| commit | f84120cd5311450de2075a91356524d4e20d457c (patch) | |
| tree | 1a9220eee3d0063b76794bca414a26132007d8dd /src/proof/sat_proof.h | |
| parent | 7f13c0713accdefa46ce2a43dbeae8c46255bea1 (diff) | |
fixes to the proof system so it works with theory lemmas and explanations
Diffstat (limited to 'src/proof/sat_proof.h')
| -rw-r--r-- | src/proof/sat_proof.h | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index d497a4eba..a552b66fd 100644 --- a/src/proof/sat_proof.h +++ b/src/proof/sat_proof.h @@ -124,7 +124,11 @@ protected: // temporary map for updating CRefs ClauseIdMap d_temp_clauseId; - IdClauseMap d_temp_idClause; + IdClauseMap d_temp_idClause; + + // unit conflict + ClauseId d_unitConflictId; + bool d_storedUnitConflict; public: SatProof(::Minisat::Solver* solver, bool checkRes = false); protected: @@ -197,6 +201,9 @@ public: /// clause registration methods ClauseId registerClause(const ::Minisat::CRef clause, bool isInput = false); ClauseId registerUnitClause(const ::Minisat::Lit lit, bool isInput = false); + + void storeUnitConflict(::Minisat::Lit lit); + /** * Marks the deleted clauses as deleted. Note we may still use them in the final * resolution. |