diff options
author | Guy <katz911@gmail.com> | 2016-03-23 12:07:59 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-03-23 12:07:59 -0700 |
commit | aa9aa46b77f048f2865c29e40ed946371fd115ef (patch) | |
tree | 254f392449a03901f7acb7a65e9499193d07ac9a /src/proof/theory_proof.h | |
parent | 786cd2dd5b1c53f650c891d6dfbf299a62840848 (diff) |
squash-merge from proof branch
Diffstat (limited to 'src/proof/theory_proof.h')
-rw-r--r-- | src/proof/theory_proof.h | 127 |
1 files changed, 91 insertions, 36 deletions
diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h index d14704760..b04dd4c60 100644 --- a/src/proof/theory_proof.h +++ b/src/proof/theory_proof.h @@ -39,14 +39,14 @@ struct LetCount { static unsigned counter; static void resetCounter() { counter = 0; } static unsigned newId() { return ++counter; } - + unsigned count; unsigned id; LetCount() : count(0) , id(-1) {} - + void increment() { ++count; } LetCount(unsigned i) : count(1) @@ -65,7 +65,7 @@ struct LetCount { count = rhs.count; return *this; } -}; +}; struct LetOrderElement { Expr expr; @@ -84,7 +84,7 @@ struct LetOrderElement { typedef __gnu_cxx::hash_map < ClauseId, prop::SatClause* > IdToSatClause; typedef __gnu_cxx::hash_map<Expr, LetCount, ExprHashFunction> LetMap; -typedef std::vector<LetOrderElement> Bindings; +typedef std::vector<LetOrderElement> Bindings; class TheoryProof; @@ -124,6 +124,14 @@ public: virtual void printSort(Type type, std::ostream& os) = 0; /** + * Go over the assertions and register all terms with the theories. + * + * @param os + * @param paren closing parenthesis + */ + virtual void registerTermsFromAssertions() = 0; + + /** * Print the theory assertions (arbitrary formulas over * theory atoms) * @@ -131,6 +139,14 @@ public: * @param paren closing parenthesis */ virtual void printAssertions(std::ostream& os, std::ostream& paren) = 0; + /** + * Print variable declarations that need to appear within the proof, + * e.g. skolemized variables. + * + * @param os + * @param paren closing parenthesis + */ + virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren) = 0; /** * Print proofs of all the theory lemmas (must prove @@ -168,11 +184,14 @@ public: LFSCTheoryProofEngine() : TheoryProofEngine() {} - void printDeclarations(std::ostream& os, std::ostream& paren); + void registerTermsFromAssertions(); + void printSortDeclarations(std::ostream& os, std::ostream& paren); + void printTermDeclarations(std::ostream& os, std::ostream& paren); virtual void printCoreTerm(Expr term, std::ostream& os, const LetMap& map); virtual void printLetTerm(Expr term, std::ostream& os); virtual void printBoundTerm(Expr term, std::ostream& os, const LetMap& map); virtual void printAssertions(std::ostream& os, std::ostream& paren); + virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren); virtual void printTheoryLemmas(const IdToSatClause& lemmas, std::ostream& os, std::ostream& paren); @@ -189,41 +208,74 @@ public: : d_theory(th) , d_proofEngine(proofEngine) {} - virtual ~TheoryProof() {}; - /** - * Print a term belonging to this theory. - * + virtual ~TheoryProof() {}; + /** + * Print a term belonging some theory, not neccessarily this one. + * * @param term expresion representing term * @param os output stream */ - virtual void printTerm(Expr term, std::ostream& os, const LetMap& map) = 0; - /** - * Print the proof representation of the given type. - * - * @param type - * @param os + void printTerm(Expr term, std::ostream& os, const LetMap& map) { + d_proofEngine->printBoundTerm(term, os, map); + } + /** + * Print a term belonging to THIS theory. + * + * @param term expresion representing term + * @param os output stream + */ + virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) = 0; + /** + * Print the proof representation of the given type that belongs to some theory. + * + * @param type + * @param os */ - virtual void printSort(Type type, std::ostream& os) = 0; - /** + void printSort(Type type, std::ostream& os) { + d_proofEngine->printSort(type, os); + } + /** + * Print the proof representation of the given type that belongs to THIS theory. + * + * @param type + * @param os + */ + virtual void printOwnedSort(Type type, std::ostream& os) = 0; + /** * Print a proof for the theory lemmas. Must prove * clause representing lemmas to be used in resolution proof. - * + * * @param os output stream */ virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren); - /** - * Print the variable/sorts declarations for this theory. - * - * @param os - * @param paren + /** + * Print the sorts declarations for this theory. + * + * @param os + * @param paren */ - virtual void printDeclarations(std::ostream& os, std::ostream& paren) = 0; - /** + virtual void printSortDeclarations(std::ostream& os, std::ostream& paren) = 0; + /** + * Print the term declarations for this theory. + * + * @param os + * @param paren + */ + virtual void printTermDeclarations(std::ostream& os, std::ostream& paren) = 0; + /** + * Print any deferred variable/sorts declarations for this theory + * (those that need to appear inside the actual proof). + * + * @param os + * @param paren + */ + virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren) = 0; + /** * Register a term of this theory that appears in the proof. - * - * @param term + * + * @param term */ - virtual void registerTerm(Expr term) = 0; + virtual void registerTerm(Expr term) = 0; }; class BooleanProof : public TheoryProof { @@ -233,12 +285,14 @@ public: BooleanProof(TheoryProofEngine* proofEngine); virtual void registerTerm(Expr term); - - virtual void printTerm(Expr term, std::ostream& os, const LetMap& map) = 0; - virtual void printSort(Type type, std::ostream& os) = 0; + virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) = 0; + + virtual void printOwnedSort(Type type, std::ostream& os) = 0; virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) = 0; - virtual void printDeclarations(std::ostream& os, std::ostream& paren) = 0; + virtual void printSortDeclarations(std::ostream& os, std::ostream& paren) = 0; + virtual void printTermDeclarations(std::ostream& os, std::ostream& paren) = 0; + virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren) = 0; }; class LFSCBooleanProof : public BooleanProof { @@ -246,13 +300,14 @@ public: LFSCBooleanProof(TheoryProofEngine* proofEngine) : BooleanProof(proofEngine) {} - virtual void printTerm(Expr term, std::ostream& os, const LetMap& map); - virtual void printSort(Type type, std::ostream& os); + virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map); + virtual void printOwnedSort(Type type, std::ostream& os); virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren); - virtual void printDeclarations(std::ostream& os, std::ostream& paren); + virtual void printSortDeclarations(std::ostream& os, std::ostream& paren); + virtual void printTermDeclarations(std::ostream& os, std::ostream& paren); + virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren); }; - } /* CVC4 namespace */ #endif /* __CVC4__THEORY_PROOF_H */ |