src/proof/array_proof.h

   1 /*********************                                                        */
   2 /*! \file array_proof.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Guy Katz, Liana Hadarean, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Arrray proof
  13  **
  14  ** Arrau proof
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef __CVC4__ARRAY__PROOF_H
  20 #define __CVC4__ARRAY__PROOF_H
  21
  22 #include <memory>
  23 #include <unordered_set>
  24
  25 #include "expr/expr.h"
  26 #include "proof/proof_manager.h"
  27 #include "proof/theory_proof.h"
  28 #include "theory/arrays/theory_arrays.h"
  29 #include "theory/uf/equality_engine.h"
  30
  31 namespace CVC4 {
  32
  33 // Proof object outputted by TheoryARRAY.
  34 class ProofArray : public Proof {
  35  public:
  36   ProofArray(std::shared_ptr<theory::eq::EqProof> pf, unsigned row,
  37              unsigned row1, unsigned ext);
  38
  39   void registerSkolem(Node equality, Node skolem);
  40
  41   void toStream(std::ostream& out) const override;
  42   void toStream(std::ostream& out, const ProofLetMap& map) const override;
  43
  44  private:
  45   void toStreamLFSC(std::ostream& out,
  46                     TheoryProof* tp,
  47                     const theory::eq::EqProof& pf,
  48                     const ProofLetMap& map) const;
  49
  50   Node toStreamRecLFSC(std::ostream& out,
  51                        TheoryProof* tp,
  52                        const theory::eq::EqProof& pf,
  53                        unsigned tb,
  54                        const ProofLetMap& map) const;
  55
  56   // It is simply an equality engine proof.
  57   std::shared_ptr<theory::eq::EqProof> d_proof;
  58
  59   /** Merge tag for ROW applications */
  60   unsigned d_reasonRow;
  61   /** Merge tag for ROW1 applications */
  62   unsigned d_reasonRow1;
  63   /** Merge tag for EXT applications */
  64   unsigned d_reasonExt;
  65 };
  66
  67 namespace theory {
  68 namespace arrays{
  69 class TheoryArrays;
  70 } /* namespace CVC4::theory::arrays */
  71 } /* namespace CVC4::theory */
  72
  73 typedef std::unordered_set<Type, TypeHashFunction > TypeSet;
  74
  75 class ArrayProof : public TheoryProof {
  76   // TODO: whatever goes in this theory
  77 protected:
  78   TypeSet d_sorts;        // all the uninterpreted sorts in this theory
  79   ExprSet d_declarations; // all the variable/function declarations
  80   ExprSet d_skolemDeclarations; // all the skolem variable declarations
  81   std::map<Expr, std::string> d_skolemToLiteral;
  82   theory::TheoryId getTheoryId();
  83
  84  public:
  85   ArrayProof(theory::arrays::TheoryArrays* arrays, TheoryProofEngine* proofEngine);
  86
  87   std::string skolemToLiteral(Expr skolem);
  88
  89   void registerTerm(Expr term) override;
  90 };
  91
  92 class LFSCArrayProof : public ArrayProof {
  93 public:
  94   LFSCArrayProof(theory::arrays::TheoryArrays* arrays, TheoryProofEngine* proofEngine)
  95     : ArrayProof(arrays, proofEngine)
  96   {}
  97
  98   void printOwnedTerm(Expr term,
  99                       std::ostream& os,
 100                       const ProofLetMap& map) override;
 101   void printOwnedSort(Type type, std::ostream& os) override;
 102   void printTheoryLemmaProof(std::vector<Expr>& lemma,
 103                              std::ostream& os,
 104                              std::ostream& paren,
 105                              const ProofLetMap& map) override;
 106   void printSortDeclarations(std::ostream& os, std::ostream& paren) override;
 107   void printTermDeclarations(std::ostream& os, std::ostream& paren) override;
 108   void printDeferredDeclarations(std::ostream& os,
 109                                  std::ostream& paren) override;
 110   void printAliasingDeclarations(std::ostream& os,
 111                                  std::ostream& paren,
 112                                  const ProofLetMap& globalLetMap) override;
 113
 114   bool printsAsBool(const Node& n) override;
 115 };
 116
 117
 118 }/* CVC4 namespace */
 119
 120 #endif /* __CVC4__ARRAY__PROOF_H */