From: lianah Date: Wed, 9 Oct 2013 19:48:42 +0000 (-0400) Subject: cleaned up proof code X-Git-Tag: cvc5-1.0.0~7280 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=44485520fae92b34e4385d4d2c4774c9dd7d0dc0;p=cvc5.git cleaned up proof code --- diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index d73202147..cb22ca819 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -28,37 +28,8 @@ namespace CVC4 { 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::addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind) { - for (unsigned i = 0; i < clause->size(); ++i) { - SatLiteral lit = clause->operator[](i); - addVariable(lit.getSatVariable()); - } - if (kind == INPUT) { - d_inputClauses.insert(std::make_pair(id, clause)); - return; - } - Assert (kind == THEORY_LEMMA); - d_theoryLemmas.insert(std::make_pair(id, clause)); -} - -void CnfProof::addVariable(prop::SatVariable var) { - d_propVars.insert(var); - Expr atom = getAtom(var); - getTheoryProof()->addAtom(atom); -} Expr CnfProof::getAtom(prop::SatVariable var) { prop::SatLiteral lit (var); @@ -67,20 +38,17 @@ Expr CnfProof::getAtom(prop::SatVariable var) { } CnfProof::~CnfProof() { - for (IdToClause::iterator it = d_inputClauses.begin(); it != d_inputClauses.end(); ++it) { - delete it->second; - } - for (IdToClause::iterator it = d_theoryLemmas.begin(); it != d_theoryLemmas.end(); ++it) { - delete it->second; - } } void LFSCCnfProof::printAtomMapping(std::ostream& os, std::ostream& paren) { - for (VarSet::iterator it = d_propVars.begin();it != d_propVars.end(); ++it) { + ProofManager::var_iterator it = ProofManager::currentPM()->begin_vars(); + ProofManager::var_iterator end = ProofManager::currentPM()->end_vars(); + + for (;it != end; ++it) { Expr atom = getAtom(*it); os << "(decl_atom "; - getTheoryProof()->printFormula(atom, os); - os << " (\\ " << ProofManager::printVarName(*it) << " (\\ " << ProofManager::printAtomName(*it) << "\n"; + LFSCTheoryProof::printFormula(atom, os); + os << " (\\ " << ProofManager::getVarName(*it) << " (\\ " << ProofManager::getAtomName(*it) << "\n"; paren << ")))"; } } @@ -91,15 +59,18 @@ void LFSCCnfProof::printClauses(std::ostream& os, std::ostream& paren) { } void LFSCCnfProof::printInputClauses(std::ostream& os, std::ostream& paren) { - os << " ;; Input Clauses \n"; - for (IdToClause::const_iterator it = d_inputClauses.begin(); it != d_inputClauses.end(); ++it) { + os << " ;; Input Clauses \n"; + ProofManager::clause_iterator it = ProofManager::currentPM()->begin_input_clauses(); + ProofManager::clause_iterator end = ProofManager::currentPM()->end_input_clauses(); + + for (; it != end; ++it) { ClauseId id = it->first; const prop::SatClause* clause = it->second; os << "(satlem _ _ "; std::ostringstream clause_paren; printClause(*clause, os, clause_paren); os << " (clausify_false trust)" << clause_paren.str(); - os << "( \\ " << ProofManager::printInputClauseName(id) << "\n"; + os << "( \\ " << ProofManager::getInputClauseName(id) << "\n"; paren << "))"; } } @@ -107,14 +78,17 @@ void LFSCCnfProof::printInputClauses(std::ostream& os, std::ostream& paren) { void LFSCCnfProof::printTheoryLemmas(std::ostream& os, std::ostream& paren) { os << " ;; Theory Lemmas \n"; - for (IdToClause::const_iterator it = d_theoryLemmas.begin(); it != d_theoryLemmas.end(); ++it) { + ProofManager::clause_iterator it = ProofManager::currentPM()->begin_lemmas(); + ProofManager::clause_iterator end = ProofManager::currentPM()->end_lemmas(); + + for (; it != end; ++it) { ClauseId id = it->first; const prop::SatClause* clause = it->second; os << "(satlem _ _ "; std::ostringstream clause_paren; printClause(*clause, os, clause_paren); os << " (clausify_false trust)" << clause_paren.str(); - os << "( \\ " << ProofManager::printLemmaClauseName(id) <<"\n"; + os << "( \\ " << ProofManager::getLemmaClauseName(id) <<"\n"; paren << "))"; } } @@ -124,10 +98,10 @@ void LFSCCnfProof::printClause(const prop::SatClause& clause, std::ostream& os, prop::SatLiteral lit = clause[i]; prop::SatVariable var = lit.getSatVariable(); if (lit.isNegated()) { - os << "(ast _ _ _ " << ProofManager::printAtomName(var) <<" (\\ " << ProofManager::printLitName(lit) << " "; + os << "(ast _ _ _ " << ProofManager::getAtomName(var) <<" (\\ " << ProofManager::getLitName(lit) << " "; paren << "))"; } else { - os << "(asf _ _ _ " << ProofManager::printAtomName(var) <<" (\\ " << ProofManager::printLitName(lit) << " "; + os << "(asf _ _ _ " << ProofManager::getAtomName(var) <<" (\\ " << ProofManager::getLitName(lit) << " "; paren << "))"; } } diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index 010b1429d..a550f274a 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -32,26 +32,13 @@ namespace prop { class CnfStream; } -typedef __gnu_cxx::hash_map < ClauseId, const prop::SatClause* > IdToClause; -typedef __gnu_cxx::hash_set VarSet; - -class TheoryProof; - class CnfProof { protected: CVC4::prop::CnfStream* d_cnfStream; - IdToClause d_inputClauses; - IdToClause d_theoryLemmas; - VarSet d_propVars; - TheoryProof* d_theoryProof; - TheoryProof* getTheoryProof(); - Expr getAtom(prop::SatVariable var); public: CnfProof(CVC4::prop::CnfStream* cnfStream); - void addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind); - void addVariable(prop::SatVariable var); - void setTheoryProof(TheoryProof* theory_proof); + virtual void printAtomMapping(std::ostream& os, std::ostream& paren) = 0; virtual void printClauses(std::ostream& os, std::ostream& paren) = 0; virtual ~CnfProof(); diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 0c3c597da..23ba0e4e7 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -47,7 +47,15 @@ ProofManager::~ProofManager() { delete d_satProof; delete d_cnfProof; delete d_theoryProof; - delete d_fullProof; + delete d_fullProof; + for (IdToClause::iterator it = d_inputClauses.begin(); it != d_inputClauses.end(); ++it) { + delete it->second; + } + for (IdToClause::iterator it = d_theoryLemmas.begin(); it != d_theoryLemmas.end(); ++it) { + delete it->second; + } + // FIXME: memory leak because there are deleted theory lemmas that were not used in the + // SatProof } ProofManager* ProofManager::currentPM() { @@ -106,12 +114,29 @@ void ProofManager::initTheoryProof() { } -std::string ProofManager::printInputClauseName(ClauseId id) {return append("pb", id); } -std::string ProofManager::printLemmaClauseName(ClauseId id) { return append("lem", id); } -std::string ProofManager::printLearntClauseName(ClauseId id) { return append("cl", id); } -std::string ProofManager::printVarName(prop::SatVariable var) { return append("v", var); } -std::string ProofManager::printAtomName(prop::SatVariable var) { return append("a", var); } -std::string ProofManager::printLitName(prop::SatLiteral lit) {return append("l", lit.toInt()); } +std::string ProofManager::getInputClauseName(ClauseId id) {return append("pb", id); } +std::string ProofManager::getLemmaClauseName(ClauseId id) { return append("lem", id); } +std::string ProofManager::getLearntClauseName(ClauseId id) { return append("cl", id); } +std::string ProofManager::getVarName(prop::SatVariable var) { return append("v", var); } +std::string ProofManager::getAtomName(prop::SatVariable var) { return append("a", var); } +std::string ProofManager::getLitName(prop::SatLiteral lit) {return append("l", lit.toInt()); } + +void ProofManager::addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind) { + for (unsigned i = 0; i < clause->size(); ++i) { + prop::SatLiteral lit = clause->operator[](i); + d_propVars.insert(lit.getSatVariable()); + } + if (kind == INPUT) { + d_inputClauses.insert(std::make_pair(id, clause)); + return; + } + Assert (kind == THEORY_LEMMA); + d_theoryLemmas.insert(std::make_pair(id, clause)); +} + +void ProofManager::addAssertion(Expr formula) { + d_inputFormulas.insert(formula); +} LFSCProof::LFSCProof(LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory) @@ -119,18 +144,12 @@ LFSCProof::LFSCProof(LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theo , d_cnfProof(cnf) , d_theoryProof(theory) { - // link the proofs - d_satProof->setCnfProof(d_cnfProof); - d_cnfProof->setTheoryProof(d_theoryProof); - // build the resolution proof out of the traces - // this sets up the other proofs with the necessary information d_satProof->constructProof(); } void LFSCProof::toStream(std::ostream& out) { std::ostringstream paren; out << "(check \n"; - d_theoryProof->printDeclarations(out, paren); d_theoryProof->printAssertions(out, paren); out << "(: (holds cln) \n"; d_cnfProof->printAtomMapping(out, paren); @@ -140,16 +159,5 @@ void LFSCProof::toStream(std::ostream& out) { out << paren.str(); } -// void ProofManager::declareAtom(Expr atom, SatLiteral lit) { -// ::Minisat::Lit mlit = toMinisatLit(lit); -// d_satProof->addLiteral(mlit); -// d_cnfProof->declareAtom(atom, mlit); -// } - -// void ProofManager::addInputClause(SatClause clause) { -// d_satProof->registerClause(clause, true); -// d_cnfProof->registerClause(clause, true); -// } - } /* CVC4 namespace */ diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index d4f1d6528..7642ba776 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -50,6 +50,7 @@ class LFSCTheoryProof; namespace prop { typedef uint64_t SatVariable; class SatLiteral; +typedef std::vector SatClause; } // different proof modes @@ -60,11 +61,29 @@ enum ProofFormat { std::string append(const std::string& str, uint64_t num); +typedef __gnu_cxx::hash_map < ClauseId, const prop::SatClause* > IdToClause; +typedef __gnu_cxx::hash_set VarSet; +typedef __gnu_cxx::hash_set ExprSet; + +typedef int ClauseId; + +enum ClauseKind { + INPUT, + THEORY_LEMMA, + LEARNT +}; + class ProofManager { - SatProof* d_satProof; - CnfProof* d_cnfProof; + SatProof* d_satProof; + CnfProof* d_cnfProof; TheoryProof* d_theoryProof; + // information that will need to be shared across proofs + IdToClause d_inputClauses; + IdToClause d_theoryLemmas; + ExprSet d_inputFormulas; + VarSet d_propVars; + Proof* d_fullProof; ProofFormat d_format; @@ -74,22 +93,44 @@ class ProofManager { ~ProofManager(); public: static ProofManager* currentPM(); - static void initSatProof(Minisat::Solver* solver); - static void initCnfProof(CVC4::prop::CnfStream* cnfStream); - static void initTheoryProof(); - static Proof* getProof(); - static SatProof* getSatProof(); - static CnfProof* getCnfProof(); + // initialization + static void initSatProof(Minisat::Solver* solver); + static void initCnfProof(CVC4::prop::CnfStream* cnfStream); + static void initTheoryProof(); + + static Proof* getProof(); + static SatProof* getSatProof(); + static CnfProof* getCnfProof(); static TheoryProof* getTheoryProof(); + // iterators over data shared by proofs + typedef IdToClause::const_iterator clause_iterator; + typedef ExprSet::const_iterator assertions_iterator; + typedef VarSet::const_iterator var_iterator; + + clause_iterator begin_input_clauses() const { return d_inputClauses.begin(); } + clause_iterator end_input_clauses() const { return d_inputClauses.end(); } + + clause_iterator begin_lemmas() const { return d_theoryLemmas.begin(); } + clause_iterator end_lemmas() const { return d_theoryLemmas.end(); } + + assertions_iterator begin_assertions() const { return d_inputFormulas.begin(); } + assertions_iterator end_assertions() const { return d_inputFormulas.end(); } + + var_iterator begin_vars() const { return d_propVars.begin(); } + var_iterator end_vars() const { return d_propVars.end(); } + + void addAssertion(Expr formula); + void addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind); + // variable prefixes - static std::string printInputClauseName(ClauseId id); - static std::string printLemmaClauseName(ClauseId id); - static std::string printLearntClauseName(ClauseId id); + static std::string getInputClauseName(ClauseId id); + static std::string getLemmaClauseName(ClauseId id); + static std::string getLearntClauseName(ClauseId id); - static std::string printVarName(prop::SatVariable var); - static std::string printAtomName(prop::SatVariable var); - static std::string printLitName(prop::SatLiteral lit); + static std::string getVarName(prop::SatVariable var); + static std::string getAtomName(prop::SatVariable var); + static std::string getLitName(prop::SatLiteral lit); };/* class ProofManager */ class LFSCProof : public Proof { diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp index e1534a635..2ac468b47 100644 --- a/src/proof/sat_proof.cpp +++ b/src/proof/sat_proof.cpp @@ -16,7 +16,6 @@ **/ #include "proof/sat_proof.h" -#include "proof/cnf_proof.h" #include "proof/proof_manager.h" #include "prop/minisat/core/Solver.h" #include "prop/minisat/minisat.h" @@ -182,22 +181,11 @@ SatProof::SatProof(Minisat::Solver* solver, bool checkRes) : d_storedUnitConflict(false), d_seenLearnt(), d_seenInput(), - d_seenLemmas(), - d_cnfProof(NULL) + d_seenLemmas() { d_proxy = new ProofProxy(this); } -CnfProof* SatProof::getCnfProof() { - Assert (d_cnfProof); - return d_cnfProof; -} - -void SatProof::setCnfProof(CnfProof* cnfProof) { - Assert (d_cnfProof == NULL); - d_cnfProof = cnfProof; -} - /** * Returns true if the resolution chain corresponding to id * does resolve to the clause associated to id @@ -638,32 +626,32 @@ void SatProof::constructProof() { std::string SatProof::clauseName(ClauseId id) { ostringstream os; if (isInputClause(id)) { - os << ProofManager::printInputClauseName(id); + os << ProofManager::getInputClauseName(id); return os.str(); } else if (isLemmaClause(id)) { - os << ProofManager::printLemmaClauseName(id); + os << ProofManager::getLemmaClauseName(id); return os.str(); }else { - os << ProofManager::printLearntClauseName(id); + os << ProofManager::getLearntClauseName(id); return os.str(); } } -void SatProof::addClauseToCnfProof(ClauseId id, ClauseKind kind) { +void SatProof::addToProofManager(ClauseId id, ClauseKind kind) { if (isUnit(id)) { Minisat::Lit lit = getUnit(id); prop::SatLiteral sat_lit = MinisatSatSolver::toSatLiteral(lit); prop::SatClause* clause = new SatClause(); clause->push_back(sat_lit); - getCnfProof()->addClause(id, clause, kind); + ProofManager::currentPM()->addClause(id, clause, kind); return; } if (isDeleted(id)) { Assert (kind == THEORY_LEMMA); SatClause* clause = d_deletedTheoryLemmas.find(id)->second; - getCnfProof()->addClause(id, clause, kind); + ProofManager::currentPM()->addClause(id, clause, kind); return; } @@ -671,7 +659,7 @@ void SatProof::addClauseToCnfProof(ClauseId id, ClauseKind kind) { const Clause& minisat_cl = getClause(ref); SatClause* clause = new SatClause(); MinisatSatSolver::toSatClause(minisat_cl, *clause); - getCnfProof()->addClause(id, clause, kind); + ProofManager::currentPM()->addClause(id, clause, kind); } void SatProof::collectClauses(ClauseId id) { @@ -686,12 +674,12 @@ void SatProof::collectClauses(ClauseId id) { } if (isInputClause(id)) { - addClauseToCnfProof(id, INPUT); + addToProofManager(id, INPUT); d_seenInput.insert(id); return; } else if (isLemmaClause(id)) { - addClauseToCnfProof(id, THEORY_LEMMA); + addToProofManager(id, THEORY_LEMMA); d_seenLemmas.insert(id); return; } @@ -732,7 +720,7 @@ void LFSCSatProof::printResolution(ClauseId id, std::ostream& out, std::ostream& out << clauseName(start_id) << " "; for(unsigned i = 0; i < steps.size(); i++) { - out << clauseName(steps[i].id) << " "< #include #include "expr/expr.h" - +#include "proof/proof_manager.h" namespace Minisat { class Solver; @@ -49,7 +49,6 @@ namespace CVC4 { void printDebug(::Minisat::Lit l); void printDebug(::Minisat::Clause& c); -typedef int ClauseId; struct ResStep { ::Minisat::Lit lit; ClauseId id; @@ -104,12 +103,6 @@ public: };/* class ProofProxy */ -enum ClauseKind { - INPUT, - THEORY_LEMMA, - LEARNT -}; - class CnfProof; class SatProof { @@ -254,11 +247,8 @@ protected: inline std::string clauseName(ClauseId id); void collectClauses(ClauseId id); - CnfProof* d_cnfProof; - CnfProof* getCnfProof(); - void addClauseToCnfProof(ClauseId id, ClauseKind kind); + void addToProofManager(ClauseId id, ClauseKind kind); public: - void setCnfProof(CnfProof* cnfProof); virtual void printResolutions(std::ostream& out, std::ostream& paren) = 0; };/* class SatProof */ diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 5b5a2ae15..4ce804a74 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -16,29 +16,15 @@ **/ #include "proof/theory_proof.h" - +#include "proof/proof_manager.h" using namespace CVC4; TheoryProof::TheoryProof() - : d_atomSet() - , d_inputFormulas() - , d_termDeclarations() + : d_termDeclarations() , d_sortDeclarations() , d_declarationCache() {} -void TheoryProof::addAtom(Expr atom) { - d_atomSet.insert(atom); - Assert (atom.getKind() == kind::EQUAL); - addDeclaration(atom[0]); - addDeclaration(atom[1]); -} - -void TheoryProof::assertFormula(Expr formula) { - d_inputFormulas.insert(formula); - addDeclaration(formula); -} - void TheoryProof::addDeclaration(Expr term) { if (d_declarationCache.count(term)) return; @@ -152,8 +138,18 @@ void LFSCTheoryProof::printFormula(Expr atom, std::ostream& os) { } void LFSCTheoryProof::printAssertions(std::ostream& os, std::ostream& paren) { - unsigned counter = 0; - for (ExprSet::const_iterator it = d_inputFormulas.begin(); it != d_inputFormulas.end(); ++it) { + unsigned counter = 0; + ProofManager::assertions_iterator it = ProofManager::currentPM()->begin_assertions(); + ProofManager::assertions_iterator end = ProofManager::currentPM()->end_assertions(); + + // collect declarations first + for(; it != end; ++it) { + addDeclaration(*it); + } + printDeclarations(os, paren); + + it = ProofManager::currentPM()->begin_assertions(); + for (; it != end; ++it) { os << "(% A" << counter++ << " (th_holds "; printFormula(*it, os); os << ")\n"; diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h index b09641fec..773428633 100644 --- a/src/proof/theory_proof.h +++ b/src/proof/theory_proof.h @@ -28,13 +28,11 @@ namespace CVC4 { - typedef __gnu_cxx::hash_set ExprSet; + typedef __gnu_cxx::hash_set SortSet; - + typedef __gnu_cxx::hash_set ExprSet; class TheoryProof { protected: - ExprSet d_atomSet; - ExprSet d_inputFormulas; ExprSet d_termDeclarations; SortSet d_sortDeclarations; ExprSet d_declarationCache; @@ -42,18 +40,14 @@ namespace CVC4 { void addDeclaration(Expr atom); public: TheoryProof(); - void addAtom(Expr atom); - void assertFormula(Expr formula); - virtual void printFormula(Expr atom, std::ostream& os) = 0; - virtual void printDeclarations(std::ostream& os, std::ostream& paren) = 0; virtual void printAssertions(std::ostream& os, std::ostream& paren) = 0; }; class LFSCTheoryProof: public TheoryProof { - void printTerm(Expr term, std::ostream& os); + static void printTerm(Expr term, std::ostream& os); + void printDeclarations(std::ostream& os, std::ostream& paren); public: - virtual void printFormula(Expr atom, std::ostream& os); - virtual void printDeclarations(std::ostream& os, std::ostream& paren); + static void printFormula(Expr atom, std::ostream& os); virtual void printAssertions(std::ostream& os, std::ostream& paren); }; } /* CVC4 namespace */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 160a16652..352db6789 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3107,7 +3107,7 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc Assert(ex.isNull() || ex.getExprManager() == d_exprManager); #ifdef CVC4_PROOF // if (options::proof()) { <-- SEGFAULT!! - ProofManager::currentPM()->getTheoryProof()->assertFormula(ex); + ProofManager::currentPM()->addAssertion(ex); //} #endif SmtScope smts(this); @@ -3255,7 +3255,7 @@ Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, Log Assert(ex.getExprManager() == d_exprManager); #ifdef CVC4_PROOF // if (options::proof()) { <-- SEGFAULT!!! - ProofManager::currentPM()->getTheoryProof()->assertFormula(ex); + ProofManager::currentPM()->addAssertion(ex); // } #endif SmtScope smts(this);