diff options
author | lianah <lianahady@gmail.com> | 2013-11-05 20:03:49 -0500 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-11-05 20:03:49 -0500 |
commit | ad0f78965f23b0994cac6a210650697b9a20cceb (patch) | |
tree | b28418322c642ecf7f3d47ba356c4026c4ece4be /src/proof | |
parent | 347ac2260da73297776c547f7397b33beb59cf2b (diff) |
fixed proof regression script and added a new uf test case
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/cnf_proof.cpp | 14 | ||||
-rw-r--r-- | src/proof/proof_manager.cpp | 19 | ||||
-rw-r--r-- | src/proof/proof_manager.h | 15 | ||||
-rw-r--r-- | src/proof/sat_proof.cpp | 6 | ||||
-rw-r--r-- | src/proof/theory_proof.cpp | 2 |
5 files changed, 42 insertions, 14 deletions
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index cb22ca819..8e9c4cd21 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -33,7 +33,8 @@ CnfProof::CnfProof(CnfStream* stream) Expr CnfProof::getAtom(prop::SatVariable var) { prop::SatLiteral lit (var); - Expr atom = d_cnfStream->getNode(lit).toExpr(); + Node node = d_cnfStream->getNode(lit); + Expr atom = node.toExpr(); return atom; } @@ -45,9 +46,16 @@ void LFSCCnfProof::printAtomMapping(std::ostream& os, std::ostream& paren) { ProofManager::var_iterator end = ProofManager::currentPM()->end_vars(); for (;it != end; ++it) { - Expr atom = getAtom(*it); os << "(decl_atom "; - LFSCTheoryProof::printFormula(atom, os); + + if (ProofManager::currentPM()->getLogic().compare("QF_UF") == 0) { + Expr atom = getAtom(*it); + LFSCTheoryProof::printFormula(atom, os); + } else { + // print fake atoms for all other logics + os << "true "; + } + os << " (\\ " << ProofManager::getVarName(*it) << " (\\ " << ProofManager::getAtomName(*it) << "\n"; paren << ")))"; } diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 23ba0e4e7..110e6b79a 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -21,6 +21,8 @@ #include "proof/cnf_proof.h" #include "proof/theory_proof.h" #include "util/cvc4_assert.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" namespace CVC4 { @@ -68,12 +70,13 @@ ProofManager* ProofManager::currentPM() { } } -Proof* ProofManager::getProof() { +Proof* ProofManager::getProof(SmtEngine* smt) { if (currentPM()->d_fullProof != NULL) return currentPM()->d_fullProof; Assert (currentPM()->d_format == LFSC); - currentPM()->d_fullProof = new LFSCProof((LFSCSatProof*)getSatProof(), + currentPM()->d_fullProof = new LFSCProof(smt, + (LFSCSatProof*)getSatProof(), (LFSCCnfProof*)getCnfProof(), (LFSCTheoryProof*)getTheoryProof()); return currentPM()->d_fullProof; @@ -138,19 +141,27 @@ void ProofManager::addAssertion(Expr formula) { d_inputFormulas.insert(formula); } +void ProofManager::setLogic(const std::string& logic_string) { + d_logic = logic_string; +} + -LFSCProof::LFSCProof(LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory) +LFSCProof::LFSCProof(SmtEngine* smtEngine, LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory) : d_satProof(sat) , d_cnfProof(cnf) , d_theoryProof(theory) + , d_smtEngine(smtEngine) { d_satProof->constructProof(); } void LFSCProof::toStream(std::ostream& out) { + smt::SmtScope scope(d_smtEngine); std::ostringstream paren; out << "(check \n"; - d_theoryProof->printAssertions(out, paren); + if (ProofManager::currentPM()->getLogic().compare("QF_UF") == 0) { + d_theoryProof->printAssertions(out, paren); + } out << "(: (holds cln) \n"; d_cnfProof->printAtomMapping(out, paren); d_cnfProof->printClauses(out, paren); diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index 7642ba776..82a1bd6be 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -36,6 +36,9 @@ namespace CVC4 { namespace prop { class CnfStream; } + +class SmtEngine; + typedef int ClauseId; class Proof; @@ -91,6 +94,8 @@ class ProofManager { static bool isInitialized; ProofManager(ProofFormat format = LFSC); ~ProofManager(); +protected: + std::string d_logic; public: static ProofManager* currentPM(); // initialization @@ -98,7 +103,7 @@ public: static void initCnfProof(CVC4::prop::CnfStream* cnfStream); static void initTheoryProof(); - static Proof* getProof(); + static Proof* getProof(SmtEngine* smt); static SatProof* getSatProof(); static CnfProof* getCnfProof(); static TheoryProof* getTheoryProof(); @@ -131,14 +136,18 @@ public: static std::string getVarName(prop::SatVariable var); static std::string getAtomName(prop::SatVariable var); static std::string getLitName(prop::SatLiteral lit); + + void setLogic(const std::string& logic_string); + const std::string getLogic() const { return d_logic; } };/* class ProofManager */ class LFSCProof : public Proof { LFSCSatProof* d_satProof; LFSCCnfProof* d_cnfProof; - LFSCTheoryProof* d_theoryProof; + LFSCTheoryProof* d_theoryProof; + SmtEngine* d_smtEngine; public: - LFSCProof(LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory); + LFSCProof(SmtEngine* smtEngine, LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory); virtual void toStream(std::ostream& out); virtual ~LFSCProof() {} }; diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp index 2ac468b47..da9df0d42 100644 --- a/src/proof/sat_proof.cpp +++ b/src/proof/sat_proof.cpp @@ -579,9 +579,9 @@ void SatProof::finalizeProof(::Minisat::CRef conflict_ref) { res->addStep(lit, res_id, !sign(lit)); } registerResolution(d_emptyClauseId, res); - // FIXME: massive hack - Proof* proof = ProofManager::getProof(); - proof->toStream(std::cout); + // // FIXME: massive hack + // Proof* proof = ProofManager::getProof(); + // proof->toStream(std::cout); } /// CRef manager diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 4ce804a74..696bd8309 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -167,7 +167,7 @@ void LFSCTheoryProof::printDeclarations(std::ostream& os, std::ostream& paren) { // declaring the terms for (ExprSet::const_iterator it = d_termDeclarations.begin(); it != d_termDeclarations.end(); ++it) { Expr term = *it; - + os << "(% " << term << " (term "; paren <<")"; |