From 867e79e0823c689889224078dfaebec03aee9730 Mon Sep 17 00:00:00 2001 From: Liana Hadarean Date: Mon, 7 Oct 2013 22:49:45 -0400 Subject: [PATCH] first draft implementation of uf proofs with holes --- src/proof/Makefile.am | 2 + src/proof/cnf_proof.cpp | 103 +++++++++++- src/proof/cnf_proof.h | 42 ++++- src/proof/proof_manager.cpp | 95 ++++++++--- src/proof/proof_manager.h | 33 +++- src/proof/sat_proof.cpp | 270 +++++++++++++++++--------------- src/proof/sat_proof.h | 90 +++++------ src/proof/theory_proof.cpp | 97 ++++++++++++ src/proof/theory_proof.h | 55 +++++++ src/prop/cnf_stream.cpp | 1 - src/prop/minisat/core/Solver.cc | 12 +- 11 files changed, 590 insertions(+), 210 deletions(-) create mode 100644 src/proof/theory_proof.cpp create mode 100644 src/proof/theory_proof.h diff --git a/src/proof/Makefile.am b/src/proof/Makefile.am index 75588ceb8..e996ddb60 100644 --- a/src/proof/Makefile.am +++ b/src/proof/Makefile.am @@ -13,6 +13,8 @@ libproof_la_SOURCES = \ sat_proof.cpp \ cnf_proof.h \ cnf_proof.cpp \ + theory_proof.h \ + theory_proof.cpp \ proof_manager.h \ proof_manager.cpp 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 */ + diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index 984dc76c6..8acb7a50f 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -16,20 +16,58 @@ ** **/ -#include "cvc4_private.h" -#include "util/proof.h" #ifndef __CVC4__CNF_PROOF_H #define __CVC4__CNF_PROOF_H +#include "cvc4_private.h" +#include "util/proof.h" +#include "proof/sat_proof.h" + +#include +#include #include + namespace CVC4 { namespace prop { class CnfStream; } + +typedef __gnu_cxx::hash_map < ClauseId, ::Minisat::Clause > 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(unsigned var); public: CnfProof(CVC4::prop::CnfStream* cnfStream); + void addInputClause(ClauseId id, const ::Minisat::Clause& clause); + void addTheoryLemma(ClauseId id, const ::Minisat::Clause& clause); + void addVariable(unsigned 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; + +}; + +class LFSCCnfProof: public CnfProof { + void printInputClauses(std::ostream& os, std::ostream& paren); + void printTheoryLemmas(std::ostream& os, std::ostream& paren); + void printClause(const Minisat::Clause& clause, std::ostream& os, std::ostream& paren); +public: + LFSCCnfProof(CVC4::prop::CnfStream* cnfStream) + : CnfProof(cnfStream) + {} + virtual void printAtomMapping(std::ostream& os, std::ostream& paren); + virtual void printClauses(std::ostream& os, std::ostream& paren); }; } /* CVC4 namespace */ diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index e03e9058b..43750a504 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -19,6 +19,7 @@ #include "util/proof.h" #include "proof/sat_proof.h" #include "proof/cnf_proof.h" +#include "proof/theory_proof.h" #include "util/cvc4_assert.h" namespace CVC4 { @@ -29,8 +30,20 @@ ProofManager* ProofManager::proofManager = NULL; ProofManager::ProofManager(ProofFormat format): d_satProof(NULL), d_cnfProof(NULL), + d_theoryProof(NULL), + d_fullProof(NULL), d_format(format) -{} +{ + // FIXME this is until it actually has theory references + initTheoryProof(); +} + +ProofManager::~ProofManager() { + delete d_satProof; + delete d_cnfProof; + delete d_theoryProof; + delete d_fullProof; +} ProofManager* ProofManager::currentPM() { if (isInitialized) { @@ -43,8 +56,14 @@ ProofManager* ProofManager::currentPM() { } Proof* ProofManager::getProof() { - // for now, this is just the SAT proof - return getSatProof(); + if (currentPM()->d_fullProof != NULL) + return currentPM()->d_fullProof; + Assert (currentPM()->d_format == LFSC); + + currentPM()->d_fullProof = new LFSCProof((LFSCSatProof*)getSatProof(), + (LFSCCnfProof*)getCnfProof(), + (LFSCTheoryProof*)getTheoryProof()); + return currentPM()->d_fullProof; } SatProof* ProofManager::getSatProof() { @@ -57,37 +76,65 @@ CnfProof* ProofManager::getCnfProof() { return currentPM()->d_cnfProof; } +TheoryProof* ProofManager::getTheoryProof() { + Assert (currentPM()->d_theoryProof); + return currentPM()->d_theoryProof; +} + + void ProofManager::initSatProof(Minisat::Solver* solver) { Assert (currentPM()->d_satProof == NULL); - switch(currentPM()->d_format) { - case LFSC : - currentPM()->d_satProof = new LFSCSatProof(solver); - break; - case NATIVE : - currentPM()->d_satProof = new SatProof(solver); - break; - default: - Assert(false); - } - + Assert(currentPM()->d_format == LFSC); + currentPM()->d_satProof = new LFSCSatProof(solver); } void ProofManager::initCnfProof(prop::CnfStream* cnfStream) { Assert (currentPM()->d_cnfProof == NULL); + Assert (currentPM()->d_format == LFSC); + currentPM()->d_cnfProof = new LFSCCnfProof(cnfStream); +} - switch(currentPM()->d_format) { - case LFSC : - currentPM()->d_cnfProof = new CnfProof(cnfStream); // FIXME - break; - case NATIVE : - currentPM()->d_cnfProof = new CnfProof(cnfStream); - break; - default: - Assert(false); - } +void ProofManager::initTheoryProof() { + Assert (currentPM()->d_theoryProof == NULL); + Assert (currentPM()->d_format == LFSC); + currentPM()->d_theoryProof = new LFSCTheoryProof(); +} +LFSCProof::LFSCProof(LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory) + : d_satProof(sat) + , 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); + out << "(: (holds cln) \n"; + d_cnfProof->printAtomMapping(out, paren); + d_cnfProof->printClauses(out, paren); + d_satProof->printResolutions(out, paren); + paren <<"))"; + 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 efd39a118..4ae8a6dae 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -23,6 +23,7 @@ #include #include "proof/proof.h" +#include "util/proof.h" // forward declarations namespace Minisat { @@ -38,7 +39,12 @@ namespace prop { class Proof; class SatProof; class CnfProof; +class TheoryProof; +class LFSCSatProof; +class LFSCCnfProof; +class LFSCTheoryProof; + // different proof modes enum ProofFormat { LFSC, @@ -48,23 +54,44 @@ enum ProofFormat { class ProofManager { SatProof* d_satProof; CnfProof* d_cnfProof; + TheoryProof* d_theoryProof; + + Proof* d_fullProof; ProofFormat d_format; static ProofManager* proofManager; static bool isInitialized; ProofManager(ProofFormat format = LFSC); + ~ProofManager(); public: static ProofManager* currentPM(); - static void initSatProof(Minisat::Solver* solver); static void initCnfProof(CVC4::prop::CnfStream* cnfStream); - - static Proof* getProof(); + static void initTheoryProof(); + static Proof* getProof(); static SatProof* getSatProof(); static CnfProof* getCnfProof(); + static TheoryProof* getTheoryProof(); + // variable prefixes + static std::string getInputClausePrefix() { return "pb"; } + static std::string getLemmaClausePrefix() { return "lem"; } + static std::string getLearntClausePrefix() { return "cl"; } + static std::string getVarPrefix() { return "v"; } + static std::string getAtomPrefix() { return "a"; } + static std::string getLitPrefix() {return "l"; } };/* class ProofManager */ +class LFSCProof : public Proof { + LFSCSatProof* d_satProof; + LFSCCnfProof* d_cnfProof; + LFSCTheoryProof* d_theoryProof; +public: + LFSCProof(LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory); + virtual void toStream(std::ostream& out); + virtual ~LFSCProof() {} +}; + }/* CVC4 namespace */ #endif /* __CVC4__PROOF_MANAGER_H */ diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp index d9b57f87e..624aac237 100644 --- a/src/proof/sat_proof.cpp +++ b/src/proof/sat_proof.cpp @@ -16,6 +16,8 @@ **/ #include "proof/sat_proof.h" +#include "proof/cnf_proof.h" +#include "proof/proof_manager.h" #include "prop/minisat/core/Solver.h" using namespace std; @@ -166,7 +168,8 @@ SatProof::SatProof(Minisat::Solver* solver, bool checkRes) : d_clauseId(), d_idUnit(), d_deleted(), - d_inputClauses(), + d_inputClauses(), + d_lemmaClauses(), d_resChains(), d_resStack(), d_checkRes(checkRes), @@ -176,11 +179,23 @@ SatProof::SatProof(Minisat::Solver* solver, bool checkRes) : d_temp_idClause(), d_unitConflictId(), d_storedUnitConflict(false), - d_atomToVar() + d_seenLearnt(), + d_seenInput(), + d_seenLemmas(), + d_cnfProof(NULL) { 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 @@ -272,8 +287,8 @@ ClauseId SatProof::getClauseId(::Minisat::Lit lit) { return d_idClause[id]; } -Clause& SatProof::getClause(ClauseId id) { - return d_solver->ca[id]; +Clause& SatProof::getClause(CRef ref) { + return d_solver->ca[ref]; } ::Minisat::Lit SatProof::getUnit(ClauseId id) { Assert (d_idUnit.find(id) != d_idUnit.end()); @@ -301,6 +316,10 @@ bool SatProof::isInputClause(ClauseId id) { return (d_inputClauses.find(id) != d_inputClauses.end()); } +bool SatProof::isLemmaClause(ClauseId id) { + return (d_lemmaClauses.find(id) != d_lemmaClauses.end()); +} + void SatProof::print(ClauseId id) { if (d_deleted.find(id) != d_deleted.end()) { @@ -344,34 +363,43 @@ void SatProof::printRes(ResChain* res) { /// registration methods -ClauseId SatProof::registerClause(::Minisat::CRef clause, bool isInput) { +ClauseId SatProof::registerClause(::Minisat::CRef clause, ClauseKind kind) { Assert(clause != CRef_Undef); ClauseIdMap::iterator it = d_clauseId.find(clause); if (it == d_clauseId.end()) { ClauseId newId = d_idCounter++; d_clauseId[clause]= newId; d_idClause[newId] =clause; - if (isInput) { + 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); + } } - Debug("proof:sat:detailed") <<"registerClause " << d_clauseId[clause] << " " <addInputClause(id, cl); d_seenInput.insert(id); return; - } else { + } + else if (isLemmaClause(id)) { + CRef lemma_ref = getClauseRef(id); + const Clause& cl = getClause(lemma_ref); + getCnfProof()->addTheoryLemma(id, cl); d_seenLemmas.insert(id); + } + else { + d_seenLearnt.insert(id); } Assert (d_resChains.find(id) != d_resChains.end()); ResChain* res = d_resChains[id]; ClauseId start = res->getStart(); - collectLemmas(start); + collectClauses(start); ResSteps steps = res->getSteps(); for(unsigned i = 0; i < steps.size(); i++) { - collectLemmas(steps[i].id); + collectClauses(steps[i].id); } } +/// LFSCSatProof class - -void LFSCSatProof::printResolution(ClauseId id) { - d_lemmaSS << "(satlem _ _ _ "; +void LFSCSatProof::printResolution(ClauseId id, std::ostream& out, std::ostream& paren) { + out << "(satlem_simplify _ _ _ "; ResChain* res = d_resChains[id]; ResSteps& steps = res->getSteps(); for (int i = steps.size()-1; i >= 0; i--) { - d_lemmaSS << "("; - d_lemmaSS << (steps[i].sign? "R" : "Q") << " _ _ "; + out << "("; + out << (steps[i].sign? "R" : "Q") << " _ _ "; } ClauseId start_id = res->getStart(); - if(isInputClause(start_id)) { - d_seenInput.insert(start_id); - } - d_lemmaSS << clauseName(start_id) << " "; + // WHY DID WE NEED THIS? + // if(isInputClause(start_id)) { + // d_seenInput.insert(start_id); + // } + out << clauseName(start_id) << " "; for(unsigned i = 0; i < steps.size(); i++) { - d_lemmaSS << clauseName(steps[i].id) << " v" << var(steps[i].lit) <<")"; + out << clauseName(steps[i].id) << " "<first << " => v" << var(it->second) << "\n"; - } -} +// void LFSCSatProof::printVariables(std::ostream& out, std::ostream& paren) { +// for (VarSet::iterator it = d_seenVars.begin(); it != d_seenVars.end(); ++it) { +// out << "(% " << ProofManager::getVarPrefix() << *it <<" var \n"; +// paren << ")"; +// } +// } } /* CVC4 namespace */ diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index fb8966400..0ab86b554 100644 --- a/src/proof/sat_proof.h +++ b/src/proof/sat_proof.h @@ -89,10 +89,10 @@ typedef std::hash_map < ClauseId, ResChain*> IdResMap; typedef std::hash_set < ClauseId > IdHashSet; typedef std::vector < ResChain* > ResStack; -typedef std::hash_set < int > VarSet; +typedef std::hash_set < unsigned > VarSet; typedef std::set < ClauseId > IdSet; typedef std::vector < ::Minisat::Lit > LitVector; -typedef __gnu_cxx::hash_map AtomToVar; +typedef __gnu_cxx::hash_map IdToMinisatClause; class SatProof; @@ -104,7 +104,16 @@ public: void updateCRef(::Minisat::CRef oldref, ::Minisat::CRef newref); };/* class ProofProxy */ -class SatProof : public Proof { + +enum ClauseKind { + INPUT, + THEORY_LEMMA, + LEARNT +}; + +class CnfProof; + +class SatProof { protected: ::Minisat::Solver* d_solver; // clauses @@ -114,7 +123,7 @@ protected: UnitIdMap d_unitId; IdHashSet d_deleted; IdHashSet d_inputClauses; - + IdHashSet d_lemmaClauses; // resolutions IdResMap d_resChains; ResStack d_resStack; @@ -133,9 +142,6 @@ protected: // unit conflict ClauseId d_unitConflictId; bool d_storedUnitConflict; - - // atom mapping - AtomToVar d_atomToVar; public: SatProof(::Minisat::Solver* solver, bool checkRes = false); protected: @@ -143,7 +149,8 @@ protected: void printRes(ClauseId id); void printRes(ResChain* res); - bool isInputClause(ClauseId id); + bool isInputClause(ClauseId id); + bool isLemmaClause(ClauseId id); bool isUnit(ClauseId id); bool isUnit(::Minisat::Lit lit); bool hasResolution(ClauseId id); @@ -155,7 +162,7 @@ protected: ::Minisat::CRef getClauseRef(ClauseId id); ::Minisat::Lit getUnit(ClauseId id); ClauseId getUnitId(::Minisat::Lit lit); - ::Minisat::Clause& getClause(ClauseId id); + ::Minisat::Clause& getClause(::Minisat::CRef ref); virtual void toStream(std::ostream& out); bool checkResolution(ClauseId id); @@ -206,8 +213,8 @@ public: void finalizeProof(::Minisat::CRef conflict); /// clause registration methods - ClauseId registerClause(const ::Minisat::CRef clause, bool isInput = false); - ClauseId registerUnitClause(const ::Minisat::Lit lit, bool isInput = false); + ClauseId registerClause(const ::Minisat::CRef clause, ClauseKind kind = LEARNT); + ClauseId registerUnitClause(const ::Minisat::Lit lit, ClauseKind kind = LEARNT); void storeUnitConflict(::Minisat::Lit lit); @@ -231,49 +238,36 @@ public: void storeUnitResolution(::Minisat::Lit lit); ProofProxy* getProxy() {return d_proxy; } - /** - * At mapping between literal and theory-atom it represents - * - * @param literal - * @param atom - */ - void storeAtom(::Minisat::Lit literal, Expr atom); -};/* class SatProof */ - -class LFSCSatProof: public SatProof { -private: - VarSet d_seenVars; - std::ostringstream d_atomsSS; - std::ostringstream d_varSS; - std::ostringstream d_lemmaSS; - std::ostringstream d_clauseSS; - std::ostringstream d_paren; - IdSet d_seenLemmas; - IdHashSet d_seenInput; + /** + Constructs the SAT proof identifying the needed lemmas + */ + void constructProof(); + +protected: + IdSet d_seenLearnt; + IdHashSet d_seenInput; + IdHashSet d_seenLemmas; + inline std::string varName(::Minisat::Lit lit); inline std::string clauseName(ClauseId id); - void collectLemmas(ClauseId id); - void printResolution(ClauseId id); - void printInputClause(ClauseId id); + void collectClauses(ClauseId id); + CnfProof* d_cnfProof; + CnfProof* getCnfProof(); +public: + void setCnfProof(CnfProof* cnfProof); + virtual void printResolutions(std::ostream& out, std::ostream& paren) = 0; +};/* class SatProof */ - void printVariables(); - void printClauses(); - void flush(std::ostream& out); - void printAtoms(); +class LFSCSatProof: public SatProof { +private: + void printResolution(ClauseId id, std::ostream& out, std::ostream& paren); public: - LFSCSatProof(::Minisat::Solver* solver, bool checkRes = false): - SatProof(solver, checkRes), - d_seenVars(), - d_atomsSS(), - d_varSS(), - d_lemmaSS(), - d_paren(), - d_seenLemmas(), - d_seenInput() - {} - virtual void toStream(std::ostream& out); + LFSCSatProof(::Minisat::Solver* solver, bool checkRes = false) + : SatProof(solver, checkRes) + {} + virtual void printResolutions(std::ostream& out, std::ostream& paren); };/* class LFSCSatProof */ }/* CVC4 namespace */ diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp new file mode 100644 index 000000000..224c74e2c --- /dev/null +++ b/src/proof/theory_proof.cpp @@ -0,0 +1,97 @@ +/********************* */ +/*! \file theory_proof.cpp + ** \verbatim + ** Original author: Liana Hadarean + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "proof/theory_proof.h" + +using namespace CVC4; + +TheoryProof::TheoryProof() + : d_atomSet() +{} +void TheoryProof::addAtom(Expr atom) { + d_atomSet.insert(atom); + Assert (atom.getKind() == kind::EQUAL); + addDeclaration(atom[0]); + addDeclaration(atom[1]); +} + +void TheoryProof::addDeclaration(Expr term) { + Type type = term.getType(); + if (type.isSort()) + d_sortDeclarations.insert(type); + if (term.getKind() == kind::APPLY_UF) { + Expr function = term.getOperator(); + d_termDeclarations.insert(function); + } else { + Assert (term.isVariable()); + Assert (type.isSort()); + d_termDeclarations.insert(term); + } +} + +void LFSCTheoryProof::printTerm(Expr term, std::ostream& os) { + if (term.isVariable()) { + os << term; + return; + } + Assert (term.getKind() == kind::APPLY_UF); + Expr func = term.getOperator(); + // only support unary functions so far + Assert (func.getNumChildren() == 1); + os << "(apply _ _ " << func << " "; + printTerm(term[0], os); + os <<")"; +} + +void LFSCTheoryProof::printFormula(Expr atom, std::ostream& os) { + // should make this more general + Assert (atom.getKind() == kind::EQUAL); + os << "(= "; + printTerm(atom[0], os); + os << " "; + printTerm(atom[1], os); + os << ")"; +} + +void LFSCTheoryProof::printDeclarations(std::ostream& os, std::ostream& paren) { + // declaring the sorts + for (SortSet::const_iterator it = d_sortDeclarations.begin(); it != d_sortDeclarations.end(); ++it) { + os << "(% " << *it << "sort \n"; + paren << ")"; + } + + // declaring the terms + for (TermSet::const_iterator it = d_termDeclarations.begin(); it != d_termDeclarations.end(); ++it) { + Expr term = *it; + + os << "(% " << term << "(term "; + paren <<")"; + + Type type = term.getType(); + if (type.isFunction()) { + FunctionType ftype = (FunctionType)type; + Assert (ftype.getArity() == 2); + Type arg_type = ftype.getArgTypes()[0]; + Type result_type = ftype.getRangeType(); + os << "(arrow " << arg_type << " " << result_type << "))\n"; + } else { + Assert (term.isVariable()); + Assert (type.isSort()); + os << type << ")\n"; + } + } +} diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h new file mode 100644 index 000000000..ac8f9f7b8 --- /dev/null +++ b/src/proof/theory_proof.h @@ -0,0 +1,55 @@ +/********************* */ +/*! \file theory_proof.h + ** \verbatim + ** Original author: Liana Hadarean + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A manager for UfProofs. + ** + ** A manager for UfProofs. + ** + ** + **/ + + +#ifndef __CVC4__THEORY_PROOF_H +#define __CVC4__THEORY_PROOF_H + +#include "cvc4_private.h" +#include "util/proof.h" +#include "expr/expr.h" +#include +#include + +namespace CVC4 { + + typedef __gnu_cxx::hash_set AtomSet; + typedef __gnu_cxx::hash_set TermSet; + typedef __gnu_cxx::hash_set SortSet; + + class TheoryProof { + protected: + AtomSet d_atomSet; + TermSet d_termDeclarations; + SortSet d_sortDeclarations; + void addDeclaration(Expr atom); + public: + TheoryProof(); + void addAtom(Expr atom); + virtual void printFormula(Expr atom, std::ostream& os) = 0; + virtual void printDeclarations(std::ostream& os, std::ostream& paren) = 0; + }; + + class LFSCTheoryProof: public TheoryProof { + void printTerm(Expr term, std::ostream& os); + public: + virtual void printFormula(Expr atom, std::ostream& os); + virtual void printDeclarations(std::ostream& os, std::ostream& paren); + }; +} /* CVC4 namespace */ +#endif /* __CVC4__THEORY_PROOF_H */ diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 8ebb461e5..47d352949 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -238,7 +238,6 @@ SatLiteral CnfStream::convertAtom(TNode node) { // Make a new literal (variables are not considered theory literals) SatLiteral lit = newLiteral(node, theoryLiteral, preRegister, canEliminate); - PROOF (ProofManager::getSatProof()->storeAtom(MinisatSatSolver::toMinisatLit(lit), node.toExpr()); ); // Return the resulting literal return lit; } diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 36e196821..45127a182 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -135,8 +135,8 @@ Solver::Solver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context, // Assert the constants uncheckedEnqueue(mkLit(varTrue, false)); uncheckedEnqueue(mkLit(varFalse, true)); - PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varTrue, false), true); ) - PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varFalse, true), true); ) + PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varTrue, false), INPUT); ) + PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varFalse, true), INPUT); ) } @@ -263,7 +263,7 @@ CRef Solver::reason(Var x) { // Construct the reason CRef real_reason = ca.alloc(explLevel, explanation, true); - PROOF (ProofManager::getSatProof()->registerClause(real_reason, true); ); + PROOF (ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA); ); vardata[x] = VarData(real_reason, level(x), user_level(x), intro_level(x), trail_index(x)); clauses_removable.push(real_reason); attachClause(real_reason); @@ -339,7 +339,7 @@ bool Solver::addClause_(vec& ps, bool removable) clauses_persistent.push(cr); attachClause(cr); - PROOF( ProofManager::getSatProof()->registerClause(cr, true); ) + PROOF( ProofManager::getSatProof()->registerClause(cr, INPUT); ) } // Check if it propagates @@ -347,7 +347,7 @@ bool Solver::addClause_(vec& ps, bool removable) if(assigns[var(ps[0])] == l_Undef) { assert(assigns[var(ps[0])] != l_False); uncheckedEnqueue(ps[0], cr); - PROOF( if (ps.size() == 1) { ProofManager::getSatProof()->registerUnitClause(ps[0], true); } ) + PROOF( if (ps.size() == 1) { ProofManager::getSatProof()->registerUnitClause(ps[0], INPUT); } ) return ok = (propagate(CHECK_WITHOUT_THEORY) == CRef_Undef); } else return ok; } @@ -1631,7 +1631,7 @@ CRef Solver::updateLemmas() { } lemma_ref = ca.alloc(clauseLevel, lemma, removable); - PROOF (ProofManager::getSatProof()->registerClause(lemma_ref, true); ); + PROOF (ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA); ); if (removable) { clauses_removable.push(lemma_ref); } else { -- 2.30.2