squash-merge from proof branch

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);
 };