diff options
Diffstat (limited to 'src/proof/theory_proof.h')
-rw-r--r-- | src/proof/theory_proof.h | 86 |
1 files changed, 43 insertions, 43 deletions
diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h index 3d700c388..d997d6e23 100644 --- a/src/proof/theory_proof.h +++ b/src/proof/theory_proof.h @@ -30,8 +30,6 @@ namespace CVC4 { -class SmtGlobals; - namespace theory { class Theory; } @@ -89,7 +87,7 @@ typedef __gnu_cxx::hash_map < ClauseId, prop::SatClause* > IdToSatClause; typedef __gnu_cxx::hash_map<Expr, LetCount, ExprHashFunction> LetMap; typedef std::vector<LetOrderElement> Bindings; -class TheoryProof; +class TheoryProof; typedef unsigned ClauseId; typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet; @@ -99,67 +97,69 @@ class TheoryProofEngine { protected: ExprSet d_registrationCache; TheoryProofTable d_theoryProofTable; - + /** * Returns whether the theory is currently supported in proof * production mode. */ bool supportedTheory(theory::TheoryId id); public: - SmtGlobals* d_globals; - - TheoryProofEngine(SmtGlobals* globals); + + TheoryProofEngine(); virtual ~TheoryProofEngine(); - /** - * Print the theory term (could be atom) by delegating to the - * proper theory - * - * @param term - * @param os - * - * @return + + /** + * Print the theory term (could be an atom) by delegating to the proper theory. + * + * @param term + * @param os */ virtual void printLetTerm(Expr term, std::ostream& os) = 0; - virtual void printBoundTerm(Expr term, std::ostream& os, const LetMap& map) = 0; - /** + virtual void printBoundTerm(Expr term, std::ostream& os, + const LetMap& map) = 0; + + /** * Print the proof representation of the given sort. - * - * @param os + * + * @param os */ - virtual void printSort(Type type, std::ostream& os) = 0; - /** + virtual void printSort(Type type, std::ostream& os) = 0; + + /** * Print the theory assertions (arbitrary formulas over * theory atoms) - * - * @param os + * + * @param os * @param paren closing parenthesis */ virtual void printAssertions(std::ostream& os, std::ostream& paren) = 0; - /** + + /** * Print proofs of all the theory lemmas (must prove * actual clause used in resolution proof). - * - * @param os - * @param paren + * + * @param os + * @param paren */ - virtual void printTheoryLemmas(const IdToSatClause& lemmas, - std::ostream& os, + virtual void printTheoryLemmas(const IdToSatClause& lemmas, std::ostream& os, std::ostream& paren) = 0; - /** - * Register theory atom (ensures all terms and atoms are declared). - * - * @param atom + + /** + * Register theory atom (ensures all terms and atoms are declared). + * + * @param atom */ void registerTerm(Expr atom); - /** - * Ensures that a theory proof class for the given theory - * is created. - * - * @param theory + + /** + * Ensures that a theory proof class for the given theory is created. + * + * @param theory */ void registerTheory(theory::Theory* theory); + theory::TheoryId getTheoryForLemma(ClauseId id); - TheoryProof* getTheoryProof(theory::TheoryId id); + TheoryProof* getTheoryProof(theory::TheoryId id); }; class LFSCTheoryProofEngine : public TheoryProofEngine { @@ -167,9 +167,9 @@ class LFSCTheoryProofEngine : public TheoryProofEngine { void printTheoryTerm(Expr term, std::ostream& os, const LetMap& map); void bind(Expr term, LetMap& map, Bindings& let_order); public: - LFSCTheoryProofEngine(SmtGlobals* globals) - : TheoryProofEngine(globals) {} - + LFSCTheoryProofEngine() + : TheoryProofEngine() {} + void printDeclarations(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); @@ -178,7 +178,7 @@ public: virtual void printTheoryLemmas(const IdToSatClause& lemmas, std::ostream& os, std::ostream& paren); - virtual void printSort(Type type, std::ostream& os); + virtual void printSort(Type type, std::ostream& os); }; class TheoryProof { |