diff options
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 20 | ||||
| -rw-r--r-- | src/theory/theory_engine.cpp | 399 | ||||
| -rw-r--r-- | src/theory/theory_engine.h | 79 | ||||
| -rw-r--r-- | src/theory/theory_model.cpp | 2 | ||||
| -rw-r--r-- | src/theory/theory_model.h | 19 | ||||
| -rw-r--r-- | src/theory/theory_model_builder.cpp | 25 | ||||
| -rw-r--r-- | src/theory/theory_model_builder.h | 21 |
7 files changed, 164 insertions, 401 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 9dc483f93..dd59628c1 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -670,23 +670,15 @@ void QuantifiersEngine::check( Theory::Effort e ){ QuantifiersModule::QEffort quant_e = static_cast<QuantifiersModule::QEffort>(qef); d_curr_effort_level = quant_e; - //build the model if any module requested it + // Force the theory engine to build the model if any module requested it. if (needsModelE == quant_e) { - if (!d_model->isBuilt()) - { - // theory engine's model builder is quantifier engine's builder if it - // has one - Assert(!getModelBuilder() - || getModelBuilder() == d_te->getModelBuilder()); - Trace("quant-engine-debug") << "Build model..." << std::endl; - if (!d_te->getModelBuilder()->buildModel(d_model.get())) - { - flushLemmas(); - } - } - if (!d_model->isBuiltSuccess()) + Trace("quant-engine-debug") << "Build model..." << std::endl; + if (!d_te->buildModel()) { + // If we failed to build the model, flush all pending lemmas and + // finish. + flushLemmas(); break; } } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 647a40999..0979d447b 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -41,8 +41,8 @@ #include "theory/arith/arith_ite_utils.h" #include "theory/bv/theory_bv_utils.h" #include "theory/care_graph.h" +#include "theory/combination_care_graph.h" #include "theory/decision_manager.h" -#include "theory/ee_manager_distributed.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fmf/model_engine.h" #include "theory/quantifiers/theory_quantifiers.h" @@ -131,27 +131,32 @@ std::string getTheoryString(theory::TheoryId id) } void TheoryEngine::finishInit() { - // initialize the quantifiers engine - if (d_logicInfo.isQuantified()) + // NOTE: This seems to be required since + // theory::TheoryTraits<THEORY>::isParametric cannot be accessed without + // using the CVC4_FOR_EACH_THEORY_STATEMENT macro. -AJR + std::vector<theory::Theory*> paraTheories; +#ifdef CVC4_FOR_EACH_THEORY_STATEMENT +#undef CVC4_FOR_EACH_THEORY_STATEMENT +#endif +#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ + if (theory::TheoryTraits<THEORY>::isParametric \ + && d_logicInfo.isTheoryEnabled(THEORY)) \ + { \ + paraTheories.push_back(theoryOf(THEORY)); \ + } + // Collect the parametric theories, which are given to the theory combination + // manager below + CVC4_FOR_EACH_THEORY; + + // Initialize the theory combination architecture + if (options::tcMode() == options::TcMode::CARE_GRAPH) { - // initialize the quantifiers engine - d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this); + d_tc.reset(new CombinationCareGraph(*this, paraTheories)); } - - // Initialize the equality engine architecture for all theories, which - // includes the master equality engine. - d_eeDistributed.reset(new EqEngineManagerDistributed(*this)); - d_eeDistributed->initializeTheories(); - - // Initialize the model and model builder. - if (d_logicInfo.isQuantified()) + else { - d_curr_model_builder = d_quantEngine->getModelBuilder(); - d_curr_model = d_quantEngine->getModel(); - } else { - d_curr_model = new theory::TheoryModel( - d_userContext, "DefaultModel", options::assignFunctionValues()); - d_aloc_curr_model = true; + Unimplemented() << "TheoryEngine::finishInit: theory combination mode " + << options::tcMode() << " not supported"; } // create the relevance filter if any option requires it if (options::relevanceFilter()) @@ -160,24 +165,24 @@ void TheoryEngine::finishInit() { new RelevanceManager(d_userContext, theory::Valuation(this))); } - //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; + // initialize the quantifiers engine + if (d_logicInfo.isQuantified()) + { + // initialize the quantifiers engine + d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this); } - - // Initialize the model - // !!!! temporary, will be part of combination engine initialization - d_eeDistributed->initializeModel(d_curr_model, nullptr); + // initialize the theory combination manager, which decides and allocates the + // equality engines to use for all theories. + d_tc->finishInit(); // set the core equality engine on quantifiers engine if (d_logicInfo.isQuantified()) { - d_quantEngine->setMasterEqualityEngine( - d_eeDistributed->getCoreEqualityEngine()); + d_quantEngine->setMasterEqualityEngine(d_tc->getCoreEqualityEngine()); } - // finish initializing the theories + // finish initializing the theories by linking them with the appropriate + // utilities and then calling their finishInit method. for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) { Theory* t = d_theoryTable[theoryId]; if (t == nullptr) @@ -185,7 +190,7 @@ void TheoryEngine::finishInit() { continue; } // setup the pointers to the utilities - const EeTheoryInfo* eeti = d_eeDistributed->getEeTheoryInfo(theoryId); + const EeTheoryInfo* eeti = d_tc->getEeTheoryInfo(theoryId); Assert(eeti != nullptr); // the theory's official equality engine is the one specified by the // equality engine manager @@ -209,14 +214,12 @@ TheoryEngine::TheoryEngine(context::Context* context, d_userContext(userContext), d_logicInfo(logicInfo), d_sharedTerms(this, context), - d_eeDistributed(nullptr), + d_tc(nullptr), d_quantEngine(nullptr), d_decManager(new DecisionManager(userContext)), d_relManager(nullptr), - d_curr_model(nullptr), - d_aloc_curr_model(false), - d_curr_model_builder(nullptr), - d_aloc_curr_model_builder(false), + d_preRegistrationVisitor(this, context), + d_sharedTermsVisitor(d_sharedTerms), d_eager_model_building(false), d_possiblePropagations(context), d_hasPropagated(context), @@ -237,8 +240,6 @@ TheoryEngine::TheoryEngine(context::Context* context, d_resourceManager(rm), d_inPreregister(false), d_factsAsserted(context, false), - d_preRegistrationVisitor(this, context), - d_sharedTermsVisitor(d_sharedTerms), d_attr_handle(), d_arithSubstitutionsAdded("theory::arith::zzz::arith::substitutions", 0) { @@ -270,13 +271,6 @@ TheoryEngine::~TheoryEngine() { } } - if( d_aloc_curr_model_builder ){ - delete d_curr_model_builder; - } - if( d_aloc_curr_model ){ - delete d_curr_model; - } - delete d_quantEngine; smtStatisticsRegistry()->unregisterStat(&d_combineTheoriesTime); @@ -311,34 +305,46 @@ void TheoryEngine::preRegister(TNode preprocessed) { Debug("theory") << "TheoryEngine::preRegister: " << preprocessed << std::endl; Assert(!expr::hasFreeVar(preprocessed)); + // Pre-register the terms in the atom - Theory::Set theories = NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed); + 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 + // 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()); + 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 = Theory::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); + NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, + preprocessed); } } @@ -444,14 +450,17 @@ void TheoryEngine::check(Theory::Effort effort) { #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 { @@ -474,6 +483,7 @@ void TheoryEngine::check(Theory::Effort effort) { { d_relManager->resetRound(); } + d_tc->resetRound(); } // Check until done @@ -514,7 +524,10 @@ void TheoryEngine::check(Theory::Effort effort) { 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(); } @@ -527,21 +540,17 @@ void TheoryEngine::check(Theory::Effort effort) { 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(); - // !!! temporary, will be part of distributed model manager - context::Context* meec = d_eeDistributed->getModelEqualityEngineContext(); - meec->pop(); - meec->push(); 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); } @@ -561,9 +570,9 @@ void TheoryEngine::check(Theory::Effort effort) { // are in "SAT mode". We build the model later only if the user asks // for it via getBuiltModel. d_inSatMode = true; - if (d_eager_model_building && !d_curr_model->isBuilt()) + if (d_eager_model_building) { - d_curr_model_builder->buildModel(d_curr_model); + d_tc->buildModel(); } } } @@ -572,27 +581,9 @@ void TheoryEngine::check(Theory::Effort effort) { Debug("theory") << ", need check = " << (needCheck() ? "YES" : "NO") << endl; if( Theory::fullEffort(effort) && !d_inConflict && !needCheck()) { - // case where we are about to answer SAT, the master equality engine, - // if it exists, must be consistent. - eq::EqualityEngine* mee = d_eeDistributed->getCoreEqualityEngine(); - if (mee != NULL) - { - AlwaysAssert(mee->consistent()); - } - if (d_curr_model->isBuilt()) - { - // model construction should always succeed unless lemmas were added - AlwaysAssert(d_curr_model->isBuiltSuccess()); - if (options::produceModels()) - { - // Do post-processing of model from the theories (used for THEORY_SEP - // to construct heap model) - postProcessModel(d_curr_model); - // also call the model builder's post-process model - d_curr_model_builder->postProcessModel(d_incomplete.get(), - d_curr_model); - } - } + // Do post-processing of model from the theories (e.g. used for THEORY_SEP + // to construct heap model) + d_tc->postProcessModel(d_incomplete.get()); } } catch(const theory::Interrupted&) { Trace("theory") << "TheoryEngine::check() => interrupted" << endl; @@ -605,80 +596,8 @@ void TheoryEngine::check(Theory::Effort effort) { } } -void TheoryEngine::combineTheories() { - - Trace("combineTheories") << "TheoryEngine::combineTheories()" << endl; - - TimerStat::CodeTimer combineTheoriesTimer(d_combineTheoriesTime); - - // Care graph we'll be building - CareGraph careGraph; - -#ifdef CVC4_FOR_EACH_THEORY_STATEMENT -#undef CVC4_FOR_EACH_THEORY_STATEMENT -#endif -#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ - if (theory::TheoryTraits<THEORY>::isParametric && d_logicInfo.isTheoryEnabled(THEORY)) { \ - theoryOf(THEORY)->getCareGraph(&careGraph); \ - } - - // Call on each parametric theory to give us its care graph - CVC4_FOR_EACH_THEORY; - - Trace("combineTheories") << "TheoryEngine::combineTheories(): care graph size = " << careGraph.size() << endl; - - // Now add splitters for the ones we are interested in - CareGraph::const_iterator care_it = careGraph.begin(); - CareGraph::const_iterator care_it_end = careGraph.end(); - - for (; care_it != care_it_end; ++ care_it) { - const CarePair& carePair = *care_it; - - Debug("combineTheories") - << "TheoryEngine::combineTheories(): checking " << carePair.d_a << " = " - << carePair.d_b << " from " << carePair.d_theory << endl; - - Assert(d_sharedTerms.isShared(carePair.d_a) || carePair.d_a.isConst()); - Assert(d_sharedTerms.isShared(carePair.d_b) || carePair.d_b.isConst()); - - // The equality in question (order for no repetition) - Node equality = carePair.d_a.eqNode(carePair.d_b); - // EqualityStatus es = getEqualityStatus(carePair.d_a, carePair.d_b); - // Debug("combineTheories") << "TheoryEngine::combineTheories(): " << - // (es == EQUALITY_TRUE_AND_PROPAGATED ? "EQUALITY_TRUE_AND_PROPAGATED" : - // es == EQUALITY_FALSE_AND_PROPAGATED ? "EQUALITY_FALSE_AND_PROPAGATED" : - // es == EQUALITY_TRUE ? "EQUALITY_TRUE" : - // es == EQUALITY_FALSE ? "EQUALITY_FALSE" : - // es == EQUALITY_TRUE_IN_MODEL ? "EQUALITY_TRUE_IN_MODEL" : - // es == EQUALITY_FALSE_IN_MODEL ? "EQUALITY_FALSE_IN_MODEL" : - // es == EQUALITY_UNKNOWN ? "EQUALITY_UNKNOWN" : - // "Unexpected case") << endl; - - // We need to split on it - Debug("combineTheories") << "TheoryEngine::combineTheories(): requesting a split " << endl; - - lemma(equality.orNode(equality.notNode()), - RULE_INVALID, - false, - LemmaProperty::NONE, - carePair.d_theory); - - // This code is supposed to force preference to follow what the theory models already have - // but it doesn't seem to make a big difference - need to explore more -Clark - // if (true) { - // if (es == EQUALITY_TRUE || es == EQUALITY_TRUE_IN_MODEL) { - Node e = ensureLiteral(equality); - d_propEngine->requirePhase(e, true); - // } - // else if (es == EQUALITY_FALSE_IN_MODEL) { - // Node e = ensureLiteral(equality); - // d_propEngine->requirePhase(e, false); - // } - // } - } -} - -void TheoryEngine::propagate(Theory::Effort effort) { +void TheoryEngine::propagate(Theory::Effort effort) +{ // Reset the interrupt flag d_interrupted = false; @@ -762,99 +681,37 @@ 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; +TheoryModel* TheoryEngine::getModel() +{ + Assert(d_tc != nullptr); + TheoryModel* m = d_tc->getModel(); + Assert(m != nullptr); + return m; } -bool TheoryEngine::collectModelInfo(theory::TheoryModel* m) +TheoryModel* TheoryEngine::getBuiltModel() { - //have shared term engine collectModelInfo - // d_sharedTerms.collectModelInfo( m ); - // Consult each active theory to get all relevant information - // concerning the model. - for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) { - if(d_logicInfo.isTheoryEnabled(theoryId)) { - Trace("model-builder") << " CollectModelInfo on theory: " << theoryId << endl; - if (!d_theoryTable[theoryId]->collectModelInfo(m)) - { - return false; - } - } - } - Trace("model-builder") << " CollectModelInfo boolean variables" << std::endl; - // Get the Boolean variables - vector<TNode> boolVars; - d_propEngine->getBooleanVariables(boolVars); - vector<TNode>::iterator it, iend = boolVars.end(); - bool hasValue, value; - for (it = boolVars.begin(); it != iend; ++it) { - TNode var = *it; - hasValue = d_propEngine->hasValue(var, value); - // TODO: Assert that hasValue is true? - if (!hasValue) { - Trace("model-builder-assertions") - << " has no value : " << var << std::endl; - value = false; - } - Trace("model-builder-assertions") << "(assert" << (value ? " " : " (not ") << var << (value ? ");" : "));") << endl; - if (!m->assertPredicate(var, value)) - { - return false; - } + 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) + { + // not available, perhaps due to interuption. + return nullptr; } - 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 ); - } + // must build model at this point + if (!d_tc->buildModel()) + { + return nullptr; } + return d_tc->getModel(); } -TheoryModel* TheoryEngine::getModel() { - return d_curr_model; -} - -TheoryModel* TheoryEngine::getBuiltModel() +bool TheoryEngine::buildModel() { - if (!d_curr_model->isBuilt()) - { - // If this method was called, we should be in SAT mode, and produceModels - // should be true. - AlwaysAssert(options::produceModels()); - if (!d_inSatMode) - { - // not available, perhaps due to interuption. - return nullptr; - } - // must build model at this point - d_curr_model_builder->buildModel(d_curr_model); - } - return d_curr_model; + Assert(d_tc != nullptr); + return d_tc->buildModel(); } bool TheoryEngine::getSynthSolutions( @@ -1209,7 +1066,6 @@ void TheoryEngine::assertFact(TNode literal) 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 @@ -1233,7 +1089,8 @@ void TheoryEngine::assertFact(TNode literal) 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 @@ -1259,7 +1116,6 @@ void TheoryEngine::assertFact(TNode literal) } bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) { - Debug("theory::propagate") << "TheoryEngine::propagate(" << literal << ", " << theory << ")" << endl; Trace("dtview::prop") << std::string(d_context->getLevel(), ' ') @@ -1821,11 +1677,6 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { }); } -SharedTermsDatabase* TheoryEngine::getSharedTermsDatabase() -{ - return &d_sharedTerms; -} - void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector, LemmaProofRecipe* proofRecipe) { Assert(explanationVector.size() > 0); @@ -2048,7 +1899,7 @@ void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) { // not relevant, skip continue; } - Node val = getModel()->getValue(assertion); + Node val = d_tc->getModel()->getValue(assertion); if (val != d_true) { std::stringstream ss; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index ff4c3bdf9..61ee30bc8 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -38,7 +38,6 @@ #include "theory/engine_output_channel.h" #include "theory/interrupted.h" #include "theory/rewriter.h" -#include "theory/shared_terms_database.h" #include "theory/sort_inference.h" #include "theory/substitutions.h" #include "theory/term_registration_visitor.h" @@ -87,11 +86,8 @@ struct NodeTheoryPairHashFunction { /* Forward declarations */ namespace theory { -class CombinationEngine; class TheoryModel; -class TheoryEngineModelBuilder; -class EqEngineManagerDistributed; - +class CombinationEngine; class DecisionManager; class RelevanceManager; @@ -122,6 +118,7 @@ class TheoryEngine { friend class theory::CombinationEngine; friend class theory::quantifiers::TermDb; friend class theory::EngineOutputChannel; + friend class theory::CombinationEngine; /** Associated PropEngine engine */ prop::PropEngine* d_propEngine; @@ -152,15 +149,8 @@ class TheoryEngine { */ SharedTermsDatabase d_sharedTerms; - /** - * The distributed equality manager. This class is responsible for - * configuring the theories of this class for handling equalties - * in a "distributed" fashion, i.e. each theory maintains a unique - * instance of an equality engine. These equality engines are memory - * managed by this class. - */ - std::unique_ptr<theory::EqEngineManagerDistributed> d_eeDistributed; - + /** The combination manager we are using */ + std::unique_ptr<theory::CombinationEngine> d_tc; /** * The quantifiers engine */ @@ -172,16 +162,12 @@ class TheoryEngine { /** The relevance manager */ std::unique_ptr<theory::RelevanceManager> d_relManager; - /** - * Default model object - */ - theory::TheoryModel* d_curr_model; - bool d_aloc_curr_model; - /** - * Model builder object - */ - theory::TheoryEngineModelBuilder* d_curr_model_builder; - bool d_aloc_curr_model_builder; + /** Default visitor for pre-registration */ + PreRegisterVisitor d_preRegistrationVisitor; + + /** Visitor for collecting shared terms */ + SharedTermsVisitor d_sharedTermsVisitor; + /** are we in eager model building mode? (see setEagerModelBuilding). */ bool d_eager_model_building; @@ -242,7 +228,6 @@ class TheoryEngine { d_incomplete = true; } - /** * Mapping of propagations from recievers to senders. */ @@ -428,11 +413,6 @@ class TheoryEngine { context::CDO<bool> d_factsAsserted; /** - * Map from equality atoms to theories that would like to be notified about them. - */ - - - /** * Assert the formula to the given theory. * @param assertion the assertion to send (not necesserily normalized) * @param original the assertion as it was sent in from the propagating theory @@ -466,8 +446,7 @@ class TheoryEngine { */ void getExplanation(std::vector<NodeTheoryPair>& explanationVector, LemmaProofRecipe* lemmaProofRecipe); -public: - + public: /** * Signal the start of a new round of assertion preprocessing */ @@ -510,7 +489,6 @@ public: * or during LAST_CALL effort. */ bool isRelevant(Node lit) const; - /** * This is called at shutdown time by the SmtEngine, just before * destruction. It is important because there are destruction @@ -543,11 +521,6 @@ public: void check(theory::Theory::Effort effort); /** - * Run the combination framework. - */ - void combineTheories(); - - /** * Calls ppStaticLearn() on all theories, accumulating their * combined contributions in the "learned" builder. */ @@ -585,8 +558,6 @@ public: Node getNextDecisionRequest(); bool properConflict(TNode conflict) const; - bool properPropagation(TNode lit) const; - bool properExplanation(TNode node, TNode expl) const; /** * Returns an explanation of the node propagated to the SAT solver. @@ -600,13 +571,6 @@ public: Node getExplanationAndRecipe(TNode node, LemmaProofRecipe* proofRecipe); /** - * collect model info - */ - bool collectModelInfo(theory::TheoryModel* m); - /** post process model */ - void postProcessModel( theory::TheoryModel* m ); - - /** * Get the pointer to the model object used by this theory engine. */ theory::TheoryModel* getModel(); @@ -622,6 +586,15 @@ public: * was interrupted), then this returns the null pointer. */ theory::TheoryModel* getBuiltModel(); + /** + * This forces the model maintained by the combination engine to be built + * if it has not been done so already. This should be called only during a + * last call effort check after theory combination is run. + * + * @return true if the model was successfully built (possibly prior to this + * call). + */ + bool buildModel(); /** set eager model building * * If this method is called, then this TheoryEngine will henceforth build @@ -650,11 +623,6 @@ public: bool getSynthSolutions(std::map<Node, std::map<Node, Node> >& sol_map); /** - * Get the model builder - */ - theory::TheoryEngineModelBuilder* getModelBuilder() { return d_curr_model_builder; } - - /** * Get the theory associated to a given Node. * * @returns the theory, or NULL if the TNode is @@ -735,11 +703,6 @@ public: std::pair<bool, Node> entailmentCheck(options::TheoryOfMode mode, TNode lit); private: - /** Default visitor for pre-registration */ - PreRegisterVisitor d_preRegistrationVisitor; - - /** Visitor for collecting shared terms */ - SharedTermsVisitor d_sharedTermsVisitor; /** Dump the assertions to the dump */ void dumpAssertions(const char* tag); @@ -747,8 +710,6 @@ public: /** For preprocessing pass lifting bit-vectors of size 1 to booleans */ public: - SharedTermsDatabase* getSharedTermsDatabase(); - SortInference* getSortInference() { return &d_sortInfer; } /** Prints the assertions to the debug stream */ diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 725a932a2..31b44aa70 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -75,8 +75,6 @@ void TheoryModel::finishInit() } void TheoryModel::reset(){ - d_modelBuilt = false; - d_modelBuiltSuccess = false; d_modelCache.clear(); d_comment_str.clear(); d_sep_heap = Node::null(); diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index f465cec88..b725cfa09 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -95,21 +95,6 @@ public: /** reset the model */ virtual void reset(); - /** is built - * - * Have we attempted to build this model since the last - * call to reset? Notice for model building techniques - * that are not guaranteed to succeed (such as - * when quantified formulas are enabled), a true return - * value does not imply that this is a model of the - * current assertions. - */ - bool isBuilt() { return d_modelBuilt; } - /** is built success - * - * Was this model successfully built since the last call to reset? - */ - bool isBuiltSuccess() { return d_modelBuiltSuccess; } //---------------------------- for building the model /** Adds a substitution from x to t. */ void addSubstitution(TNode x, TNode t, bool invalidateCache = true); @@ -363,10 +348,6 @@ public: std::string d_name; /** substitution map for this model */ SubstitutionMap d_substitutions; - /** whether we have tried to build this model in the current context */ - bool d_modelBuilt; - /** whether this model has been built successfully */ - bool d_modelBuiltSuccess; /** equality engine containing all known equalities/disequalities */ eq::EqualityEngine* d_equalityEngine; /** approximations (see recordApproximation) */ diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index c82486bdd..31ba60be1 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -372,32 +372,11 @@ void TheoryEngineModelBuilder::addToTypeList( } } -bool TheoryEngineModelBuilder::buildModel(Model* m) +bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) { Trace("model-builder") << "TheoryEngineModelBuilder: buildModel" << std::endl; - TheoryModel* tm = (TheoryModel*)m; eq::EqualityEngine* ee = tm->d_equalityEngine; - // buildModel should only be called once per check - Assert(!tm->isBuilt()); - - // Reset model - tm->reset(); - - // mark as built - tm->d_modelBuilt = true; - tm->d_modelBuiltSuccess = false; - - // Collect model info from the theories - Trace("model-builder") << "TheoryEngineModelBuilder: Collect model info..." - << std::endl; - if (!d_te->collectModelInfo(tm)) - { - Trace("model-builder") - << "TheoryEngineModelBuilder: fail collect model info" << std::endl; - return false; - } - Trace("model-builder") << "TheoryEngineModelBuilder: Preprocess build model..." << std::endl; // model-builder specific initialization @@ -943,7 +922,6 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) return false; } Trace("model-builder") << "TheoryEngineModelBuilder: success" << std::endl; - tm->d_modelBuiltSuccess = true; return true; } void TheoryEngineModelBuilder::computeAssignableInfo( @@ -1124,7 +1102,6 @@ void TheoryEngineModelBuilder::postProcessModel(bool incomplete, Model* m) void TheoryEngineModelBuilder::debugCheckModel(TheoryModel* tm) { #ifdef CVC4_ASSERTIONS - Assert(tm->isBuilt()); if (tm->hasApproximations()) { // models with approximations may fail the assertions below diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h index 0be92c95c..898ca7dbc 100644 --- a/src/theory/theory_model_builder.h +++ b/src/theory/theory_model_builder.h @@ -46,19 +46,22 @@ class TheoryEngineModelBuilder public: TheoryEngineModelBuilder(TheoryEngine* te); virtual ~TheoryEngineModelBuilder() {} - /** Build model function. - * - * Should be called only on TheoryModels m. + /** + * Should be called only on models m after they have been prepared + * (e.g. using ModelManager). In other words, the equality engine of model + * m contains all relevant information from each theory that is needed + * for building a model. This class is responsible simply for ensuring + * that all equivalence classes of the equality engine of m are assigned + * constants. * * This constructs the model m, via the following steps: - * (1) call TheoryEngine::collectModelInfo, - * (2) builder-specified pre-processing, - * (3) find the equivalence classes of m's + * (1) builder-specified pre-processing, + * (2) find the equivalence classes of m's * equality engine that initially contain constants, - * (4) assign constants to all equivalence classes + * (3) assign constants to all equivalence classes * of m's equality engine, through alternating * iterations of evaluation and enumeration, - * (5) builder-specific processing, which includes assigning total + * (4) builder-specific processing, which includes assigning total * interpretations to uninterpreted functions. * * This function returns false if any of the above @@ -67,7 +70,7 @@ class TheoryEngineModelBuilder * builder in steps (2) or (5), for instance, if the model we * are building fails to satisfy a quantified formula. */ - bool buildModel(Model* m); + bool buildModel(TheoryModel* m); /** postprocess model * |