diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-14 12:11:14 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-14 12:11:14 -0500 |
| commit | 126966a8d9cb6564b0ac31dd20f32059cc35156f (patch) | |
| tree | a9de10f9e2efad78437aa05c5c832c6f9d885c05 /src/theory/quantifiers/inst_gen.cpp | |
| parent | 24d60fa5654a32b09dc8de79b7704fbf40051478 (diff) | |
Refactoring to separate old and new model building/checking code.
Diffstat (limited to 'src/theory/quantifiers/inst_gen.cpp')
| -rw-r--r-- | src/theory/quantifiers/inst_gen.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/quantifiers/inst_gen.cpp b/src/theory/quantifiers/inst_gen.cpp index e495b39c0..192e58d7c 100644 --- a/src/theory/quantifiers/inst_gen.cpp +++ b/src/theory/quantifiers/inst_gen.cpp @@ -47,7 +47,7 @@ void InstGenProcess::addMatchValue( QuantifiersEngine* qe, Node f, Node val, Ins if( d_inst_trie[val].addInstMatch( qe, f, m, true ) ){ d_match_values.push_back( val ); d_matches.push_back( InstMatch( &m ) ); - qe->getModelEngine()->getModelBuilder()->d_instGenMatches++; + ((QModelBuilderIG*)qe->getModelEngine()->getModelBuilder())->d_instGenMatches++; } } } @@ -92,7 +92,7 @@ void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vecto //for each term we consider, calculate a current match for( size_t i=0; i<considerTerms.size(); i++ ){ Node n = considerTerms[i]; - bool isSelected = qe->getModelEngine()->getModelBuilder()->isTermSelected( n ); + bool isSelected = ((QModelBuilderIG*)qe->getModelEngine()->getModelBuilder())->isTermSelected( n ); bool hadSuccess CVC4_UNUSED = false; for( int t=(isSelected ? 0 : 1); t<2; t++ ){ if( t==0 || !n.getAttribute(NoMatchAttribute()) ){ @@ -193,7 +193,7 @@ void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f, std::vecto //process all values for( size_t i=0; i<considerTerms.size(); i++ ){ Node n = considerTerms[i]; - bool isSelected = qe->getModelEngine()->getModelBuilder()->isTermSelected( n ); + bool isSelected = ((QModelBuilderIG*)qe->getModelEngine()->getModelBuilder())->isTermSelected( n ); for( int t=(isSelected ? 0 : 1); t<2; t++ ){ //do not consider ground case if it is already congruent to another ground term if( t==0 || !n.getAttribute(NoMatchAttribute()) ){ |