diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-27 11:20:50 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-10-27 11:20:50 -0500 |
commit | 079ed9540d498bcbb58f2f0fbe87bdae28101d1e (patch) | |
tree | 8c3ba1818dc515c1714b23555460a3a39192acc5 /src/theory/quantifiers/model_engine.cpp | |
parent | 03cc40cc070df0bc11c1556cef3016f784a95d23 (diff) |
Refactor theory model (#1236)
* Refactor theory model, working on making RepSet references const.
* Encapsulation of members of rep set.
* More documentation on rep set.
* Swap names
* Reference issues.
* Minor
* Minor
* New clang format.
Diffstat (limited to 'src/theory/quantifiers/model_engine.cpp')
-rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 19 |
1 files changed, 13 insertions, 6 deletions
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 081d4e66a..b3acb408f 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -165,11 +165,15 @@ int ModelEngine::checkModel(){ //flatten the representatives //Trace("model-engine-debug") << "Flattening representatives...." << std::endl; - //d_quantEngine->getEqualityQuery()->flattenRepresentatives( fm->d_rep_set.d_type_reps ); + // d_quantEngine->getEqualityQuery()->flattenRepresentatives( + // fm->getRepSet()->d_type_reps ); //for debugging, setup - for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin(); - it != fm->d_rep_set.d_type_reps.end(); ++it ){ + for (std::map<TypeNode, std::vector<Node> >::iterator it = + fm->getRepSetPtr()->d_type_reps.begin(); + it != fm->getRepSetPtr()->d_type_reps.end(); + ++it) + { if( it->first.isSort() ){ Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl; Trace("model-engine-debug") << " Reps : "; @@ -199,8 +203,10 @@ int ModelEngine::checkModel(){ int totalInst = 1; for( unsigned j=0; j<f[0].getNumChildren(); j++ ){ TypeNode tn = f[0][j].getType(); - if( fm->d_rep_set.hasType( tn ) ){ - totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size(); + if (fm->getRepSet()->hasType(tn)) + { + totalInst = + totalInst * (int)fm->getRepSet()->getNumRepresentatives(tn); } } d_totalLemmas += totalInst; @@ -271,7 +277,8 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ Trace("fmf-exh-inst-debug") << std::endl; } //create a rep set iterator and iterate over the (relevant) domain of the quantifier - RepSetIterator riter( d_quantEngine, &(d_quantEngine->getModel()->d_rep_set) ); + RepSetIterator riter(d_quantEngine, + d_quantEngine->getModel()->getRepSetPtr()); if( riter.setQuantifier( f ) ){ Trace("fmf-exh-inst") << "...exhaustive instantiation set, incomplete=" << riter.isIncomplete() << "..." << std::endl; if( !riter.isIncomplete() ){ |