diff options
Diffstat (limited to 'src/proof/cnf_proof.cpp')
-rw-r--r-- | src/proof/cnf_proof.cpp | 103 |
1 files changed, 101 insertions, 2 deletions
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index 5f03ef5cf..caafa6b83 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -16,11 +16,110 @@ **/ #include "proof/cnf_proof.h" +#include "proof/theory_proof.h" +#include "proof/proof_manager.h" +#include "prop/sat_solver_types.h" +#include "prop/minisat/minisat.h" +#include "prop/cnf_stream.h" + using namespace CVC4::prop; namespace CVC4 { -CnfProof::CnfProof(CnfStream* stream) : - d_cnfStream(stream) {} +CnfProof::CnfProof(CnfStream* stream) + : d_cnfStream(stream) + , d_theoryProof(NULL) +{} + +TheoryProof* CnfProof::getTheoryProof() { + Assert (d_theoryProof); + return d_theoryProof; +} + +void CnfProof::setTheoryProof(TheoryProof* theory_proof) { + Assert (d_theoryProof == NULL); + d_theoryProof = theory_proof; +} + +void CnfProof::addInputClause(ClauseId id, const ::Minisat::Clause& clause) { + d_inputClauses.insert(std::make_pair(id, clause)); +} + +void CnfProof::addTheoryLemma(ClauseId id, const ::Minisat::Clause& clause) { + d_theoryLemmas.insert(std::make_pair(id, clause)); +} + +void CnfProof::addVariable(unsigned var) { + d_propVars.insert(var); + Expr atom = getAtom(var); + getTheoryProof()->addAtom(atom); +} + +Expr CnfProof::getAtom(unsigned var) { + Minisat::Lit m_lit = Minisat::mkLit(var); + prop::SatLiteral sat_lit = prop::MinisatSatSolver::toSatLiteral(m_lit); + Expr atom = d_cnfStream->getNode(sat_lit).toExpr(); + return atom; +} + +void LFSCCnfProof::printAtomMapping(std::ostream& os, std::ostream& paren) { + for (VarSet::iterator it = d_propVars.begin();it != d_propVars.end(); ++it) { + Expr atom = getAtom(*it); + os << "(decl_atom "; + getTheoryProof()->printFormula(atom, os); + os << " (\\ " << ProofManager::getVarPrefix() <<*it << " (\\ " << ProofManager::getAtomPrefix() <<*it << "\n"; + paren << ")))"; + } +} + +void LFSCCnfProof::printClauses(std::ostream& os, std::ostream& paren) { + printInputClauses(os, paren); + printTheoryLemmas(os, paren); +} + +void LFSCCnfProof::printInputClauses(std::ostream& os, std::ostream& paren) { + for (IdToClause::const_iterator it = d_inputClauses.begin(); it != d_inputClauses.end(); ++it) { + ClauseId id = it->first; + const Minisat::Clause& clause = it->second; + os << " ;; input clause \n"; + os << "(satlem _ _ "; + std::ostringstream clause_paren; + printClause(clause, os, clause_paren); + os << " (clausify_false trust)" << clause_paren.str(); + os << "( \\ " << ProofManager::getInputClausePrefix() << id <<"\n"; + paren << "))"; + } +} + + +void LFSCCnfProof::printTheoryLemmas(std::ostream& os, std::ostream& paren) { + for (IdToClause::const_iterator it = d_inputClauses.begin(); it != d_inputClauses.end(); ++it) { + ClauseId id = it->first; + const Minisat::Clause& clause = it->second; + os << " ;; theory lemma \n"; + os << "(satlem _ _ "; + std::ostringstream clause_paren; + printClause(clause, os, clause_paren); + os << " (clausify_false trust)" << clause_paren.str(); + os << "( \\ " << ProofManager::getLemmaClausePrefix() << id <<"\n"; + paren << "))"; + } +} + +void LFSCCnfProof::printClause(const Minisat::Clause& clause, std::ostream& os, std::ostream& paren) { + for (int i = 0; i < clause.size(); ++i) { + Minisat::Lit lit = clause[i]; + unsigned var = Minisat::var(lit); + if (sign(lit)) { + os << "(asf _ _ _ " << ProofManager::getAtomPrefix()<< var <<" (\\ " << ProofManager::getLitPrefix() << Minisat::toInt(lit) << " "; + paren << ")"; + } else { + os << "(ast _ _ _ " << ProofManager::getAtomPrefix()<< var <<" (\\ " << ProofManager::getLitPrefix() << Minisat::toInt(lit) << " "; + paren << ")"; + } + } +} + } /* CVC4 namespace */ + |