src/theory/inference_manager_buffered.cpp

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