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   d_pendingLem.push_back(std::make_shared<Lemma>(lem, p, pg));
  53 }
  54
  55 void InferenceManagerBuffered::addPendingLemma(std::shared_ptr<Lemma> lemma)
  56 {
  57   d_pendingLem.emplace_back(std::move(lemma));
  58 }
  59
  60 void InferenceManagerBuffered::addPendingFact(Node fact, Node exp)
  61 {
  62   Assert(fact.getKind() != AND && fact.getKind() != OR);
  63   d_pendingFact.push_back(std::pair<Node, Node>(fact, exp));
  64 }
  65
  66 void InferenceManagerBuffered::addPendingPhaseRequirement(Node lit, bool pol)
  67 {
  68   // must ensure rewritten
  69   lit = Rewriter::rewrite(lit);
  70   d_pendingReqPhase[lit] = pol;
  71 }
  72
  73 void InferenceManagerBuffered::doPendingFacts()
  74 {
  75   size_t i = 0;
  76   while (!d_theoryState.isInConflict() && i < d_pendingFact.size())
  77   {
  78     std::pair<Node, Node>& pfact = d_pendingFact[i];
  79     Node fact = pfact.first;
  80     Node exp = pfact.second;
  81     bool polarity = fact.getKind() != NOT;
  82     TNode atom = polarity ? fact : fact[0];
  83     // no double negation or conjunctive conclusions
  84     Assert(atom.getKind() != NOT && atom.getKind() != AND);
  85     assertInternalFact(atom, polarity, exp);
  86     i++;
  87   }
  88   d_pendingFact.clear();
  89 }
  90
  91 void InferenceManagerBuffered::doPendingLemmas()
  92 {
  93   // process all the pending lemmas
  94   for (const std::shared_ptr<Lemma>& plem : d_pendingLem)
  95   {
  96     if (!plem->notifySend())
  97     {
  98       // the lemma indicated that it should not be sent after all
  99       continue;
 100     }
 101     Node lem = plem->d_node;
 102     LemmaProperty p = plem->d_property;
 103     ProofGenerator* pg = plem->d_pg;
 104     Assert(!lem.isNull());
 105     // send (trusted) lemma on the output channel with property p
 106     trustedLemma(TrustNode::mkTrustLemma(lem, pg), p);
 107   }
 108   d_pendingLem.clear();
 109 }
 110
 111 void InferenceManagerBuffered::doPendingPhaseRequirements()
 112 {
 113   // process the pending require phase calls
 114   for (const std::pair<const Node, bool>& prp : d_pendingReqPhase)
 115   {
 116     d_out.requirePhase(prp.first, prp.second);
 117   }
 118   d_pendingReqPhase.clear();
 119 }
 120
 121 }  // namespace theory
 122 }  // namespace CVC4