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                                                    const std::string& name,
  29                                                    bool cacheLemmas)
  30     : TheoryInferenceManager(t, state, pnm, name, cacheLemmas),
  31       d_processingPendingLemmas(false)
  32 {
  33 }
  34
  35 bool InferenceManagerBuffered::hasPending() const
  36 {
  37   return hasPendingFact() || hasPendingLemma();
  38 }
  39
  40 bool InferenceManagerBuffered::hasPendingFact() const
  41 {
  42   return !d_pendingFact.empty();
  43 }
  44
  45 bool InferenceManagerBuffered::hasPendingLemma() const
  46 {
  47   return !d_pendingLem.empty();
  48 }
  49
  50 bool InferenceManagerBuffered::addPendingLemma(Node lem,
  51                                                InferenceId id,
  52                                                LemmaProperty p,
  53                                                ProofGenerator* pg,
  54                                                bool checkCache)
  55 {
  56   if (checkCache)
  57   {
  58     // check if it is unique up to rewriting
  59     Node lemr = Rewriter::rewrite(lem);
  60     if (hasCachedLemma(lemr, p))
  61     {
  62       return false;
  63     }
  64   }
  65   // make the simple theory lemma
  66   d_pendingLem.emplace_back(new SimpleTheoryLemma(id, lem, p, pg));
  67   return true;
  68 }
  69
  70 void InferenceManagerBuffered::addPendingLemma(
  71     std::unique_ptr<TheoryInference> lemma)
  72 {
  73   d_pendingLem.emplace_back(std::move(lemma));
  74 }
  75
  76 void InferenceManagerBuffered::addPendingFact(Node conc,
  77                                               InferenceId id,
  78                                               Node exp,
  79                                               ProofGenerator* pg)
  80 {
  81   // make a simple theory internal fact
  82   Assert(conc.getKind() != AND && conc.getKind() != OR);
  83   d_pendingFact.emplace_back(new SimpleTheoryInternalFact(id, conc, exp, pg));
  84 }
  85
  86 void InferenceManagerBuffered::addPendingFact(
  87     std::unique_ptr<TheoryInference> fact)
  88 {
  89   d_pendingFact.emplace_back(std::move(fact));
  90 }
  91
  92 void InferenceManagerBuffered::addPendingPhaseRequirement(Node lit, bool pol)
  93 {
  94   // it is the responsibility of the caller to ensure lit is rewritten
  95   d_pendingReqPhase[lit] = pol;
  96 }
  97
  98 void InferenceManagerBuffered::doPendingFacts()
  99 {
 100   size_t i = 0;
 101   while (!d_theoryState.isInConflict() && i < d_pendingFact.size())
 102   {
 103     // assert the internal fact, which notice may enqueue more pending facts in
 104     // this loop, or result in a conflict.
 105     assertInternalFactTheoryInference(d_pendingFact[i].get());
 106     i++;
 107   }
 108   d_pendingFact.clear();
 109 }
 110
 111 void InferenceManagerBuffered::doPendingLemmas()
 112 {
 113   if (d_processingPendingLemmas)
 114   {
 115     // already processing
 116     return;
 117   }
 118   d_processingPendingLemmas = true;
 119   size_t i = 0;
 120   while (i < d_pendingLem.size())
 121   {
 122     // process this lemma, which notice may enqueue more pending lemmas in this
 123     // loop, or clear the lemmas.
 124     lemmaTheoryInference(d_pendingLem[i].get());
 125     i++;
 126   }
 127   d_pendingLem.clear();
 128   d_processingPendingLemmas = false;
 129 }
 130
 131 void InferenceManagerBuffered::doPendingPhaseRequirements()
 132 {
 133   // process the pending require phase calls
 134   for (const std::pair<const Node, bool>& prp : d_pendingReqPhase)
 135   {
 136     requirePhase(prp.first, prp.second);
 137   }
 138   d_pendingReqPhase.clear();
 139 }
 140 void InferenceManagerBuffered::clearPending()
 141 {
 142   d_pendingFact.clear();
 143   d_pendingLem.clear();
 144   d_pendingReqPhase.clear();
 145 }
 146 void InferenceManagerBuffered::clearPendingFacts() { d_pendingFact.clear(); }
 147 void InferenceManagerBuffered::clearPendingLemmas() { d_pendingLem.clear(); }
 148 void InferenceManagerBuffered::clearPendingPhaseRequirements()
 149 {
 150   d_pendingReqPhase.clear();
 151 }
 152
 153 std::size_t InferenceManagerBuffered::numPendingLemmas() const
 154 {
 155   return d_pendingLem.size();
 156 }
 157 std::size_t InferenceManagerBuffered::numPendingFacts() const
 158 {
 159   return d_pendingFact.size();
 160 }
 161
 162 void InferenceManagerBuffered::lemmaTheoryInference(TheoryInference* lem)
 163 {
 164   // process this lemma
 165   LemmaProperty p = LemmaProperty::NONE;
 166   TrustNode tlem = lem->processLemma(p);
 167   Assert(!tlem.isNull());
 168   // send the lemma
 169   trustedLemma(tlem, lem->getId(), p);
 170 }
 171
 172 void InferenceManagerBuffered::assertInternalFactTheoryInference(
 173     TheoryInference* fact)
 174 {
 175   // process this fact
 176   std::vector<Node> exp;
 177   ProofGenerator* pg = nullptr;
 178   Node lit = fact->processFact(exp, pg);
 179   Assert(!lit.isNull());
 180   bool pol = lit.getKind() != NOT;
 181   TNode atom = pol ? lit : lit[0];
 182   // no double negation or conjunctive conclusions
 183   Assert(atom.getKind() != NOT && atom.getKind() != AND);
 184   // assert the internal fact
 185   assertInternalFact(atom, pol, fact->getId(), exp, pg);
 186 }
 187
 188 }  // namespace theory
 189 }  // namespace CVC4