1 /********************* */
2 /*! \file array_proof.h
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
12 ** \brief Arrray proof
17 #include "cvc4_private.h"
19 #ifndef __CVC4__ARRAY__PROOF_H
20 #define __CVC4__ARRAY__PROOF_H
23 #include <unordered_set>
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"
33 // Proof object outputted by TheoryARRAY.
34 class ProofArray
: public Proof
{
36 ProofArray(std::shared_ptr
<theory::eq::EqProof
> pf
, unsigned row
,
37 unsigned row1
, unsigned ext
);
39 void registerSkolem(Node equality
, Node skolem
);
41 void toStream(std::ostream
& out
) const override
;
42 void toStream(std::ostream
& out
, const ProofLetMap
& map
) const override
;
45 void toStreamLFSC(std::ostream
& out
,
47 const theory::eq::EqProof
& pf
,
48 const ProofLetMap
& map
) const;
50 Node
toStreamRecLFSC(std::ostream
& out
,
52 const theory::eq::EqProof
& pf
,
54 const ProofLetMap
& map
) const;
56 // It is simply an equality engine proof.
57 std::shared_ptr
<theory::eq::EqProof
> d_proof
;
59 /** Merge tag for ROW applications */
61 /** Merge tag for ROW1 applications */
62 unsigned d_reasonRow1
;
63 /** Merge tag for EXT applications */
70 } /* namespace CVC4::theory::arrays */
71 } /* namespace CVC4::theory */
73 typedef std::unordered_set
<Type
, TypeHashFunction
> TypeSet
;
75 class ArrayProof
: public TheoryProof
{
76 // TODO: whatever goes in this theory
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();
85 ArrayProof(theory::arrays::TheoryArrays
* arrays
, TheoryProofEngine
* proofEngine
);
87 std::string
skolemToLiteral(Expr skolem
);
89 void registerTerm(Expr term
) override
;
92 class LFSCArrayProof
: public ArrayProof
{
94 LFSCArrayProof(theory::arrays::TheoryArrays
* arrays
, TheoryProofEngine
* proofEngine
)
95 : ArrayProof(arrays
, proofEngine
)
98 void printOwnedTerm(Expr term
,
100 const ProofLetMap
& map
) override
;
101 void printOwnedSort(Type type
, std::ostream
& os
) override
;
102 void printTheoryLemmaProof(std::vector
<Expr
>& lemma
,
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
,
112 const ProofLetMap
& globalLetMap
) override
;
114 bool printsAsBool(const Node
& n
) override
;
118 }/* CVC4 namespace */
120 #endif /* __CVC4__ARRAY__PROOF_H */