diff options
author | lianah <lianahady@gmail.com> | 2013-10-08 19:22:19 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-10-08 19:22:19 -0400 |
commit | 000f574406c29df4c60947169ef527ee5316beb7 (patch) | |
tree | e2bc0426627689ccd59d63976c9497cb9f0dc335 /src/proof/theory_proof.cpp | |
parent | 3361081acd11178d0eb580ce91279a2ecaa7aa65 (diff) |
added currying for uf proofs; still needs debugging
Diffstat (limited to 'src/proof/theory_proof.cpp')
-rw-r--r-- | src/proof/theory_proof.cpp | 133 |
1 files changed, 112 insertions, 21 deletions
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<Type> 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()); |