src/proof/proof_output_channel.h

   1 /*********************                                                        */
   2 /*! \file proof_output_channel.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Guy Katz, Tim King
   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
  11  **
  12  **/
  13
  14 #include "cvc4_private.h"
  15
  16 #ifndef __CVC4__PROOF_OUTPUT_CHANNEL_H
  17 #define __CVC4__PROOF_OUTPUT_CHANNEL_H
  18
  19 #include <set>
  20 #include <unordered_set>
  21
  22 #include "expr/node.h"
  23 #include "util/proof.h"
  24 #include "theory/output_channel.h"
  25 #include "theory/theory.h"
  26
  27 namespace CVC4 {
  28
  29 class ProofOutputChannel : public theory::OutputChannel {
  30  public:
  31   ProofOutputChannel();
  32   ~ProofOutputChannel() override {}
  33
  34   /**
  35    * This may be called at most once per ProofOutputChannel.
  36    * Requires that `n` and `pf` are non-null.
  37    */
  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;
  45
  46   /** Has conflict() has been called? */
  47   bool hasConflict() const { return !d_conflict.isNull(); }
  48
  49   /**
  50    * Returns the proof passed into the conflict() call.
  51    * Requires hasConflict() to hold.
  52    */
  53   Proof* getConflictProof();
  54   Node getLastLemma() const { return d_lemma; }
  55
  56  private:
  57   Node d_conflict;
  58   Proof* d_proof;
  59   Node d_lemma;
  60   std::set<Node> d_propagations;
  61 }; /* class ProofOutputChannel */
  62
  63 class MyPreRegisterVisitor {
  64   theory::Theory* d_theory;
  65   std::unordered_set<TNode, TNodeHashFunction> d_visited;
  66 public:
  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 */
  74
  75 } /* CVC4 namespace */
  76
  77 #endif /* __CVC4__PROOF_OUTPUT_CHANNEL_H */