9516eb71b22bb2a099b54979ff7af602bdad65f8
1 /********************* */
2 /*! \file proof_output_channel.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
14 #include "cvc4_private.h"
16 #ifndef __CVC4__PROOF_OUTPUT_CHANNEL_H
17 #define __CVC4__PROOF_OUTPUT_CHANNEL_H
20 #include <unordered_set>
22 #include "expr/node.h"
23 #include "util/proof.h"
24 #include "theory/output_channel.h"
25 #include "theory/theory.h"
29 class ProofOutputChannel
: public theory::OutputChannel
{
32 ~ProofOutputChannel() override
{}
35 * This may be called at most once per ProofOutputChannel.
36 * Requires that `n` and `pf` are non-null.
38 void conflict(TNode n
, Proof
* pf
) override
;
39 bool propagate(TNode x
) override
;
40 theory::LemmaStatus
lemma(TNode n
, ProofRule rule
, bool, bool, bool) override
;
41 theory::LemmaStatus
splitLemma(TNode
, bool) override
;
42 void requirePhase(TNode n
, bool b
) override
;
43 bool flipDecision() override
;
44 void setIncomplete() override
;
46 /** Has conflict() has been called? */
47 bool hasConflict() const { return !d_conflict
.isNull(); }
50 * Returns the proof passed into the conflict() call.
51 * Requires hasConflict() to hold.
53 Proof
* getConflictProof();
54 Node
getLastLemma() const { return d_lemma
; }
60 std::set
<Node
> d_propagations
;
61 }; /* class ProofOutputChannel */
63 class MyPreRegisterVisitor
{
64 theory::Theory
* d_theory
;
65 std::unordered_set
<TNode
, TNodeHashFunction
> d_visited
;
67 typedef void return_type
;
68 MyPreRegisterVisitor(theory::Theory
* theory
);
69 bool alreadyVisited(TNode current
, TNode parent
);
70 void visit(TNode current
, TNode parent
);
71 void start(TNode node
);
72 void done(TNode node
);
73 }; /* class MyPreRegisterVisitor */
75 } /* CVC4 namespace */
77 #endif /* __CVC4__PROOF_OUTPUT_CHANNEL_H */