diff options
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. |