/*! \file theory_engine.cpp
** \verbatim
** Top contributors (to current version):
- ** Dejan Jovanovic, Morgan Deters, Guy Katz
+ ** Andrew Reynolds, Dejan Jovanovic, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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
**
#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/lazy_proof.h"
#include "expr/node_builder.h"
-#include "options/bv_options.h"
-#include "options/options.h"
-#include "options/proof_options.h"
+#include "expr/node_visitor.h"
+#include "expr/proof_ensure_closed.h"
#include "options/quantifiers_options.h"
-#include "proof/cnf_proof.h"
-#include "proof/lemma_proof.h"
-#include "proof/proof_manager.h"
-#include "proof/theory_proof.h"
-#include "smt/term_formula_removal.h"
+#include "options/smt_options.h"
+#include "options/theory_options.h"
+#include "printer/printer.h"
+#include "prop/prop_engine.h"
+#include "smt/dump.h"
#include "smt/logic_exception.h"
-#include "smt_util/lemma_output_channel.h"
-#include "smt_util/node_visitor.h"
-#include "theory/arith/arith_ite_utils.h"
-#include "theory/bv/theory_bv_utils.h"
-#include "theory/care_graph.h"
-#include "theory/ite_utilities.h"
+#include "theory/combination_care_graph.h"
+#include "theory/decision_manager.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"
-#include "theory/unconstrained_simplifier.h"
#include "util/resource_manager.h"
using namespace std;
+using namespace CVC4::preprocessing;
using namespace CVC4::theory;
namespace CVC4 {
+/* -------------------------------------------------------------------------- */
+
+namespace theory {
+
+/**
+ * IMPORTANT: The order of the theories is important. For example, strings
+ * depends on arith, quantifiers needs to come as the very last.
+ * Do not change this order.
+ */
+
+#define CVC4_FOR_EACH_THEORY \
+ CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_BUILTIN) \
+ CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_BOOL) \
+ CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_UF) \
+ CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_ARITH) \
+ CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_BV) \
+ CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_FP) \
+ CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_ARRAYS) \
+ 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)
+
+} // namespace theory
+
+/* -------------------------------------------------------------------------- */
+
inline void flattenAnd(Node n, std::vector<TNode>& out){
Assert(n.getKind() == kind::AND);
for(Node::iterator i=n.begin(), i_end=n.end(); i != i_end; ++i){
return NodeManager::currentNM()->mkNode(kind::AND, out);
}
-theory::LemmaStatus TheoryEngine::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); });
-
- theory::LemmaStatus result =
- d_engine->lemma(lemma, rule, false, removable, preprocess,
- sendAtoms ? d_theory : theory::THEORY_LAST);
- return result;
-}
-
-void TheoryEngine::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() == kind::NOT);
- Node nnLemma = negated ? lemma[0] : lemma;
-
- switch (nnLemma.getKind()) {
-
- case kind::AND:
- if (!negated) {
- for (unsigned i = 0; i < nnLemma.getNumChildren(); ++i)
- registerLemmaRecipe(nnLemma[i], originalLemma, false, theoryId);
- } else {
- NodeBuilder<> builder(kind::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 kind::EQUAL:
- if( nnLemma[0].getType().isBoolean() ){
- if (!negated) {
- registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[1].negate()), originalLemma, false, theoryId);
- registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1]), originalLemma, false, theoryId);
- } else {
- registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[1]), originalLemma, false, theoryId);
- registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1].negate()), originalLemma, false, theoryId);
- }
- }
- break;
-
- case kind::ITE:
- if (!negated) {
- registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1]), originalLemma, false, theoryId);
- registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[2]), originalLemma, false, theoryId);
- } else {
- registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1].negate()), originalLemma, false, theoryId);
- registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[2].negate()), originalLemma, false, theoryId);
- }
- break;
-
- default:
- break;
+/**
+ * Compute the string for a given theory id. In this module, we use
+ * THEORY_SAT_SOLVER as an id, which is not a normal id but maps to
+ * THEORY_LAST. Thus, we need our own string conversion here.
+ *
+ * @param id The theory id
+ * @return The string corresponding to the theory id
+ */
+std::string getTheoryString(theory::TheoryId id)
+{
+ if (id == theory::THEORY_SAT_SOLVER)
+ {
+ return "THEORY_SAT_SOLVER";
}
-
- // 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() == kind::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);
+ else
+ {
+ std::stringstream ss;
+ ss << id;
+ return ss.str();
}
- proofRecipe.addStep(proofStep);
- ProofManager::getCnfProof()->setProofRecipe(&proofRecipe);
-}
-
-theory::LemmaStatus TheoryEngine::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") << "TheoryEngine::EngineOutputChannel::splitLemma( "
- << lemma << " )" << std::endl;
- theory::LemmaStatus result =
- d_engine->lemma(lemma, RULE_SPLIT, false, removable, false, d_theory);
- return result;
-}
-
-bool TheoryEngine::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 TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode,
- std::unique_ptr<Proof> proof)
+void TheoryEngine::finishInit()
{
- 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;
- d_engine->conflict(conflictNode, d_theory);
-}
-
-void TheoryEngine::finishInit() {
-
- //initialize the quantifiers engine, master equality engine, model, model builder
- if( d_logicInfo.isQuantified() ) {
- // initialize the quantifiers engine
- d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this);
- Assert(d_masterEqualityEngine == 0);
- d_masterEqualityEngine = new eq::EqualityEngine(d_masterEENotify,getSatContext(), "theory::master", false);
-
- for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
- if (d_theoryTable[theoryId]) {
- d_theoryTable[theoryId]->setQuantifiersEngine(d_quantEngine);
- d_theoryTable[theoryId]->setMasterEqualityEngine(d_masterEqualityEngine);
- }
- }
-
- d_curr_model_builder = d_quantEngine->getModelBuilder();
- d_curr_model = d_quantEngine->getModel();
- } else {
- d_curr_model = new theory::TheoryModel(d_userContext, "DefaultModel", true);
- d_aloc_curr_model = true;
- }
- //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;
- }
+ // 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;
- for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
- if (d_theoryTable[theoryId]) {
- d_theoryTable[theoryId]->finishInit();
- }
+ // Initialize the theory combination architecture
+ if (options::tcMode() == options::TcMode::CARE_GRAPH)
+ {
+ d_tc.reset(new CombinationCareGraph(*this, paraTheories, d_pnm));
}
-}
-
-void TheoryEngine::eqNotifyNewClass(TNode t){
- if (d_logicInfo.isQuantified()) {
- d_quantEngine->eqNotifyNewClass( t );
+ else
+ {
+ Unimplemented() << "TheoryEngine::finishInit: theory combination mode "
+ << options::tcMode() << " not supported";
}
-}
-
-void TheoryEngine::eqNotifyPreMerge(TNode t1, TNode t2){
- if (d_logicInfo.isQuantified()) {
- d_quantEngine->eqNotifyPreMerge( t1, t2 );
+ // create the relevance filter if any option requires it
+ if (options::relevanceFilter())
+ {
+ d_relManager.reset(
+ new RelevanceManager(d_userContext, theory::Valuation(this)));
}
-}
-void TheoryEngine::eqNotifyPostMerge(TNode t1, TNode t2){
- if (d_logicInfo.isQuantified()) {
- d_quantEngine->eqNotifyPostMerge( t1, t2 );
+ // 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->finishInit(this, d_decManager.get());
}
-}
-void TheoryEngine::eqNotifyDisequal(TNode t1, TNode t2, TNode reason){
- if (d_logicInfo.isQuantified()) {
- d_quantEngine->eqNotifyDisequal( t1, t2, reason );
+ // 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_tc->getEeTheoryInfo(theoryId);
+ Assert(eeti != nullptr);
+ // the theory's official equality engine is the one specified by the
+ // equality engine manager
+ t->setEqualityEngine(eeti->d_usedEe);
+ // set the quantifiers engine
+ t->setQuantifiersEngine(d_quantEngine);
+ // set the decision manager for the theory
+ t->setDecisionManager(d_decManager.get());
+ // finish initializing the theory
+ t->finishInit();
}
}
+ProofNodeManager* TheoryEngine::getProofNodeManager() const { return d_pnm; }
TheoryEngine::TheoryEngine(context::Context* context,
context::UserContext* userContext,
- RemoveTermFormulas& iteRemover,
+ ResourceManager* rm,
const LogicInfo& logicInfo,
- LemmaChannels* channels)
-: d_propEngine(NULL),
- d_decisionEngine(NULL),
- d_context(context),
- d_userContext(userContext),
- d_logicInfo(logicInfo),
- d_sharedTerms(this, context),
- d_masterEqualityEngine(NULL),
- d_masterEENotify(*this),
- d_quantEngine(NULL),
- d_curr_model(NULL),
- d_aloc_curr_model(false),
- d_curr_model_builder(NULL),
- d_aloc_curr_model_builder(false),
- d_ppCache(),
- d_possiblePropagations(context),
- d_hasPropagated(context),
- d_inConflict(context, false),
- d_hasShutDown(false),
- d_incomplete(context, false),
- d_propagationMap(context),
- d_propagationMapTimestamp(context, 0),
- d_propagatedLiterals(context),
- d_propagatedLiteralsIndex(context, 0),
- d_atomRequests(context),
- d_tform_remover(iteRemover),
- d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"),
- d_true(),
- d_false(),
- d_interrupted(false),
- d_resourceManager(NodeManager::currentResourceManager()),
- d_channels(channels),
- d_inPreregister(false),
- d_factsAsserted(context, false),
- d_preRegistrationVisitor(this, context),
- d_sharedTermsVisitor(d_sharedTerms),
- d_unconstrainedSimp(new UnconstrainedSimplifier(context, logicInfo)),
- d_bvToBoolPreprocessor(),
- d_theoryAlternatives(),
- d_attr_handle(),
- d_arithSubstitutionsAdded("theory::arith::zzz::arith::substitutions", 0)
+ OutputManager& outMgr,
+ ProofNodeManager* pnm)
+ : d_propEngine(nullptr),
+ d_context(context),
+ d_userContext(userContext),
+ d_logicInfo(logicInfo),
+ 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_relManager(nullptr),
+ d_preRegistrationVisitor(this, context),
+ d_eager_model_building(false),
+ d_inConflict(context, false),
+ d_inSatMode(false),
+ d_hasShutDown(false),
+ d_incomplete(context, false),
+ d_propagationMap(context),
+ d_propagationMapTimestamp(context, 0),
+ d_propagatedLiterals(context),
+ d_propagatedLiteralsIndex(context, 0),
+ d_atomRequests(context),
+ d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"),
+ d_true(),
+ d_false(),
+ d_interrupted(false),
+ d_resourceManager(rm),
+ d_inPreregister(false),
+ d_factsAsserted(context, false),
+ d_attr_handle(),
+ d_arithSubstitutionsAdded("theory::arith::zzz::arith::substitutions", 0)
{
for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST;
++ theoryId)
d_theoryTable[theoryId] = NULL;
d_theoryOut[theoryId] = NULL;
}
-
+
smtStatisticsRegistry()->registerStat(&d_combineTheoriesTime);
d_true = NodeManager::currentNM()->mkConst<bool>(true);
d_false = NodeManager::currentNM()->mkConst<bool>(false);
-#ifdef CVC4_PROOF
- ProofManager::currentPM()->initTheoryProofEngine();
-#endif
-
- d_iteUtilities = new ITEUtilities(d_tform_remover.getContainsVisitor());
-
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;
-
- delete d_masterEqualityEngine;
-
smtStatisticsRegistry()->unregisterStat(&d_combineTheoriesTime);
-
- delete d_unconstrainedSimp;
-
- delete d_iteUtilities;
-
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(!preprocessed.hasFreeVar());
+ 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
if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
Trace(tag) << "--------------------------------------------" << endl;
Trace(tag) << "Assertions of " << theory->getId() << ": " << endl;
- context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
- for (unsigned i = 0; it != it_end; ++ it, ++i) {
- if ((*it).isPreregistered) {
+ {
+ context::CDList<Assertion>::const_iterator it = theory->facts_begin(),
+ it_end =
+ theory->facts_end();
+ for (unsigned i = 0; it != it_end; ++it, ++i)
+ {
+ if ((*it).d_isPreregistered)
+ {
Trace(tag) << "[" << i << "]: ";
- } else {
+ }
+ else
+ {
Trace(tag) << "(" << i << "): ";
}
- Trace(tag) << (*it).assertion << endl;
+ Trace(tag) << (*it).d_assertion << endl;
+ }
}
if (d_logicInfo.isSharingEnabled()) {
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
- Node assertionNode = (*it).assertion;
+ Node assertionNode = (*it).d_assertion;
// Purify all the terms
- if ((*it).isPreregistered) {
- Dump(tag) << CommentCommand("Preregistered");
- } else {
- Dump(tag) << CommentCommand("Shared assertion");
+ if ((*it).d_isPreregistered)
+ {
+ printer.toStreamCmdComment(out, "Preregistered");
+ }
+ else
+ {
+ 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);
}
}
}
}
- if( ! d_inConflict && ! needCheck() ){
+ if (!d_inConflict)
+ {
if(d_logicInfo.isQuantified()) {
// quantifiers engine must check at last call effort
d_quantEngine->check(Theory::EFFORT_LAST_CALL);
}
if (!d_inConflict && !needCheck())
{
- if (options::produceModels() && !d_curr_model->isBuilt())
+ // If d_eager_model_building is false, then we only mark that we
+ // 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)
{
- // must build model at this point
- 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
- if( d_masterEqualityEngine != NULL ){
- AlwaysAssert(d_masterEqualityEngine->consistent());
- }
- if (d_curr_model->isBuilt())
- {
- // model construction should always succeed unless lemmas were added
- AlwaysAssert(d_curr_model->isBuiltSuccess());
- if (options::produceModels())
- {
- // if we are incomplete, there is no guarantee on the model.
- // thus, we do not check the model here. (related to #1693)
- if (!d_incomplete)
- {
- d_curr_model_builder->debugCheckModel(d_curr_model);
- }
- // Do post-processing of model from the theories (used for THEORY_SEP
- // to construct heap model)
- postProcessModel(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.a << " = " << carePair.b << " from " << carePair.theory << endl;
-
- Assert(d_sharedTerms.isShared(carePair.a) || carePair.a.isConst());
- Assert(d_sharedTerms.isShared(carePair.b) || carePair.b.isConst());
-
- // The equality in question (order for no repetition)
- Node equality = carePair.a.eqNode(carePair.b);
- // EqualityStatus es = getEqualityStatus(carePair.a, carePair.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, false, false, carePair.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() {
- // Definition of the statement that is to be run by every theory
- unsigned min_priority = 0;
- Node dec;
-#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
-#undef CVC4_FOR_EACH_THEORY_STATEMENT
-#endif
-#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
- if (theory::TheoryTraits<THEORY>::hasGetNextDecisionRequest && d_logicInfo.isTheoryEnabled(THEORY)) { \
- unsigned priority; \
- Node n = theoryOf(THEORY)->getNextDecisionRequest( priority ); \
- if(! n.isNull() && ( dec.isNull() || priority<min_priority ) ) { \
- dec = n; \
- min_priority = priority; \
- } \
- }
-
- // Request decision from each theory using the statement above
- CVC4_FOR_EACH_THEORY;
-
- return dec;
+Node TheoryEngine::getNextDecisionRequest()
+{
+ return d_decManager->getNextDecisionRequest();
}
bool TheoryEngine::properConflict(TNode conflict) const {
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;
- }
- }
- }
- // 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) {
- 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 );
- }
- }
-}
-
-/* get model */
-TheoryModel* TheoryEngine::getModel() {
- return d_curr_model;
+ Assert(d_tc != nullptr);
+ TheoryModel* m = d_tc->getModel();
+ Assert(m != nullptr);
+ return m;
}
-void TheoryEngine::getSynthSolutions(std::map<Node, Node>& sol_map)
+TheoryModel* TheoryEngine::getBuiltModel()
{
- if (d_quantEngine)
+ 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)
{
- d_quantEngine->getSynthSolutions(sol_map);
+ // not available, perhaps due to interuption.
+ return nullptr;
}
- else
+ // must build model at this point
+ if (!d_tc->buildModel())
{
- Assert(false);
+ return nullptr;
}
+ return d_tc->getModel();
+}
+
+bool TheoryEngine::buildModel()
+{
+ Assert(d_tc != nullptr);
+ return d_tc->buildModel();
}
bool TheoryEngine::presolve() {
// Reset the interrupt flag
d_interrupted = false;
+ // Reset the decision manager. This clears its decision strategies that are
+ // no longer valid in this user context.
+ d_decManager->presolve();
+
try {
// Definition of the statement that is to be run by every theory
#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
}/* TheoryEngine::presolve() */
void TheoryEngine::postsolve() {
+ // no longer in SAT mode
+ d_inSatMode = false;
// Reset the interrupt flag
d_interrupted = false;
bool CVC4_UNUSED wasInConflict = d_inConflict;
#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
#undef CVC4_FOR_EACH_THEORY_STATEMENT
#endif
-#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
- if (theory::TheoryTraits<THEORY>::hasPostsolve) { \
- theoryOf(THEORY)->postsolve(); \
- Assert(! d_inConflict || wasInConflict, "conflict raised during postsolve()"); \
- }
+#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
+ if (theory::TheoryTraits<THEORY>::hasPostsolve) \
+ { \
+ theoryOf(THEORY)->postsolve(); \
+ Assert(!d_inConflict || wasInConflict) \
+ << "conflict raised during postsolve()"; \
+ }
// Postsolve for each theory using the statement above
CVC4_FOR_EACH_THEORY;
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_ppCache.clear();
}
-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;
}
-// Recursively traverse a term and call the theory rewriter on its sub-terms
-Node TheoryEngine::ppTheoryRewrite(TNode term) {
- NodeMap::iterator find = d_ppCache.find(term);
- if (find != d_ppCache.end()) {
- return (*find).second;
- }
- unsigned nc = term.getNumChildren();
- if (nc == 0) {
- return theoryOf(term)->ppRewrite(term);
- }
- Trace("theory-pp") << "ppTheoryRewrite { " << term << endl;
-
- Node newTerm;
- // do not rewrite inside quantifiers
- if (term.getKind() == kind::FORALL || term.getKind() == kind::EXISTS
- || term.getKind() == kind::CHOICE
- || term.getKind() == kind::LAMBDA)
- {
- newTerm = Rewriter::rewrite(term);
- }
- else
- {
- NodeBuilder<> newNode(term.getKind());
- if (term.getMetaKind() == kind::metakind::PARAMETERIZED) {
- newNode << term.getOperator();
- }
- unsigned i;
- for (i = 0; i < nc; ++i) {
- newNode << ppTheoryRewrite(term[i]);
- }
- newTerm = Rewriter::rewrite(Node(newNode));
- }
- Node newTerm2 = theoryOf(newTerm)->ppRewrite(newTerm);
- if (newTerm != newTerm2) {
- newTerm = ppTheoryRewrite(Rewriter::rewrite(newTerm2));
- }
- d_ppCache[term] = newTerm;
- Trace("theory-pp")<< "ppTheoryRewrite returning " << newTerm << "}" << endl;
- return newTerm;
-}
-
-
-void TheoryEngine::preprocessStart()
+theory::TrustNode TheoryEngine::ppRewriteEquality(TNode eq)
{
- d_ppCache.clear();
-}
-
-
-struct preprocess_stack_element {
- TNode node;
- bool children_added;
- preprocess_stack_element(TNode node)
- : node(node), children_added(false) {}
-};/* struct preprocess_stack_element */
-
-
-Node TheoryEngine::preprocess(TNode assertion) {
-
- Trace("theory::preprocess") << "TheoryEngine::preprocess(" << assertion << ")" << endl;
- // spendResource();
-
- // Do a topological sort of the subexpressions and substitute them
- vector<preprocess_stack_element> toVisit;
- toVisit.push_back(assertion);
-
- while (!toVisit.empty())
- {
- // The current node we are processing
- preprocess_stack_element& stackHead = toVisit.back();
- TNode current = stackHead.node;
-
- Debug("theory::internal") << "TheoryEngine::preprocess(" << assertion << "): processing " << current << endl;
-
- // If node already in the cache we're done, pop from the stack
- NodeMap::iterator find = d_ppCache.find(current);
- if (find != d_ppCache.end()) {
- toVisit.pop_back();
- continue;
- }
-
- if(! d_logicInfo.isTheoryEnabled(Theory::theoryOf(current)) &&
- Theory::theoryOf(current) != THEORY_SAT_SOLVER) {
- stringstream ss;
- ss << "The logic was specified as " << d_logicInfo.getLogicString()
- << ", which doesn't include " << Theory::theoryOf(current)
- << ", but got a preprocessing-time fact for that theory." << endl
- << "The fact:" << endl
- << current;
- throw LogicException(ss.str());
- }
-
- // If this is an atom, we preprocess its terms with the theory ppRewriter
- if (Theory::theoryOf(current) != THEORY_BOOL) {
- Node ppRewritten = ppTheoryRewrite(current);
- d_ppCache[current] = ppRewritten;
- Assert(Rewriter::rewrite(d_ppCache[current]) == d_ppCache[current]);
- continue;
- }
-
- // Not yet substituted, so process
- if (stackHead.children_added) {
- // Children have been processed, so substitute
- NodeBuilder<> builder(current.getKind());
- if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
- builder << current.getOperator();
- }
- for (unsigned i = 0; i < current.getNumChildren(); ++ i) {
- Assert(d_ppCache.find(current[i]) != d_ppCache.end());
- builder << d_ppCache[current[i]];
- }
- // Mark the substitution and continue
- Node result = builder;
- if (result != current) {
- result = Rewriter::rewrite(result);
- }
- Debug("theory::internal") << "TheoryEngine::preprocess(" << assertion << "): setting " << current << " -> " << result << endl;
- d_ppCache[current] = result;
- toVisit.pop_back();
- } else {
- // Mark that we have added the children if any
- if (current.getNumChildren() > 0) {
- stackHead.children_added = true;
- // We need to add the children
- for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) {
- TNode childNode = *child_it;
- NodeMap::iterator childFind = d_ppCache.find(childNode);
- if (childFind == d_ppCache.end()) {
- toVisit.push_back(childNode);
- }
- }
- } else {
- // No children, so we're done
- Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << assertion << "): setting " << current << " -> " << current << endl;
- d_ppCache[current] = current;
- toVisit.pop_back();
- }
- }
- }
-
- // Return the substituted version
- return d_ppCache[assertion];
+ 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) {
if (d_propEngine->hasValue(assertion, value)) {
if (!value) {
Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << "): conflict (no sharing)" << endl;
+ Trace("dtview::conflict")
+ << ":THEORY-CONFLICT: " << assertion << std::endl;
d_inConflict = true;
} else {
return;
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 `%s'", atom.toString().c_str());
+ 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;
}
// Check for propositional conflicts
bool value;
if (d_propEngine->hasValue(assertion, value) && !value) {
- Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << "): conflict (sharing)" << endl;
+ Trace("theory::propagate")
+ << "TheoryEngine::assertToTheory(" << assertion << ", "
+ << toTheoryId << ", " << fromTheoryId << "): conflict (sharing)"
+ << endl;
+ Trace("dtview::conflict")
+ << ":THEORY-CONFLICT: " << assertion << std::endl;
d_inConflict = true;
}
}
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
AtomRequests::atom_iterator it = d_atomRequests.getAtomIterator(atom);
while (!it.done()) {
const AtomRequests::Request& request = it.get();
- Node toAssert = polarity ? (Node) request.atom : request.atom.notNode();
+ Node toAssert =
+ polarity ? (Node)request.d_atom : request.d_atom.notNode();
Debug("theory::atoms") << "TheoryEngine::assertFact(" << literal << "): sending requested " << toAssert << endl;
- assertToTheory(toAssert, literal, request.toTheory, THEORY_SAT_SOLVER);
+ assertToTheory(
+ toAssert, literal, request.d_toTheory, THEORY_SAT_SOLVER);
it.next();
}
}
bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
-
Debug("theory::propagate") << "TheoryEngine::propagate(" << literal << ", " << theory << ")" << endl;
- // spendResource();
+ Trace("dtview::prop") << std::string(d_context->getLevel(), ' ')
+ << ":THEORY-PROP: " << literal << endl;
- 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);
- }
+ // spendResource();
// Get the atom
bool polarity = literal.getKind() != kind::NOT;
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);
return !d_inConflict;
}
+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()) return var; // FIXME: HACK!!!
- 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 );
+bool TheoryEngine::getSepHeapTypes(TypeNode& locType, TypeNode& dataType) const
+{
+ if (d_sepLocType.isNull())
+ {
+ 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].theory == THEORY_SAT_SOLVER);
- all.insert(explanation[i].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].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;
-
- Node explanation = theoryOf(atom)->explain(node);
- 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;
+ 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;
+ 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);
Assert(d_propagationMap.find(toExplain) != d_propagationMap.end());
NodeTheoryPair nodeExplainerPair = d_propagationMap[toExplain];
- Debug("theory::explain") << "TheoryEngine::getExplanation: explainer for node "
- << nodeExplainerPair.node
- << " is theory: " << nodeExplainerPair.theory << std::endl;
- TheoryId explainer = nodeExplainerPair.theory;
+ Debug("theory::explain")
+ << "TheoryEngine::getExplanation: explainer for node "
+ << nodeExplainerPair.d_node
+ << " is theory: " << nodeExplainerPair.d_theory << std::endl;
// 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 {
}
continue;
}else if( eqNormalized.getKind() != kind::EQUAL){
- Assert( eqNormalized.getKind()==kind::BOOLEAN_TERM_VARIABLE ||
- ( eqNormalized.getKind()==kind::NOT && eqNormalized[0].getKind()==kind::BOOLEAN_TERM_VARIABLE ) );
+ Assert(eqNormalized.getKind() == kind::BOOLEAN_TERM_VARIABLE
+ || (eqNormalized.getKind() == kind::NOT
+ && eqNormalized[0].getKind() == kind::BOOLEAN_TERM_VARIABLE));
// this happens for Boolean term equalities V = true that are rewritten to V, we should skip
// TODO : revisit this
continue;
}
}
-theory::LemmaStatus TheoryEngine::lemma(TNode node,
- ProofRule rule,
- bool negated,
- bool removable,
- bool preprocess,
- 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")
- << QueryCommand(n.toExpr());
+ // 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);
}
- // Share with other portfolio threads
- if(d_channels->getLemmaOutputChannel() != NULL) {
- d_channels->getLemmaOutputChannel()->notifyNewLemma(node.toExpr());
- }
-
- std::vector<Node> additionalLemmas;
- IteSkolemMap iteSkolemMap;
-
- // Run theory preprocessing, maybe
- Node ppNode = preprocess ? this->preprocess(node) : Node(node);
-
- // Remove the ITEs
- Debug("ite") << "Remove ITE from " << ppNode << std::endl;
- additionalLemmas.push_back(ppNode);
- d_tform_remover.run(additionalLemmas, iteSkolemMap);
- Debug("ite") << "..done " << additionalLemmas[0] << std::endl;
- additionalLemmas[0] = theory::Rewriter::rewrite(additionalLemmas[0]);
+ // assert the lemma
+ d_propEngine->assertLemma(tlemma, p);
- if(Debug.isOn("lemma-ites")) {
- Debug("lemma-ites") << "removed ITEs from lemma: " << ppNode << endl;
- Debug("lemma-ites") << " + now have the following "
- << additionalLemmas.size() << " lemma(s):" << endl;
- for(std::vector<Node>::const_iterator i = additionalLemmas.begin();
- i != additionalLemmas.end();
- ++i) {
- Debug("lemma-ites") << " + " << *i << endl;
- }
- Debug("lemma-ites") << endl;
- }
-
- // assert to prop engine
- d_propEngine->assertLemma(additionalLemmas[0], negated, removable, rule, node);
- for (unsigned i = 1; i < additionalLemmas.size(); ++ i) {
- additionalLemmas[i] = theory::Rewriter::rewrite(additionalLemmas[i]);
- d_propEngine->assertLemma(additionalLemmas[i], false, removable, rule, node);
- }
-
- // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
- if(negated) {
- additionalLemmas[0] = additionalLemmas[0].notNode();
- negated = false;
- }
-
- // assert to decision engine
- if(!removable) {
- d_decisionEngine->addAssertions(additionalLemmas, 1, iteSkolemMap);
+ // 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))
+ {
+ 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.
- return theory::LemmaStatus(additionalLemmas[0], d_userContext->getLevel());
}
-void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
+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);
- Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << ")" << endl;
+ Trace("dtview::conflict") << ":THEORY-CONFLICT: " << conflict << std::endl;
// Mark that we are in conflict
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, true, false, 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, true, false, 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() == bv::BITVECTOR_SLICER_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() == bv::BITVECTOR_SLICER_OFF)
- {
- return;
- }
- else if (options::bitvectorEqualitySlicer() == bv::BITVECTOR_SLICER_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();
- }
-}
-
-void TheoryEngine::ppBvToBool(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) {
- d_bvToBoolPreprocessor.liftBvToBool(assertions, new_assertions);
-}
-
-void TheoryEngine::ppBoolToBv(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) {
- d_bvToBoolPreprocessor.lowerBoolToBv(assertions, new_assertions);
-}
-
-bool TheoryEngine::ppBvAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) {
- bv::TheoryBV* bv_theory = (bv::TheoryBV*)d_theoryTable[THEORY_BV];
- return bv_theory->applyAbstraction(assertions, new_assertions);
-}
-
-void TheoryEngine::mkAckermanizationAssertions(std::vector<Node>& assertions) {
- bv::TheoryBV* bv_theory = (bv::TheoryBV*)d_theoryTable[THEORY_BV];
- bv_theory->mkAckermanizationAssertions(assertions);
-}
-
-Node TheoryEngine::ppSimpITE(TNode assertion)
-{
- if (!d_tform_remover.containsTermITE(assertion)) {
- return assertion;
- } else {
- Node result = d_iteUtilities->simpITE(assertion);
- Node res_rewritten = Rewriter::rewrite(result);
-
- if(options::simplifyWithCareEnabled()){
- Chat() << "starting simplifyWithCare()" << endl;
- Node postSimpWithCare = d_iteUtilities->simplifyWithCare(res_rewritten);
- Chat() << "ending simplifyWithCare()"
- << " post simplifyWithCare()" << postSimpWithCare.getId() << endl;
- result = Rewriter::rewrite(postSimpWithCare);
- } else {
- result = res_rewritten;
- }
- return result;
- }
-}
-
-bool TheoryEngine::donePPSimpITE(std::vector<Node>& assertions){
- // This pass does not support dependency tracking yet
- // (learns substitutions from all assertions so just
- // adding addDependence is not enough)
- if (options::unsatCores() || options::fewerPreprocessingHoles()) {
- return true;
- }
- bool result = true;
- bool simpDidALotOfWork = d_iteUtilities->simpIteDidALotOfWorkHeuristic();
- if(simpDidALotOfWork){
- if(options::compressItes()){
- result = d_iteUtilities->compress(assertions);
- }
-
- if(result){
- // if false, don't bother to reclaim memory here.
- NodeManager* nm = NodeManager::currentNM();
- if(nm->poolSize() >= options::zombieHuntThreshold()){
- Chat() << "..ite simplifier did quite a bit of work.. " << nm->poolSize() << endl;
- Chat() << "....node manager contains " << nm->poolSize() << " nodes before cleanup" << endl;
- d_iteUtilities->clear();
- Rewriter::clearCaches();
- d_tform_remover.garbageCollect();
- nm->reclaimZombiesUntil(options::zombieHuntThreshold());
- Chat() << "....node manager contains " << nm->poolSize() << " nodes after cleanup" << endl;
- }
- }
- }
-
- // Do theory specific preprocessing passes
- if(d_logicInfo.isTheoryEnabled(theory::THEORY_ARITH)
- && !options::incrementalSolving() ){
- if(!simpDidALotOfWork){
- ContainsTermITEVisitor& contains = *d_tform_remover.getContainsVisitor();
- arith::ArithIteUtils aiteu(contains, d_userContext, getModel());
- bool anyItes = false;
- for(size_t i = 0; i < assertions.size(); ++i){
- Node curr = assertions[i];
- if(contains.containsTermITE(curr)){
- anyItes = true;
- Node res = aiteu.reduceVariablesInItes(curr);
- Debug("arith::ite::red") << "@ " << i << " ... " << curr << endl << " ->" << res << endl;
- if(curr != res){
- Node more = aiteu.reduceConstantIteByGCD(res);
- Debug("arith::ite::red") << " gcd->" << more << endl;
- assertions[i] = Rewriter::rewrite(more);
- }
- }
- }
- if(!anyItes){
- unsigned prevSubCount = aiteu.getSubCount();
- aiteu.learnSubstitutions(assertions);
- if(prevSubCount < aiteu.getSubCount()){
- d_arithSubstitutionsAdded += aiteu.getSubCount() - prevSubCount;
- bool anySuccess = false;
- for(size_t i = 0, N = assertions.size(); i < N; ++i){
- Node curr = assertions[i];
- Node next = Rewriter::rewrite(aiteu.applySubstitutions(curr));
- Node res = aiteu.reduceVariablesInItes(next);
- Debug("arith::ite::red") << "@ " << i << " ... " << next << endl << " ->" << res << endl;
- Node more = aiteu.reduceConstantIteByGCD(res);
- Debug("arith::ite::red") << " gcd->" << more << endl;
- if(more != next){
- anySuccess = true;
- break;
- }
- }
- for(size_t i = 0, N = assertions.size(); anySuccess && i < N; ++i){
- Node curr = assertions[i];
- Node next = Rewriter::rewrite(aiteu.applySubstitutions(curr));
- Node res = aiteu.reduceVariablesInItes(next);
- Debug("arith::ite::red") << "@ " << i << " ... " << next << endl << " ->" << res << endl;
- Node more = aiteu.reduceConstantIteByGCD(res);
- Debug("arith::ite::red") << " gcd->" << more << endl;
- assertions[i] = Rewriter::rewrite(more);
- }
- }
- }
- }
+ Trace("te-proof-exp") << "=== TheoryEngine::getExplanation " << conclusion
+ << std::endl;
+ lcp.reset(new LazyCDProof(
+ d_pnm, nullptr, nullptr, "TheoryEngine::LazyCDProof::getExplanation"));
}
- return result;
-}
-
-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::set<Node> inputAssertions;
- PROOF(inputAssertions = proofRecipe->getStep(0)->getAssertions(););
+ std::unique_ptr<std::set<Node>> inputAssertions = nullptr;
+ // 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;
while (i < explanationVector.size()) {
// Get the current literal to explain
NodeTheoryPair toExplain = explanationVector[i];
- Debug("theory::explain") << "[i=" << i << "] TheoryEngine::explain(): processing [" << toExplain.timestamp << "] " << toExplain.node << " sent from " << toExplain.theory << endl;
-
+ Debug("theory::explain")
+ << "[i=" << i << "] TheoryEngine::explain(): processing ["
+ << toExplain.d_timestamp << "] " << toExplain.d_node << " sent from "
+ << toExplain.d_theory << endl;
- // If a true constant or a negation of a false constant we can ignore it
- if (toExplain.node.isConst() && toExplain.node.getConst<bool>()) {
- ++ i;
+ if (cache.find(toExplain.d_node) != cache.end()
+ && cache[toExplain.d_node] < toExplain.d_timestamp)
+ {
+ ++i;
continue;
}
- if (toExplain.node.getKind() == kind::NOT && toExplain.node[0].isConst() && !toExplain.node[0].getConst<bool>()) {
+ 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>())
+ || (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 from the SAT solver, keep it
- if (toExplain.theory == THEORY_SAT_SOLVER) {
+ 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;
}
// If an and, expand it
- if (toExplain.node.getKind() == kind::AND) {
- Debug("theory::explain") << "TheoryEngine::explain(): expanding " << toExplain.node << " got from " << toExplain.theory << endl;
- for (unsigned k = 0; k < toExplain.node.getNumChildren(); ++ k) {
- NodeTheoryPair newExplain(toExplain.node[k], toExplain.theory, toExplain.timestamp);
+ if (toExplain.d_node.getKind() == kind::AND)
+ {
+ Debug("theory::explain")
+ << "TheoryEngine::explain(): expanding " << toExplain.d_node
+ << " got from " << toExplain.d_theory << endl;
+ 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;
}
// See if it was sent to the theory by another theory
PropagationMap::const_iterator find = d_propagationMap.find(toExplain);
if (find != d_propagationMap.end()) {
- Debug("theory::explain") << "\tTerm was propagated by another theory (theory = "
- << theoryOf((*find).second.theory)->getId() << ")" << std::endl;
+ Debug("theory::explain")
+ << "\tTerm was propagated by another theory (theory = "
+ << getTheoryString((*find).second.d_theory) << ")" << std::endl;
// There is some propagation, check if its a timely one
- if ((*find).second.timestamp < toExplain.timestamp) {
- Debug("theory::explain") << "\tRelevant timetsamp, pushing "
- << (*find).second.node << "to index = " << explanationVector.size() << std::endl;
+ if ((*find).second.d_timestamp < toExplain.d_timestamp)
+ {
+ Debug("theory::explain")
+ << "\tRelevant timetsamp, pushing " << (*find).second.d_node
+ << "to index = " << explanationVector.size() << std::endl;
explanationVector.push_back((*find).second);
++i;
- PROOF({
- if (toExplain.node != (*find).second.node) {
- Debug("pf::explain") << "TheoryEngine::getExplanation: Rewrite alert! toAssert = " << toExplain.node
- << ", toExplain = " << (*find).second.node << std::endl;
-
- if (proofRecipe) {
- proofRecipe->addRewriteRule(toExplain.node, (*find).second.node);
- }
- }
- })
-
+ if (lcp != nullptr)
+ {
+ if (!CDProof::isSame(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;
}
}
-
// It was produced by the theory, so ask for an explanation
- Node explanation;
- if (toExplain.theory == THEORY_BUILTIN) {
- explanation = d_sharedTerms.explain(toExplain.node);
- Debug("theory::explain") << "\tTerm was propagated by THEORY_BUILTIN. Explanation: " << explanation << std::endl;
- } else {
- explanation = theoryOf(toExplain.theory)->explain(toExplain.node);
- Debug("theory::explain") << "\tTerm was propagated by owner theory: "
- << theoryOf(toExplain.theory)->getId()
- << ". Explanation: " << explanation << std::endl;
+ TrustNode texplanation =
+ d_sharedSolver->explain(toExplain.d_node, toExplain.d_theory);
+ if (lcp != nullptr)
+ {
+ 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 << " got from " << toExplain.theory << endl;
- Assert( explanation != toExplain.node, "wasn't sent to you, so why are you explaining it trivially");
+ Debug("theory::explain")
+ << "TheoryEngine::explain(): got explanation " << explanation
+ << " got from " << toExplain.d_theory << endl;
+ Assert(explanation != toExplain.d_node)
+ << "wasn't sent to you, so why are you explaining it trivially";
// Mark the explanation
- NodeTheoryPair newExplain(explanation, toExplain.theory, toExplain.timestamp);
+ NodeTheoryPair newExplain(
+ explanation, toExplain.d_theory, toExplain.d_timestamp);
explanationVector.push_back(newExplain);
++ i;
-
- PROOF({
- if (proofRecipe) {
- // 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 (inputAssertions.find(toExplain.node) == inputAssertions.end()) {
- LemmaProofRecipe::ProofStep proofStep(toExplain.theory, toExplain.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);
- }
- }
- });
}
- // 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].node.negate());
+ // 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 (exp.find(symTConc) != exp.end())
+ {
+ // symmetric direction
+ Trace("te-proof-exp") << "...already added (SYMM)" << std::endl;
+ continue;
}
}
- });
-}
+ // 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;
+ }
-void TheoryEngine::ppUnconstrainedSimp(vector<Node>& assertions)
-{
- d_unconstrainedSimp->processAssertions(assertions);
+ 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_end = theory->facts_end();
it != it_end;
++it) {
- Node assertion = (*it).assertion;
- Node val = getModel()->getValue(assertion);
- if(val != d_true) {
- stringstream ss;
- ss << theoryId << " has an asserted fact that the model doesn't satisfy." << endl
+ Node assertion = (*it).d_assertion;
+ if (!isRelevant(assertion))
+ {
+ // not relevant, skip
+ continue;
+ }
+ Node val = d_tc->getModel()->getValue(assertion);
+ if (val != d_true)
+ {
+ std::stringstream ss;
+ ss << " " << theoryId
+ << " has an asserted fact that the model doesn't satisfy." << endl
<< "The fact: " << assertion << endl
<< "Model value: " << val << endl;
- if(hardFailure) {
- InternalError(ss.str());
- }
+ if (hardFailure)
+ {
+ if (val == d_false)
+ {
+ // Always an error if it is false
+ InternalError() << ss.str();
+ }
+ else
+ {
+ // Otherwise just a warning. Notice this case may happen for
+ // assertions with unevaluable operators, e.g. transcendental
+ // functions. It also may happen for separation logic, where
+ // check-model support is limited.
+ Warning() << ss.str();
+ }
+ }
}
}
}
}
}
-std::pair<bool, Node> TheoryEngine::entailmentCheck(theory::TheoryOfMode mode, TNode lit, const EntailmentCheckParameters* params, EntailmentCheckSideEffects* seffects) {
+std::pair<bool, Node> TheoryEngine::entailmentCheck(options::TheoryOfMode mode,
+ TNode lit)
+{
TNode atom = (lit.getKind() == kind::NOT) ? lit[0] : lit;
if( atom.getKind()==kind::AND || atom.getKind()==kind::OR || atom.getKind()==kind::IMPLIES ){
//Boolean connective, recurse
if( pol==( lit.getKind()==kind::IMPLIES && i==0 ) ){
ch = atom[i].negate();
}
- std::pair<bool, Node> chres = entailmentCheck( mode, ch, params, seffects );
+ std::pair<bool, Node> chres = entailmentCheck(mode, ch);
if( chres.first ){
if( !is_conjunction ){
return chres;
if( r==1 ){
ch = ch.negate();
}
- std::pair<bool, Node> chres = entailmentCheck( mode, ch, params, seffects );
+ std::pair<bool, Node> chres = entailmentCheck(mode, ch);
if( chres.first ){
Node ch2 = atom[ atom.getKind()==kind::ITE ? r+1 : 1 ];
if( pol==( atom.getKind()==kind::ITE ? true : r==1 ) ){
ch2 = ch2.negate();
}
- std::pair<bool, Node> chres2 = entailmentCheck( mode, ch2, params, seffects );
+ std::pair<bool, Node> chres2 = entailmentCheck(mode, ch2);
if( chres2.first ){
return std::pair<bool, Node>(true, NodeManager::currentNM()->mkNode(kind::AND, chres.second, chres2.second));
}else{
theory::Theory* th = theoryOf(tid);
Assert(th != NULL);
- Assert(params == NULL || tid == params->getTheoryId());
- Assert(seffects == NULL || tid == seffects->getTheoryId());
Trace("theory-engine-entc") << "Entailment check : " << lit << std::endl;
- std::pair<bool, Node> chres = th->entailmentCheck(lit, params, seffects);
+ std::pair<bool, Node> chres = th->entailmentCheck(lit);
return chres;
}
}
-void TheoryEngine::spendResource(unsigned amount)
+void TheoryEngine::spendResource(ResourceManager::Resource r)
{
- d_resourceManager->spendResource(amount);
-}
-
-void TheoryEngine::enableTheoryAlternative(const std::string& name){
- Debug("TheoryEngine::enableTheoryAlternative")
- << "TheoryEngine::enableTheoryAlternative(" << name << ")" << std::endl;
-
- d_theoryAlternatives.insert(name);
-}
-
-bool TheoryEngine::useTheoryAlternative(const std::string& name) {
- return d_theoryAlternatives.find(name) != d_theoryAlternatives.end();
-}
-
-
-TheoryEngine::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),
- flipDecision(getStatsPrefix(theory) + "::flipDecision", 0),
- restartDemands(getStatsPrefix(theory) + "::restartDemands", 0)
-{
- smtStatisticsRegistry()->registerStat(&conflicts);
- smtStatisticsRegistry()->registerStat(&propagations);
- smtStatisticsRegistry()->registerStat(&lemmas);
- smtStatisticsRegistry()->registerStat(&requirePhase);
- smtStatisticsRegistry()->registerStat(&flipDecision);
- smtStatisticsRegistry()->registerStat(&restartDemands);
-}
-
-TheoryEngine::Statistics::~Statistics() {
- smtStatisticsRegistry()->unregisterStat(&conflicts);
- smtStatisticsRegistry()->unregisterStat(&propagations);
- smtStatisticsRegistry()->unregisterStat(&lemmas);
- smtStatisticsRegistry()->unregisterStat(&requirePhase);
- smtStatisticsRegistry()->unregisterStat(&flipDecision);
- smtStatisticsRegistry()->unregisterStat(&restartDemands);
+ d_resourceManager->spendResource(r);
}
}/* CVC4 namespace */