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