src/theory/engine_output_channel.cpp

   1 /*********************                                                        */
   2 /*! \file engine_output_channel.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Guy Katz, Tim King
   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 "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                                                LemmaProperty p)
  77 {
  78   Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma("
  79                          << lemma << ")"
  80                          << ", properties = " << p << std::endl;
  81   ++d_statistics.lemmas;
  82   d_engine->d_outputChannelUsed = true;
  83
  84   PROOF({
  85     bool preprocess = isLemmaPropertyPreprocess(p);
  86     registerLemmaRecipe(lemma, lemma, preprocess, d_theory);
  87   });
  88
  89   TrustNode tlem = TrustNode::mkTrustLemma(lemma);
  90   theory::LemmaStatus result = d_engine->lemma(
  91       tlem.getNode(),
  92       rule,
  93       false,
  94       p,
  95       isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST);
  96   return result;
  97 }
  98
  99 void EngineOutputChannel::registerLemmaRecipe(Node lemma,
 100                                               Node originalLemma,
 101                                               bool preprocess,
 102                                               theory::TheoryId theoryId)
 103 {
 104   // During CNF conversion, conjunctions will be broken down into
 105   // multiple lemmas. In order for the recipes to match, we have to do
 106   // the same here.
 107   NodeManager* nm = NodeManager::currentNM();
 108
 109   if (preprocess) lemma = d_engine->preprocess(lemma);
 110
 111   bool negated = (lemma.getKind() == NOT);
 112   Node nnLemma = negated ? lemma[0] : lemma;
 113
 114   switch (nnLemma.getKind())
 115   {
 116     case AND:
 117       if (!negated)
 118       {
 119         for (unsigned i = 0; i < nnLemma.getNumChildren(); ++i)
 120           registerLemmaRecipe(nnLemma[i], originalLemma, false, theoryId);
 121       }
 122       else
 123       {
 124         NodeBuilder<> builder(OR);
 125         for (unsigned i = 0; i < nnLemma.getNumChildren(); ++i)
 126           builder << nnLemma[i].negate();
 127
 128         Node disjunction =
 129             (builder.getNumChildren() == 1) ? builder[0] : builder;
 130         registerLemmaRecipe(disjunction, originalLemma, false, theoryId);
 131       }
 132       break;
 133
 134     case EQUAL:
 135       if (nnLemma[0].getType().isBoolean())
 136       {
 137         if (!negated)
 138         {
 139           registerLemmaRecipe(nm->mkNode(OR, nnLemma[0], nnLemma[1].negate()),
 140                               originalLemma,
 141                               false,
 142                               theoryId);
 143           registerLemmaRecipe(nm->mkNode(OR, nnLemma[0].negate(), nnLemma[1]),
 144                               originalLemma,
 145                               false,
 146                               theoryId);
 147         }
 148         else
 149         {
 150           registerLemmaRecipe(nm->mkNode(OR, nnLemma[0], nnLemma[1]),
 151                               originalLemma,
 152                               false,
 153                               theoryId);
 154           registerLemmaRecipe(
 155               nm->mkNode(OR, nnLemma[0].negate(), nnLemma[1].negate()),
 156               originalLemma,
 157               false,
 158               theoryId);
 159         }
 160       }
 161       break;
 162
 163     case ITE:
 164       if (!negated)
 165       {
 166         registerLemmaRecipe(nm->mkNode(OR, nnLemma[0].negate(), nnLemma[1]),
 167                             originalLemma,
 168                             false,
 169                             theoryId);
 170         registerLemmaRecipe(nm->mkNode(OR, nnLemma[0], nnLemma[2]),
 171                             originalLemma,
 172                             false,
 173                             theoryId);
 174       }
 175       else
 176       {
 177         registerLemmaRecipe(
 178             nm->mkNode(OR, nnLemma[0].negate(), nnLemma[1].negate()),
 179             originalLemma,
 180             false,
 181             theoryId);
 182         registerLemmaRecipe(nm->mkNode(OR, nnLemma[0], nnLemma[2].negate()),
 183                             originalLemma,
 184                             false,
 185                             theoryId);
 186       }
 187       break;
 188
 189     default: break;
 190   }
 191
 192   // Theory lemmas have one step that proves the empty clause
 193   LemmaProofRecipe proofRecipe;
 194   Node emptyNode;
 195   LemmaProofRecipe::ProofStep proofStep(theoryId, emptyNode);
 196
 197   // Remember the original lemma, so we can report this later when asked to
 198   proofRecipe.setOriginalLemma(originalLemma);
 199
 200   // Record the assertions and rewrites
 201   Node rewritten;
 202   if (lemma.getKind() == OR)
 203   {
 204     for (unsigned i = 0; i < lemma.getNumChildren(); ++i)
 205     {
 206       rewritten = theory::Rewriter::rewrite(lemma[i]);
 207       if (rewritten != lemma[i])
 208       {
 209         proofRecipe.addRewriteRule(lemma[i].negate(), rewritten.negate());
 210       }
 211       proofStep.addAssertion(lemma[i]);
 212       proofRecipe.addBaseAssertion(rewritten);
 213     }
 214   }
 215   else
 216   {
 217     rewritten = theory::Rewriter::rewrite(lemma);
 218     if (rewritten != lemma)
 219     {
 220       proofRecipe.addRewriteRule(lemma.negate(), rewritten.negate());
 221     }
 222     proofStep.addAssertion(lemma);
 223     proofRecipe.addBaseAssertion(rewritten);
 224   }
 225   proofRecipe.addStep(proofStep);
 226   ProofManager::getCnfProof()->setProofRecipe(&proofRecipe);
 227 }
 228
 229 theory::LemmaStatus EngineOutputChannel::splitLemma(TNode lemma, bool removable)
 230 {
 231   Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma("
 232                          << lemma << ")" << std::endl;
 233   ++d_statistics.lemmas;
 234   d_engine->d_outputChannelUsed = true;
 235
 236   Debug("pf::explain") << "EngineOutputChannel::splitLemma( " << lemma << " )"
 237                        << std::endl;
 238   TrustNode tlem = TrustNode::mkTrustLemma(lemma);
 239   LemmaProperty p = removable ? LemmaProperty::REMOVABLE : LemmaProperty::NONE;
 240   theory::LemmaStatus result =
 241       d_engine->lemma(tlem.getNode(), RULE_SPLIT, false, p, d_theory);
 242   return result;
 243 }
 244
 245 bool EngineOutputChannel::propagate(TNode literal)
 246 {
 247   Debug("theory::propagate") << "EngineOutputChannel<" << d_theory
 248                              << ">::propagate(" << literal << ")" << std::endl;
 249   ++d_statistics.propagations;
 250   d_engine->d_outputChannelUsed = true;
 251   return d_engine->propagate(literal, d_theory);
 252 }
 253
 254 void EngineOutputChannel::conflict(TNode conflictNode,
 255                                    std::unique_ptr<Proof> proof)
 256 {
 257   Trace("theory::conflict")
 258       << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode
 259       << ")" << std::endl;
 260   Assert(!proof);  // Theory shouldn't be producing proofs yet
 261   ++d_statistics.conflicts;
 262   d_engine->d_outputChannelUsed = true;
 263   TrustNode tConf = TrustNode::mkTrustConflict(conflictNode);
 264   d_engine->conflict(tConf.getNode(), d_theory);
 265 }
 266
 267 void EngineOutputChannel::demandRestart()
 268 {
 269   NodeManager* curr = NodeManager::currentNM();
 270   Node restartVar = curr->mkSkolem(
 271       "restartVar",
 272       curr->booleanType(),
 273       "A boolean variable asserted to be true to force a restart");
 274   Trace("theory::restart") << "EngineOutputChannel<" << d_theory
 275                            << ">::restart(" << restartVar << ")" << std::endl;
 276   ++d_statistics.restartDemands;
 277   lemma(restartVar, RULE_INVALID, LemmaProperty::REMOVABLE);
 278 }
 279
 280 void EngineOutputChannel::requirePhase(TNode n, bool phase)
 281 {
 282   Debug("theory") << "EngineOutputChannel::requirePhase(" << n << ", " << phase
 283                   << ")" << std::endl;
 284   ++d_statistics.requirePhase;
 285   d_engine->getPropEngine()->requirePhase(n, phase);
 286 }
 287
 288 void EngineOutputChannel::setIncomplete()
 289 {
 290   Trace("theory") << "setIncomplete()" << std::endl;
 291   d_engine->setIncomplete(d_theory);
 292 }
 293
 294 void EngineOutputChannel::spendResource(ResourceManager::Resource r)
 295 {
 296   d_engine->spendResource(r);
 297 }
 298
 299 void EngineOutputChannel::handleUserAttribute(const char* attr,
 300                                               theory::Theory* t)
 301 {
 302   d_engine->handleUserAttribute(attr, t);
 303 }
 304
 305 void EngineOutputChannel::trustedConflict(TrustNode pconf)
 306 {
 307   Assert(pconf.getKind() == TrustNodeKind::CONFLICT);
 308   Trace("theory::conflict")
 309       << "EngineOutputChannel<" << d_theory << ">::conflict(" << pconf.getNode()
 310       << ")" << std::endl;
 311   if (pconf.getGenerator() != nullptr)
 312   {
 313     ++d_statistics.trustedConflicts;
 314   }
 315   ++d_statistics.conflicts;
 316   d_engine->d_outputChannelUsed = true;
 317   d_engine->conflict(pconf.getNode(), d_theory);
 318 }
 319
 320 LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem, LemmaProperty p)
 321 {
 322   Assert(plem.getKind() == TrustNodeKind::LEMMA);
 323   if (plem.getGenerator() != nullptr)
 324   {
 325     ++d_statistics.trustedLemmas;
 326   }
 327   ++d_statistics.lemmas;
 328   d_engine->d_outputChannelUsed = true;
 329   // now, call the normal interface for lemma
 330   return d_engine->lemma(
 331       plem.getNode(),
 332       RULE_INVALID,
 333       false,
 334       p,
 335       isLemmaPropertySendAtoms(p) ? d_theory : theory::THEORY_LAST);
 336 }
 337
 338 }  // namespace theory
 339 }  // namespace CVC4