1 /********************* */
4 ** Top contributors (to current version):
5 ** Liana Hadarean, Mathias Preiner, Tim King
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
17 #include "cvc4_private.h"
19 #ifndef __CVC4__UF__PROOF_H
20 #define __CVC4__UF__PROOF_H
23 #include <unordered_set>
25 #include "expr/expr.h"
26 #include "proof/theory_proof.h"
27 #include "theory/uf/equality_engine.h"
28 #include "util/proof.h"
32 // proof object outputted by TheoryUF
33 class ProofUF
: public Proof
36 ProofUF(std::shared_ptr
<theory::eq::EqProof
> pf
) : d_proof(pf
) {}
37 void toStream(std::ostream
& out
) const override
;
38 void toStream(std::ostream
& out
, const ProofLetMap
& map
) const override
;
41 static void toStreamLFSC(std::ostream
& out
, TheoryProof
* tp
,
42 const theory::eq::EqProof
& pf
,
43 const ProofLetMap
& map
);
44 static Node
toStreamRecLFSC(std::ostream
& out
, TheoryProof
* tp
,
45 const theory::eq::EqProof
& pf
, unsigned tb
,
46 const ProofLetMap
& map
);
48 // it is simply an equality engine proof
49 std::shared_ptr
<theory::eq::EqProof
> d_proof
;
58 typedef std::unordered_set
<Type
, TypeHashFunction
> TypeSet
;
61 class UFProof
: public TheoryProof
{
63 TypeSet d_sorts
; // all the uninterpreted sorts in this theory
64 ExprSet d_declarations
; // all the variable/function declarations
65 theory::TheoryId
getTheoryId() override
;
68 UFProof(theory::uf::TheoryUF
* uf
, TheoryProofEngine
* proofEngine
);
70 void registerTerm(Expr term
) override
;
73 class LFSCUFProof
: public UFProof
{
75 LFSCUFProof(theory::uf::TheoryUF
* uf
, TheoryProofEngine
* proofEngine
)
76 : UFProof(uf
, proofEngine
)
78 void printOwnedTerm(Expr term
,
80 const ProofLetMap
& map
) override
;
81 void printOwnedSort(Type type
, std::ostream
& os
) override
;
82 void printTheoryLemmaProof(std::vector
<Expr
>& lemma
,
85 const ProofLetMap
& map
) override
;
86 void printSortDeclarations(std::ostream
& os
, std::ostream
& paren
) override
;
87 void printTermDeclarations(std::ostream
& os
, std::ostream
& paren
) override
;
88 void printDeferredDeclarations(std::ostream
& os
,
89 std::ostream
& paren
) override
;
90 void printAliasingDeclarations(std::ostream
& os
,
92 const ProofLetMap
& globalLetMap
) override
;
94 bool printsAsBool(const Node
& n
) override
;
96 void printConstantDisequalityProof(std::ostream
& os
,
99 const ProofLetMap
& globalLetMap
) override
;
103 }/* CVC4 namespace */
105 #endif /* __CVC4__UF__PROOF_H */