diff options
Diffstat (limited to 'src/proof/theory_proof.h')
| -rw-r--r-- | src/proof/theory_proof.h | 166 |
1 files changed, 109 insertions, 57 deletions
diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h index d997d6e23..54c86f3f3 100644 --- a/src/proof/theory_proof.h +++ b/src/proof/theory_proof.h @@ -1,19 +1,18 @@ /********************* */ /*! \file theory_proof.h -** \verbatim -** Original author: Liana Hadarean -** Major contributors: Morgan Deters -** Minor contributors (to current version): none -** This file is part of the CVC4 project. -** Copyright (c) 2009-2014 New York University and The University of Iowa -** See the file COPYING in the top-level source directory for licensing -** information.\endverbatim -** -** \brief A manager for UfProofs. -** -** A manager for UfProofs. -** -** + ** \verbatim + ** Top contributors (to current version): + ** Liana Hadarean, Guy Katz, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** [[ Add lengthier description here ]] + + ** \todo document this file + **/ #include "cvc4_private.h" @@ -21,33 +20,32 @@ #ifndef __CVC4__THEORY_PROOF_H #define __CVC4__THEORY_PROOF_H -#include "util/proof.h" -#include "expr/expr.h" -#include "prop/sat_solver_types.h" #include <ext/hash_set> #include <iosfwd> +#include "expr/expr.h" +#include "proof/clause_id.h" +#include "prop/sat_solver_types.h" +#include "util/proof.h" namespace CVC4 { namespace theory { class Theory; -} - -typedef unsigned ClauseId; +} /* namespace CVC4::theory */ 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) @@ -66,7 +64,7 @@ struct LetCount { count = rhs.count; return *this; } -}; +}; struct LetOrderElement { Expr expr; @@ -85,10 +83,9 @@ 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; -typedef unsigned ClauseId; typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet; typedef std::map<theory::TheoryId, TheoryProof* > TheoryProofTable; @@ -126,6 +123,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) * @@ -133,6 +138,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 @@ -170,11 +183,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); @@ -191,41 +207,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 printSort(Type type, std::ostream& os) = 0; - /** + 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 + */ + 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 { @@ -235,12 +284,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 { @@ -248,13 +299,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 */ |