src/theory/engine_output_channel.cpp

   1 /*********************                                                        */
   2 /*! \file engine_output_channel.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Tim King, Morgan Deters
   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 The theory engine output channel.
  13  **/
  14
  15 #include "theory/engine_output_channel.h"
  16
  17 #include "prop/prop_engine.h"
  18 #include "smt/smt_statistics_registry.h"
  19 #include "theory/theory_engine.h"
  20
  21 using namespace CVC4::kind;
  22
  23 namespace CVC4 {
  24 namespace theory {
  25
  26 EngineOutputChannel::Statistics::Statistics(theory::TheoryId theory)
  27     : conflicts(getStatsPrefix(theory) + "::conflicts", 0),
  28       propagations(getStatsPrefix(theory) + "::propagations", 0),
  29       lemmas(getStatsPrefix(theory) + "::lemmas", 0),
  30       requirePhase(getStatsPrefix(theory) + "::requirePhase", 0),
  31       restartDemands(getStatsPrefix(theory) + "::restartDemands", 0),
  32       trustedConflicts(getStatsPrefix(theory) + "::trustedConflicts", 0),
  33       trustedLemmas(getStatsPrefix(theory) + "::trustedLemmas", 0)
  34 {
  35   smtStatisticsRegistry()->registerStat(&conflicts);
  36   smtStatisticsRegistry()->registerStat(&propagations);
  37   smtStatisticsRegistry()->registerStat(&lemmas);
  38   smtStatisticsRegistry()->registerStat(&requirePhase);
  39   smtStatisticsRegistry()->registerStat(&restartDemands);
  40   smtStatisticsRegistry()->registerStat(&trustedConflicts);
  41   smtStatisticsRegistry()->registerStat(&trustedLemmas);
  42 }
  43
  44 EngineOutputChannel::Statistics::~Statistics()
  45 {
  46   smtStatisticsRegistry()->unregisterStat(&conflicts);
  47   smtStatisticsRegistry()->unregisterStat(&propagations);
  48   smtStatisticsRegistry()->unregisterStat(&lemmas);
  49   smtStatisticsRegistry()->unregisterStat(&requirePhase);
  50   smtStatisticsRegistry()->unregisterStat(&restartDemands);
  51   smtStatisticsRegistry()->unregisterStat(&trustedConflicts);
  52   smtStatisticsRegistry()->unregisterStat(&trustedLemmas);
  53 }
  54
  55 EngineOutputChannel::EngineOutputChannel(TheoryEngine* engine,
  56                                          theory::TheoryId theory)
  57     : d_engine(engine), d_statistics(theory), d_theory(theory)
  58 {
  59 }
  60
  61 void EngineOutputChannel::safePoint(ResourceManager::Resource r)
  62 {
  63   spendResource(r);
  64   if (d_engine->d_interrupted)
  65   {
  66     throw theory::Interrupted();
  67   }
  68 }
  69
  70 theory::LemmaStatus EngineOutputChannel::lemma(TNode lemma, LemmaProperty p)
  71 {
  72   Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma("
  73                          << lemma << ")"
  74                          << ", properties = " << p << std::endl;
  75   ++d_statistics.lemmas;
  76   d_engine->d_outputChannelUsed = true;
  77
  78   TrustNode tlem = TrustNode::mkTrustLemma(lemma);
  79   theory::LemmaStatus result = d_engine->lemma(
  80       tlem,
  81       p,
  82       isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST,
  83       d_theory);
  84   return result;
  85 }
  86
  87 theory::LemmaStatus EngineOutputChannel::splitLemma(TNode lemma, bool removable)
  88 {
  89   Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma("
  90                          << lemma << ")" << std::endl;
  91   ++d_statistics.lemmas;
  92   d_engine->d_outputChannelUsed = true;
  93
  94   Debug("pf::explain") << "EngineOutputChannel::splitLemma( " << lemma << " )"
  95                        << std::endl;
  96   TrustNode tlem = TrustNode::mkTrustLemma(lemma);
  97   LemmaProperty p = removable ? LemmaProperty::REMOVABLE : LemmaProperty::NONE;
  98   theory::LemmaStatus result = d_engine->lemma(tlem, p, d_theory);
  99   return result;
 100 }
 101
 102 bool EngineOutputChannel::propagate(TNode literal)
 103 {
 104   Debug("theory::propagate") << "EngineOutputChannel<" << d_theory
 105                              << ">::propagate(" << literal << ")" << std::endl;
 106   ++d_statistics.propagations;
 107   d_engine->d_outputChannelUsed = true;
 108   return d_engine->propagate(literal, d_theory);
 109 }
 110
 111 void EngineOutputChannel::conflict(TNode conflictNode)
 112 {
 113   Trace("theory::conflict")
 114       << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode
 115       << ")" << std::endl;
 116   ++d_statistics.conflicts;
 117   d_engine->d_outputChannelUsed = true;
 118   TrustNode tConf = TrustNode::mkTrustConflict(conflictNode);
 119   d_engine->conflict(tConf, d_theory);
 120 }
 121
 122 void EngineOutputChannel::demandRestart()
 123 {
 124   NodeManager* curr = NodeManager::currentNM();
 125   Node restartVar = curr->mkSkolem(
 126       "restartVar",
 127       curr->booleanType(),
 128       "A boolean variable asserted to be true to force a restart");
 129   Trace("theory::restart") << "EngineOutputChannel<" << d_theory
 130                            << ">::restart(" << restartVar << ")" << std::endl;
 131   ++d_statistics.restartDemands;
 132   lemma(restartVar, LemmaProperty::REMOVABLE);
 133 }
 134
 135 void EngineOutputChannel::requirePhase(TNode n, bool phase)
 136 {
 137   Debug("theory") << "EngineOutputChannel::requirePhase(" << n << ", " << phase
 138                   << ")" << std::endl;
 139   ++d_statistics.requirePhase;
 140   d_engine->getPropEngine()->requirePhase(n, phase);
 141 }
 142
 143 void EngineOutputChannel::setIncomplete()
 144 {
 145   Trace("theory") << "setIncomplete()" << std::endl;
 146   d_engine->setIncomplete(d_theory);
 147 }
 148
 149 void EngineOutputChannel::spendResource(ResourceManager::Resource r)
 150 {
 151   d_engine->spendResource(r);
 152 }
 153
 154 void EngineOutputChannel::handleUserAttribute(const char* attr,
 155                                               theory::Theory* t)
 156 {
 157   d_engine->handleUserAttribute(attr, t);
 158 }
 159
 160 void EngineOutputChannel::trustedConflict(TrustNode pconf)
 161 {
 162   Assert(pconf.getKind() == TrustNodeKind::CONFLICT);
 163   Trace("theory::conflict")
 164       << "EngineOutputChannel<" << d_theory << ">::trustedConflict("
 165       << pconf.getNode() << ")" << std::endl;
 166   if (pconf.getGenerator() != nullptr)
 167   {
 168     ++d_statistics.trustedConflicts;
 169   }
 170   ++d_statistics.conflicts;
 171   d_engine->d_outputChannelUsed = true;
 172   d_engine->conflict(pconf, d_theory);
 173 }
 174
 175 LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem, LemmaProperty p)
 176 {
 177   Debug("theory::lemma") << "EngineOutputChannel<" << d_theory
 178                          << ">::trustedLemma(" << plem << ")" << std::endl;
 179   Assert(plem.getKind() == TrustNodeKind::LEMMA);
 180   if (plem.getGenerator() != nullptr)
 181   {
 182     ++d_statistics.trustedLemmas;
 183   }
 184   ++d_statistics.lemmas;
 185   d_engine->d_outputChannelUsed = true;
 186   // now, call the normal interface for lemma
 187   return d_engine->lemma(
 188       plem,
 189       p,
 190       isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST,
 191       d_theory);
 192 }
 193
 194 }  // namespace theory
 195 }  // namespace CVC4