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, Haniel Barbosa
   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) override;
  49   bool propagate(TNode literal) override;
  50
  51   theory::LemmaStatus lemma(TNode lemma,
  52                             LemmaProperty p = LemmaProperty::NONE) override;
  53
  54   theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) override;
  55
  56   void demandRestart() override;
  57
  58   void requirePhase(TNode n, bool phase) override;
  59
  60   void setIncomplete() override;
  61
  62   void spendResource(ResourceManager::Resource r) override;
  63
  64   void handleUserAttribute(const char* attr, theory::Theory* t) override;
  65
  66   /**
  67    * Let pconf be the pair (Node conf, ProofGenerator * pfg). This method
  68    * sends conf on the output channel of this class whose proof can be generated
  69    * by the generator pfg. Apart from pfg, the interface for this method is
  70    * the same as calling OutputChannel::lemma on conf.
  71    */
  72   void trustedConflict(TrustNode pconf) override;
  73   /**
  74    * Let plem be the pair (Node lem, ProofGenerator * pfg).
  75    * Send lem on the output channel of this class whose proof can be generated
  76    * by the generator pfg. Apart from pfg, the interface for this method is
  77    * the same as calling OutputChannel::lemma on lem.
  78    */
  79   LemmaStatus trustedLemma(TrustNode plem,
  80                            LemmaProperty p = LemmaProperty::NONE) override;
  81
  82  protected:
  83   /**
  84    * Statistics for a particular theory.
  85    */
  86   class Statistics
  87   {
  88    public:
  89     Statistics(theory::TheoryId theory);
  90     ~Statistics();
  91     /** Number of calls to conflict, propagate, lemma, requirePhase,
  92      * restartDemands */
  93     IntStat conflicts, propagations, lemmas, requirePhase, restartDemands,
  94         trustedConflicts, trustedLemmas;
  95   };
  96   /** The theory engine we're communicating with. */
  97   TheoryEngine* d_engine;
  98   /** The statistics of the theory interractions. */
  99   Statistics d_statistics;
 100   /** The theory owning this channel. */
 101   theory::TheoryId d_theory;
 102   /** A helper function for registering lemma recipes with the proof engine */
 103   void registerLemmaRecipe(Node lemma,
 104                            Node originalLemma,
 105                            bool preprocess,
 106                            theory::TheoryId theoryId);
 107 };
 108
 109 }  // namespace theory
 110 }  // namespace CVC4
 111
 112 #endif /* CVC4__THEORY__ENGINE_OUTPUT_CHANNEL_H */