src/theory/engine_output_channel.h

   1 /*********************                                                        */
   2 /*! \file engine_output_channel.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Tim King, Dejan Jovanovic
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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  ** \brief The theory engine output channel.
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__ENGINE_OUTPUT_CHANNEL_H
  18 #define CVC4__THEORY__ENGINE_OUTPUT_CHANNEL_H
  19
  20 #include "expr/node.h"
  21 #include "theory/output_channel.h"
  22 #include "theory/theory.h"
  23 #include "util/statistics_registry.h"
  24
  25 namespace CVC4 {
  26
  27 class TheoryEngine;
  28
  29 namespace theory {
  30
  31 /**
  32  * An output channel for Theory that passes messages back to a TheoryEngine
  33  * for a given Theory.
  34  *
  35  * Notice that it has interfaces trustedConflict and trustedLemma which are
  36  * used for ensuring that proof generators are associated with the lemmas
  37  * and conflicts sent on this output channel.
  38  */
  39 class EngineOutputChannel : public theory::OutputChannel
  40 {
  41   friend class TheoryEngine;
  42
  43  public:
  44   EngineOutputChannel(TheoryEngine* engine, theory::TheoryId theory);
  45
  46   void safePoint(ResourceManager::Resource r) override;
  47
  48   void conflict(TNode conflictNode,
  49                 std::unique_ptr<Proof> pf = nullptr) override;
  50   bool propagate(TNode literal) override;
  51
  52   theory::LemmaStatus lemma(TNode lemma,
  53                             ProofRule rule,
  54                             bool removable = false,
  55                             bool preprocess = false,
  56                             bool sendAtoms = false) override;
  57
  58   theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) override;
  59
  60   void demandRestart() override;
  61
  62   void requirePhase(TNode n, bool phase) override;
  63
  64   void setIncomplete() override;
  65
  66   void spendResource(ResourceManager::Resource r) override;
  67
  68   void handleUserAttribute(const char* attr, theory::Theory* t) override;
  69
  70  protected:
  71   /**
  72    * Statistics for a particular theory.
  73    */
  74   class Statistics
  75   {
  76    public:
  77     Statistics(theory::TheoryId theory);
  78     ~Statistics();
  79     /** Number of calls to conflict, propagate, lemma, requirePhase,
  80      * restartDemands */
  81     IntStat conflicts, propagations, lemmas, requirePhase, restartDemands,
  82         trustedConflicts, trustedLemmas;
  83   };
  84   /** The theory engine we're communicating with. */
  85   TheoryEngine* d_engine;
  86   /** The statistics of the theory interractions. */
  87   Statistics d_statistics;
  88   /** The theory owning this channel. */
  89   theory::TheoryId d_theory;
  90   /** A helper function for registering lemma recipes with the proof engine */
  91   void registerLemmaRecipe(Node lemma,
  92                            Node originalLemma,
  93                            bool preprocess,
  94                            theory::TheoryId theoryId);
  95 };
  96
  97 }  // namespace theory
  98 }  // namespace CVC4
  99
 100 #endif /* CVC4__THEORY__ENGINE_OUTPUT_CHANNEL_H */