src/theory/inference_manager_buffered.cpp

   1 /*********************                                                        */
   2 /*! \file inference_manager_buffered.cpp
   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 "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)
  29 {
  30 }
  31
  32 bool InferenceManagerBuffered::hasProcessed() const
  33 {
  34   return d_theoryState.isInConflict() || !d_pendingLem.empty()
  35          || !d_pendingFact.empty();
  36 }
  37
  38 bool InferenceManagerBuffered::hasPendingFact() const
  39 {
  40   return !d_pendingFact.empty();
  41 }
  42
  43 bool InferenceManagerBuffered::hasPendingLemma() const
  44 {
  45   return !d_pendingLem.empty();
  46 }
  47
  48 void InferenceManagerBuffered::addPendingLemma(Node lem,
  49                                                LemmaProperty p,
  50                                                ProofGenerator* pg)
  51 {
  52   // make the simple theory lemma
  53   d_pendingLem.push_back(std::make_shared<SimpleTheoryLemma>(lem, p, pg));
  54 }
  55
  56 void InferenceManagerBuffered::addPendingLemma(
  57     std::shared_ptr<TheoryInference> lemma)
  58 {
  59   d_pendingLem.emplace_back(std::move(lemma));
  60 }
  61
  62 void InferenceManagerBuffered::addPendingFact(Node conc,
  63                                               Node exp,
  64                                               ProofGenerator* pg)
  65 {
  66   // make a simple theory internal fact
  67   Assert(conc.getKind() != AND && conc.getKind() != OR);
  68   d_pendingFact.push_back(
  69       std::make_shared<SimpleTheoryInternalFact>(conc, exp, pg));
  70 }
  71
  72 void InferenceManagerBuffered::addPendingFact(
  73     std::shared_ptr<TheoryInference> fact)
  74 {
  75   d_pendingFact.emplace_back(std::move(fact));
  76 }
  77
  78 void InferenceManagerBuffered::addPendingPhaseRequirement(Node lit, bool pol)
  79 {
  80   // must ensure rewritten
  81   lit = Rewriter::rewrite(lit);
  82   d_pendingReqPhase[lit] = pol;
  83 }
  84
  85 void InferenceManagerBuffered::doPendingFacts()
  86 {
  87   size_t i = 0;
  88   while (!d_theoryState.isInConflict() && i < d_pendingFact.size())
  89   {
  90     // process this fact, which notice may enqueue more pending facts in this
  91     // loop.
  92     d_pendingFact[i]->process(this);
  93     i++;
  94   }
  95   d_pendingFact.clear();
  96 }
  97
  98 void InferenceManagerBuffered::doPendingLemmas()
  99 {
 100   for (const std::shared_ptr<TheoryInference>& plem : d_pendingLem)
 101   {
 102     // process this lemma
 103     plem->process(this);
 104   }
 105   d_pendingLem.clear();
 106 }
 107
 108 void InferenceManagerBuffered::doPendingPhaseRequirements()
 109 {
 110   // process the pending require phase calls
 111   for (const std::pair<const Node, bool>& prp : d_pendingReqPhase)
 112   {
 113     d_out.requirePhase(prp.first, prp.second);
 114   }
 115   d_pendingReqPhase.clear();
 116 }
 117 void InferenceManagerBuffered::clearPendingFacts() { d_pendingFact.clear(); }
 118 void InferenceManagerBuffered::clearPendingLemmas() { d_pendingLem.clear(); }
 119 void InferenceManagerBuffered::clearPendingPhaseRequirements()
 120 {
 121   d_pendingReqPhase.clear();
 122 }
 123
 124 }  // namespace theory
 125 }  // namespace CVC4