From: lianah Date: Tue, 8 Oct 2013 23:22:19 +0000 (-0400) Subject: added currying for uf proofs; still needs debugging X-Git-Tag: cvc5-1.0.0~7282 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=000f574406c29df4c60947169ef527ee5316beb7;p=cvc5.git added currying for uf proofs; still needs debugging --- diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index e1f85b93f..0c3c597da 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -131,6 +131,7 @@ 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); d_cnfProof->printClauses(out, paren); diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 948ced393..ecd9f9810 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -21,7 +21,12 @@ using namespace CVC4; TheoryProof::TheoryProof() : d_atomSet() + , d_inputFormulas() + , d_termDeclarations() + , d_sortDeclarations() + , d_declarationCache() {} + void TheoryProof::addAtom(Expr atom) { d_atomSet.insert(atom); Assert (atom.getKind() == kind::EQUAL); @@ -29,20 +34,30 @@ void TheoryProof::addAtom(Expr atom) { 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; + 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); - Assert (term.getNumChildren() == 1); - addDeclaration(term[0]); - } else { - Assert (term.isVariable()); + } else if (term.isVariable()) { Assert (type.isSort()); d_termDeclarations.insert(term); } + // recursively declare all other terms + for (unsigned i = 0; i < term.getNumChildren(); ++i) { + addDeclaration(term[i]); + } + d_declarationCache.insert(term); } void LFSCTheoryProof::printTerm(Expr term, std::ostream& os) { @@ -50,22 +65,88 @@ void LFSCTheoryProof::printTerm(Expr term, std::ostream& os) { os << term; return; } - Assert (term.getKind() == kind::APPLY_UF && term.getNumChildren() == 1); + std::ostringstream paren; + Assert (term.getKind() == kind::APPLY_UF); Expr func = term.getOperator(); os << "(apply _ _ " << func << " "; - printTerm(term[0], os); - os <<")"; + for (unsigned i = 0; i < term.getNumChildren(); ++i) { + printTerm(term[i], os); + if (i < term.getNumChildren() - 1) { + os << "(apply _ _ " << func << " "; + paren << ")"; + } + os << ")" ; + } + os << paren.str(); +} + +std::string toLFSCKind(Kind kind) { + switch(kind) { + case kind::OR : return "or"; + case kind::AND: return "and"; + case kind::XOR: return "xor"; + case kind::EQUAL: return "="; + case kind::IMPLIES: return "impl"; + case kind::NOT: return "not"; + default: + Unreachable(); + } } void LFSCTheoryProof::printFormula(Expr atom, std::ostream& os) { - // should make this more general - Assert (atom.getKind() == kind::EQUAL); - os << "(= "; - os << atom[0].getType() <<" "; - printTerm(atom[0], os); - os << " "; - printTerm(atom[1], os); - os << ")"; + // should make this more general and overall sane + Assert (atom.getType().isBoolean()); + Kind kind = atom.getKind(); + // this is the only predicate we have + if (kind == kind::EQUAL) { + os << "("; + os <<"= "; + os << atom[0].getType() <<" "; + printTerm(atom[0], os); + os <<" "; + printTerm(atom[1], os); + os <<")"; + } else if ( kind == kind::OR || + kind == kind::AND || + kind == kind::XOR || + kind == kind::IMPLIES || + kind == kind::NOT) { + // print the boolean operators + os << "("; + os << toLFSCKind(kind); + if (atom.getNumChildren() > 2) { + std::ostringstream paren; + os << " "; + for (unsigned i =0; i < atom.getNumChildren(); ++i) { + printFormula(atom[i], os); + os << " "; + if (i < atom.getNumChildren() - 2) { + os << "("<< toLFSCKind(kind) << " "; + paren << ")"; + } + } + os << paren.str() <<")"; + } else { + // this is for binary and unary operators + for (unsigned i = 0; i < atom.getNumChildren(); ++i) { + os <<" "; + printFormula(atom[i], os); + } + os <<")"; + } + } else { + Assert (false); + } +} + +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) { + os << "(% A" << counter++ << " (th_holds "; + printFormula(*it, os); + os << ")\n"; + paren <<")"; + } } void LFSCTheoryProof::printDeclarations(std::ostream& os, std::ostream& paren) { @@ -76,7 +157,7 @@ void LFSCTheoryProof::printDeclarations(std::ostream& os, std::ostream& paren) { } // declaring the terms - for (TermSet::const_iterator it = d_termDeclarations.begin(); it != d_termDeclarations.end(); ++it) { + for (ExprSet::const_iterator it = d_termDeclarations.begin(); it != d_termDeclarations.end(); ++it) { Expr term = *it; os << "(% " << term << " (term "; @@ -84,11 +165,21 @@ void LFSCTheoryProof::printDeclarations(std::ostream& os, std::ostream& paren) { Type type = term.getType(); if (type.isFunction()) { - FunctionType ftype = (FunctionType)type; - Assert (ftype.getArity() == 1); - Type arg_type = ftype.getArgTypes()[0]; - Type result_type = ftype.getRangeType(); - os << "(arrow " << arg_type << " " << result_type << "))\n"; + std::ostringstream fparen; + FunctionType ftype = (FunctionType)type; + std::vector args = ftype.getArgTypes(); + args.push_back(ftype.getRangeType()); + os << "(arrow "; + for (unsigned i = 0; i < args.size(); i++) { + Type arg_type = args[i]; + Assert (arg_type.isSort()); + os << arg_type << " "; + if (i < args.size() - 2) { + os << "(arrow "; + fparen <<")"; + } + } + os << fparen.str() << "))\n"; } else { Assert (term.isVariable()); Assert (type.isSort()); diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h index ac8f9f7b8..b09641fec 100644 --- a/src/proof/theory_proof.h +++ b/src/proof/theory_proof.h @@ -28,28 +28,33 @@ namespace CVC4 { - typedef __gnu_cxx::hash_set AtomSet; - typedef __gnu_cxx::hash_set TermSet; + typedef __gnu_cxx::hash_set ExprSet; typedef __gnu_cxx::hash_set SortSet; class TheoryProof { protected: - AtomSet d_atomSet; - TermSet d_termDeclarations; + ExprSet d_atomSet; + ExprSet d_inputFormulas; + ExprSet d_termDeclarations; SortSet d_sortDeclarations; + ExprSet d_declarationCache; + 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 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); public: virtual void printFormula(Expr atom, std::ostream& os); - virtual void printDeclarations(std::ostream& os, std::ostream& paren); + virtual void printDeclarations(std::ostream& os, std::ostream& paren); + virtual void printAssertions(std::ostream& os, std::ostream& paren); }; } /* CVC4 namespace */ #endif /* __CVC4__THEORY_PROOF_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index be6acd09c..5a3334d64 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -38,6 +38,7 @@ #include "expr/node.h" #include "expr/node_self_iterator.h" #include "prop/prop_engine.h" +#include "proof/theory_proof.h" #include "smt/modal_exception.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" @@ -46,6 +47,7 @@ #include "theory/bv/theory_bv_rewriter.h" #include "proof/proof_manager.h" #include "util/proof.h" +#include "proof/proof.h" #include "util/boolean_simplification.h" #include "util/node_visitor.h" #include "util/configuration.h" @@ -3103,6 +3105,11 @@ void SmtEngine::ensureBoolean(const Expr& e) throw(TypeCheckingException) { Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalException, LogicException) { Assert(ex.isNull() || ex.getExprManager() == d_exprManager); + // PROOF ( + ProofManager* pm = ProofManager::currentPM(); + TheoryProof* pf = pm->getTheoryProof(); + pf->assertFormula(ex); + // ); SmtScope smts(this); finalOptionsAreSet(); doPendingPops(); @@ -3246,6 +3253,8 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, LogicException) { Assert(ex.getExprManager() == d_exprManager); + //PROOF ( + ProofManager::currentPM()->getTheoryProof()->assertFormula(ex); //); SmtScope smts(this); finalOptionsAreSet(); doPendingPops();