/*! \file theory_engine.cpp
** \verbatim
** Top contributors (to current version):
- ** Dejan Jovanovic, Andrew Reynolds, Morgan Deters
+ ** Andrew Reynolds, Dejan Jovanovic, Morgan Deters
** 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.
+ ** 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
**
#include "theory/theory_engine.h"
-#include <list>
-#include <vector>
-
#include "base/map_util.h"
#include "decision/decision_engine.h"
#include "expr/attribute.h"
-#include "expr/node.h"
-#include "expr/node_algorithm.h"
+#include "expr/lazy_proof.h"
#include "expr/node_builder.h"
#include "expr/node_visitor.h"
-#include "options/bv_options.h"
-#include "options/options.h"
-#include "options/proof_options.h"
+#include "expr/proof_ensure_closed.h"
#include "options/quantifiers_options.h"
+#include "options/smt_options.h"
#include "options/theory_options.h"
-#include "preprocessing/assertion_pipeline.h"
-#include "proof/cnf_proof.h"
-#include "proof/lemma_proof.h"
-#include "proof/proof_manager.h"
-#include "proof/theory_proof.h"
+#include "printer/printer.h"
+#include "prop/prop_engine.h"
+#include "smt/dump.h"
#include "smt/logic_exception.h"
-#include "smt/term_formula_removal.h"
-#include "theory/arith/arith_ite_utils.h"
-#include "theory/bv/theory_bv_utils.h"
-#include "theory/care_graph.h"
+#include "theory/combination_care_graph.h"
#include "theory/decision_manager.h"
-#include "theory/ee_manager_distributed.h"
#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/fmf/model_engine.h"
-#include "theory/quantifiers/theory_quantifiers.h"
#include "theory/quantifiers_engine.h"
+#include "theory/relevance_manager.h"
#include "theory/rewriter.h"
#include "theory/theory.h"
+#include "theory/theory_engine_proof_generator.h"
+#include "theory/theory_id.h"
#include "theory/theory_model.h"
#include "theory/theory_traits.h"
#include "theory/uf/equality_engine.h"
CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_DATATYPES) \
CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_SEP) \
CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_SETS) \
+ CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_BAGS) \
CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_STRINGS) \
CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_QUANTIFIERS)
}
}
-void TheoryEngine::finishInit() {
- // initialize the quantifiers engine
- if (d_logicInfo.isQuantified())
+void TheoryEngine::finishInit()
+{
+ // NOTE: This seems to be required since
+ // theory::TheoryTraits<THEORY>::isParametric cannot be accessed without
+ // using the CVC4_FOR_EACH_THEORY_STATEMENT macro. -AJR
+ std::vector<theory::Theory*> paraTheories;
+#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
+#undef CVC4_FOR_EACH_THEORY_STATEMENT
+#endif
+#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
+ if (theory::TheoryTraits<THEORY>::isParametric \
+ && d_logicInfo.isTheoryEnabled(THEORY)) \
+ { \
+ paraTheories.push_back(theoryOf(THEORY)); \
+ }
+ // Collect the parametric theories, which are given to the theory combination
+ // manager below
+ CVC4_FOR_EACH_THEORY;
+
+ // Initialize the theory combination architecture
+ if (options::tcMode() == options::TcMode::CARE_GRAPH)
{
- // initialize the quantifiers engine
- d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this);
+ d_tc.reset(new CombinationCareGraph(*this, paraTheories, d_pnm));
}
-
- // Initialize the equality engine architecture for all theories, which
- // includes the master equality engine.
- d_eeDistributed.reset(new EqEngineManagerDistributed(*this));
- d_eeDistributed->finishInit();
-
- // Initialize the model and model builder.
- if (d_logicInfo.isQuantified())
+ else
{
- d_curr_model_builder = d_quantEngine->getModelBuilder();
- d_curr_model = d_quantEngine->getModel();
- } else {
- d_curr_model = new theory::TheoryModel(
- d_userContext, "DefaultModel", options::assignFunctionValues());
- d_aloc_curr_model = true;
+ Unimplemented() << "TheoryEngine::finishInit: theory combination mode "
+ << options::tcMode() << " not supported";
}
-
- //make the default builder, e.g. in the case that the quantifiers engine does not have a model builder
- if( d_curr_model_builder==NULL ){
- d_curr_model_builder = new theory::TheoryEngineModelBuilder(this);
- d_aloc_curr_model_builder = true;
+ // create the relevance filter if any option requires it
+ if (options::relevanceFilter())
+ {
+ d_relManager.reset(
+ new RelevanceManager(d_userContext, theory::Valuation(this)));
}
- // set the core equality engine on quantifiers engine
+ // initialize the quantifiers engine
+ if (d_logicInfo.isQuantified())
+ {
+ // get the quantifiers engine, which is initialized by the quantifiers
+ // theory
+ d_quantEngine = d_theoryTable[THEORY_QUANTIFIERS]->getQuantifiersEngine();
+ Assert(d_quantEngine != nullptr);
+ }
+ // initialize the theory combination manager, which decides and allocates the
+ // equality engines to use for all theories.
+ d_tc->finishInit();
+ // get pointer to the shared solver
+ d_sharedSolver = d_tc->getSharedSolver();
+
+ // finish initializing the quantifiers engine
if (d_logicInfo.isQuantified())
{
- d_quantEngine->setMasterEqualityEngine(
- d_eeDistributed->getMasterEqualityEngine());
+ d_quantEngine->finishInit(this, d_decManager.get());
}
- // finish initializing the theories
+ // finish initializing the theories by linking them with the appropriate
+ // utilities and then calling their finishInit method.
for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
Theory* t = d_theoryTable[theoryId];
if (t == nullptr)
continue;
}
// setup the pointers to the utilities
- const EeTheoryInfo* eeti = d_eeDistributed->getEeTheoryInfo(theoryId);
+ const EeTheoryInfo* eeti = d_tc->getEeTheoryInfo(theoryId);
Assert(eeti != nullptr);
// the theory's official equality engine is the one specified by the
// equality engine manager
}
}
+ProofNodeManager* TheoryEngine::getProofNodeManager() const { return d_pnm; }
+
TheoryEngine::TheoryEngine(context::Context* context,
context::UserContext* userContext,
ResourceManager* rm,
- RemoveTermFormulas& iteRemover,
- const LogicInfo& logicInfo)
+ const LogicInfo& logicInfo,
+ OutputManager& outMgr,
+ ProofNodeManager* pnm)
: d_propEngine(nullptr),
d_context(context),
d_userContext(userContext),
d_logicInfo(logicInfo),
- d_sharedTerms(this, context),
- d_eeDistributed(nullptr),
+ d_outMgr(outMgr),
+ d_pnm(pnm),
+ d_lazyProof(
+ d_pnm != nullptr
+ ? new LazyCDProof(
+ d_pnm, nullptr, d_userContext, "TheoryEngine::LazyCDProof")
+ : nullptr),
+ d_tepg(new TheoryEngineProofGenerator(d_pnm, d_userContext)),
+ d_tc(nullptr),
+ d_sharedSolver(nullptr),
d_quantEngine(nullptr),
d_decManager(new DecisionManager(userContext)),
- d_curr_model(nullptr),
- d_aloc_curr_model(false),
- d_curr_model_builder(nullptr),
- d_aloc_curr_model_builder(false),
+ d_relManager(nullptr),
+ d_preRegistrationVisitor(this, context),
d_eager_model_building(false),
- d_possiblePropagations(context),
- d_hasPropagated(context),
d_inConflict(context, false),
d_inSatMode(false),
d_hasShutDown(false),
d_propagatedLiterals(context),
d_propagatedLiteralsIndex(context, 0),
d_atomRequests(context),
- d_tpp(*this, iteRemover),
d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"),
d_true(),
d_false(),
d_resourceManager(rm),
d_inPreregister(false),
d_factsAsserted(context, false),
- d_preRegistrationVisitor(this, context),
- d_sharedTermsVisitor(d_sharedTerms),
d_attr_handle(),
d_arithSubstitutionsAdded("theory::arith::zzz::arith::substitutions", 0)
{
d_true = NodeManager::currentNM()->mkConst<bool>(true);
d_false = NodeManager::currentNM()->mkConst<bool>(false);
-#ifdef CVC4_PROOF
- ProofManager::currentPM()->initTheoryProofEngine();
-#endif
-
smtStatisticsRegistry()->registerStat(&d_arithSubstitutionsAdded);
}
}
}
- if( d_aloc_curr_model_builder ){
- delete d_curr_model_builder;
- }
- if( d_aloc_curr_model ){
- delete d_curr_model;
- }
-
- delete d_quantEngine;
-
smtStatisticsRegistry()->unregisterStat(&d_combineTheoriesTime);
smtStatisticsRegistry()->unregisterStat(&d_arithSubstitutionsAdded);
}
void TheoryEngine::interrupt() { d_interrupted = true; }
void TheoryEngine::preRegister(TNode preprocessed) {
-
- Debug("theory") << "TheoryEngine::preRegister( " << preprocessed << ")" << std::endl;
- if(Dump.isOn("missed-t-propagations")) {
- d_possiblePropagations.push_back(preprocessed);
- }
+ Debug("theory") << "TheoryEngine::preRegister( " << preprocessed << ")"
+ << std::endl;
d_preregisterQueue.push(preprocessed);
if (!d_inPreregister) {
preprocessed = d_preregisterQueue.front();
d_preregisterQueue.pop();
- if (d_logicInfo.isSharingEnabled() && preprocessed.getKind() == kind::EQUAL) {
- // When sharing is enabled, we propagate from the shared terms manager also
- d_sharedTerms.addEqualityToPropagate(preprocessed);
- }
-
// the atom should not have free variables
Debug("theory") << "TheoryEngine::preRegister: " << preprocessed
<< std::endl;
Assert(!expr::hasFreeVar(preprocessed));
+ // should not have witness
+ Assert(!expr::hasSubtermKind(kind::WITNESS, preprocessed));
+
// Pre-register the terms in the atom
- Theory::Set theories = NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed);
- theories = Theory::setRemove(THEORY_BOOL, theories);
- // Remove the top theory, if any more that means multiple theories were involved
- bool multipleTheories = Theory::setRemove(Theory::theoryOf(preprocessed), theories);
- TheoryId i;
- // These checks don't work with finite model finding, because it
- // uses Rational constants to represent cardinality constraints,
- // even though arithmetic isn't actually involved.
- if(!options::finiteModelFind()) {
- while((i = Theory::setPop(theories)) != THEORY_LAST) {
- if(!d_logicInfo.isTheoryEnabled(i)) {
- LogicInfo newLogicInfo = d_logicInfo.getUnlockedCopy();
- newLogicInfo.enableTheory(i);
- newLogicInfo.lock();
- stringstream ss;
- ss << "The logic was specified as " << d_logicInfo.getLogicString()
- << ", which doesn't include " << i
- << ", but found a term in that theory." << endl
- << "You might want to extend your logic to "
- << newLogicInfo.getLogicString() << endl;
- throw LogicException(ss.str());
+ theory::TheoryIdSet theories = NodeVisitor<PreRegisterVisitor>::run(
+ d_preRegistrationVisitor, preprocessed);
+ theories = TheoryIdSetUtil::setRemove(THEORY_BOOL, theories);
+ // Remove the top theory, if any more that means multiple theories were
+ // involved
+ bool multipleTheories =
+ TheoryIdSetUtil::setRemove(Theory::theoryOf(preprocessed), theories);
+ if (Configuration::isAssertionBuild())
+ {
+ TheoryId i;
+ // This should never throw an exception, since theories should be
+ // guaranteed to be initialized.
+ // These checks don't work with finite model finding, because it
+ // uses Rational constants to represent cardinality constraints,
+ // even though arithmetic isn't actually involved.
+ if (!options::finiteModelFind())
+ {
+ while ((i = TheoryIdSetUtil::setPop(theories)) != THEORY_LAST)
+ {
+ if (!d_logicInfo.isTheoryEnabled(i))
+ {
+ LogicInfo newLogicInfo = d_logicInfo.getUnlockedCopy();
+ newLogicInfo.enableTheory(i);
+ newLogicInfo.lock();
+ std::stringstream ss;
+ ss << "The logic was specified as " << d_logicInfo.getLogicString()
+ << ", which doesn't include " << i
+ << ", but found a term in that theory." << std::endl
+ << "You might want to extend your logic to "
+ << newLogicInfo.getLogicString() << std::endl;
+ throw LogicException(ss.str());
+ }
}
}
}
- if (multipleTheories) {
- // Collect the shared terms if there are multiple theories
- NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, preprocessed);
- }
+
+ // pre-register with the shared solver, which also handles
+ // calling prepregister on individual theories.
+ Assert(d_sharedSolver != nullptr);
+ d_sharedSolver->preRegisterShared(preprocessed, multipleTheories);
}
// Leaving pre-register
void TheoryEngine::dumpAssertions(const char* tag) {
if (Dump.isOn(tag)) {
- Dump(tag) << CommentCommand("Starting completeness check");
+ const Printer& printer = d_outMgr.getPrinter();
+ std::ostream& out = d_outMgr.getDumpOut();
+ printer.toStreamCmdComment(out, "Starting completeness check");
for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
Theory* theory = d_theoryTable[theoryId];
if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
- Dump(tag) << CommentCommand("Completeness check");
- Dump(tag) << PushCommand();
+ printer.toStreamCmdComment(out, "Completeness check");
+ printer.toStreamCmdPush(out);
// Dump the shared terms
if (d_logicInfo.isSharingEnabled()) {
- Dump(tag) << CommentCommand("Shared terms");
+ printer.toStreamCmdComment(out, "Shared terms");
context::CDList<TNode>::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end();
for (unsigned i = 0; it != it_end; ++ it, ++i) {
stringstream ss;
ss << (*it);
- Dump(tag) << CommentCommand(ss.str());
+ printer.toStreamCmdComment(out, ss.str());
}
}
// Dump the assertions
- Dump(tag) << CommentCommand("Assertions");
+ printer.toStreamCmdComment(out, "Assertions");
context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
for (; it != it_end; ++ it) {
// Get the assertion
if ((*it).d_isPreregistered)
{
- Dump(tag) << CommentCommand("Preregistered");
+ printer.toStreamCmdComment(out, "Preregistered");
}
else
{
- Dump(tag) << CommentCommand("Shared assertion");
+ printer.toStreamCmdComment(out, "Shared assertion");
}
- Dump(tag) << AssertCommand(assertionNode.toExpr());
+ printer.toStreamCmdAssert(out, assertionNode);
}
- Dump(tag) << CheckSatCommand();
+ printer.toStreamCmdCheckSat(out);
- Dump(tag) << PopCommand();
+ printer.toStreamCmdPop(out);
}
}
}
#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
#undef CVC4_FOR_EACH_THEORY_STATEMENT
#endif
-#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
- if (theory::TheoryTraits<THEORY>::hasCheck && d_logicInfo.isTheoryEnabled(THEORY)) { \
- theoryOf(THEORY)->check(effort); \
- if (d_inConflict) { \
- Debug("conflict") << THEORY << " in conflict. " << std::endl; \
- break; \
- } \
- }
+#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
+ if (theory::TheoryTraits<THEORY>::hasCheck \
+ && d_logicInfo.isTheoryEnabled(THEORY)) \
+ { \
+ theoryOf(THEORY)->check(effort); \
+ if (d_inConflict) \
+ { \
+ Debug("conflict") << THEORY << " in conflict. " << std::endl; \
+ break; \
+ } \
+ }
// Do the checking
try {
// If in full effort, we have a fake new assertion just to jumpstart the checking
if (Theory::fullEffort(effort)) {
d_factsAsserted = true;
+ // Reset round for the relevance manager, which notice only sets a flag
+ // to indicate that its information must be recomputed.
+ if (d_relManager != nullptr)
+ {
+ d_relManager->resetRound();
+ }
+ d_tc->resetRound();
}
// Check until done
// Do the checking
CVC4_FOR_EACH_THEORY;
- if(Dump.isOn("missed-t-conflicts")) {
- Dump("missed-t-conflicts")
- << CommentCommand("Completeness check for T-conflicts; expect sat")
- << CheckSatCommand();
- }
-
Debug("theory") << "TheoryEngine::check(" << effort << "): running propagation after the initial check" << endl;
// We are still satisfiable, propagate as much as possible
if (Theory::fullEffort(effort) && d_logicInfo.isSharingEnabled() && !d_factsAsserted && !d_lemmasAdded && !d_inConflict) {
// Do the combination
Debug("theory") << "TheoryEngine::check(" << effort << "): running combination" << endl;
- combineTheories();
+ {
+ TimerStat::CodeTimer combineTheoriesTimer(d_combineTheoriesTime);
+ d_tc->combineTheories();
+ }
if(d_logicInfo.isQuantified()){
d_quantEngine->notifyCombineTheories();
}
if (Trace.isOn("theory::assertions-model")) {
printAssertions("theory::assertions-model");
}
+ // reset the model in the combination engine
+ d_tc->resetModel();
//checks for theories requiring the model go at last call
- d_curr_model->reset();
for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
if( theoryId!=THEORY_QUANTIFIERS ){
Theory* theory = d_theoryTable[theoryId];
if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
if( theory->needsCheckLastEffort() ){
- if( !d_curr_model->isBuilt() ){
- if( !d_curr_model_builder->buildModel(d_curr_model) ){
- break;
- }
+ if (!d_tc->buildModel())
+ {
+ break;
}
theory->check(Theory::EFFORT_LAST_CALL);
}
// are in "SAT mode". We build the model later only if the user asks
// for it via getBuiltModel.
d_inSatMode = true;
- if (d_eager_model_building && !d_curr_model->isBuilt())
+ if (d_eager_model_building)
{
- d_curr_model_builder->buildModel(d_curr_model);
+ d_tc->buildModel();
}
}
}
Debug("theory") << ", need check = " << (needCheck() ? "YES" : "NO") << endl;
if( Theory::fullEffort(effort) && !d_inConflict && !needCheck()) {
- // case where we are about to answer SAT, the master equality engine,
- // if it exists, must be consistent.
- eq::EqualityEngine* mee = d_eeDistributed->getMasterEqualityEngine();
- if (mee != NULL)
- {
- AlwaysAssert(mee->consistent());
- }
- if (d_curr_model->isBuilt())
- {
- // model construction should always succeed unless lemmas were added
- AlwaysAssert(d_curr_model->isBuiltSuccess());
- if (options::produceModels())
- {
- // Do post-processing of model from the theories (used for THEORY_SEP
- // to construct heap model)
- postProcessModel(d_curr_model);
- // also call the model builder's post-process model
- d_curr_model_builder->postProcessModel(d_incomplete.get(),
- d_curr_model);
- }
- }
+ // Do post-processing of model from the theories (e.g. used for THEORY_SEP
+ // to construct heap model)
+ d_tc->postProcessModel(d_incomplete.get());
}
} catch(const theory::Interrupted&) {
Trace("theory") << "TheoryEngine::check() => interrupted" << endl;
}
}
-void TheoryEngine::combineTheories() {
-
- Trace("combineTheories") << "TheoryEngine::combineTheories()" << endl;
-
- TimerStat::CodeTimer combineTheoriesTimer(d_combineTheoriesTime);
-
- // Care graph we'll be building
- CareGraph careGraph;
-
-#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
-#undef CVC4_FOR_EACH_THEORY_STATEMENT
-#endif
-#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
- if (theory::TheoryTraits<THEORY>::isParametric && d_logicInfo.isTheoryEnabled(THEORY)) { \
- theoryOf(THEORY)->getCareGraph(&careGraph); \
- }
-
- // Call on each parametric theory to give us its care graph
- CVC4_FOR_EACH_THEORY;
-
- Trace("combineTheories") << "TheoryEngine::combineTheories(): care graph size = " << careGraph.size() << endl;
-
- // Now add splitters for the ones we are interested in
- CareGraph::const_iterator care_it = careGraph.begin();
- CareGraph::const_iterator care_it_end = careGraph.end();
-
- for (; care_it != care_it_end; ++ care_it) {
- const CarePair& carePair = *care_it;
-
- Debug("combineTheories")
- << "TheoryEngine::combineTheories(): checking " << carePair.d_a << " = "
- << carePair.d_b << " from " << carePair.d_theory << endl;
-
- Assert(d_sharedTerms.isShared(carePair.d_a) || carePair.d_a.isConst());
- Assert(d_sharedTerms.isShared(carePair.d_b) || carePair.d_b.isConst());
-
- // The equality in question (order for no repetition)
- Node equality = carePair.d_a.eqNode(carePair.d_b);
- // EqualityStatus es = getEqualityStatus(carePair.d_a, carePair.d_b);
- // Debug("combineTheories") << "TheoryEngine::combineTheories(): " <<
- // (es == EQUALITY_TRUE_AND_PROPAGATED ? "EQUALITY_TRUE_AND_PROPAGATED" :
- // es == EQUALITY_FALSE_AND_PROPAGATED ? "EQUALITY_FALSE_AND_PROPAGATED" :
- // es == EQUALITY_TRUE ? "EQUALITY_TRUE" :
- // es == EQUALITY_FALSE ? "EQUALITY_FALSE" :
- // es == EQUALITY_TRUE_IN_MODEL ? "EQUALITY_TRUE_IN_MODEL" :
- // es == EQUALITY_FALSE_IN_MODEL ? "EQUALITY_FALSE_IN_MODEL" :
- // es == EQUALITY_UNKNOWN ? "EQUALITY_UNKNOWN" :
- // "Unexpected case") << endl;
-
- // We need to split on it
- Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << endl;
-
- lemma(equality.orNode(equality.notNode()),
- RULE_INVALID,
- false,
- LemmaProperty::NONE,
- carePair.d_theory);
-
- // This code is supposed to force preference to follow what the theory models already have
- // but it doesn't seem to make a big difference - need to explore more -Clark
- // if (true) {
- // if (es == EQUALITY_TRUE || es == EQUALITY_TRUE_IN_MODEL) {
- Node e = ensureLiteral(equality);
- d_propEngine->requirePhase(e, true);
- // }
- // else if (es == EQUALITY_FALSE_IN_MODEL) {
- // Node e = ensureLiteral(equality);
- // d_propEngine->requirePhase(e, false);
- // }
- // }
- }
-}
-
-void TheoryEngine::propagate(Theory::Effort effort) {
+void TheoryEngine::propagate(Theory::Effort effort)
+{
// Reset the interrupt flag
d_interrupted = false;
// Propagate for each theory using the statement above
CVC4_FOR_EACH_THEORY;
-
- if(Dump.isOn("missed-t-propagations")) {
- for(unsigned i = 0; i < d_possiblePropagations.size(); ++i) {
- Node atom = d_possiblePropagations[i];
- bool value;
- if(d_propEngine->hasValue(atom, value)) {
- continue;
- }
- // Doesn't have a value, check it (and the negation)
- if(d_hasPropagated.find(atom) == d_hasPropagated.end()) {
- Dump("missed-t-propagations")
- << CommentCommand("Completeness check for T-propagations; expect invalid")
- << EchoCommand(atom.toString())
- << QueryCommand(atom.toExpr())
- << EchoCommand(atom.notNode().toString())
- << QueryCommand(atom.notNode().toExpr());
- }
- }
- }
}
Node TheoryEngine::getNextDecisionRequest()
return true;
}
-bool TheoryEngine::properPropagation(TNode lit) const {
- if(!getPropEngine()->isSatLiteral(lit)) {
- return false;
- }
- bool b;
- return !getPropEngine()->hasValue(lit, b);
-}
-
-bool TheoryEngine::properExplanation(TNode node, TNode expl) const {
- // Explanation must be either a conjunction of true literals that have true SAT values already
- // or a singled literal that has a true SAT value already.
- if (expl.getKind() == kind::AND) {
- for (unsigned i = 0; i < expl.getNumChildren(); ++ i) {
- bool value;
- if (!d_propEngine->hasValue(expl[i], value) || !value) {
- return false;
- }
- }
- } else {
- bool value;
- return d_propEngine->hasValue(expl, value) && value;
- }
- return true;
-}
-
-bool TheoryEngine::collectModelInfo(theory::TheoryModel* m)
+TheoryModel* TheoryEngine::getModel()
{
- //have shared term engine collectModelInfo
- // d_sharedTerms.collectModelInfo( m );
- // Consult each active theory to get all relevant information
- // concerning the model.
- for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) {
- if(d_logicInfo.isTheoryEnabled(theoryId)) {
- Trace("model-builder") << " CollectModelInfo on theory: " << theoryId << endl;
- if (!d_theoryTable[theoryId]->collectModelInfo(m))
- {
- return false;
- }
- }
- }
- Trace("model-builder") << " CollectModelInfo boolean variables" << std::endl;
- // Get the Boolean variables
- vector<TNode> boolVars;
- d_propEngine->getBooleanVariables(boolVars);
- vector<TNode>::iterator it, iend = boolVars.end();
- bool hasValue, value;
- for (it = boolVars.begin(); it != iend; ++it) {
- TNode var = *it;
- hasValue = d_propEngine->hasValue(var, value);
- // TODO: Assert that hasValue is true?
- if (!hasValue) {
- Trace("model-builder-assertions")
- << " has no value : " << var << std::endl;
- value = false;
- }
- Trace("model-builder-assertions") << "(assert" << (value ? " " : " (not ") << var << (value ? ");" : "));") << endl;
- if (!m->assertPredicate(var, value))
- {
- return false;
- }
- }
- return true;
-}
-
-void TheoryEngine::postProcessModel( theory::TheoryModel* m ){
- for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) {
- if(d_logicInfo.isTheoryEnabled(theoryId)) {
- Trace("model-builder-debug") << " PostProcessModel on theory: " << theoryId << endl;
- d_theoryTable[theoryId]->postProcessModel( m );
- }
- }
-}
-
-TheoryModel* TheoryEngine::getModel() {
- return d_curr_model;
+ Assert(d_tc != nullptr);
+ TheoryModel* m = d_tc->getModel();
+ Assert(m != nullptr);
+ return m;
}
TheoryModel* TheoryEngine::getBuiltModel()
{
- if (!d_curr_model->isBuilt())
+ Assert(d_tc != nullptr);
+ // If this method was called, we should be in SAT mode, and produceModels
+ // should be true.
+ AlwaysAssert(options::produceModels());
+ if (!d_inSatMode)
{
- // If this method was called, we should be in SAT mode, and produceModels
- // should be true.
- AlwaysAssert(options::produceModels());
- if (!d_inSatMode)
- {
- // not available, perhaps due to interuption.
- return nullptr;
- }
- // must build model at this point
- d_curr_model_builder->buildModel(d_curr_model);
+ // not available, perhaps due to interuption.
+ return nullptr;
+ }
+ // must build model at this point
+ if (!d_tc->buildModel())
+ {
+ return nullptr;
}
- return d_curr_model;
+ return d_tc->getModel();
}
-bool TheoryEngine::getSynthSolutions(
- std::map<Node, std::map<Node, Node>>& sol_map)
+bool TheoryEngine::buildModel()
{
- if (d_quantEngine)
- {
- return d_quantEngine->getSynthSolutions(sol_map);
- }
- // we are not in a quantified logic, there is no synthesis solution
- return false;
+ Assert(d_tc != nullptr);
+ return d_tc->buildModel();
}
bool TheoryEngine::presolve() {
CVC4_FOR_EACH_THEORY;
}
+bool TheoryEngine::isRelevant(Node lit) const
+{
+ if (d_relManager != nullptr)
+ {
+ return d_relManager->isRelevant(lit);
+ }
+ // otherwise must assume its relevant
+ return true;
+}
+
void TheoryEngine::shutdown() {
// Set this first; if a Theory shutdown() throws an exception,
// at least the destruction of the TheoryEngine won't confound
theoryOf(theoryId)->shutdown();
}
}
-
- d_tpp.clearCache();
}
-theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitutionOut) {
+theory::Theory::PPAssertStatus TheoryEngine::solve(
+ TrustNode tliteral, TrustSubstitutionMap& substitutionOut)
+{
// Reset the interrupt flag
d_interrupted = false;
+ TNode literal = tliteral.getNode();
TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
Trace("theory::solve") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << endl;
throw LogicException(ss.str());
}
- Theory::PPAssertStatus solveStatus = theoryOf(atom)->ppAssert(literal, substitutionOut);
+ Theory::PPAssertStatus solveStatus =
+ theoryOf(atom)->ppAssert(tliteral, substitutionOut);
Trace("theory::solve") << "TheoryEngine::solve(" << literal << ") => " << solveStatus << endl;
return solveStatus;
}
-void TheoryEngine::preprocessStart() { d_tpp.clearCache(); }
-
-Node TheoryEngine::preprocess(TNode assertion) {
- TrustNode trn = d_tpp.theoryPreprocess(assertion);
- if (trn.isNull())
- {
- // no change
- return assertion;
- }
- return trn.getNode();
+theory::TrustNode TheoryEngine::ppRewriteEquality(TNode eq)
+{
+ Assert(eq.getKind() == kind::EQUAL);
+ return theoryOf(eq)->ppRewrite(eq);
}
void TheoryEngine::notifyPreprocessedAssertions(
theoryOf(theoryId)->ppNotifyAssertions(assertions);
}
}
+ if (d_relManager != nullptr)
+ {
+ d_relManager->notifyPreprocessedAssertions(assertions);
+ }
}
bool TheoryEngine::markPropagation(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId) {
return;
}
- // Polarity of the assertion
- bool polarity = assertion.getKind() != kind::NOT;
-
- // Atom of the assertion
- TNode atom = polarity ? assertion : assertion[0];
-
// If sending to the shared terms database, it's also simple
if (toTheoryId == THEORY_BUILTIN) {
- Assert(atom.getKind() == kind::EQUAL)
- << "atom should be an EQUALity, not `" << atom << "'";
+ Assert(assertion.getKind() == kind::EQUAL
+ || (assertion.getKind() == kind::NOT
+ && assertion[0].getKind() == kind::EQUAL))
+ << "atom should be an EQUALity, not `" << assertion << "'";
if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) {
- d_sharedTerms.assertEquality(atom, polarity, assertion);
+ // assert to the shared solver
+ bool polarity = assertion.getKind() != kind::NOT;
+ TNode atom = polarity ? assertion : assertion[0];
+ d_sharedSolver->assertSharedEquality(atom, polarity, assertion);
}
return;
}
return;
}
- Assert(atom.getKind() == kind::EQUAL);
+ Assert(assertion.getKind() == kind::EQUAL
+ || (assertion.getKind() == kind::NOT
+ && assertion[0].getKind() == kind::EQUAL));
// Normalize
Node normalizedLiteral = Rewriter::rewrite(assertion);
if (!normalizedLiteral.getConst<bool>()) {
// Mark the propagation for explanations
if (markPropagation(normalizedLiteral, originalAssertion, toTheoryId, fromTheoryId)) {
+ // special case, trust node has no proof generator
+ TrustNode trnn = TrustNode::mkTrustConflict(normalizedLiteral);
// Get the explanation (conflict will figure out where it came from)
- conflict(normalizedLiteral, toTheoryId);
+ conflict(trnn, toTheoryId);
} else {
Unreachable();
}
TNode atom = polarity ? literal : literal[0];
if (d_logicInfo.isSharingEnabled()) {
-
// If any shared terms, it's time to do sharing work
- if (d_sharedTerms.hasSharedTerms(atom)) {
- // Notify the theories the shared terms
- SharedTermsDatabase::shared_terms_iterator it = d_sharedTerms.begin(atom);
- SharedTermsDatabase::shared_terms_iterator it_end = d_sharedTerms.end(atom);
- for (; it != it_end; ++ it) {
- TNode term = *it;
- Theory::Set theories = d_sharedTerms.getTheoriesToNotify(atom, term);
- for (TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++ id) {
- if (Theory::setContains(id, theories)) {
- theoryOf(id)->addSharedTermInternal(term);
- }
- }
- d_sharedTerms.markNotified(term, theories);
- }
- }
+ d_sharedSolver->preNotifySharedFact(atom);
// If it's an equality, assert it to the shared term manager, even though the terms are not
// yet shared. As the terms become shared later, the shared terms manager will then add them
if (atom.getKind() == kind::EQUAL) {
// Assert it to the the owning theory
assertToTheory(literal, literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER);
- // Shared terms manager will assert to interested theories directly, as the terms become shared
+ // Shared terms manager will assert to interested theories directly, as
+ // the terms become shared
assertToTheory(literal, literal, /* to */ THEORY_BUILTIN, /* from */ THEORY_SAT_SOLVER);
// Now, let's check for any atom triggers from lemmas
}
bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
-
Debug("theory::propagate") << "TheoryEngine::propagate(" << literal << ", " << theory << ")" << endl;
Trace("dtview::prop") << std::string(d_context->getLevel(), ' ')
// spendResource();
- if(Dump.isOn("t-propagations")) {
- Dump("t-propagations") << CommentCommand("negation of theory propagation: expect valid")
- << QueryCommand(literal.toExpr());
- }
- if(Dump.isOn("missed-t-propagations")) {
- d_hasPropagated.insert(literal);
- }
-
// Get the atom
bool polarity = literal.getKind() != kind::NOT;
TNode atom = polarity ? literal : literal[0];
assertToTheory(literal, literal, /* to */ THEORY_BUILTIN, /* from */ theory);
}
} else {
- // We could be propagating a unit-clause lemma. In this case, we need to provide a
- // recipe.
- // TODO: Consider putting this someplace else? This is the only refence to the proof
- // manager in this class.
-
- PROOF({
- LemmaProofRecipe proofRecipe;
- proofRecipe.addBaseAssertion(literal);
-
- Node emptyNode;
- LemmaProofRecipe::ProofStep proofStep(theory, emptyNode);
- proofStep.addAssertion(literal);
- proofRecipe.addStep(proofStep);
-
- ProofManager::getCnfProof()->setProofRecipe(&proofRecipe);
- });
-
// Just send off to the SAT solver
Assert(d_propEngine->isSatLiteral(literal));
assertToTheory(literal, literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory);
const LogicInfo& TheoryEngine::getLogicInfo() const { return d_logicInfo; }
-theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) {
- Assert(a.getType().isComparableTo(b.getType()));
- if (d_sharedTerms.isShared(a) && d_sharedTerms.isShared(b)) {
- if (d_sharedTerms.areEqual(a,b)) {
- return EQUALITY_TRUE_AND_PROPAGATED;
- }
- else if (d_sharedTerms.areDisequal(a,b)) {
- return EQUALITY_FALSE_AND_PROPAGATED;
- }
- }
- return theoryOf(Theory::theoryOf(a.getType()))->getEqualityStatus(a, b);
-}
-
-Node TheoryEngine::getModelValue(TNode var) {
- if (var.isConst())
+bool TheoryEngine::getSepHeapTypes(TypeNode& locType, TypeNode& dataType) const
+{
+ if (d_sepLocType.isNull())
{
- // the model value of a constant must be itself
- return var;
- }
- Assert(d_sharedTerms.isShared(var));
- return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var);
-}
-
-
-Node TheoryEngine::ensureLiteral(TNode n) {
- Debug("ensureLiteral") << "rewriting: " << n << std::endl;
- Node rewritten = Rewriter::rewrite(n);
- Debug("ensureLiteral") << " got: " << rewritten << std::endl;
- Node preprocessed = preprocess(rewritten);
- Debug("ensureLiteral") << "preprocessed: " << preprocessed << std::endl;
- d_propEngine->ensureLiteral(preprocessed);
- return preprocessed;
-}
-
-
-void TheoryEngine::printInstantiations( std::ostream& out ) {
- if( d_quantEngine ){
- d_quantEngine->printInstantiations( out );
- }else{
- out << "Internal error : instantiations not available when quantifiers are not present." << std::endl;
- Assert(false);
- }
-}
-
-void TheoryEngine::printSynthSolution( std::ostream& out ) {
- if( d_quantEngine ){
- d_quantEngine->printSynthSolution( out );
- }else{
- out << "Internal error : synth solution not available when quantifiers are not present." << std::endl;
- Assert(false);
- }
-}
-
-void TheoryEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ) {
- if( d_quantEngine ){
- d_quantEngine->getInstantiatedQuantifiedFormulas( qs );
- }else{
- Assert(false);
+ return false;
}
+ locType = d_sepLocType;
+ dataType = d_sepDataType;
+ return true;
}
-void TheoryEngine::getInstantiations( Node q, std::vector< Node >& insts ) {
- if( d_quantEngine ){
- d_quantEngine->getInstantiations( q, insts );
- }else{
- Assert(false);
+void TheoryEngine::declareSepHeap(TypeNode locT, TypeNode dataT)
+{
+ Theory* tsep = theoryOf(THEORY_SEP);
+ if (tsep == nullptr)
+ {
+ Assert(false) << "TheoryEngine::declareSepHeap called without the "
+ "separation logic theory enabled";
+ return;
}
-}
-void TheoryEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) {
- if( d_quantEngine ){
- d_quantEngine->getInstantiationTermVectors( q, tvecs );
- }else{
- Assert(false);
- }
-}
+ // Definition of the statement that is to be run by every theory
+#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
+#undef CVC4_FOR_EACH_THEORY_STATEMENT
+#endif
+#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
+ theoryOf(THEORY)->declareSepHeap(locT, dataT);
-void TheoryEngine::getInstantiations( std::map< Node, std::vector< Node > >& insts ) {
- if( d_quantEngine ){
- d_quantEngine->getInstantiations( insts );
- }else{
- Assert(false);
- }
-}
+ // notify each theory using the statement above
+ CVC4_FOR_EACH_THEORY;
-void TheoryEngine::getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ) {
- if( d_quantEngine ){
- d_quantEngine->getInstantiationTermVectors( insts );
- }else{
- Assert(false);
- }
+ // remember the types we have set
+ d_sepLocType = locT;
+ d_sepDataType = dataT;
}
-Node TheoryEngine::getInstantiatedConjunction( Node q ) {
- if( d_quantEngine ){
- return d_quantEngine->getInstantiatedConjunction( q );
- }else{
- Assert(false);
- return Node::null();
- }
+theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) {
+ Assert(a.getType().isComparableTo(b.getType()));
+ return d_sharedSolver->getEqualityStatus(a, b);
}
-
-static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) {
-
- std::set<TNode> all;
- for (unsigned i = 0; i < explanation.size(); ++ i) {
- Assert(explanation[i].d_theory == THEORY_SAT_SOLVER);
- all.insert(explanation[i].d_node);
- }
-
- if (all.size() == 0) {
- // Normalize to true
- return NodeManager::currentNM()->mkConst<bool>(true);
- }
-
- if (all.size() == 1) {
- // All the same, or just one
- return explanation[0].d_node;
- }
-
- NodeBuilder<> conjunction(kind::AND);
- std::set<TNode>::const_iterator it = all.begin();
- std::set<TNode>::const_iterator it_end = all.end();
- while (it != it_end) {
- conjunction << *it;
- ++ it;
+Node TheoryEngine::getModelValue(TNode var) {
+ if (var.isConst())
+ {
+ // the model value of a constant must be itself
+ return var;
}
-
- return conjunction;
+ Assert(d_sharedSolver->isShared(var));
+ return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var);
}
-Node TheoryEngine::getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRecipe) {
- Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << "): current propagation index = " << d_propagationMapTimestamp << endl;
-
+TrustNode TheoryEngine::getExplanation(TNode node)
+{
+ Debug("theory::explain") << "TheoryEngine::getExplanation(" << node
+ << "): current propagation index = "
+ << d_propagationMapTimestamp << endl;
bool polarity = node.getKind() != kind::NOT;
TNode atom = polarity ? node : node[0];
// If we're not in shared mode, explanations are simple
- if (!d_logicInfo.isSharingEnabled()) {
- Debug("theory::explain") << "TheoryEngine::getExplanation: sharing is NOT enabled. "
- << " Responsible theory is: "
- << theoryOf(atom)->getId() << std::endl;
+ if (!d_logicInfo.isSharingEnabled())
+ {
+ Debug("theory::explain")
+ << "TheoryEngine::getExplanation: sharing is NOT enabled. "
+ << " Responsible theory is: " << theoryOf(atom)->getId() << std::endl;
TrustNode texplanation = theoryOf(atom)->explain(node);
Node explanation = texplanation.getNode();
- Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << endl;
- PROOF({
- if(proofRecipe) {
- Node emptyNode;
- LemmaProofRecipe::ProofStep proofStep(theoryOf(atom)->getId(), emptyNode);
- proofStep.addAssertion(node);
- proofRecipe->addBaseAssertion(node);
-
- if (explanation.getKind() == kind::AND) {
- // If the explanation is a conjunction, the recipe for the corresponding lemma is
- // the negation of its conjuncts.
- Node flat = flattenAnd(explanation);
- for (unsigned i = 0; i < flat.getNumChildren(); ++i) {
- if (flat[i].isConst() && flat[i].getConst<bool>()) {
- ++ i;
- continue;
- }
- if (flat[i].getKind() == kind::NOT &&
- flat[i][0].isConst() && !flat[i][0].getConst<bool>()) {
- ++ i;
- continue;
- }
- Debug("theory::explain") << "TheoryEngine::getExplanationAndRecipe: adding recipe assertion: "
- << flat[i].negate() << std::endl;
- proofStep.addAssertion(flat[i].negate());
- proofRecipe->addBaseAssertion(flat[i].negate());
- }
- } else {
- // The recipe for proving it is by negating it. "True" is not an acceptable reason.
- if (!((explanation.isConst() && explanation.getConst<bool>()) ||
- (explanation.getKind() == kind::NOT &&
- explanation[0].isConst() && !explanation[0].getConst<bool>()))) {
- proofStep.addAssertion(explanation.negate());
- proofRecipe->addBaseAssertion(explanation.negate());
- }
- }
-
- proofRecipe->addStep(proofStep);
- }
- });
-
- return explanation;
+ Debug("theory::explain") << "TheoryEngine::getExplanation(" << node
+ << ") => " << explanation << endl;
+ if (isProofEnabled())
+ {
+ texplanation.debugCheckClosed(
+ "te-proof-exp", "texplanation no share", false);
+ // check if no generator, if so, add THEORY_LEMMA
+ if (texplanation.getGenerator() == nullptr)
+ {
+ Node proven = texplanation.getProven();
+ TheoryId tid = theoryOf(atom)->getId();
+ Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(tid);
+ d_lazyProof->addStep(proven, PfRule::THEORY_LEMMA, {}, {proven, tidn});
+ texplanation =
+ TrustNode::mkTrustPropExp(node, explanation, d_lazyProof.get());
+ }
+ }
+ return texplanation;
}
- Debug("theory::explain") << "TheoryEngine::getExplanation: sharing IS enabled" << std::endl;
+ Debug("theory::explain") << "TheoryEngine::getExplanation: sharing IS enabled"
+ << std::endl;
// Initial thing to explain
NodeTheoryPair toExplain(node, THEORY_SAT_SOLVER, d_propagationMapTimestamp);
<< "TheoryEngine::getExplanation: explainer for node "
<< nodeExplainerPair.d_node
<< " is theory: " << nodeExplainerPair.d_theory << std::endl;
- TheoryId explainer = nodeExplainerPair.d_theory;
// Create the workplace for explanations
- std::vector<NodeTheoryPair> explanationVector;
- explanationVector.push_back(d_propagationMap[toExplain]);
+ std::vector<NodeTheoryPair> vec{d_propagationMap[toExplain]};
// Process the explanation
- if (proofRecipe) {
- Node emptyNode;
- LemmaProofRecipe::ProofStep proofStep(explainer, emptyNode);
- proofStep.addAssertion(node);
- proofRecipe->addStep(proofStep);
- proofRecipe->addBaseAssertion(node);
- }
-
- getExplanation(explanationVector, proofRecipe);
- Node explanation = mkExplanation(explanationVector);
-
- Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << endl;
-
- return explanation;
-}
-
-Node TheoryEngine::getExplanation(TNode node) {
- LemmaProofRecipe *dontCareRecipe = NULL;
- return getExplanationAndRecipe(node, dontCareRecipe);
+ TrustNode texplanation = getExplanation(vec);
+ Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => "
+ << texplanation.getNode() << endl;
+ return texplanation;
}
struct AtomsCollect {
}
}
-theory::LemmaStatus TheoryEngine::lemma(TNode node,
- ProofRule rule,
- bool negated,
- theory::LemmaProperty p,
- theory::TheoryId atomsTo)
+void TheoryEngine::lemma(theory::TrustNode tlemma,
+ theory::LemmaProperty p,
+ theory::TheoryId atomsTo,
+ theory::TheoryId from)
{
// For resource-limiting (also does a time check).
// spendResource();
+ Assert(tlemma.getKind() == TrustNodeKind::LEMMA
+ || tlemma.getKind() == TrustNodeKind::CONFLICT);
+ // get the node
+ Node node = tlemma.getNode();
+ Node lemma = tlemma.getProven();
+ Trace("te-lemma") << "Lemma, input: " << lemma << ", property = " << p
+ << std::endl;
+
+ Assert(!expr::hasFreeVar(lemma));
+
+ // when proofs are enabled, we ensure the trust node has a generator by
+ // adding a trust step to the lazy proof maintained by this class
+ if (isProofEnabled())
+ {
+ // ensure proof: set THEORY_LEMMA if no generator is provided
+ if (tlemma.getGenerator() == nullptr)
+ {
+ // internal lemmas should have generators
+ Assert(from != THEORY_LAST);
+ // add theory lemma step to proof
+ Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(from);
+ d_lazyProof->addStep(lemma, PfRule::THEORY_LEMMA, {}, {lemma, tidn});
+ // update the trust node
+ tlemma = TrustNode::mkTrustLemma(lemma, d_lazyProof.get());
+ }
+ // ensure closed
+ tlemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma_initial");
+ }
// Do we need to check atoms
if (atomsTo != theory::THEORY_LAST) {
}
if(Dump.isOn("t-lemmas")) {
- Node n = node;
- if (!negated) {
- n = node.negate();
- }
- Dump("t-lemmas") << CommentCommand("theory lemma: expect valid")
- << CheckSatCommand(n.toExpr());
- }
- bool removable = isLemmaPropertyRemovable(p);
- bool preprocess = isLemmaPropertyPreprocess(p);
-
- // call preprocessor
- std::vector<TrustNode> newLemmas;
- std::vector<Node> newSkolems;
- TrustNode tlemma = d_tpp.preprocess(node, newLemmas, newSkolems, preprocess);
-
- // !!!!!!! temporary, until this method is fully updated from proof-new
- if (tlemma.isNull())
- {
- tlemma = TrustNode::mkTrustLemma(node);
+ // we dump the negation of the lemma, to show validity of the lemma
+ Node n = lemma.negate();
+ const Printer& printer = d_outMgr.getPrinter();
+ std::ostream& out = d_outMgr.getDumpOut();
+ printer.toStreamCmdComment(out, "theory lemma: expect valid");
+ printer.toStreamCmdCheckSat(out, n);
}
- // must use an assertion pipeline due to decision engine below
- AssertionPipeline lemmas;
- // make the assertion pipeline
- lemmas.push_back(tlemma.getNode());
- lemmas.updateRealAssertionsEnd();
- Assert(newSkolems.size() == newLemmas.size());
- for (size_t i = 0, nsize = newLemmas.size(); i < nsize; i++)
- {
- // store skolem mapping here
- IteSkolemMap& imap = lemmas.getIteSkolemMap();
- imap[newSkolems[i]] = lemmas.size();
- lemmas.push_back(newLemmas[i].getNode());
- }
-
- // assert lemmas to prop engine
- for (size_t i = 0, lsize = lemmas.size(); i < lsize; ++i)
- {
- d_propEngine->assertLemma(
- lemmas[i], i == 0 && negated, removable, rule, node);
- }
-
- // WARNING: Below this point don't assume lemmas[0] to be not negated.
- if(negated) {
- lemmas.replace(0, lemmas[0].notNode());
- negated = false;
- }
+ // assert the lemma
+ d_propEngine->assertLemma(tlemma, p);
- // assert to decision engine
- if (!removable)
+ // If specified, we must add this lemma to the set of those that need to be
+ // justified, where note we pass all auxiliary lemmas in skAsserts as well,
+ // since these by extension must be justified as well.
+ if (d_relManager != nullptr && isLemmaPropertyNeedsJustify(p))
{
- d_propEngine->addAssertionsToDecisionEngine(lemmas);
+ std::vector<Node> skAsserts;
+ std::vector<Node> sks;
+ Node retLemma =
+ d_propEngine->getPreprocessedTerm(tlemma.getProven(), skAsserts, sks);
+ d_relManager->notifyPreprocessedAssertion(retLemma);
+ d_relManager->notifyPreprocessedAssertions(skAsserts);
}
// Mark that we added some lemmas
d_lemmasAdded = true;
-
- // Lemma analysis isn't online yet; this lemma may only live for this
- // user level.
- Node retLemma = lemmas[0];
- if (lemmas.size() > 1)
- {
- // the returned lemma is the conjunction of all additional lemmas.
- retLemma = NodeManager::currentNM()->mkNode(kind::AND, lemmas.ref());
- }
- return theory::LemmaStatus(retLemma, d_userContext->getLevel());
}
-void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
-
- Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << ")" << endl;
+void TheoryEngine::conflict(theory::TrustNode tconflict, TheoryId theoryId)
+{
+ Assert(tconflict.getKind() == TrustNodeKind::CONFLICT);
+ TNode conflict = tconflict.getNode();
+ Trace("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", "
+ << theoryId << ")" << endl;
+ Trace("te-proof-debug") << "Check closed conflict" << std::endl;
+ // doesn't require proof generator, yet, since THEORY_LEMMA is added below
+ tconflict.debugCheckClosed(
+ "te-proof-debug", "TheoryEngine::conflict_initial", false);
Trace("dtview::conflict") << ":THEORY-CONFLICT: " << conflict << std::endl;
d_inConflict = true;
if(Dump.isOn("t-conflicts")) {
- Dump("t-conflicts") << CommentCommand("theory conflict: expect unsat")
- << CheckSatCommand(conflict.toExpr());
+ const Printer& printer = d_outMgr.getPrinter();
+ std::ostream& out = d_outMgr.getDumpOut();
+ printer.toStreamCmdComment(out, "theory conflict: expect unsat");
+ printer.toStreamCmdCheckSat(out, conflict);
}
- LemmaProofRecipe* proofRecipe = NULL;
- PROOF({
- proofRecipe = new LemmaProofRecipe;
- Node emptyNode;
- LemmaProofRecipe::ProofStep proofStep(theoryId, emptyNode);
-
- if (conflict.getKind() == kind::AND) {
- for (unsigned i = 0; i < conflict.getNumChildren(); ++i) {
- proofStep.addAssertion(conflict[i].negate());
- }
- } else {
- proofStep.addAssertion(conflict.negate());
- }
-
- proofRecipe->addStep(proofStep);
- });
-
// In the multiple-theories case, we need to reconstruct the conflict
if (d_logicInfo.isSharingEnabled()) {
// Create the workplace for explanations
- std::vector<NodeTheoryPair> explanationVector;
- explanationVector.push_back(NodeTheoryPair(conflict, theoryId, d_propagationMapTimestamp));
+ std::vector<NodeTheoryPair> vec;
+ vec.push_back(
+ NodeTheoryPair(conflict, theoryId, d_propagationMapTimestamp));
// Process the explanation
- getExplanation(explanationVector, proofRecipe);
- PROOF(ProofManager::getCnfProof()->setProofRecipe(proofRecipe));
- Node fullConflict = mkExplanation(explanationVector);
+ TrustNode tncExp = getExplanation(vec);
+ Trace("te-proof-debug")
+ << "Check closed conflict explained with sharing" << std::endl;
+ tncExp.debugCheckClosed("te-proof-debug",
+ "TheoryEngine::conflict_explained_sharing");
+ Node fullConflict = tncExp.getNode();
+
+ if (isProofEnabled())
+ {
+ Trace("te-proof-debug") << "Process conflict: " << conflict << std::endl;
+ Trace("te-proof-debug") << "Conflict " << tconflict << " from "
+ << tconflict.identifyGenerator() << std::endl;
+ Trace("te-proof-debug") << "Explanation " << tncExp << " from "
+ << tncExp.identifyGenerator() << std::endl;
+ Assert(d_lazyProof != nullptr);
+ if (tconflict.getGenerator() != nullptr)
+ {
+ d_lazyProof->addLazyStep(tconflict.getProven(),
+ tconflict.getGenerator());
+ }
+ else
+ {
+ // add theory lemma step
+ Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId);
+ Node conf = tconflict.getProven();
+ d_lazyProof->addStep(conf, PfRule::THEORY_LEMMA, {}, {conf, tidn});
+ }
+ // store the explicit step, which should come from a different
+ // generator, e.g. d_tepg.
+ Node proven = tncExp.getProven();
+ Assert(tncExp.getGenerator() != d_lazyProof.get());
+ Trace("te-proof-debug") << "add lazy step " << tncExp.identifyGenerator()
+ << " for " << proven << std::endl;
+ d_lazyProof->addLazyStep(proven, tncExp.getGenerator());
+ pfgEnsureClosed(proven,
+ d_lazyProof.get(),
+ "te-proof-debug",
+ "TheoryEngine::conflict_during");
+ Node fullConflictNeg = fullConflict.notNode();
+ std::vector<Node> children;
+ children.push_back(proven);
+ std::vector<Node> args;
+ args.push_back(fullConflictNeg);
+ if (conflict == d_false)
+ {
+ AlwaysAssert(proven == fullConflictNeg);
+ }
+ else
+ {
+ if (fullConflict != conflict)
+ {
+ // ------------------------- explained ---------- from theory
+ // fullConflict => conflict ~conflict
+ // ------------------------------------------ MACRO_SR_PRED_TRANSFORM
+ // ~fullConflict
+ children.push_back(conflict.notNode());
+ args.push_back(mkMethodId(MethodId::SB_LITERAL));
+ d_lazyProof->addStep(
+ fullConflictNeg, PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
+ }
+ }
+ }
+ // pass the processed trust node
+ TrustNode tconf =
+ TrustNode::mkTrustConflict(fullConflict, d_lazyProof.get());
Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl;
Assert(properConflict(fullConflict));
- lemma(fullConflict,
- RULE_CONFLICT,
- true,
- LemmaProperty::REMOVABLE,
- THEORY_LAST);
+ Trace("te-proof-debug")
+ << "Check closed conflict with sharing" << std::endl;
+ tconf.debugCheckClosed("te-proof-debug", "TheoryEngine::conflict:sharing");
+ lemma(tconf, LemmaProperty::REMOVABLE);
} else {
// When only one theory, the conflict should need no processing
Assert(properConflict(conflict));
- PROOF({
- if (conflict.getKind() == kind::AND) {
- // If the conflict is a conjunction, the corresponding lemma is derived by negating
- // its conjuncts.
- for (unsigned i = 0; i < conflict.getNumChildren(); ++i) {
- if (conflict[i].isConst() && conflict[i].getConst<bool>()) {
- ++ i;
- continue;
- }
- if (conflict[i].getKind() == kind::NOT &&
- conflict[i][0].isConst() && !conflict[i][0].getConst<bool>()) {
- ++ i;
- continue;
- }
- proofRecipe->getStep(0)->addAssertion(conflict[i].negate());
- proofRecipe->addBaseAssertion(conflict[i].negate());
- }
- } else {
- proofRecipe->getStep(0)->addAssertion(conflict.negate());
- proofRecipe->addBaseAssertion(conflict.negate());
- }
-
- ProofManager::getCnfProof()->setProofRecipe(proofRecipe);
- });
-
- lemma(conflict, RULE_CONFLICT, true, LemmaProperty::REMOVABLE, THEORY_LAST);
+ // pass the trust node that was sent from the theory
+ lemma(tconflict, LemmaProperty::REMOVABLE, THEORY_LAST, theoryId);
}
-
- PROOF({
- delete proofRecipe;
- proofRecipe = NULL;
- });
}
-void TheoryEngine::staticInitializeBVOptions(
- const std::vector<Node>& assertions)
+theory::TrustNode TheoryEngine::getExplanation(
+ std::vector<NodeTheoryPair>& explanationVector)
{
- bool useSlicer = true;
- if (options::bitvectorEqualitySlicer() == options::BvSlicerMode::ON)
- {
- if (!d_logicInfo.isPure(theory::THEORY_BV) || d_logicInfo.isQuantified())
- throw ModalException(
- "Slicer currently only supports pure QF_BV formulas. Use "
- "--bv-eq-slicer=off");
- if (options::incrementalSolving())
- throw ModalException(
- "Slicer does not currently support incremental mode. Use "
- "--bv-eq-slicer=off");
- if (options::produceModels())
- throw ModalException(
- "Slicer does not currently support model generation. Use "
- "--bv-eq-slicer=off");
- }
- else if (options::bitvectorEqualitySlicer() == options::BvSlicerMode::OFF)
- {
- return;
- }
- else if (options::bitvectorEqualitySlicer() == options::BvSlicerMode::AUTO)
- {
- if ((!d_logicInfo.isPure(theory::THEORY_BV) || d_logicInfo.isQuantified())
- || options::incrementalSolving()
- || options::produceModels())
- return;
-
- bv::utils::TNodeBoolMap cache;
- for (unsigned i = 0; i < assertions.size(); ++i)
- {
- useSlicer = useSlicer && bv::utils::isCoreTerm(assertions[i], cache);
- }
- }
-
- if (useSlicer)
+ Assert(explanationVector.size() == 1);
+ Node conclusion = explanationVector[0].d_node;
+ std::shared_ptr<LazyCDProof> lcp;
+ if (isProofEnabled())
{
- bv::TheoryBV* bv_theory = (bv::TheoryBV*)d_theoryTable[THEORY_BV];
- bv_theory->enableCoreTheorySlicer();
+ Trace("te-proof-exp") << "=== TheoryEngine::getExplanation " << conclusion
+ << std::endl;
+ lcp.reset(new LazyCDProof(
+ d_pnm, nullptr, nullptr, "TheoryEngine::LazyCDProof::getExplanation"));
}
-}
-
-SharedTermsDatabase* TheoryEngine::getSharedTermsDatabase()
-{
- return &d_sharedTerms;
-}
-
-void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector, LemmaProofRecipe* proofRecipe) {
- Assert(explanationVector.size() > 0);
-
unsigned i = 0; // Index of the current literal we are processing
- unsigned j = 0; // Index of the last literal we are keeping
std::unique_ptr<std::set<Node>> inputAssertions = nullptr;
- PROOF({
- if (proofRecipe)
- {
- inputAssertions.reset(
- new std::set<Node>(proofRecipe->getStep(0)->getAssertions()));
- }
- });
+ // the overall explanation
+ std::set<TNode> exp;
+ // vector of trust nodes to explain at the end
+ std::vector<std::pair<TheoryId, TrustNode>> texplains;
// cache of nodes we have already explained by some theory
std::unordered_map<Node, size_t, NodeHashFunction> cache;
cache[toExplain.d_node] = toExplain.d_timestamp;
// If a true constant or a negation of a false constant we can ignore it
- if (toExplain.d_node.isConst() && toExplain.d_node.getConst<bool>())
- {
- ++ i;
- continue;
- }
- if (toExplain.d_node.getKind() == kind::NOT && toExplain.d_node[0].isConst()
- && !toExplain.d_node[0].getConst<bool>())
+ if ((toExplain.d_node.isConst() && toExplain.d_node.getConst<bool>())
+ || (toExplain.d_node.getKind() == kind::NOT
+ && toExplain.d_node[0].isConst()
+ && !toExplain.d_node[0].getConst<bool>()))
{
++ i;
+ // if we are building a proof
+ if (lcp != nullptr)
+ {
+ Trace("te-proof-exp")
+ << "- explain " << toExplain.d_node << " trivially..." << std::endl;
+ // ------------------MACRO_SR_PRED_INTRO
+ // toExplain.d_node
+ std::vector<Node> children;
+ std::vector<Node> args;
+ args.push_back(toExplain.d_node);
+ lcp->addStep(
+ toExplain.d_node, PfRule::MACRO_SR_PRED_INTRO, children, args);
+ }
continue;
}
if (toExplain.d_theory == THEORY_SAT_SOLVER)
{
Debug("theory::explain") << "\tLiteral came from THEORY_SAT_SOLVER. Kepping it." << endl;
- explanationVector[j++] = explanationVector[i++];
+ exp.insert(explanationVector[i++].d_node);
+ // it will be a free assumption in the proof
+ Trace("te-proof-exp") << "- keep " << toExplain.d_node << std::endl;
continue;
}
Debug("theory::explain")
<< "TheoryEngine::explain(): expanding " << toExplain.d_node
<< " got from " << toExplain.d_theory << endl;
- for (unsigned k = 0; k < toExplain.d_node.getNumChildren(); ++k)
+ size_t nchild = toExplain.d_node.getNumChildren();
+ for (size_t k = 0; k < nchild; ++k)
{
NodeTheoryPair newExplain(
toExplain.d_node[k], toExplain.d_theory, toExplain.d_timestamp);
explanationVector.push_back(newExplain);
}
+ if (lcp != nullptr)
+ {
+ Trace("te-proof-exp")
+ << "- AND expand " << toExplain.d_node << std::endl;
+ // delay explanation, use a dummy trust node
+ TrustNode tnAndExp = TrustNode::mkTrustPropExp(
+ toExplain.d_node, toExplain.d_node, nullptr);
+ texplains.push_back(
+ std::pair<TheoryId, TrustNode>(THEORY_LAST, tnAndExp));
+ }
++ i;
continue;
}
explanationVector.push_back((*find).second);
++i;
- PROOF({
- if (toExplain.d_node != (*find).second.d_node)
+ if (lcp != nullptr)
+ {
+ if (!CDProof::isSame(toExplain.d_node, (*find).second.d_node))
{
- Debug("pf::explain")
- << "TheoryEngine::getExplanation: Rewrite alert! toAssert = "
- << toExplain.d_node << ", toExplain = " << (*find).second.d_node
- << std::endl;
-
- if (proofRecipe)
- {
- proofRecipe->addRewriteRule(toExplain.d_node,
- (*find).second.d_node);
- }
+ Trace("te-proof-exp")
+ << "- t-explained cached: " << toExplain.d_node << " by "
+ << (*find).second.d_node << std::endl;
+ // delay explanation, use a dummy trust node that says that
+ // (*find).second.d_node explains toExplain.d_node.
+ TrustNode tnRewExp = TrustNode::mkTrustPropExp(
+ toExplain.d_node, (*find).second.d_node, nullptr);
+ texplains.push_back(
+ std::pair<TheoryId, TrustNode>(THEORY_LAST, tnRewExp));
}
- })
-
+ }
continue;
}
}
-
- Node explanation;
- if (toExplain.d_theory == THEORY_BUILTIN)
- {
- explanation = d_sharedTerms.explain(toExplain.d_node);
- Debug("theory::explain") << "\tTerm was propagated by THEORY_BUILTIN. Explanation: " << explanation << std::endl;
- }
- else
+ // It was produced by the theory, so ask for an explanation
+ TrustNode texplanation =
+ d_sharedSolver->explain(toExplain.d_node, toExplain.d_theory);
+ if (lcp != nullptr)
{
- TrustNode texp = theoryOf(toExplain.d_theory)->explain(toExplain.d_node);
- explanation = texp.getNode();
- Debug("theory::explain") << "\tTerm was propagated by owner theory: "
- << theoryOf(toExplain.d_theory)->getId()
- << ". Explanation: " << explanation << std::endl;
+ texplanation.debugCheckClosed("te-proof-exp", "texplanation", false);
+ Trace("te-proof-exp")
+ << "- t-explained[" << toExplain.d_theory << "]: " << toExplain.d_node
+ << " by " << texplanation.getNode() << std::endl;
+ // if not a trivial explanation
+ if (!CDProof::isSame(texplanation.getNode(), toExplain.d_node))
+ {
+ // We add it to the list of theory explanations, to be processed at
+ // the end of this method. We wait to explain here because it may
+ // be that a later explanation may preempt the need for proving this
+ // step. For instance, if the conclusion lit is later added as an
+ // assumption in the final explanation. This avoids cyclic proofs.
+ texplains.push_back(
+ std::pair<TheoryId, TrustNode>(toExplain.d_theory, texplanation));
+ }
}
+ Node explanation = texplanation.getNode();
Debug("theory::explain")
<< "TheoryEngine::explain(): got explanation " << explanation
explanationVector.push_back(newExplain);
++ i;
+ }
- PROOF({
- if (proofRecipe && inputAssertions)
+ // make the explanation node
+ Node expNode;
+ if (exp.size() == 0)
+ {
+ // Normalize to true
+ expNode = NodeManager::currentNM()->mkConst<bool>(true);
+ }
+ else if (exp.size() == 1)
+ {
+ // All the same, or just one
+ expNode = *exp.begin();
+ }
+ else
+ {
+ NodeBuilder<> conjunction(kind::AND);
+ std::set<TNode>::const_iterator it = exp.begin();
+ std::set<TNode>::const_iterator it_end = exp.end();
+ while (it != it_end)
+ {
+ conjunction << *it;
+ ++it;
+ }
+ expNode = conjunction;
+ }
+ // if we are building a proof, go back through the explanations and
+ // build the proof
+ if (lcp != nullptr)
+ {
+ if (Trace.isOn("te-proof-exp"))
+ {
+ Trace("te-proof-exp") << "Explanation is:" << std::endl;
+ for (TNode e : exp)
+ {
+ Trace("te-proof-exp") << " " << e << std::endl;
+ }
+ Trace("te-proof-exp") << "=== Replay explanations..." << std::endl;
+ }
+ // Now, go back and add the necessary steps of theory explanations, i.e.
+ // add those that prove things that aren't in the final explanation. We
+ // iterate in reverse order so that most recent steps take priority. This
+ // avoids cyclic proofs in the lazy proof we are building (lcp).
+ for (std::vector<std::pair<TheoryId, TrustNode>>::reverse_iterator
+ it = texplains.rbegin(),
+ itEnd = texplains.rend();
+ it != itEnd;
+ ++it)
+ {
+ TrustNode trn = it->second;
+ Assert(trn.getKind() == TrustNodeKind::PROP_EXP);
+ Node proven = trn.getProven();
+ Assert(proven.getKind() == kind::IMPLIES);
+ Node tConc = proven[1];
+ Trace("te-proof-exp") << "- Process " << trn << std::endl;
+ if (exp.find(tConc) != exp.end())
+ {
+ // already added to proof
+ Trace("te-proof-exp") << "...already added" << std::endl;
+ continue;
+ }
+ Node symTConc = CDProof::getSymmFact(tConc);
+ if (!symTConc.isNull())
{
- // If we're expanding the target node of the explanation (this is the
- // first expansion...), we don't want to add it as a separate proof
- // step. It is already part of the assertions.
- if (!ContainsKey(*inputAssertions, toExplain.d_node))
+ if (exp.find(symTConc) != exp.end())
{
- LemmaProofRecipe::ProofStep proofStep(toExplain.d_theory,
- toExplain.d_node);
- if (explanation.getKind() == kind::AND)
- {
- Node flat = flattenAnd(explanation);
- for (unsigned k = 0; k < flat.getNumChildren(); ++k)
- {
- // If a true constant or a negation of a false constant we can
- // ignore it
- if (!((flat[k].isConst() && flat[k].getConst<bool>())
- || (flat[k].getKind() == kind::NOT && flat[k][0].isConst()
- && !flat[k][0].getConst<bool>())))
- {
- proofStep.addAssertion(flat[k].negate());
- }
- }
- }
- else
- {
- if (!((explanation.isConst() && explanation.getConst<bool>())
- || (explanation.getKind() == kind::NOT
- && explanation[0].isConst()
- && !explanation[0].getConst<bool>())))
- {
- proofStep.addAssertion(explanation.negate());
- }
- }
- proofRecipe->addStep(proofStep);
+ // symmetric direction
+ Trace("te-proof-exp") << "...already added (SYMM)" << std::endl;
+ continue;
}
}
- });
- }
-
- // Keep only the relevant literals
- explanationVector.resize(j);
-
- PROOF({
- if (proofRecipe) {
- // The remaining literals are the base of the proof
- for (unsigned k = 0; k < explanationVector.size(); ++k) {
- proofRecipe->addBaseAssertion(explanationVector[k].d_node.negate());
+ // remember that we've explained this formula, to avoid cycles in lcp
+ exp.insert(tConc);
+ TheoryId ttid = it->first;
+ Node tExp = proven[0];
+ if (ttid == THEORY_LAST)
+ {
+ if (tConc == tExp)
+ {
+ // dummy trust node, do AND expansion
+ Assert(tConc.getKind() == kind::AND);
+ // tConc[0] ... tConc[n]
+ // ---------------------- AND_INTRO
+ // tConc
+ std::vector<Node> pfChildren;
+ pfChildren.insert(pfChildren.end(), tConc.begin(), tConc.end());
+ lcp->addStep(tConc, PfRule::AND_INTRO, pfChildren, {});
+ Trace("te-proof-exp") << "...via AND_INTRO" << std::endl;
+ continue;
}
+ // otherwise should hold by rewriting
+ Assert(Rewriter::rewrite(tConc) == Rewriter::rewrite(tExp));
+ // tExp
+ // ---- MACRO_SR_PRED_TRANSFORM
+ // tConc
+ lcp->addStep(tConc, PfRule::MACRO_SR_PRED_TRANSFORM, {tExp}, {tConc});
+ Trace("te-proof-exp") << "...via MACRO_SR_PRED_TRANSFORM" << std::endl;
+ continue;
+ }
+ if (tExp == tConc)
+ {
+ // trivial
+ Trace("te-proof-exp") << "...trivial" << std::endl;
+ continue;
}
- });
+ // ------------- Via theory
+ // tExp tExp => tConc
+ // ---------------------------------MODUS_PONENS
+ // tConc
+ if (trn.getGenerator() != nullptr)
+ {
+ Trace("te-proof-exp") << "...via theory generator" << std::endl;
+ lcp->addLazyStep(proven, trn.getGenerator());
+ }
+ else
+ {
+ Trace("te-proof-exp") << "...via trust THEORY_LEMMA" << std::endl;
+ // otherwise, trusted theory lemma
+ Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(it->first);
+ lcp->addStep(proven, PfRule::THEORY_LEMMA, {}, {proven, tidn});
+ }
+ std::vector<Node> pfChildren;
+ pfChildren.push_back(trn.getNode());
+ pfChildren.push_back(proven);
+ lcp->addStep(tConc, PfRule::MODUS_PONENS, pfChildren, {});
+ }
+ // store in the proof generator
+ TrustNode trn = d_tepg->mkTrustExplain(conclusion, expNode, lcp);
+ // return the trust node
+ return trn;
+ }
+
+ return theory::TrustNode::mkTrustLemma(expNode, nullptr);
}
+bool TheoryEngine::isProofEnabled() const { return d_pnm != nullptr; }
+
void TheoryEngine::setUserAttribute(const std::string& attr,
Node n,
const std::vector<Node>& node_values,
it != it_end;
++it) {
Node assertion = (*it).d_assertion;
- Node val = getModel()->getValue(assertion);
+ if (!isRelevant(assertion))
+ {
+ // not relevant, skip
+ continue;
+ }
+ Node val = d_tc->getModel()->getValue(assertion);
if (val != d_true)
{
std::stringstream ss;
projects / cvc5.git / blobdiff