diff options
Diffstat (limited to 'src/proof/proof_output_channel.h')
-rw-r--r-- | src/proof/proof_output_channel.h | 50 |
1 files changed, 0 insertions, 50 deletions
diff --git a/src/proof/proof_output_channel.h b/src/proof/proof_output_channel.h deleted file mode 100644 index b85af5fb5..000000000 --- a/src/proof/proof_output_channel.h +++ /dev/null @@ -1,50 +0,0 @@ -/********************* */ -/*! \file proof_output_channel.h - ** \verbatim - ** - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__PROOF_OUTPUT_CHANNEL_H -#define __CVC4__PROOF_OUTPUT_CHANNEL_H - -#include "theory/output_channel.h" - -namespace CVC4 { - -class ProofOutputChannel : public theory::OutputChannel { -public: - Node d_conflict; - Proof* d_proof; - Node d_lemma; - std::set<Node> d_propagations; - - ProofOutputChannel(); - - virtual ~ProofOutputChannel() throw() {} - - void conflict(TNode n, Proof* pf) throw(); - bool propagate(TNode x) throw(); - theory::LemmaStatus lemma(TNode n, ProofRule rule, bool, bool, bool) throw(); - theory::LemmaStatus splitLemma(TNode, bool) throw(); - void requirePhase(TNode n, bool b) throw(); - bool flipDecision() throw(); - void setIncomplete() throw(); -};/* class ProofOutputChannel */ - -class MyPreRegisterVisitor { - theory::Theory* d_theory; - __gnu_cxx::hash_set<TNode, TNodeHashFunction> d_visited; -public: - typedef void return_type; - MyPreRegisterVisitor(theory::Theory* theory); - bool alreadyVisited(TNode current, TNode parent); - void visit(TNode current, TNode parent); - void start(TNode node); - void done(TNode node); -}; /* class MyPreRegisterVisitor */ - -} /* CVC4 namespace */ - -#endif /* __CVC4__PROOF_OUTPUT_CHANNEL_H */ |