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
21 #include <unordered_set>
23 #include "expr/node.h"
24 #include "theory/output_channel.h"
25 #include "theory/theory.h"
26 #include "util/proof.h"
30 class ProofOutputChannel
: public theory::OutputChannel
{
33 ~ProofOutputChannel() override
{}
36 * This may be called at most once per ProofOutputChannel.
37 * Requires that `n` and `pf` are non-null.
39 void conflict(TNode n
, std::unique_ptr
<Proof
> pf
) override
;
40 bool propagate(TNode x
) override
;
41 theory::LemmaStatus
lemma(TNode n
, ProofRule rule
, bool, bool, bool) override
;
42 theory::LemmaStatus
splitLemma(TNode
, bool) override
;
43 void requirePhase(TNode n
, bool b
) override
;
44 bool flipDecision() override
;
45 void setIncomplete() override
;
47 /** Has conflict() has been called? */
48 bool hasConflict() const { return !d_conflict
.isNull(); }
51 * Returns the proof passed into the conflict() call.
52 * Requires hasConflict() to hold.
54 const Proof
& getConflictProof() const;
55 Node
getLastLemma() const { return d_lemma
; }
59 std::unique_ptr
<Proof
> d_proof
;
61 std::set
<Node
> d_propagations
;
62 }; /* class ProofOutputChannel */
64 class MyPreRegisterVisitor
{
65 theory::Theory
* d_theory
;
66 std::unordered_set
<TNode
, TNodeHashFunction
> d_visited
;
68 typedef void return_type
;
69 MyPreRegisterVisitor(theory::Theory
* theory
);
70 bool alreadyVisited(TNode current
, TNode parent
);
71 void visit(TNode current
, TNode parent
);
72 void start(TNode node
);
73 void done(TNode node
);
74 }; /* class MyPreRegisterVisitor */
76 } /* CVC4 namespace */
78 #endif /* __CVC4__PROOF_OUTPUT_CHANNEL_H */