diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-04-04 11:21:30 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-04-04 11:21:30 -0500 |
commit | 6c0a62d69368b1af7e9777efcd703da6dc1cda11 (patch) | |
tree | 677d518d345a230c35bfbcb016fca199185f131e | |
parent | 6cb3f49d3933061000fe63d2ee7e004cae06d6ba (diff) |
Simplify Theory::collectModelInfo interface to not take deprecated fullModel argument.
27 files changed, 43 insertions, 49 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 5af613a94..45dcd5d51 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -102,8 +102,8 @@ void TheoryArith::propagate(Effort e) { d_internal->propagate(e); } -void TheoryArith::collectModelInfo( TheoryModel* m, bool fullModel ){ - d_internal->collectModelInfo(m, fullModel); +void TheoryArith::collectModelInfo( TheoryModel* m ){ + d_internal->collectModelInfo(m); } void TheoryArith::notifyRestart(){ diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 267c10e4b..5dcea4be0 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -61,7 +61,7 @@ public: bool getCurrentSubstitution( int effort, std::vector< Node >& vars, std::vector< Node >& subs, std::map< Node, std::vector< Node > >& exp ); bool isExtfReduced( int effort, Node n, Node on, std::vector< Node >& exp ); - void collectModelInfo( TheoryModel* m, bool fullModel ); + void collectModelInfo( TheoryModel* m ); void shutdown(){ } diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index ba48f1704..fc700fbdc 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -4422,7 +4422,7 @@ Rational TheoryArithPrivate::deltaValueForTotalOrder() const{ return belowMin; } -void TheoryArithPrivate::collectModelInfo( TheoryModel* m, bool fullModel ){ +void TheoryArithPrivate::collectModelInfo( TheoryModel* m ){ AlwaysAssert(d_qflraStatus == Result::SAT); //AlwaysAssert(!d_nlIncomplete, "Arithmetic solver cannot currently produce models for input with nonlinear arithmetic constraints"); diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index d4afaccc6..79e7a77bc 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -443,7 +443,7 @@ public: Rational deltaValueForTotalOrder() const; - void collectModelInfo( TheoryModel* m, bool fullModel ); + void collectModelInfo( TheoryModel* m ); void shutdown(){ } diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 05094d5a8..8c619eeae 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -1038,7 +1038,7 @@ void TheoryArrays::computeCareGraph() ///////////////////////////////////////////////////////////////////////////// -void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ) +void TheoryArrays::collectModelInfo( TheoryModel* m ) { set<Node> termSet; diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index a1d275364..574702368 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -246,7 +246,7 @@ class TheoryArrays : public Theory { public: - void collectModelInfo(TheoryModel* m, bool fullModel); + void collectModelInfo(TheoryModel* m); ///////////////////////////////////////////////////////////////////////////// // NOTIFICATIONS diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 651d44841..9db909c22 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -576,14 +576,14 @@ bool TheoryBV::needsCheckLastEffort() { return d_needsLastCallCheck; } -void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){ +void TheoryBV::collectModelInfo( TheoryModel* m ){ Assert(!inConflict()); if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { - d_eagerSolver->collectModelInfo(m, fullModel); + d_eagerSolver->collectModelInfo(m, true); } for (unsigned i = 0; i < d_subtheories.size(); ++i) { if (d_subtheories[i]->isComplete()) { - d_subtheories[i]->collectModelInfo(m, fullModel); + d_subtheories[i]->collectModelInfo(m, true); return; } } diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 9973b0736..62eb6f6b5 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -77,7 +77,7 @@ public: Node explain(TNode n); - void collectModelInfo( TheoryModel* m, bool fullModel ); + void collectModelInfo( TheoryModel* m ); std::string identify() const { return std::string("TheoryBV"); } diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 4a47618f1..4ca631184 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -1407,7 +1407,7 @@ void TheoryDatatypes::computeCareGraph(){ Trace("dt-cg-summary") << "...done, # pairs = " << n_pairs << std::endl; } -void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ +void TheoryDatatypes::collectModelInfo( TheoryModel* m ){ Trace("dt-cmi") << "Datatypes : Collect model info " << d_equalityEngine.consistent() << std::endl; Trace("dt-model") << std::endl; printModelDebug( "dt-model" ); diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index fffc4bdd7..6a26352ad 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -263,7 +263,7 @@ public: void presolve(); void addSharedTerm(TNode t); EqualityStatus getEqualityStatus(TNode a, TNode b); - void collectModelInfo( TheoryModel* m, bool fullModel ); + void collectModelInfo( TheoryModel* m ); void shutdown() { } std::string identify() const { return std::string("TheoryDatatypes"); } /** equality engine */ diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 4d3e584b4..7321f00c4 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -117,16 +117,14 @@ void TheoryQuantifiers::computeCareGraph() { //do nothing } -void TheoryQuantifiers::collectModelInfo(TheoryModel* m, bool fullModel) { - if(fullModel) { - for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) { - if((*i).assertion.getKind() == kind::NOT) { - Debug("quantifiers::collectModelInfo") << "got quant FALSE: " << (*i).assertion[0] << endl; - m->assertPredicate((*i).assertion[0], false); - } else { - Debug("quantifiers::collectModelInfo") << "got quant TRUE : " << *i << endl; - m->assertPredicate(*i, true); - } +void TheoryQuantifiers::collectModelInfo(TheoryModel* m) { + for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) { + if((*i).assertion.getKind() == kind::NOT) { + Debug("quantifiers::collectModelInfo") << "got quant FALSE: " << (*i).assertion[0] << endl; + m->assertPredicate((*i).assertion[0], false); + } else { + Debug("quantifiers::collectModelInfo") << "got quant TRUE : " << *i << endl; + m->assertPredicate(*i, true); } } } diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 462dcb339..38552d333 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -62,7 +62,7 @@ public: void check(Effort e); Node getNextDecisionRequest( unsigned& priority ); Node getValue(TNode n); - void collectModelInfo( TheoryModel* m, bool fullModel ); + void collectModelInfo( TheoryModel* m ); void shutdown() { } std::string identify() const { return std::string("TheoryQuantifiers"); } void setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value); diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 3f9f70c25..ce5c02179 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -200,7 +200,7 @@ void TheorySep::computeCareGraph() { ///////////////////////////////////////////////////////////////////////////// -void TheorySep::collectModelInfo( TheoryModel* m, bool fullModel ){ +void TheorySep::collectModelInfo( TheoryModel* m ){ set<Node> termSet; // Compute terms appearing in assertions and shared terms diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index bdbea7e6c..8dd1ed356 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -110,7 +110,7 @@ class TheorySep : public Theory { public: - void collectModelInfo(TheoryModel* m, bool fullModel); + void collectModelInfo(TheoryModel* m); void postProcessModel(TheoryModel* m); ///////////////////////////////////////////////////////////////////////////// diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index 52afe05e2..3c749b262 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -46,8 +46,8 @@ void TheorySets::check(Effort e) { d_internal->check(e); } -void TheorySets::collectModelInfo(TheoryModel* m, bool fullModel) { - d_internal->collectModelInfo(m, fullModel); +void TheorySets::collectModelInfo(TheoryModel* m) { + d_internal->collectModelInfo(m); } void TheorySets::computeCareGraph() { diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index 2ebb9947d..59117d905 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -50,7 +50,7 @@ public: void check(Effort); - void collectModelInfo(TheoryModel*, bool fullModel); + void collectModelInfo(TheoryModel* m); void computeCareGraph(); diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 7662f1544..5b9f4bf03 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1773,7 +1773,7 @@ EqualityStatus TheorySetsPrivate::getEqualityStatus(TNode a, TNode b) { /******************** Model generation ********************/ -void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel) { +void TheorySetsPrivate::collectModelInfo(TheoryModel* m) { Trace("sets-model") << "Set collect model info" << std::endl; set<Node> termSet; // Compute terms appearing in assertions and shared terms diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index affc09fb9..b7f911a70 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -167,7 +167,7 @@ public: void check(Theory::Effort); - void collectModelInfo(TheoryModel*, bool fullModel); + void collectModelInfo(TheoryModel* m); void computeCareGraph(); diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 930520725..42e43b543 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -452,8 +452,8 @@ void TheoryStrings::presolve() { ///////////////////////////////////////////////////////////////////////////// -void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) { - Trace("strings-model") << "TheoryStrings : Collect model info, fullModel = " << fullModel << std::endl; +void TheoryStrings::collectModelInfo( TheoryModel* m ) { + Trace("strings-model") << "TheoryStrings : Collect model info" << std::endl; Trace("strings-model") << "TheoryStrings : assertEqualityEngine." << std::endl; //AJR : no use doing this since we cannot preregister terms with finite types that don't belong to strings. diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index ab0256237..a905189af 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -217,7 +217,7 @@ private: // MODEL GENERATION ///////////////////////////////////////////////////////////////////////////// public: - void collectModelInfo(TheoryModel* m, bool fullModel); + void collectModelInfo(TheoryModel* m); ///////////////////////////////////////////////////////////////////////////// // NOTIFICATIONS diff --git a/src/theory/theory.h b/src/theory/theory.h index 611e487f1..37d818eac 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -515,11 +515,8 @@ public: * Get all relevant information in this theory regarding the current * model. This should be called after a call to check( FULL_EFFORT ) * for all theories with no conflicts and no lemmas added. - * If fullModel is true, then we must specify sufficient information for - * the model class to construct constant representatives for each equivalence - * class. */ - virtual void collectModelInfo( TheoryModel* m, bool fullModel ){ } + virtual void collectModelInfo( TheoryModel* m ){ } /** if theories want to do something with model after building, do it here */ virtual void postProcessModel( TheoryModel* m ){ } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index ba80b130e..4d2998c68 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -616,7 +616,7 @@ void TheoryEngine::check(Theory::Effort effort) { if(d_logicInfo.isQuantified()) { // quantifiers engine must pass effort last call check d_quantEngine->check(Theory::EFFORT_LAST_CALL); - // if returning incomplete or SAT, we have ensured that d_curr_model has been built with fullModel=true + // if returning incomplete or SAT, we have ensured that d_curr_model has been built } else if(options::produceModels() && !d_curr_model->isBuilt()) { // must build model at this point d_curr_model_builder->buildModel(d_curr_model); @@ -843,16 +843,15 @@ bool TheoryEngine::properExplanation(TNode node, TNode expl) const { return true; } -void TheoryEngine::collectModelInfo( theory::TheoryModel* m, bool fullModel ){ - Assert( fullModel ); // AJR : FIXME : remove/simplify fullModel argument everywhere +void TheoryEngine::collectModelInfo( theory::TheoryModel* m ){ //have shared term engine collectModelInfo - // d_sharedTerms.collectModelInfo( m, fullModel ); + // 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; - d_theoryTable[theoryId]->collectModelInfo( m, fullModel ); + d_theoryTable[theoryId]->collectModelInfo( m ); } } // Get the Boolean variables diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index dd2b4f14d..e821b4017 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -714,7 +714,7 @@ public: /** * collect model info */ - void collectModelInfo( theory::TheoryModel* m, bool fullModel ); + void collectModelInfo( theory::TheoryModel* m ); /** post process model */ void postProcessModel( theory::TheoryModel* m ); diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index de48c956a..4de0d6a54 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -586,7 +586,7 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) Trace("model-builder") << "TheoryEngineModelBuilder: buildModel" << std::endl; TheoryModel* tm = (TheoryModel*)m; - // buildModel with fullModel = true should only be called once in any context + // buildModel should only be called once per check Assert(!tm->isBuilt()); tm->d_modelBuilt = true; @@ -595,7 +595,7 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) // Collect model info from the theories Trace("model-builder") << "TheoryEngineModelBuilder: Collect model info..." << std::endl; - d_te->collectModelInfo(tm, true); + d_te->collectModelInfo(tm); // model-builder specific initialization if( !preProcessBuildModel(tm) ){ diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 82341c377..1d3906eee 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -106,7 +106,7 @@ public: * This function tells the model that n should be the representative of its equivalence class. * It should be called during model generation, before final representatives are chosen. In the * case of TheoryEngineModelBuilder, it should be called during Theory's collectModelInfo( ... ) - * functions where fullModel = true. + * functions. */ void assertRepresentative(TNode n); public: diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 1b47b0245..8166e3574 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -245,7 +245,7 @@ Node TheoryUF::explain(TNode literal, eq::EqProof* pf) { return mkAnd(assumptions); } -void TheoryUF::collectModelInfo( TheoryModel* m, bool fullModel ){ +void TheoryUF::collectModelInfo( TheoryModel* m ){ set<Node> termSet; // Compute terms appearing in assertions and shared terms diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 41bafcb84..28db0195d 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -185,7 +185,7 @@ public: void preRegisterTerm(TNode term); Node explain(TNode n); - void collectModelInfo( TheoryModel* m, bool fullModel ); + void collectModelInfo( TheoryModel* m ); void ppStaticLearn(TNode in, NodeBuilder<>& learned); void presolve(); |