diff options
Diffstat (limited to 'src/proof/theory_proof.h')
-rw-r--r-- | src/proof/theory_proof.h | 89 |
1 files changed, 26 insertions, 63 deletions
diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h index 352cc1b53..f6f00fa11 100644 --- a/src/proof/theory_proof.h +++ b/src/proof/theory_proof.h @@ -35,57 +35,8 @@ namespace theory { class Theory; } /* 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) - , id(i) - {} - LetCount(const LetCount& other) - : count(other.count) - , id (other.id) - {} - bool operator==(const LetCount &other) const { - return other.id == id && other.count == count; - } - LetCount& operator=(const LetCount &rhs) { - if (&rhs == this) return *this; - id = rhs.id; - count = rhs.count; - return *this; - } -}; - -struct LetOrderElement { - Expr expr; - unsigned id; - LetOrderElement(Expr e, unsigned i) - : expr(e) - , id(i) - {} - - LetOrderElement() - : expr() - , id(-1) - {} -}; - 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; typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet; @@ -118,7 +69,7 @@ public: */ virtual void printLetTerm(Expr term, std::ostream& os) = 0; virtual void printBoundTerm(Expr term, std::ostream& os, - const LetMap& map) = 0; + const ProofLetMap& map) = 0; /** * Print the proof representation of the given sort. @@ -168,7 +119,7 @@ public: * @param paren */ virtual void printTheoryLemmas(const IdToSatClause& lemmas, std::ostream& os, - std::ostream& paren) = 0; + std::ostream& paren, ProofLetMap& map) = 0; /** * Register theory atom (ensures all terms and atoms are declared). @@ -192,40 +143,43 @@ public: void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2); virtual void treatBoolsAsFormulas(bool value) {}; + + virtual void printTheoryTerm(Expr term, std::ostream& os, const ProofLetMap& map) = 0; }; class LFSCTheoryProofEngine : public TheoryProofEngine { - LetMap d_letMap; - void printTheoryTerm(Expr term, std::ostream& os, const LetMap& map); - void bind(Expr term, LetMap& map, Bindings& let_order); + void bind(Expr term, ProofLetMap& map, Bindings& let_order); public: LFSCTheoryProofEngine() : TheoryProofEngine() {} + void printTheoryTerm(Expr term, std::ostream& os, const ProofLetMap& map); + 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 printCoreTerm(Expr term, std::ostream& os, const ProofLetMap& map); virtual void printLetTerm(Expr term, std::ostream& os); - virtual void printBoundTerm(Expr term, std::ostream& os, const LetMap& map); + virtual void printBoundTerm(Expr term, std::ostream& os, const ProofLetMap& map); virtual void printAssertions(std::ostream& os, std::ostream& paren); virtual void printLemmaRewrites(NodePairSet& rewrites, std::ostream& os, std::ostream& paren); virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren); virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren); virtual void printTheoryLemmas(const IdToSatClause& lemmas, std::ostream& os, - std::ostream& paren); + std::ostream& paren, + ProofLetMap& map); virtual void printSort(Type type, std::ostream& os); void performExtraRegistrations(); void treatBoolsAsFormulas(bool value); + void finalizeBvConflicts(const IdToSatClause& lemmas, std::ostream& os); private: static void dumpTheoryLemmas(const IdToSatClause& lemmas); // TODO: this function should be moved into the BV prover. - void finalizeBvConflicts(const IdToSatClause& lemmas, std::ostream& os, std::ostream& paren); std::map<Node, std::string> d_assertionToRewrite; }; @@ -247,7 +201,7 @@ public: * @param term expresion representing term * @param os output stream */ - void printTerm(Expr term, std::ostream& os, const LetMap& map) { + void printTerm(Expr term, std::ostream& os, const ProofLetMap& map) { d_proofEngine->printBoundTerm(term, os, map); } /** @@ -256,7 +210,7 @@ public: * @param term expresion representing term * @param os output stream */ - virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) = 0; + virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) = 0; /** * Print the proof representation of the given type that belongs to some theory. * @@ -279,7 +233,10 @@ public: * * @param os output stream */ - virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren); + virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, + std::ostream& os, + std::ostream& paren, + const ProofLetMap& map); /** * Print the sorts declarations for this theory. * @@ -321,6 +278,12 @@ public: * @param term */ virtual void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2); + /** + * Print a proof for the equivalence of n1 and n2. + * + * @param term + */ + virtual void printRewriteProof(std::ostream& os, const Node &n1, const Node &n2); virtual void treatBoolsAsFormulas(bool value) {} }; @@ -333,7 +296,7 @@ public: virtual void registerTerm(Expr term); - virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) = 0; + virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& 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; @@ -348,7 +311,7 @@ public: LFSCBooleanProof(TheoryProofEngine* proofEngine) : BooleanProof(proofEngine), d_treatBoolsAsFormulas(true) {} - virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map); + virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map); virtual void printOwnedSort(Type type, std::ostream& os); virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren); virtual void printSortDeclarations(std::ostream& os, std::ostream& paren); |