src/theory/inference_manager_buffered.h

   1 /*********************                                                        */
   2 /*! \file inference_manager_buffered.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Gereon Kremer
   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.h"
  23 #include "theory/theory_inference_manager.h"
  24
  25 namespace CVC4 {
  26 namespace theory {
  27
  28 /**
  29  * The buffered inference manager.  This class implements standard methods
  30  * for buffering facts, lemmas and phase requirements.
  31  */
  32 class InferenceManagerBuffered : public TheoryInferenceManager
  33 {
  34  public:
  35   InferenceManagerBuffered(Theory& t,
  36                            TheoryState& state,
  37                            ProofNodeManager* pnm);
  38   virtual ~InferenceManagerBuffered() {}
  39   /**
  40    * Do we have a pending fact or lemma?
  41    */
  42   bool hasPending() const;
  43   /**
  44    * Do we have a pending fact to add as an internal fact to the equality
  45    * engine?
  46    */
  47   bool hasPendingFact() const;
  48   /** Do we have a pending lemma to send on the output channel? */
  49   bool hasPendingLemma() const;
  50   /**
  51    * Add pending lemma lem with property p, with proof generator pg. If
  52    * non-null, pg must be able to provide a proof for lem for the remainder
  53    * of the user context. Pending lemmas are sent to the output channel using
  54    * doPendingLemmas.
  55    */
  56   void addPendingLemma(Node lem,
  57                        LemmaProperty p = LemmaProperty::NONE,
  58                        ProofGenerator* pg = nullptr);
  59   /**
  60    * Add pending lemma, where lemma can be a (derived) class of the
  61    * theory inference base class.
  62    */
  63   void addPendingLemma(std::unique_ptr<TheoryInference> lemma);
  64   /**
  65    * Add pending fact, which adds a fact on the pending fact queue. It must
  66    * be the case that:
  67    * (1) exp => conc is valid,
  68    * (2) exp is a literal (or conjunction of literals) that holds in the
  69    * equality engine of the theory.
  70    *
  71    * Pending facts are sent to the equality engine of this class using
  72    * doPendingFacts.
  73    */
  74   void addPendingFact(Node conc, Node exp, ProofGenerator* pg = nullptr);
  75   /**
  76    * Add pending fact, where fact can be a (derived) class of the
  77    * theory inference base class.
  78    */
  79   void addPendingFact(std::unique_ptr<TheoryInference> fact);
  80   /** Add pending phase requirement
  81    *
  82    * This method is called to indicate this class should send a phase
  83    * requirement request to the output channel for literal lit to be
  84    * decided with polarity pol. The literal lit should be a SAT literal
  85    * by the time that doPendingPhaseRequirements is called. Typically,
  86    * lit is a literal that is a subformula of a pending lemma that is processed
  87    * prior to sending the phase requirement.
  88    */
  89   void addPendingPhaseRequirement(Node lit, bool pol);
  90   /** Do pending facts
  91    *
  92    * This method asserts pending facts (d_pendingFact) with explanations
  93    * to the equality engine of the theory via calls
  94    * to assertInternalFact.
  95    *
  96    * It terminates early if a conflict is encountered, for instance, by
  97    * equality reasoning within the equality engine.
  98    *
  99    * Regardless of whether a conflict is encountered, the vector d_pendingFact
 100    * is cleared after this call.
 101    */
 102   void doPendingFacts();
 103   /** Do pending lemmas
 104    *
 105    * This method send all pending lemmas (d_pendingLem) on the output
 106    * channel of the theory.
 107    *
 108    * Unlike doPendingFacts, this function will not terminate early if a conflict
 109    * has already been encountered by the theory. The vector d_pendingLem is
 110    * cleared after this call.
 111    */
 112   void doPendingLemmas();
 113   /**
 114    * Do pending phase requirements. Calls the output channel for all pending
 115    * phase requirements and clears d_pendingReqPhase.
 116    */
 117   void doPendingPhaseRequirements();
 118   /** Clear pending facts, lemmas, and phase requirements without processing */
 119   void clearPending();
 120   /** Clear pending facts, without processing */
 121   void clearPendingFacts();
 122   /** Clear pending lemmas, without processing */
 123   void clearPendingLemmas();
 124   /** Clear pending phase requirements, without processing */
 125   void clearPendingPhaseRequirements();
 126
 127   /** Returns the number of pending lemmas. */
 128   std::size_t numPendingLemmas() const;
 129   /** Returns the number of pending facts. */
 130   std::size_t numPendingFacts() const;
 131
 132  protected:
 133   /** A set of pending inferences to be processed as lemmas */
 134   std::vector<std::unique_ptr<TheoryInference>> d_pendingLem;
 135   /** A set of pending inferences to be processed as facts */
 136   std::vector<std::unique_ptr<TheoryInference>> d_pendingFact;
 137   /** A map from literals to their pending phase requirement */
 138   std::map<Node, bool> d_pendingReqPhase;
 139   /**
 140    * Whether we are currently processing pending lemmas. This flag ensures
 141    * that we do not call pending lemmas recursively, which may lead to
 142    * segfaults.
 143    */
 144   bool d_processingPendingLemmas;
 145 };
 146
 147 }  // namespace theory
 148 }  // namespace CVC4
 149
 150 #endif