b36909f785dc93d9d123c76269fc48ffe34a8bfe
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
) override
;
38 static void toStreamLFSC(std::ostream
& out
, TheoryProof
* tp
,
39 const theory::eq::EqProof
& pf
,
40 const ProofLetMap
& map
);
41 static Node
toStreamRecLFSC(std::ostream
& out
, TheoryProof
* tp
,
42 const theory::eq::EqProof
& pf
,
43 unsigned tb
, const ProofLetMap
& map
);
44 // it is simply an equality engine proof
45 std::shared_ptr
<theory::eq::EqProof
> d_proof
;
54 typedef std::unordered_set
<Type
, TypeHashFunction
> TypeSet
;
57 class ArithProof
: public TheoryProof
{
59 // std::map<Expr, std::string> d_constRationalString; // all the variable/function declarations
61 // TypeSet d_sorts; // all the uninterpreted sorts in this theory
62 ExprSet d_declarations
; // all the variable/function declarations
67 ArithProof(theory::arith::TheoryArith
* arith
, TheoryProofEngine
* proofEngine
);
69 virtual void registerTerm(Expr term
);
72 class LFSCArithProof
: public ArithProof
{
74 LFSCArithProof(theory::arith::TheoryArith
* arith
, TheoryProofEngine
* proofEngine
)
75 : ArithProof(arith
, proofEngine
)
77 virtual void printOwnedTerm(Expr term
, std::ostream
& os
, const ProofLetMap
& map
);
78 virtual void printOwnedSort(Type type
, std::ostream
& os
);
79 virtual void printTheoryLemmaProof(std::vector
<Expr
>& lemma
, std::ostream
& os
, std::ostream
& paren
, const ProofLetMap
& map
);
80 virtual void printSortDeclarations(std::ostream
& os
, std::ostream
& paren
);
81 virtual void printTermDeclarations(std::ostream
& os
, std::ostream
& paren
);
82 virtual void printDeferredDeclarations(std::ostream
& os
, std::ostream
& paren
);
83 virtual void printAliasingDeclarations(std::ostream
& os
, std::ostream
& paren
, const ProofLetMap
&globalLetMap
);
89 #endif /* __CVC4__ARITH__PROOF_H */