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   /**
  71    * Let pconf be the pair (Node conf, ProofGenerator * pfg). This method
  72    * sends conf on the output channel of this class whose proof can be generated
  73    * by the generator pfg. Apart from pfg, the interface for this method is
  74    * the same as calling OutputChannel::lemma on conf.
  75    */
  76   void trustedConflict(TrustNode pconf) override;
  77   /**
  78    * Let plem be the pair (Node lem, ProofGenerator * pfg).
  79    * Send lem on the output channel of this class whose proof can be generated
  80    * by the generator pfg. Apart from pfg, the interface for this method is
  81    * the same as calling OutputChannel::lemma on lem.
  82    */
  83   LemmaStatus trustedLemma(TrustNode plem,
  84                            bool removable = false,
  85                            bool preprocess = false,
  86                            bool sendAtoms = false) override;
  87
  88  protected:
  89   /**
  90    * Statistics for a particular theory.
  91    */
  92   class Statistics
  93   {
  94    public:
  95     Statistics(theory::TheoryId theory);
  96     ~Statistics();
  97     /** Number of calls to conflict, propagate, lemma, requirePhase,
  98      * restartDemands */
  99     IntStat conflicts, propagations, lemmas, requirePhase, restartDemands,
 100         trustedConflicts, trustedLemmas;
 101   };
 102   /** The theory engine we're communicating with. */
 103   TheoryEngine* d_engine;
 104   /** The statistics of the theory interractions. */
 105   Statistics d_statistics;
 106   /** The theory owning this channel. */
 107   theory::TheoryId d_theory;
 108   /** A helper function for registering lemma recipes with the proof engine */
 109   void registerLemmaRecipe(Node lemma,
 110                            Node originalLemma,
 111                            bool preprocess,
 112                            theory::TheoryId theoryId);
 113 };
 114
 115 }  // namespace theory
 116 }  // namespace CVC4
 117
 118 #endif /* CVC4__THEORY__ENGINE_OUTPUT_CHANNEL_H */