src/theory/inference_manager_buffered.h

   1 /*********************                                                        */
   2 /*! \file inference_manager_buffered.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   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 A buffered inference manager
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__INFERENCE_MANAGER_BUFFERED_H
  18 #define CVC4__THEORY__INFERENCE_MANAGER_BUFFERED_H
  19
  20 #include "context/cdhashmap.h"
  21 #include "expr/node.h"
  22 #include "theory/theory_inference_manager.h"
  23
  24 namespace CVC4 {
  25 namespace theory {
  26
  27 /**
  28  * A lemma base class. This class is an abstract data structure for storing
  29  * pending lemmas in the inference manager below.
  30  */
  31 class Lemma
  32 {
  33  public:
  34   Lemma(Node n, LemmaProperty p, ProofGenerator* pg)
  35       : d_node(n), d_property(p), d_pg(pg)
  36   {
  37   }
  38   virtual ~Lemma() {}
  39   /**
  40    * Called just before this lemma is sent on the output channel. The purpose
  41    * of this callback is to do any specific process of the lemma, e.g. take
  42    * debug statistics, cache, etc.
  43    *
  44    * @return true if the lemma should be sent on the output channel.
  45    */
  46   virtual bool notifySend() { return true; }
  47   /** The lemma to send */
  48   Node d_node;
  49   /** The lemma property (see OutputChannel::lemma) */
  50   LemmaProperty d_property;
  51   /**
  52    * The proof generator for this lemma, which if non-null, is wrapped in a
  53    * TrustNode to be set on the output channel via trustedLemma at the time
  54    * the lemma is sent. This proof generator must be able to provide a proof
  55    * for d_node in the remainder of the user context.
  56    */
  57   ProofGenerator* d_pg;
  58 };
  59
  60 /**
  61  * The buffered inference manager.  This class implements standard methods
  62  * for buffering facts, lemmas and phase requirements.
  63  */
  64 class InferenceManagerBuffered : public TheoryInferenceManager
  65 {
  66  public:
  67   InferenceManagerBuffered(Theory& t,
  68                            TheoryState& state,
  69                            ProofNodeManager* pnm);
  70   ~InferenceManagerBuffered() {}
  71   /**
  72    * Have we processed an inference during this call to check? In particular,
  73    * this returns true if we have a pending fact or lemma, or have encountered
  74    * a conflict.
  75    */
  76   bool hasProcessed() const;
  77   /**
  78    * Do we have a pending fact to add as an internal fact to the equality
  79    * engine?
  80    */
  81   bool hasPendingFact() const;
  82   /** Do we have a pending lemma to send on the output channel? */
  83   bool hasPendingLemma() const;
  84   /**
  85    * Add pending lemma lem with property p, with proof generator pg. If
  86    * non-null, pg must be able to provide a proof for lem for the remainder
  87    * of the user context. Pending lemmas are sent to the output channel using
  88    * doPendingLemmas.
  89    */
  90   void addPendingLemma(Node lem,
  91                        LemmaProperty p = LemmaProperty::NONE,
  92                        ProofGenerator* pg = nullptr);
  93   /**
  94    * Add pending lemma, where lemma can be a (derived) class of the
  95    * above one. Pending lemmas are sent to the output channel using
  96    * doPendingLemmas.
  97    */
  98   void addPendingLemma(std::shared_ptr<Lemma> lemma);
  99   /**
 100    * Add pending fact, which adds a fact on the pending fact queue. It must
 101    * be the case that:
 102    * (1) exp => fact is valid,
 103    * (2) exp is a literal (or conjunction of literals) that holds in the
 104    * equality engine of the theory.
 105    *
 106    * Pending facts are sent to the equality engine of this class using
 107    * doPendingFacts.
 108    */
 109   void addPendingFact(Node fact, Node exp);
 110   /** Add pending phase requirement
 111    *
 112    * This method is called to indicate this class should send a phase
 113    * requirement request to the output channel for literal lit to be
 114    * decided with polarity pol. The literal lit should be a SAT literal
 115    * by the time that doPendingPhaseRequirements is called. Typically,
 116    * lit is a literal that is a subformula of a pending lemma that is processed
 117    * prior to sending the phase requirement.
 118    */
 119   void addPendingPhaseRequirement(Node lit, bool pol);
 120   /** Do pending facts
 121    *
 122    * This method asserts pending facts (d_pendingFact) with explanations
 123    * to the equality engine of the theory via calls
 124    * to assertInternalFact.
 125    *
 126    * It terminates early if a conflict is encountered, for instance, by
 127    * equality reasoning within the equality engine.
 128    *
 129    * Regardless of whether a conflict is encountered, the vector d_pendingFact
 130    * is cleared after this call.
 131    */
 132   void doPendingFacts();
 133   /** Do pending lemmas
 134    *
 135    * This method send all pending lemmas (d_pendingLem) on the output
 136    * channel of the theory.
 137    *
 138    * Unlike doPendingFacts, this function will not terminate early if a conflict
 139    * has already been encountered by the theory. The vector d_pendingLem is
 140    * cleared after this call.
 141    */
 142   void doPendingLemmas();
 143   /**
 144    * Do pending phase requirements. Calls the output channel for all pending
 145    * phase requirements and clears d_pendingReqPhase.
 146    */
 147   void doPendingPhaseRequirements();
 148
 149  protected:
 150   /** A set of pending lemmas */
 151   std::vector<std::shared_ptr<Lemma>> d_pendingLem;
 152   /** A set of pending facts, paired with their explanations */
 153   std::vector<std::pair<Node, Node>> d_pendingFact;
 154   /** A map from literals to their pending phase requirement */
 155   std::map<Node, bool> d_pendingReqPhase;
 156 };
 157
 158 }  // namespace theory
 159 }  // namespace CVC4
 160
 161 #endif