src/theory/inference_manager_buffered.cpp

   1 /*********************                                                        */
   2 /*! \file inference_manager_buffered.cpp
   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 "theory/inference_manager_buffered.h"
  16
  17 #include "theory/rewriter.h"
  18 #include "theory/theory.h"
  19
  20 using namespace CVC4::kind;
  21
  22 namespace CVC4 {
  23 namespace theory {
  24
  25 InferenceManagerBuffered::InferenceManagerBuffered(Theory& t,
  26                                                    TheoryState& state,
  27                                                    ProofNodeManager* pnm)
  28     : TheoryInferenceManager(t, state, pnm), d_processingPendingLemmas(false)
  29 {
  30 }
  31
  32 bool InferenceManagerBuffered::hasPending() const
  33 {
  34   return hasPendingFact() || hasPendingLemma();
  35 }
  36
  37 bool InferenceManagerBuffered::hasPendingFact() const
  38 {
  39   return !d_pendingFact.empty();
  40 }
  41
  42 bool InferenceManagerBuffered::hasPendingLemma() const
  43 {
  44   return !d_pendingLem.empty();
  45 }
  46
  47 void InferenceManagerBuffered::addPendingLemma(Node lem,
  48                                                LemmaProperty p,
  49                                                ProofGenerator* pg)
  50 {
  51   // make the simple theory lemma
  52   d_pendingLem.emplace_back(new SimpleTheoryLemma(lem, p, pg));
  53 }
  54
  55 void InferenceManagerBuffered::addPendingLemma(
  56     std::unique_ptr<TheoryInference> lemma)
  57 {
  58   d_pendingLem.emplace_back(std::move(lemma));
  59 }
  60
  61 void InferenceManagerBuffered::addPendingFact(Node conc,
  62                                               Node exp,
  63                                               ProofGenerator* pg)
  64 {
  65   // make a simple theory internal fact
  66   Assert(conc.getKind() != AND && conc.getKind() != OR);
  67   d_pendingFact.emplace_back(new SimpleTheoryInternalFact(conc, exp, pg));
  68 }
  69
  70 void InferenceManagerBuffered::addPendingFact(
  71     std::unique_ptr<TheoryInference> fact)
  72 {
  73   d_pendingFact.emplace_back(std::move(fact));
  74 }
  75
  76 void InferenceManagerBuffered::addPendingPhaseRequirement(Node lit, bool pol)
  77 {
  78   // it is the responsibility of the caller to ensure lit is rewritten
  79   d_pendingReqPhase[lit] = pol;
  80 }
  81
  82 void InferenceManagerBuffered::doPendingFacts()
  83 {
  84   size_t i = 0;
  85   while (!d_theoryState.isInConflict() && i < d_pendingFact.size())
  86   {
  87     // process this fact, which notice may enqueue more pending facts in this
  88     // loop.
  89     d_pendingFact[i]->process(this, false);
  90     i++;
  91   }
  92   d_pendingFact.clear();
  93 }
  94
  95 void InferenceManagerBuffered::doPendingLemmas()
  96 {
  97   if (d_processingPendingLemmas)
  98   {
  99     // already processing
 100     return;
 101   }
 102   d_processingPendingLemmas = true;
 103   size_t i = 0;
 104   while (i < d_pendingLem.size())
 105   {
 106     // process this lemma, which notice may enqueue more pending lemmas in this
 107     // loop, or clear the lemmas.
 108     d_pendingLem[i]->process(this, true);
 109     i++;
 110   }
 111   d_pendingLem.clear();
 112   d_processingPendingLemmas = false;
 113 }
 114
 115 void InferenceManagerBuffered::doPendingPhaseRequirements()
 116 {
 117   // process the pending require phase calls
 118   for (const std::pair<const Node, bool>& prp : d_pendingReqPhase)
 119   {
 120     requirePhase(prp.first, prp.second);
 121   }
 122   d_pendingReqPhase.clear();
 123 }
 124 void InferenceManagerBuffered::clearPending()
 125 {
 126   d_pendingFact.clear();
 127   d_pendingLem.clear();
 128   d_pendingReqPhase.clear();
 129 }
 130 void InferenceManagerBuffered::clearPendingFacts() { d_pendingFact.clear(); }
 131 void InferenceManagerBuffered::clearPendingLemmas() { d_pendingLem.clear(); }
 132 void InferenceManagerBuffered::clearPendingPhaseRequirements()
 133 {
 134   d_pendingReqPhase.clear();
 135 }
 136
 137
 138   std::size_t InferenceManagerBuffered::numPendingLemmas() const {
 139     return d_pendingLem.size();
 140   }
 141   std::size_t InferenceManagerBuffered::numPendingFacts() const {
 142     return d_pendingFact.size();
 143   }
 144
 145 }  // namespace theory
 146 }  // namespace CVC4