diff options
Diffstat (limited to 'src/proof/sat_proof_implementation.h')
-rw-r--r-- | src/proof/sat_proof_implementation.h | 1100 |
1 files changed, 1100 insertions, 0 deletions
diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h new file mode 100644 index 000000000..92645e105 --- /dev/null +++ b/src/proof/sat_proof_implementation.h @@ -0,0 +1,1100 @@ +/********************* */ +/*! \file sat_proof_implementation.h + ** \verbatim + ** Original author: Liana Hadarean + ** Major contributors: Morgan Deters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Resolution proof + ** + ** Resolution proof + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__SAT__PROOF_IMPLEMENTATION_H +#define __CVC4__SAT__PROOF_IMPLEMENTATION_H + +#include "proof/sat_proof.h" +#include "proof/cnf_proof.h" +#include "prop/minisat/minisat.h" +#include "prop/bvminisat/bvminisat.h" +#include "prop/minisat/core/Solver.h" +#include "prop/bvminisat/core/Solver.h" +#include "prop/sat_solver_types.h" +#include "smt/smt_statistics_registry.h" + +namespace CVC4 { + +template <class Solver> +void printLit (typename Solver::TLit l) { + Debug("proof:sat") << (sign(l) ? "-" : "") << var(l) + 1; +} + +template <class Solver> +void printClause (typename Solver::TClause& c) { + for (int i = 0; i < c.size(); i++) { + Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; + } +} + +template <class Solver> +void printClause (std::vector<typename Solver::TLit>& c) { + for (unsigned i = 0; i < c.size(); i++) { + Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; + } +} + + +template <class Solver> +void printLitSet(const std::set<typename Solver::TLit>& s) { + typename std::set < typename Solver::TLit>::const_iterator it = s.begin(); + for(; it != s.end(); ++it) { + printLit<Solver>(*it); + Debug("proof:sat") << " "; + } + Debug("proof:sat") << std::endl; +} + +// purely debugging functions +template <class Solver> +void printDebug (typename Solver::TLit l) { + Debug("proof:sat") << (sign(l) ? "-" : "") << var(l) + 1 << std::endl; +} +template <class Solver> +void printDebug (typename Solver::TClause& c) { + for (int i = 0; i < c.size(); i++) { + Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; + } + Debug("proof:sat") << std::endl; +} + + +/** + * Converts the clause associated to id to a set of literals + * + * @param id the clause id + * @param set the clause converted to a set of literals + */ +template <class Solver> +void TSatProof<Solver>::createLitSet(ClauseId id, LitSet& set) { + Assert(set.empty()); + if(isUnit(id)) { + set.insert(getUnit(id)); + return; + } + if ( id == d_emptyClauseId) { + return; + } + // if it's an assumption + if (d_assumptionConflictsDebug.find(id) != d_assumptionConflictsDebug.end()) { + LitVector* clause = d_assumptionConflictsDebug[id]; + for (unsigned i = 0; i < clause->size(); ++i) { + set.insert(clause->operator[](i)); + } + return; + } + + typename Solver::TCRef ref = getClauseRef(id); + typename Solver::TClause& c = getClause(ref); + for (int i = 0; i < c.size(); i++) { + set.insert(c[i]); + } +} + + +/** + * Resolves clause1 and clause2 on variable var and stores the + * result in clause1 + * @param v + * @param clause1 + * @param clause2 + */ +template <class Solver> +bool resolve(const typename Solver::TLit v, + std::set<typename Solver::TLit>& clause1, + std::set<typename Solver::TLit>& clause2, bool s) { + Assert(!clause1.empty()); + Assert(!clause2.empty()); + typename Solver::TLit var = sign(v) ? ~v : v; + if (s) { + // literal appears positive in the first clause + if( !clause2.count(~var)) { + if(Debug.isOn("proof:sat")) { + Debug("proof:sat") << "proof:resolve: Missing literal "; + printLit<Solver>(var); + Debug("proof:sat") << std::endl; + } + return false; + } + clause1.erase(var); + clause2.erase(~var); + typename std::set<typename Solver::TLit>::iterator it = clause2.begin(); + for (; it!= clause2.end(); ++it) { + clause1.insert(*it); + } + } else { + // literal appears negative in the first clause + if( !clause1.count(~var) || !clause2.count(var)) { + if(Debug.isOn("proof:sat")) { + Debug("proof:sat") << "proof:resolve: Missing literal "; + printLit<Solver>(var); + Debug("proof:sat") << std::endl; + } + return false; + } + clause1.erase(~var); + clause2.erase(var); + typename std::set<typename Solver::TLit>::iterator it = clause2.begin(); + for (; it!= clause2.end(); ++it) { + clause1.insert(*it); + } + } + return true; +} + +/// ResChain +template <class Solver> +ResChain<Solver>::ResChain(ClauseId start) : + d_start(start), + d_steps(), + d_redundantLits(NULL) + {} +template <class Solver> +void ResChain<Solver>::addStep(typename Solver::TLit lit, ClauseId id, bool sign) { + ResStep<Solver> step(lit, id, sign); + d_steps.push_back(step); +} + +template <class Solver> +void ResChain<Solver>::addRedundantLit(typename Solver::TLit lit) { + if (d_redundantLits) { + d_redundantLits->insert(lit); + } else { + d_redundantLits = new LitSet(); + d_redundantLits->insert(lit); + } +} + + +/// ProxyProof +template <class Solver> +ProofProxy<Solver>::ProofProxy(TSatProof<Solver>* proof): + d_proof(proof) +{} + +template <class Solver> +void ProofProxy<Solver>::updateCRef(typename Solver::TCRef oldref, typename Solver::TCRef newref) { + d_proof->updateCRef(oldref, newref); +} + + +/// SatProof +template <class Solver> +TSatProof<Solver>::TSatProof(Solver* solver, const std::string& name, bool checkRes) + : d_solver(solver) + , d_cnfProof(NULL) + , d_idClause() + , d_clauseId() + , d_idUnit() + , d_deleted() + , d_inputClauses() + , d_lemmaClauses() + , d_assumptions() + , d_assumptionConflicts() + , d_assumptionConflictsDebug() + , d_resChains() + , d_resStack() + , d_checkRes(checkRes) + , d_emptyClauseId(ClauseIdEmpty) + , d_nullId(-2) + , d_temp_clauseId() + , d_temp_idClause() + , d_unitConflictId() + , d_storedUnitConflict(false) + , d_trueLit(ClauseIdUndef) + , d_falseLit(ClauseIdUndef) + , d_name(name) + , d_seenLearnt() + , d_seenInputs() + , d_seenLemmas() + , d_statistics(name) +{ + d_proxy = new ProofProxy<Solver>(this); +} + +template <class Solver> +TSatProof<Solver>::~TSatProof() { + delete d_proxy; + + // FIXME: double free if deleted clause also appears in d_seenLemmas? + IdToSatClause::iterator it = d_deletedTheoryLemmas.begin(); + IdToSatClause::iterator end = d_deletedTheoryLemmas.end(); + + for (; it != end; ++it) { + ClauseId id = it->first; + // otherwise deleted in next loop + if (d_seenLemmas.find(id) == d_seenLemmas.end()) + delete it->second; + } + + IdToSatClause::iterator seen_it = d_seenLemmas.begin(); + IdToSatClause::iterator seen_end = d_seenLemmas.end(); + + for (; seen_it != seen_end; ++seen_it) { + delete seen_it->second; + } + + seen_it = d_seenInputs.begin(); + seen_end = d_seenInputs.end(); + + for (; seen_it != seen_end; ++seen_it) { + delete seen_it->second; + } +} + +template <class Solver> +void TSatProof<Solver>::setCnfProof(CnfProof* cnf_proof) { + Assert (d_cnfProof == NULL); + d_cnfProof = cnf_proof; +} + +/** + * Returns true if the resolution chain corresponding to id + * does resolve to the clause associated to id + * @param id + * + * @return + */ +template <class Solver> +bool TSatProof<Solver>::checkResolution(ClauseId id) { + if(d_checkRes) { + bool validRes = true; + Assert(d_resChains.find(id) != d_resChains.end()); + ResChain<Solver>* res = d_resChains[id]; + LitSet clause1; + createLitSet(res->getStart(), clause1); + typename ResChain<Solver>::ResSteps& steps = res->getSteps(); + for (unsigned i = 0; i < steps.size(); i++) { + typename Solver::TLit var = steps[i].lit; + LitSet clause2; + createLitSet (steps[i].id, clause2); + bool res = resolve<Solver> (var, clause1, clause2, steps[i].sign); + if(res == false) { + validRes = false; + break; + } + } + // compare clause we claimed to prove with the resolution result + if (isUnit(id)) { + // special case if it was a unit clause + typename Solver::TLit unit = getUnit(id); + validRes = clause1.size() == clause1.count(unit) && !clause1.empty(); + return validRes; + } + if (id == d_emptyClauseId) { + return clause1.empty(); + } + + LitVector c; + getLitVec(id, c); + + for (unsigned i = 0; i < c.size(); ++i) { + int count = clause1.erase(c[i]); + if (count == 0) { + if(Debug.isOn("proof:sat")) { + Debug("proof:sat") << "proof:checkResolution::literal not in computed result "; + printLit<Solver>(c[i]); + Debug("proof:sat") << "\n"; + } + validRes = false; + } + } + validRes = clause1.empty(); + if (! validRes) { + if(Debug.isOn("proof:sat")) { + Debug("proof:sat") << "proof:checkResolution::Invalid Resolution, unremoved literals: \n"; + printLitSet<Solver>(clause1); + Debug("proof:sat") << "proof:checkResolution:: result should be: \n"; + printClause<Solver>(c); + } + } + return validRes; + + } else { + return true; + } +} + + + + +/// helper methods +template <class Solver> +ClauseId TSatProof<Solver>::getClauseId(typename Solver::TCRef ref) { + if(d_clauseId.find(ref) == d_clauseId.end()) { + Debug("proof:sat") << "Missing clause \n"; + } + Assert(d_clauseId.find(ref) != d_clauseId.end()); + return d_clauseId[ref]; +} + +template <class Solver> +ClauseId TSatProof<Solver>::getClauseId(typename Solver::TLit lit) { + Assert(d_unitId.find(toInt(lit)) != d_unitId.end()); + return d_unitId[toInt(lit)]; +} +template <class Solver> +typename Solver::TCRef TSatProof<Solver>::getClauseRef(ClauseId id) { + if (d_idClause.find(id) == d_idClause.end()) { + Debug("proof:sat") << "proof:getClauseRef cannot find clause "<<id<<" " + << ((d_deleted.find(id) != d_deleted.end()) ? "deleted" : "") + << (isUnit(id)? "Unit" : "") << std::endl; + } + Assert(d_idClause.find(id) != d_idClause.end()); + return d_idClause[id]; +} + +template <class Solver> +typename Solver::TClause& TSatProof<Solver>::getClause(typename Solver::TCRef ref) { + Assert(ref != Solver::TCRef_Undef); + Assert(ref >= 0 && ref < d_solver->ca.size()); + return d_solver->ca[ref]; +} + +template <class Solver> +void TSatProof<Solver>::getLitVec(ClauseId id, LitVector& vec) { + if (isUnit(id)) { + typename Solver::TLit lit = getUnit(id); + vec.push_back(lit); + return; + } + if (isAssumptionConflict(id)) { + vec = *(d_assumptionConflictsDebug[id]); + return; + } + typename Solver::TCRef cref = getClauseRef(id); + typename Solver::TClause& cl = getClause(cref); + for (int i = 0; i < cl.size(); ++i) { + vec.push_back(cl[i]); + } +} + + +template <class Solver> +typename Solver::TLit TSatProof<Solver>::getUnit(ClauseId id) { + Assert(d_idUnit.find(id) != d_idUnit.end()); + return d_idUnit[id]; +} +template <class Solver> +bool TSatProof<Solver>::isUnit(ClauseId id) { + return d_idUnit.find(id) != d_idUnit.end(); +} +template <class Solver> +bool TSatProof<Solver>::isUnit(typename Solver::TLit lit) { + return d_unitId.find(toInt(lit)) != d_unitId.end(); +} +template <class Solver> +ClauseId TSatProof<Solver>::getUnitId(typename Solver::TLit lit) { + Assert(isUnit(lit)); + return d_unitId[toInt(lit)]; +} +template <class Solver> +bool TSatProof<Solver>::hasResolution(ClauseId id) { + return d_resChains.find(id) != d_resChains.end(); +} +template <class Solver> +bool TSatProof<Solver>::isInputClause(ClauseId id) { + return (d_inputClauses.find(id) != d_inputClauses.end()); +} +template <class Solver> +bool TSatProof<Solver>::isLemmaClause(ClauseId id) { + return (d_lemmaClauses.find(id) != d_lemmaClauses.end()); +} + +template <class Solver> +bool TSatProof<Solver>::isAssumptionConflict(ClauseId id) { + return d_assumptionConflicts.find(id) != d_assumptionConflicts.end(); +} + + +template <class Solver> +void TSatProof<Solver>::print(ClauseId id) { + if (d_deleted.find(id) != d_deleted.end()) { + Debug("proof:sat") << "del"<<id; + } else if (isUnit(id)) { + printLit<Solver>(getUnit(id)); + } else if (id == d_emptyClauseId) { + Debug("proof:sat") << "empty "<< std::endl; + } + else { + typename Solver::TCRef ref = getClauseRef(id); + printClause<Solver>(getClause(ref)); + } +} +template <class Solver> +void TSatProof<Solver>::printRes(ClauseId id) { + Assert(hasResolution(id)); + Debug("proof:sat") << "id "<< id <<": "; + printRes(d_resChains[id]); +} +template <class Solver> +void TSatProof<Solver>::printRes(ResChain<Solver>* res) { + ClauseId start_id = res->getStart(); + + if(Debug.isOn("proof:sat")) { + Debug("proof:sat") << "("; + print(start_id); + } + + typename ResChain<Solver>::ResSteps& steps = res->getSteps(); + for(unsigned i = 0; i < steps.size(); i++ ) { + typename Solver::TLit v = steps[i].lit; + ClauseId id = steps[i].id; + + if(Debug.isOn("proof:sat")) { + Debug("proof:sat") << "["; + printLit<Solver>(v); + Debug("proof:sat") << "] "; + print(id); + } + } + Debug("proof:sat") << ") \n"; +} + +/// registration methods +template <class Solver> + ClauseId TSatProof<Solver>::registerClause(typename Solver::TCRef clause, + ClauseKind kind) { + Assert(clause != Solver::TCRef_Undef); + typename ClauseIdMap::iterator it = d_clauseId.find(clause); + if (it == d_clauseId.end()) { + ClauseId newId = ProofManager::currentPM()->nextId(); + d_clauseId.insert(std::make_pair(clause, newId)); + d_idClause.insert(std::make_pair(newId, clause)); + if (kind == INPUT) { + Assert(d_inputClauses.find(newId) == d_inputClauses.end()); + d_inputClauses.insert(newId); + } + if (kind == THEORY_LEMMA) { + Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end()); + d_lemmaClauses.insert(newId); + } + } + + ClauseId id = d_clauseId[clause]; + Assert(kind != INPUT || d_inputClauses.count(id)); + Assert(kind != THEORY_LEMMA || d_lemmaClauses.count(id)); + + Debug("proof:sat:detailed") << "registerClause CRef: " << clause << " id: " << d_clauseId[clause] + <<" kind: " << kind << "\n"; + //ProofManager::currentPM()->setRegisteredClauseId( d_clauseId[clause] ); + return id; +} + +template <class Solver> +ClauseId TSatProof<Solver>::registerUnitClause(typename Solver::TLit lit, + ClauseKind kind) { + Debug("cores") << "registerUnitClause " << kind << std::endl; + typename UnitIdMap::iterator it = d_unitId.find(toInt(lit)); + if (it == d_unitId.end()) { + ClauseId newId = ProofManager::currentPM()->nextId(); + d_unitId.insert(std::make_pair(toInt(lit), newId)); + d_idUnit.insert(std::make_pair(newId, lit)); + + if (kind == INPUT) { + Assert(d_inputClauses.find(newId) == d_inputClauses.end()); + d_inputClauses.insert(newId); + } + if (kind == THEORY_LEMMA) { + Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end()); + d_lemmaClauses.insert(newId); + } + } + ClauseId id = d_unitId[toInt(lit)]; + Assert(kind != INPUT || d_inputClauses.count(id)); + Assert(kind != THEORY_LEMMA || d_lemmaClauses.count(id)); + Debug("proof:sat:detailed") << "registerUnitClause id: " << id + <<" kind: " << kind << "\n"; + // ProofManager::currentPM()->setRegisteredClauseId( d_unitId[toInt(lit)] ); + return id; +} +template <class Solver> +void TSatProof<Solver>::registerTrueLit(const typename Solver::TLit lit) { + Assert (d_trueLit == ClauseIdUndef); + d_trueLit = registerUnitClause(lit, INPUT); +} + +template <class Solver> +void TSatProof<Solver>::registerFalseLit(const typename Solver::TLit lit) { + Assert (d_falseLit == ClauseIdUndef); + d_falseLit = registerUnitClause(lit, INPUT); +} + +template <class Solver> +ClauseId TSatProof<Solver>::getTrueUnit() const { + Assert (d_trueLit != ClauseIdUndef); + return d_trueLit; +} + +template <class Solver> +ClauseId TSatProof<Solver>::getFalseUnit() const { + Assert (d_falseLit != ClauseIdUndef); + return d_falseLit; +} + + +template <class Solver> +void TSatProof<Solver>::registerAssumption(const typename Solver::TVar var) { + Assert (d_assumptions.find(var) == d_assumptions.end()); + d_assumptions.insert(var); +} + +template <class Solver> +ClauseId TSatProof<Solver>::registerAssumptionConflict(const typename Solver::TLitVec& confl) { + Debug("proof:sat:detailed") << "registerAssumptionConflict " << std::endl; + // Uniqueness is checked in the bit-vector proof + // should be vars + for (int i = 0; i < confl.size(); ++i) { + Assert (d_assumptions.find(var(confl[i])) != d_assumptions.end()); + } + ClauseId new_id = ProofManager::currentPM()->nextId(); + d_assumptionConflicts.insert(new_id); + LitVector* vec_confl = new LitVector(confl.size()); + for (int i = 0; i < confl.size(); ++i) { + vec_confl->operator[](i) = confl[i]; + } + if (Debug.isOn("proof:sat:detailed")) { + printClause<Solver>(*vec_confl); + Debug("proof:sat:detailed") << "\n"; + } + + d_assumptionConflictsDebug[new_id] = vec_confl; + return new_id; +} + + +template <class Solver> +void TSatProof<Solver>::removedDfs(typename Solver::TLit lit, LitSet* removedSet, LitVector& removeStack, LitSet& inClause, LitSet& seen) { + // if we already added the literal return + if (seen.count(lit)) { + return; + } + + typename Solver::TCRef reason_ref = d_solver->reason(var(lit)); + if (reason_ref == Solver::TCRef_Undef) { + seen.insert(lit); + removeStack.push_back(lit); + return; + } + + int size = getClause(reason_ref).size(); + for (int i = 1; i < size; i++ ) { + typename Solver::TLit v = getClause(reason_ref)[i]; + if(inClause.count(v) == 0 && seen.count(v) == 0) { + removedDfs(v, removedSet, removeStack, inClause, seen); + } + } + if(seen.count(lit) == 0) { + seen.insert(lit); + removeStack.push_back(lit); + } +} + +template <class Solver> +void TSatProof<Solver>::removeRedundantFromRes(ResChain<Solver>* res, ClauseId id) { + LitSet* removed = res->getRedundant(); + if (removed == NULL) { + return; + } + + LitSet inClause; + createLitSet(id, inClause); + + LitVector removeStack; + LitSet seen; + for (typename LitSet::iterator it = removed->begin(); it != removed->end(); ++it) { + removedDfs(*it, removed, removeStack, inClause, seen); + } + + for (int i = removeStack.size()-1; i >= 0; --i) { + typename Solver::TLit lit = removeStack[i]; + typename Solver::TCRef reason_ref = d_solver->reason(var(lit)); + ClauseId reason_id; + + if (reason_ref == Solver::TCRef_Undef) { + Assert(isUnit(~lit)); + reason_id = getUnitId(~lit); + } else { + reason_id = registerClause(reason_ref, LEARNT); + } + res->addStep(lit, reason_id, !sign(lit)); + } + removed->clear(); +} + +template <class Solver> +void TSatProof<Solver>::registerResolution(ClauseId id, ResChain<Solver>* res) { + Assert(res != NULL); + + removeRedundantFromRes(res, id); + Assert(res->redundantRemoved()); + + d_resChains[id] = res; + if(Debug.isOn("proof:sat")) { + printRes(id); + } + if(d_checkRes) { + Assert(checkResolution(id)); + } + + PSTATS( + d_statistics.d_resChainLengths << ((uint64_t)res->getSteps().size()); + d_statistics.d_avgChainLength.addEntry((uint64_t)res->getSteps().size()); + ++(d_statistics.d_numLearnedClauses); + ) +} + + +/// recording resolutions +template <class Solver> +void TSatProof<Solver>::startResChain(typename Solver::TCRef start) { + ClauseId id = getClauseId(start); + ResChain<Solver>* res = new ResChain<Solver>(id); + d_resStack.push_back(res); +} + +template <class Solver> +void TSatProof<Solver>::startResChain(typename Solver::TLit start) { + ClauseId id = getUnitId(start); + ResChain<Solver>* res = new ResChain<Solver>(id); + d_resStack.push_back(res); +} + + +template <class Solver> +void TSatProof<Solver>::addResolutionStep(typename Solver::TLit lit, + typename Solver::TCRef clause, bool sign) { + ClauseId id = registerClause(clause, LEARNT); + ResChain<Solver>* res = d_resStack.back(); + res->addStep(lit, id, sign); +} + +template <class Solver> +void TSatProof<Solver>::endResChain(ClauseId id) { + Debug("proof:sat:detailed") <<"endResChain " << id << "\n"; + Assert(d_resStack.size() > 0); + ResChain<Solver>* res = d_resStack.back(); + registerResolution(id, res); + d_resStack.pop_back(); +} + + +// template <class Solver> +// void TSatProof<Solver>::endResChain(typename Solver::TCRef clause) { +// Assert(d_resStack.size() > 0); +// ClauseId id = registerClause(clause, LEARNT); +// ResChain<Solver>* res = d_resStack.back(); +// registerResolution(id, res); +// d_resStack.pop_back(); +// } + +template <class Solver> +void TSatProof<Solver>::endResChain(typename Solver::TLit lit) { + Assert(d_resStack.size() > 0); + ClauseId id = registerUnitClause(lit, LEARNT); + Debug("proof:sat:detailed") <<"endResChain unit " << id << "\n"; + ResChain<Solver>* res = d_resStack.back(); + d_glueMap[id] = 1; + registerResolution(id, res); + d_resStack.pop_back(); +} + + +template <class Solver> +void TSatProof<Solver>::cancelResChain() { + Assert(d_resStack.size() > 0); + d_resStack.pop_back(); +} + + +template <class Solver> +void TSatProof<Solver>::storeLitRedundant(typename Solver::TLit lit) { + Assert(d_resStack.size() > 0); + ResChain<Solver>* res = d_resStack.back(); + res->addRedundantLit(lit); +} + +/// constructing resolutions +template <class Solver> +void TSatProof<Solver>::resolveOutUnit(typename Solver::TLit lit) { + ClauseId id = resolveUnit(~lit); + ResChain<Solver>* res = d_resStack.back(); + res->addStep(lit, id, !sign(lit)); +} +template <class Solver> +void TSatProof<Solver>::storeUnitResolution(typename Solver::TLit lit) { + Debug("cores") << "STORE UNIT RESOLUTION" << std::endl; + resolveUnit(lit); +} +template <class Solver> +ClauseId TSatProof<Solver>::resolveUnit(typename Solver::TLit lit) { + // first check if we already have a resolution for lit + if(isUnit(lit)) { + ClauseId id = getClauseId(lit); + Assert(hasResolution(id) || isInputClause(id) || isLemmaClause(id)); + return id; + } + typename Solver::TCRef reason_ref = d_solver->reason(var(lit)); + Assert(reason_ref != Solver::TCRef_Undef); + + ClauseId reason_id = registerClause(reason_ref, LEARNT); + + ResChain<Solver>* res = new ResChain<Solver>(reason_id); + // Here, the call to resolveUnit() can reallocate memory in the + // clause allocator. So reload reason ptr each time. + typename Solver::TClause* reason = &getClause(reason_ref); + for (int i = 0; + i < reason->size(); + i++, reason = &getClause(reason_ref)) { + typename Solver::TLit l = (*reason)[i]; + if(lit != l) { + ClauseId res_id = resolveUnit(~l); + res->addStep(l, res_id, !sign(l)); + } + } + ClauseId unit_id = registerUnitClause(lit, LEARNT); + registerResolution(unit_id, res); + return unit_id; +} +template <class Solver> +void TSatProof<Solver>::toStream(std::ostream& out) { + Debug("proof:sat") << "TSatProof<Solver>::printProof\n"; + Unimplemented("native proof printing not supported yet"); +} +template <class Solver> +ClauseId TSatProof<Solver>::storeUnitConflict(typename Solver::TLit conflict_lit, + ClauseKind kind) { + Debug("cores") << "STORE UNIT CONFLICT" << std::endl; + Assert(!d_storedUnitConflict); + d_unitConflictId = registerUnitClause(conflict_lit, kind); + d_storedUnitConflict = true; + Debug("proof:sat:detailed") <<"storeUnitConflict " << d_unitConflictId << "\n"; + return d_unitConflictId; +} +template <class Solver> +void TSatProof<Solver>::finalizeProof(typename Solver::TCRef conflict_ref) { + Assert(d_resStack.size() == 0); + Assert(conflict_ref != Solver::TCRef_Undef); + ClauseId conflict_id; + if (conflict_ref == Solver::TCRef_Lazy) { + Assert(d_storedUnitConflict); + conflict_id = d_unitConflictId; + + ResChain<Solver>* res = new ResChain<Solver>(conflict_id); + typename Solver::TLit lit = d_idUnit[conflict_id]; + ClauseId res_id = resolveUnit(~lit); + res->addStep(lit, res_id, !sign(lit)); + + registerResolution(d_emptyClauseId, res); + + return; + } else { + Assert(!d_storedUnitConflict); + conflict_id = registerClause(conflict_ref, LEARNT); //FIXME + } + + if(Debug.isOn("proof:sat")) { + Debug("proof:sat") << "proof::finalizeProof Final Conflict "; + print(conflict_id); + } + + ResChain<Solver>* res = new ResChain<Solver>(conflict_id); + // Here, the call to resolveUnit() can reallocate memory in the + // clause allocator. So reload conflict ptr each time. + typename Solver::TClause* conflict = &getClause(conflict_ref); + for (int i = 0; + i < conflict->size(); + ++i, conflict = &getClause(conflict_ref)) { + typename Solver::TLit lit = (*conflict)[i]; + ClauseId res_id = resolveUnit(~lit); + res->addStep(lit, res_id, !sign(lit)); + } + registerResolution(d_emptyClauseId, res); +} + +/// CRef manager +template <class Solver> +void TSatProof<Solver>::updateCRef(typename Solver::TCRef oldref, + typename Solver::TCRef newref) { + if (d_clauseId.find(oldref) == d_clauseId.end()) { + return; + } + ClauseId id = getClauseId(oldref); + Assert(d_temp_clauseId.find(newref) == d_temp_clauseId.end()); + Assert(d_temp_idClause.find(id) == d_temp_idClause.end()); + d_temp_clauseId[newref] = id; + d_temp_idClause[id] = newref; +} +template <class Solver> +void TSatProof<Solver>::finishUpdateCRef() { + d_clauseId.swap(d_temp_clauseId); + d_temp_clauseId.clear(); + + d_idClause.swap(d_temp_idClause); + d_temp_idClause.clear(); +} +template <class Solver> +void TSatProof<Solver>::markDeleted(typename Solver::TCRef clause) { + if (d_clauseId.find(clause) != d_clauseId.end()) { + ClauseId id = getClauseId(clause); + Assert(d_deleted.find(id) == d_deleted.end()); + d_deleted.insert(id); + if (isLemmaClause(id)) { + const typename Solver::TClause& minisat_cl = getClause(clause); + prop::SatClause* sat_cl = new prop::SatClause(); + toSatClause<Solver>(minisat_cl, *sat_cl); + d_deletedTheoryLemmas.insert(std::make_pair(id, sat_cl)); + } + } +} + +// template<> +// void toSatClause< ::BVMinisat::Solver> (const BVMinisat::Solver::TClause& minisat_cl, +// prop::SatClause& sat_cl) { + +// prop::BVMinisatSatSolver::toSatClause(minisat_cl, sat_cl); +// } + + + +template <class Solver> +void TSatProof<Solver>::constructProof(ClauseId conflict) { + collectClauses(conflict); +} + +template <class Solver> +std::string TSatProof<Solver>::clauseName(ClauseId id) { + std::ostringstream os; + if (isInputClause(id)) { + os << ProofManager::getInputClauseName(id, d_name); + return os.str(); + } else + if (isLemmaClause(id)) { + os << ProofManager::getLemmaClauseName(id, d_name); + return os.str(); + }else { + os << ProofManager::getLearntClauseName(id, d_name); + return os.str(); + } +} + +template <class Solver> +prop::SatClause* TSatProof<Solver>::buildClause(ClauseId id) { + if (isUnit(id)) { + typename Solver::TLit lit = getUnit(id); + prop::SatLiteral sat_lit = toSatLiteral<Solver>(lit); + prop::SatClause* clause = new prop::SatClause(); + clause->push_back(sat_lit); + return clause; + } + + if (isDeleted(id)) { + prop::SatClause* clause = d_deletedTheoryLemmas.find(id)->second; + return clause; + } + + typename Solver::TCRef ref = getClauseRef(id); + const typename Solver::TClause& minisat_cl = getClause(ref); + prop::SatClause* clause = new prop::SatClause(); + toSatClause<Solver>(minisat_cl, *clause); + return clause; +} + +template <class Solver> +void TSatProof<Solver>::collectClauses(ClauseId id) { + if (d_seenInputs.find(id) != d_seenInputs.end() || + d_seenLemmas.find(id) != d_seenLemmas.end() || + d_seenLearnt.find(id) != d_seenLearnt.end()) { + return; + } + + if (isInputClause(id)) { + d_seenInputs.insert(std::make_pair(id, buildClause(id))); + return; + } else if (isLemmaClause(id)) { + d_seenLemmas.insert(std::make_pair(id, buildClause(id))); + return; + } else if (!isAssumptionConflict(id)) { + d_seenLearnt.insert(id); + } + + Assert(d_resChains.find(id) != d_resChains.end()); + ResChain<Solver>* res = d_resChains[id]; + PSTATS( + d_statistics.d_usedResChainLengths << ((uint64_t)res->getSteps().size()); + d_statistics.d_usedClauseGlue << ((uint64_t) d_glueMap[id]); + ); + ClauseId start = res->getStart(); + collectClauses(start); + + typename ResChain<Solver>::ResSteps steps = res->getSteps(); + for(size_t i = 0; i < steps.size(); i++) { + collectClauses(steps[i].id); + } +} + +template <class Solver> +void TSatProof<Solver>::collectClausesUsed(IdToSatClause& inputs, + IdToSatClause& lemmas) { + inputs = d_seenInputs; + lemmas = d_seenLemmas; + PSTATS ( + d_statistics.d_numLearnedInProof.setData(d_seenLearnt.size()); + d_statistics.d_numLemmasInProof.setData(d_seenLemmas.size()); + ); +} + +template <class Solver> +void TSatProof<Solver>::storeClauseGlue(ClauseId clause, int glue) { + Assert (d_glueMap.find(clause) == d_glueMap.end()); + d_glueMap.insert(std::make_pair(clause, glue)); +} + +template <class Solver> +TSatProof<Solver>::Statistics::Statistics(const std::string& prefix) + : d_numLearnedClauses("satproof::"+prefix+"::NumLearnedClauses", 0) + , d_numLearnedInProof("satproof::"+prefix+"::NumLearnedInProof", 0) + , d_numLemmasInProof("satproof::"+prefix+"::NumLemmasInProof", 0) + , d_avgChainLength("satproof::"+prefix+"::AvgResChainLength") + , d_resChainLengths("satproof::"+prefix+"::ResChainLengthsHist") + , d_usedResChainLengths("satproof::"+prefix+"::UsedResChainLengthsHist") + , d_clauseGlue("satproof::"+prefix+"::ClauseGlueHist") + , d_usedClauseGlue("satproof::"+prefix+"::UsedClauseGlueHist") { + smtStatisticsRegistry()->registerStat(&d_numLearnedClauses); + smtStatisticsRegistry()->registerStat(&d_numLearnedInProof); + smtStatisticsRegistry()->registerStat(&d_numLemmasInProof); + smtStatisticsRegistry()->registerStat(&d_avgChainLength); + smtStatisticsRegistry()->registerStat(&d_resChainLengths); + smtStatisticsRegistry()->registerStat(&d_usedResChainLengths); + smtStatisticsRegistry()->registerStat(&d_clauseGlue); + smtStatisticsRegistry()->registerStat(&d_usedClauseGlue); +} + +template <class Solver> +TSatProof<Solver>::Statistics::~Statistics() { + smtStatisticsRegistry()->unregisterStat(&d_numLearnedClauses); + smtStatisticsRegistry()->unregisterStat(&d_numLearnedInProof); + smtStatisticsRegistry()->unregisterStat(&d_numLemmasInProof); + smtStatisticsRegistry()->unregisterStat(&d_avgChainLength); + smtStatisticsRegistry()->unregisterStat(&d_resChainLengths); + smtStatisticsRegistry()->unregisterStat(&d_usedResChainLengths); + smtStatisticsRegistry()->unregisterStat(&d_clauseGlue); + smtStatisticsRegistry()->unregisterStat(&d_usedClauseGlue); +} + + +/// LFSCSatProof class +template <class Solver> +void LFSCSatProof<Solver>::printResolution(ClauseId id, std::ostream& out, std::ostream& paren) { + out << "(satlem_simplify _ _ _ "; + + ResChain<Solver>* res = this->d_resChains[id]; + typename ResChain<Solver>::ResSteps& steps = res->getSteps(); + + for (int i = steps.size()-1; i >= 0; i--) { + out << "("; + out << (steps[i].sign? "R" : "Q") << " _ _ "; + } + + ClauseId start_id = res->getStart(); + out << this->clauseName(start_id) << " "; + + for(unsigned i = 0; i < steps.size(); i++) { + prop::SatVariable v = prop::MinisatSatSolver::toSatVariable(var(steps[i].lit)); + out << this->clauseName(steps[i].id) << " "<<ProofManager::getVarName(v, this->d_name) <<")"; + } + + if (id == this->d_emptyClauseId) { + out <<"(\\empty empty)"; + return; + } + + out << "(\\" << this->clauseName(id) << "\n"; // bind to lemma name + paren << "))"; // closing parethesis for lemma binding and satlem +} + +/// LFSCSatProof class +template <class Solver> +void LFSCSatProof<Solver>::printAssumptionsResolution(ClauseId id, std::ostream& out, std::ostream& paren) { + Assert (this->isAssumptionConflict(id)); + // print the resolution proving the assumption conflict + printResolution(id, out, paren); + // resolve out assumptions to prove empty clause + out << "(satlem_simplify _ _ _ "; + std::vector<typename Solver::TLit>& confl = *(this->d_assumptionConflictsDebug[id]); + + Assert (confl.size()); + + for (unsigned i = 0; i < confl.size(); ++i) { + prop::SatLiteral lit = toSatLiteral<Solver>(confl[i]); + out <<"("; + out << (lit.isNegated() ? "Q" : "R") <<" _ _ "; + } + + out << this->clauseName(id)<< " "; + for (int i = confl.size() - 1; i >= 0; --i) { + prop::SatLiteral lit = toSatLiteral<Solver>(confl[i]); + prop::SatVariable v = lit.getSatVariable(); + out << "unit"<< v <<" "; + out << ProofManager::getVarName(v, this->d_name) <<")"; + } + out <<"(\\ e e)\n"; + paren <<")"; +} + + +template <class Solver> +void LFSCSatProof<Solver>::printResolutions(std::ostream& out, std::ostream& paren) { + Debug("bv-proof") << "; print resolutions" << std::endl; + std::set<ClauseId>::iterator it = this->d_seenLearnt.begin(); + for(; it!= this->d_seenLearnt.end(); ++it) { + if(*it != this->d_emptyClauseId) { + Debug("bv-proof") << "; print resolution for " << *it << std::endl; + printResolution(*it, out, paren); + } + } + Debug("bv-proof") << "; done print resolutions" << std::endl; +} + +template <class Solver> +void LFSCSatProof<Solver>::printResolutionEmptyClause(std::ostream& out, std::ostream& paren) { + printResolution(this->d_emptyClauseId, out, paren); +} + + +inline std::ostream& operator<<(std::ostream& out, CVC4::ClauseKind k) { + switch(k) { + case CVC4::INPUT: + out << "INPUT"; + break; + case CVC4::THEORY_LEMMA: + out << "THEORY_LEMMA"; + break; + case CVC4::LEARNT: + out << "LEARNT"; + break; + default: + out << "ClauseKind Unknown! [" << unsigned(k) << "]"; + } + + return out; +} + +}/* CVC4 namespace */ + +#endif /* __CVC4__SAT__PROOF_IMPLEMENTATION_H */ |