src/theory/engine_output_channel.cpp

   1 /*********************                                                        */
   2 /*! \file engine_output_channel.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-2019 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 "proof/cnf_proof.h"
  18 #include "proof/lemma_proof.h"
  19 #include "proof/proof_manager.h"
  20 #include "proof/theory_proof.h"
  21 #include "prop/prop_engine.h"
  22 #include "smt/smt_statistics_registry.h"
  23 #include "theory/theory_engine.h"
  24
  25 using namespace CVC4::kind;
  26
  27 namespace CVC4 {
  28 namespace theory {
  29
  30 EngineOutputChannel::Statistics::Statistics(theory::TheoryId theory)
  31     : conflicts(getStatsPrefix(theory) + "::conflicts", 0),
  32       propagations(getStatsPrefix(theory) + "::propagations", 0),
  33       lemmas(getStatsPrefix(theory) + "::lemmas", 0),
  34       requirePhase(getStatsPrefix(theory) + "::requirePhase", 0),
  35       restartDemands(getStatsPrefix(theory) + "::restartDemands", 0),
  36       trustedConflicts(getStatsPrefix(theory) + "::trustedConflicts", 0),
  37       trustedLemmas(getStatsPrefix(theory) + "::trustedLemmas", 0)
  38 {
  39   smtStatisticsRegistry()->registerStat(&conflicts);
  40   smtStatisticsRegistry()->registerStat(&propagations);
  41   smtStatisticsRegistry()->registerStat(&lemmas);
  42   smtStatisticsRegistry()->registerStat(&requirePhase);
  43   smtStatisticsRegistry()->registerStat(&restartDemands);
  44   smtStatisticsRegistry()->registerStat(&trustedConflicts);
  45   smtStatisticsRegistry()->registerStat(&trustedLemmas);
  46 }
  47
  48 EngineOutputChannel::Statistics::~Statistics()
  49 {
  50   smtStatisticsRegistry()->unregisterStat(&conflicts);
  51   smtStatisticsRegistry()->unregisterStat(&propagations);
  52   smtStatisticsRegistry()->unregisterStat(&lemmas);
  53   smtStatisticsRegistry()->unregisterStat(&requirePhase);
  54   smtStatisticsRegistry()->unregisterStat(&restartDemands);
  55   smtStatisticsRegistry()->unregisterStat(&trustedConflicts);
  56   smtStatisticsRegistry()->unregisterStat(&trustedLemmas);
  57 }
  58
  59 EngineOutputChannel::EngineOutputChannel(TheoryEngine* engine,
  60                                          theory::TheoryId theory)
  61     : d_engine(engine), d_statistics(theory), d_theory(theory)
  62 {
  63 }
  64
  65 void EngineOutputChannel::safePoint(ResourceManager::Resource r)
  66 {
  67   spendResource(r);
  68   if (d_engine->d_interrupted)
  69   {
  70     throw theory::Interrupted();
  71   }
  72 }
  73
  74 theory::LemmaStatus EngineOutputChannel::lemma(TNode lemma,
  75                                                ProofRule rule,
  76                                                bool removable,
  77                                                bool preprocess,
  78                                                bool sendAtoms)
  79 {
  80   Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma("
  81                          << lemma << ")"
  82                          << ", preprocess = " << preprocess << std::endl;
  83   ++d_statistics.lemmas;
  84   d_engine->d_outputChannelUsed = true;
  85
  86   PROOF({ registerLemmaRecipe(lemma, lemma, preprocess, d_theory); });
  87
  88   theory::LemmaStatus result =
  89       d_engine->lemma(lemma,
  90                       rule,
  91                       false,
  92                       removable,
  93                       preprocess,
  94                       sendAtoms ? d_theory : theory::THEORY_LAST);
  95   return result;
  96 }
  97
  98 void EngineOutputChannel::registerLemmaRecipe(Node lemma,
  99                                               Node originalLemma,
 100                                               bool preprocess,
 101                                               theory::TheoryId theoryId)
 102 {
 103   // During CNF conversion, conjunctions will be broken down into
 104   // multiple lemmas. In order for the recipes to match, we have to do
 105   // the same here.
 106   NodeManager* nm = NodeManager::currentNM();
 107
 108   if (preprocess) lemma = d_engine->preprocess(lemma);
 109
 110   bool negated = (lemma.getKind() == NOT);
 111   Node nnLemma = negated ? lemma[0] : lemma;
 112
 113   switch (nnLemma.getKind())
 114   {
 115     case AND:
 116       if (!negated)
 117       {
 118         for (unsigned i = 0; i < nnLemma.getNumChildren(); ++i)
 119           registerLemmaRecipe(nnLemma[i], originalLemma, false, theoryId);
 120       }
 121       else
 122       {
 123         NodeBuilder<> builder(OR);
 124         for (unsigned i = 0; i < nnLemma.getNumChildren(); ++i)
 125           builder << nnLemma[i].negate();
 126
 127         Node disjunction =
 128             (builder.getNumChildren() == 1) ? builder[0] : builder;
 129         registerLemmaRecipe(disjunction, originalLemma, false, theoryId);
 130       }
 131       break;
 132
 133     case EQUAL:
 134       if (nnLemma[0].getType().isBoolean())
 135       {
 136         if (!negated)
 137         {
 138           registerLemmaRecipe(nm->mkNode(OR, nnLemma[0], nnLemma[1].negate()),
 139                               originalLemma,
 140                               false,
 141                               theoryId);
 142           registerLemmaRecipe(nm->mkNode(OR, nnLemma[0].negate(), nnLemma[1]),
 143                               originalLemma,
 144                               false,
 145                               theoryId);
 146         }
 147         else
 148         {
 149           registerLemmaRecipe(nm->mkNode(OR, nnLemma[0], nnLemma[1]),
 150                               originalLemma,
 151                               false,
 152                               theoryId);
 153           registerLemmaRecipe(
 154               nm->mkNode(OR, nnLemma[0].negate(), nnLemma[1].negate()),
 155               originalLemma,
 156               false,
 157               theoryId);
 158         }
 159       }
 160       break;
 161
 162     case ITE:
 163       if (!negated)
 164       {
 165         registerLemmaRecipe(nm->mkNode(OR, nnLemma[0].negate(), nnLemma[1]),
 166                             originalLemma,
 167                             false,
 168                             theoryId);
 169         registerLemmaRecipe(nm->mkNode(OR, nnLemma[0], nnLemma[2]),
 170                             originalLemma,
 171                             false,
 172                             theoryId);
 173       }
 174       else
 175       {
 176         registerLemmaRecipe(
 177             nm->mkNode(OR, nnLemma[0].negate(), nnLemma[1].negate()),
 178             originalLemma,
 179             false,
 180             theoryId);
 181         registerLemmaRecipe(nm->mkNode(OR, nnLemma[0], nnLemma[2].negate()),
 182                             originalLemma,
 183                             false,
 184                             theoryId);
 185       }
 186       break;
 187
 188     default: break;
 189   }
 190
 191   // Theory lemmas have one step that proves the empty clause
 192   LemmaProofRecipe proofRecipe;
 193   Node emptyNode;
 194   LemmaProofRecipe::ProofStep proofStep(theoryId, emptyNode);
 195
 196   // Remember the original lemma, so we can report this later when asked to
 197   proofRecipe.setOriginalLemma(originalLemma);
 198
 199   // Record the assertions and rewrites
 200   Node rewritten;
 201   if (lemma.getKind() == OR)
 202   {
 203     for (unsigned i = 0; i < lemma.getNumChildren(); ++i)
 204     {
 205       rewritten = theory::Rewriter::rewrite(lemma[i]);
 206       if (rewritten != lemma[i])
 207       {
 208         proofRecipe.addRewriteRule(lemma[i].negate(), rewritten.negate());
 209       }
 210       proofStep.addAssertion(lemma[i]);
 211       proofRecipe.addBaseAssertion(rewritten);
 212     }
 213   }
 214   else
 215   {
 216     rewritten = theory::Rewriter::rewrite(lemma);
 217     if (rewritten != lemma)
 218     {
 219       proofRecipe.addRewriteRule(lemma.negate(), rewritten.negate());
 220     }
 221     proofStep.addAssertion(lemma);
 222     proofRecipe.addBaseAssertion(rewritten);
 223   }
 224   proofRecipe.addStep(proofStep);
 225   ProofManager::getCnfProof()->setProofRecipe(&proofRecipe);
 226 }
 227
 228 theory::LemmaStatus EngineOutputChannel::splitLemma(TNode lemma, bool removable)
 229 {
 230   Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma("
 231                          << lemma << ")" << std::endl;
 232   ++d_statistics.lemmas;
 233   d_engine->d_outputChannelUsed = true;
 234
 235   Debug("pf::explain") << "EngineOutputChannel::splitLemma( " << lemma << " )"
 236                        << std::endl;
 237   theory::LemmaStatus result =
 238       d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory);
 239   return result;
 240 }
 241
 242 bool EngineOutputChannel::propagate(TNode literal)
 243 {
 244   Debug("theory::propagate") << "EngineOutputChannel<" << d_theory
 245                              << ">::propagate(" << literal << ")" << std::endl;
 246   ++d_statistics.propagations;
 247   d_engine->d_outputChannelUsed = true;
 248   return d_engine->propagate(literal, d_theory);
 249 }
 250
 251 void EngineOutputChannel::conflict(TNode conflictNode,
 252                                    std::unique_ptr<Proof> proof)
 253 {
 254   Trace("theory::conflict")
 255       << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode
 256       << ")" << std::endl;
 257   Assert(!proof);  // Theory shouldn't be producing proofs yet
 258   ++d_statistics.conflicts;
 259   d_engine->d_outputChannelUsed = true;
 260   d_engine->conflict(conflictNode, d_theory);
 261 }
 262
 263 void EngineOutputChannel::demandRestart()
 264 {
 265   NodeManager* curr = NodeManager::currentNM();
 266   Node restartVar = curr->mkSkolem(
 267       "restartVar",
 268       curr->booleanType(),
 269       "A boolean variable asserted to be true to force a restart");
 270   Trace("theory::restart") << "EngineOutputChannel<" << d_theory
 271                            << ">::restart(" << restartVar << ")" << std::endl;
 272   ++d_statistics.restartDemands;
 273   lemma(restartVar, RULE_INVALID, true);
 274 }
 275
 276 void EngineOutputChannel::requirePhase(TNode n, bool phase)
 277 {
 278   Debug("theory") << "EngineOutputChannel::requirePhase(" << n << ", " << phase
 279                   << ")" << std::endl;
 280   ++d_statistics.requirePhase;
 281   d_engine->getPropEngine()->requirePhase(n, phase);
 282 }
 283
 284 void EngineOutputChannel::setIncomplete()
 285 {
 286   Trace("theory") << "setIncomplete()" << std::endl;
 287   d_engine->setIncomplete(d_theory);
 288 }
 289
 290 void EngineOutputChannel::spendResource(ResourceManager::Resource r)
 291 {
 292   d_engine->spendResource(r);
 293 }
 294
 295 void EngineOutputChannel::handleUserAttribute(const char* attr,
 296                                               theory::Theory* t)
 297 {
 298   d_engine->handleUserAttribute(attr, t);
 299 }
 300
 301 }  // namespace theory
 302 }  // namespace CVC4