1 /********************* */
2 /*! \file arith_proof.h
4 ** Top contributors (to current version):
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
17 #include "cvc4_private.h"
19 #ifndef __CVC4__ARITH__PROOF_H
20 #define __CVC4__ARITH__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/uf/equality_engine.h"
32 //proof object outputted by TheoryArith
33 class ProofArith
: public Proof
{
35 ProofArith(std::shared_ptr
<theory::eq::EqProof
> pf
) : d_proof(pf
) {}
36 void toStream(std::ostream
& out
) const override
;
39 static void toStreamLFSC(std::ostream
& out
, TheoryProof
* tp
,
40 const theory::eq::EqProof
& pf
,
41 const ProofLetMap
& map
);
42 static Node
toStreamRecLFSC(std::ostream
& out
, TheoryProof
* tp
,
43 const theory::eq::EqProof
& pf
,
44 unsigned tb
, const ProofLetMap
& map
);
45 // it is simply an equality engine proof
46 std::shared_ptr
<theory::eq::EqProof
> d_proof
;
55 typedef std::unordered_set
<Type
, TypeHashFunction
> TypeSet
;
58 class ArithProof
: public TheoryProof
{
60 // std::map<Expr, std::string> d_constRationalString; // all the variable/function declarations
62 // TypeSet d_sorts; // all the uninterpreted sorts in this theory
63 ExprSet d_declarations
; // all the variable/function declarations
68 ArithProof(theory::arith::TheoryArith
* arith
, TheoryProofEngine
* proofEngine
);
70 void registerTerm(Expr term
) override
;
73 class LFSCArithProof
: public ArithProof
{
75 LFSCArithProof(theory::arith::TheoryArith
* arith
, TheoryProofEngine
* proofEngine
)
76 : ArithProof(arith
, 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
;
98 #endif /* __CVC4__ARITH__PROOF_H */