1 /*********************                                                        */
2 /*! \file array_proof.h
3  ** \verbatim
4  ** Top contributors (to current version):
5  **   Tim King, Mathias Preiner, Guy Katz
6  ** This file is part of the CVC4 project.
7  ** Copyright (c) 2009-2019 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() override;
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:
LFSCArrayProof(theory::arrays::TheoryArrays * arrays,TheoryProofEngine * proofEngine)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 */
121