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 | |
parent | 7f13c0713accdefa46ce2a43dbeae8c46255bea1 (diff) |
fixes to the proof system so it works with theory lemmas and explanations
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/sat_proof.cpp | 34 | ||||
-rw-r--r-- | src/proof/sat_proof.h | 9 |
2 files changed, 39 insertions, 4 deletions
diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp index df695c2d1..2c0c7d036 100644 --- a/src/proof/sat_proof.cpp +++ b/src/proof/sat_proof.cpp @@ -173,7 +173,9 @@ SatProof::SatProof(Minisat::Solver* solver, bool checkRes) : d_emptyClauseId(-1), d_nullId(-2), d_temp_clauseId(), - d_temp_idClause() + d_temp_idClause(), + d_unitConflictId(), + d_storedUnitConflict(false) { d_proxy = new ProofProxy(this); } @@ -353,6 +355,7 @@ ClauseId SatProof::registerClause(::Minisat::CRef clause, bool isInput) { d_inputClauses.insert(newId); } } + Debug("proof:sat:detailed") <<"registerClause " << d_clauseId[clause] << " " <<isInput << "\n"; return d_clauseId[clause]; } @@ -367,6 +370,7 @@ ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, bool isInput) { d_inputClauses.insert(newId); } } + Debug("proof:sat:detailed") <<"registerUnitClause " << d_unitId[toInt(lit)] << " " << isInput <<"\n"; return d_unitId[toInt(lit)]; } @@ -527,10 +531,25 @@ void SatProof::toStream(std::ostream& out) { Unimplemented("native proof printing not supported yet"); } +void SatProof::storeUnitConflict(::Minisat::Lit conflict_lit) { + Assert (!d_storedUnitConflict); + d_unitConflictId = registerUnitClause(conflict_lit); + d_storedUnitConflict = true; + Debug("proof:sat:detailed") <<"storeUnitConflict " << d_unitConflictId << "\n"; +} + void SatProof::finalizeProof(::Minisat::CRef conflict_ref) { Assert(d_resStack.size() == 0); - //ClauseId conflict_id = getClauseId(conflict_ref); - ClauseId conflict_id = registerClause(conflict_ref); //FIXME + Assert (conflict_ref != ::Minisat::CRef_Undef); + ClauseId conflict_id; + if (conflict_ref == ::Minisat::CRef_Lazy) { + Assert (d_storedUnitConflict); + conflict_id = d_unitConflictId; + } else { + Assert (!d_storedUnitConflict); + conflict_id = registerClause(conflict_ref); //FIXME + } + Debug("proof:sat") << "proof::finalizeProof Final Conflict "; print(conflict_id); @@ -613,6 +632,7 @@ void LFSCSatProof::collectLemmas(ClauseId id) { d_seenLemmas.insert(id); } + Assert (d_resChains.find(id) != d_resChains.end()); ResChain* res = d_resChains[id]; ClauseId start = res->getStart(); collectLemmas(start); @@ -658,6 +678,14 @@ void LFSCSatProof::printResolution(ClauseId id) { void LFSCSatProof::printInputClause(ClauseId id) { + if (isUnit(id)) { + ::Minisat::Lit lit = getUnit(id); + d_clauseSS << "(% " << clauseName(id) << " (holds (clc "; + d_clauseSS << varName(lit) << "cln ))"; + d_paren << ")"; + return; + } + ostringstream os; CRef ref = getClauseRef(id); Assert (ref != CRef_Undef); 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. |