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/array_proof.h | |
parent | 786cd2dd5b1c53f650c891d6dfbf299a62840848 (diff) |
squash-merge from proof branch
Diffstat (limited to 'src/proof/array_proof.h')
-rw-r--r-- | src/proof/array_proof.h | 70 |
1 files changed, 41 insertions, 29 deletions
diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h index beaf5194c..9b308dcd8 100644 --- a/src/proof/array_proof.h +++ b/src/proof/array_proof.h @@ -23,53 +23,65 @@ #include "proof/proof_manager.h" #include "proof/theory_proof.h" #include "theory/arrays/theory_arrays.h" +#include "theory/uf/equality_engine.h" namespace CVC4 { +//proof object outputted by TheoryARRAY +class ProofArray : public Proof { +private: + static Node toStreamRecLFSC(std::ostream& out, TheoryProof* tp, + theory::eq::EqProof* pf, + unsigned tb, + const LetMap& map); + + std::hash_map<Node, Node, NodeHashFunction> d_nodeToSkolem; +public: + ProofArray(theory::eq::EqProof* pf) : d_proof(pf) {} + //it is simply an equality engine proof + theory::eq::EqProof *d_proof; + void toStream(std::ostream& out); + static void toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, const LetMap& map); + + void registerSkolem(Node equality, Node skolem); +}; + namespace theory { namespace arrays{ class TheoryArrays; } /* namespace CVC4::theory::arrays */ } /* namespace CVC4::theory */ +typedef __gnu_cxx::hash_set<Type, TypeHashFunction > TypeSet; + class ArrayProof : public TheoryProof { // TODO: whatever goes in this theory +protected: + TypeSet d_sorts; // all the uninterpreted sorts in this theory + ExprSet d_declarations; // all the variable/function declarations + ExprSet d_skolemDeclarations; // all the skolem variable declarations + std::map<Expr, std::string> d_skolemToLiteral; + public: - ArrayProof(theory::arrays::TheoryArrays* arrays, TheoryProofEngine* proofEngine) - : TheoryProof(arrays, 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; - /** - * Print a proof for the theory lemma. Must prove - * clause representing lemma to be used in resolution proof. - * - * @param lemma clausal form of lemma - * @param os output stream - */ - virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) = 0; - /** - * Print the variable/sorts declarations for this theory. - * - * @param os - * @param paren - */ - virtual void printDeclarations(std::ostream& os, std::ostream& paren) = 0; + ArrayProof(theory::arrays::TheoryArrays* arrays, TheoryProofEngine* proofEngine); + + std::string skolemToLiteral(Expr skolem); + + virtual void registerTerm(Expr term); }; class LFSCArrayProof : public ArrayProof { public: - LFSCArrayProof(theory::arrays::TheoryArrays* uf, TheoryProofEngine* proofEngine) - : ArrayProof(uf, proofEngine) + LFSCArrayProof(theory::arrays::TheoryArrays* arrays, TheoryProofEngine* proofEngine) + : ArrayProof(arrays, proofEngine) {} - // TODO implement - virtual void printTerm(Expr term, std::ostream& os, const LetMap& map) {} - virtual void printSort(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 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 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); }; |