diff options
Diffstat (limited to 'src/theory/engine_output_channel.cpp')
| -rw-r--r-- | src/theory/engine_output_channel.cpp | 341 |
1 files changed, 341 insertions, 0 deletions
diff --git a/src/theory/engine_output_channel.cpp b/src/theory/engine_output_channel.cpp new file mode 100644 index 000000000..d83d2ba62 --- /dev/null +++ b/src/theory/engine_output_channel.cpp @@ -0,0 +1,341 @@ +/********************* */ +/*! \file engine_output_channel.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Guy Katz, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The theory engine output channel. + **/ + +#include "theory/engine_output_channel.h" + +#include "proof/cnf_proof.h" +#include "proof/lemma_proof.h" +#include "proof/proof_manager.h" +#include "proof/theory_proof.h" +#include "prop/prop_engine.h" +#include "smt/smt_statistics_registry.h" +#include "theory/theory_engine.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { + +EngineOutputChannel::Statistics::Statistics(theory::TheoryId theory) + : conflicts(getStatsPrefix(theory) + "::conflicts", 0), + propagations(getStatsPrefix(theory) + "::propagations", 0), + lemmas(getStatsPrefix(theory) + "::lemmas", 0), + requirePhase(getStatsPrefix(theory) + "::requirePhase", 0), + restartDemands(getStatsPrefix(theory) + "::restartDemands", 0), + trustedConflicts(getStatsPrefix(theory) + "::trustedConflicts", 0), + trustedLemmas(getStatsPrefix(theory) + "::trustedLemmas", 0) +{ + smtStatisticsRegistry()->registerStat(&conflicts); + smtStatisticsRegistry()->registerStat(&propagations); + smtStatisticsRegistry()->registerStat(&lemmas); + smtStatisticsRegistry()->registerStat(&requirePhase); + smtStatisticsRegistry()->registerStat(&restartDemands); + smtStatisticsRegistry()->registerStat(&trustedConflicts); + smtStatisticsRegistry()->registerStat(&trustedLemmas); +} + +EngineOutputChannel::Statistics::~Statistics() +{ + smtStatisticsRegistry()->unregisterStat(&conflicts); + smtStatisticsRegistry()->unregisterStat(&propagations); + smtStatisticsRegistry()->unregisterStat(&lemmas); + smtStatisticsRegistry()->unregisterStat(&requirePhase); + smtStatisticsRegistry()->unregisterStat(&restartDemands); + smtStatisticsRegistry()->unregisterStat(&trustedConflicts); + smtStatisticsRegistry()->unregisterStat(&trustedLemmas); +} + +EngineOutputChannel::EngineOutputChannel(TheoryEngine* engine, + theory::TheoryId theory) + : d_engine(engine), d_statistics(theory), d_theory(theory) +{ +} + +void EngineOutputChannel::safePoint(ResourceManager::Resource r) +{ + spendResource(r); + if (d_engine->d_interrupted) + { + throw theory::Interrupted(); + } +} + +theory::LemmaStatus EngineOutputChannel::lemma(TNode lemma, + ProofRule rule, + bool removable, + bool preprocess, + bool sendAtoms) +{ + Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" + << lemma << ")" + << ", preprocess = " << preprocess << std::endl; + ++d_statistics.lemmas; + d_engine->d_outputChannelUsed = true; + + PROOF({ registerLemmaRecipe(lemma, lemma, preprocess, d_theory); }); + + TrustNode tlem = TrustNode::mkTrustLemma(lemma); + theory::LemmaStatus result = + d_engine->lemma(tlem.getNode(), + rule, + false, + removable, + preprocess, + sendAtoms ? d_theory : theory::THEORY_LAST); + return result; +} + +void EngineOutputChannel::registerLemmaRecipe(Node lemma, + Node originalLemma, + bool preprocess, + theory::TheoryId theoryId) +{ + // During CNF conversion, conjunctions will be broken down into + // multiple lemmas. In order for the recipes to match, we have to do + // the same here. + NodeManager* nm = NodeManager::currentNM(); + + if (preprocess) lemma = d_engine->preprocess(lemma); + + bool negated = (lemma.getKind() == NOT); + Node nnLemma = negated ? lemma[0] : lemma; + + switch (nnLemma.getKind()) + { + case AND: + if (!negated) + { + for (unsigned i = 0; i < nnLemma.getNumChildren(); ++i) + registerLemmaRecipe(nnLemma[i], originalLemma, false, theoryId); + } + else + { + NodeBuilder<> builder(OR); + for (unsigned i = 0; i < nnLemma.getNumChildren(); ++i) + builder << nnLemma[i].negate(); + + Node disjunction = + (builder.getNumChildren() == 1) ? builder[0] : builder; + registerLemmaRecipe(disjunction, originalLemma, false, theoryId); + } + break; + + case EQUAL: + if (nnLemma[0].getType().isBoolean()) + { + if (!negated) + { + registerLemmaRecipe(nm->mkNode(OR, nnLemma[0], nnLemma[1].negate()), + originalLemma, + false, + theoryId); + registerLemmaRecipe(nm->mkNode(OR, nnLemma[0].negate(), nnLemma[1]), + originalLemma, + false, + theoryId); + } + else + { + registerLemmaRecipe(nm->mkNode(OR, nnLemma[0], nnLemma[1]), + originalLemma, + false, + theoryId); + registerLemmaRecipe( + nm->mkNode(OR, nnLemma[0].negate(), nnLemma[1].negate()), + originalLemma, + false, + theoryId); + } + } + break; + + case ITE: + if (!negated) + { + registerLemmaRecipe(nm->mkNode(OR, nnLemma[0].negate(), nnLemma[1]), + originalLemma, + false, + theoryId); + registerLemmaRecipe(nm->mkNode(OR, nnLemma[0], nnLemma[2]), + originalLemma, + false, + theoryId); + } + else + { + registerLemmaRecipe( + nm->mkNode(OR, nnLemma[0].negate(), nnLemma[1].negate()), + originalLemma, + false, + theoryId); + registerLemmaRecipe(nm->mkNode(OR, nnLemma[0], nnLemma[2].negate()), + originalLemma, + false, + theoryId); + } + break; + + default: break; + } + + // Theory lemmas have one step that proves the empty clause + LemmaProofRecipe proofRecipe; + Node emptyNode; + LemmaProofRecipe::ProofStep proofStep(theoryId, emptyNode); + + // Remember the original lemma, so we can report this later when asked to + proofRecipe.setOriginalLemma(originalLemma); + + // Record the assertions and rewrites + Node rewritten; + if (lemma.getKind() == OR) + { + for (unsigned i = 0; i < lemma.getNumChildren(); ++i) + { + rewritten = theory::Rewriter::rewrite(lemma[i]); + if (rewritten != lemma[i]) + { + proofRecipe.addRewriteRule(lemma[i].negate(), rewritten.negate()); + } + proofStep.addAssertion(lemma[i]); + proofRecipe.addBaseAssertion(rewritten); + } + } + else + { + rewritten = theory::Rewriter::rewrite(lemma); + if (rewritten != lemma) + { + proofRecipe.addRewriteRule(lemma.negate(), rewritten.negate()); + } + proofStep.addAssertion(lemma); + proofRecipe.addBaseAssertion(rewritten); + } + proofRecipe.addStep(proofStep); + ProofManager::getCnfProof()->setProofRecipe(&proofRecipe); +} + +theory::LemmaStatus EngineOutputChannel::splitLemma(TNode lemma, bool removable) +{ + Debug("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" + << lemma << ")" << std::endl; + ++d_statistics.lemmas; + d_engine->d_outputChannelUsed = true; + + Debug("pf::explain") << "EngineOutputChannel::splitLemma( " << lemma << " )" + << std::endl; + TrustNode tlem = TrustNode::mkTrustLemma(lemma); + theory::LemmaStatus result = d_engine->lemma( + tlem.getNode(), RULE_SPLIT, false, removable, false, d_theory); + return result; +} + +bool EngineOutputChannel::propagate(TNode literal) +{ + Debug("theory::propagate") << "EngineOutputChannel<" << d_theory + << ">::propagate(" << literal << ")" << std::endl; + ++d_statistics.propagations; + d_engine->d_outputChannelUsed = true; + return d_engine->propagate(literal, d_theory); +} + +void EngineOutputChannel::conflict(TNode conflictNode, + std::unique_ptr<Proof> proof) +{ + Trace("theory::conflict") + << "EngineOutputChannel<" << d_theory << ">::conflict(" << conflictNode + << ")" << std::endl; + Assert(!proof); // Theory shouldn't be producing proofs yet + ++d_statistics.conflicts; + d_engine->d_outputChannelUsed = true; + TrustNode tConf = TrustNode::mkTrustConflict(conflictNode); + d_engine->conflict(tConf.getNode(), d_theory); +} + +void EngineOutputChannel::demandRestart() +{ + NodeManager* curr = NodeManager::currentNM(); + Node restartVar = curr->mkSkolem( + "restartVar", + curr->booleanType(), + "A boolean variable asserted to be true to force a restart"); + Trace("theory::restart") << "EngineOutputChannel<" << d_theory + << ">::restart(" << restartVar << ")" << std::endl; + ++d_statistics.restartDemands; + lemma(restartVar, RULE_INVALID, true); +} + +void EngineOutputChannel::requirePhase(TNode n, bool phase) +{ + Debug("theory") << "EngineOutputChannel::requirePhase(" << n << ", " << phase + << ")" << std::endl; + ++d_statistics.requirePhase; + d_engine->getPropEngine()->requirePhase(n, phase); +} + +void EngineOutputChannel::setIncomplete() +{ + Trace("theory") << "setIncomplete()" << std::endl; + d_engine->setIncomplete(d_theory); +} + +void EngineOutputChannel::spendResource(ResourceManager::Resource r) +{ + d_engine->spendResource(r); +} + +void EngineOutputChannel::handleUserAttribute(const char* attr, + theory::Theory* t) +{ + d_engine->handleUserAttribute(attr, t); +} + +void EngineOutputChannel::trustedConflict(TrustNode pconf) +{ + Assert(pconf.getKind() == TrustNodeKind::CONFLICT); + Trace("theory::conflict") + << "EngineOutputChannel<" << d_theory << ">::conflict(" << pconf.getNode() + << ")" << std::endl; + if (pconf.getGenerator() != nullptr) + { + ++d_statistics.trustedConflicts; + } + ++d_statistics.conflicts; + d_engine->d_outputChannelUsed = true; + d_engine->conflict(pconf.getNode(), d_theory); +} + +LemmaStatus EngineOutputChannel::trustedLemma(TrustNode plem, + bool removable, + bool preprocess, + bool sendAtoms) +{ + Assert(plem.getKind() == TrustNodeKind::LEMMA); + if (plem.getGenerator() != nullptr) + { + ++d_statistics.trustedLemmas; + } + ++d_statistics.lemmas; + d_engine->d_outputChannelUsed = true; + // now, call the normal interface for lemma + return d_engine->lemma(plem.getNode(), + RULE_INVALID, + false, + removable, + preprocess, + sendAtoms ? d_theory : theory::THEORY_LAST); +} + +} // namespace theory +} // namespace CVC4 |