diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-31 00:54:24 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-31 00:54:24 +0000 |
commit | f40d0a7cc8d6af511cc0817caf8df3296a59f380 (patch) | |
tree | a79f142c5b6fbeaec34978f8da2b2db308a33e79 /src/theory/quantifiers/model_builder.cpp | |
parent | 5b4c416608bda1df62e1ffe7131648a89882ddc7 (diff) |
cleaning up some of the equality query stuff, implemented a new representative selection strategy for quantifier instantiation
Diffstat (limited to 'src/theory/quantifiers/model_builder.cpp')
-rw-r--r-- | src/theory/quantifiers/model_builder.cpp | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index f2e195d2e..8b34a3a12 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -33,20 +33,20 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; -bool TermArgBasisTrie::addTerm2( QuantifiersEngine* qe, Node n, int argIndex ){ +bool TermArgBasisTrie::addTerm2( FirstOrderModel* fm, Node n, int argIndex ){ if( argIndex<(int)n.getNumChildren() ){ Node r; if( n[ argIndex ].getAttribute(ModelBasisAttribute()) ){ r = n[ argIndex ]; }else{ - r = qe->getEqualityQuery()->getRepresentative( n[ argIndex ] ); + r = fm->getRepresentative( n[ argIndex ] ); } std::map< Node, TermArgBasisTrie >::iterator it = d_data.find( r ); if( it==d_data.end() ){ - d_data[r].addTerm2( qe, n, argIndex+1 ); + d_data[r].addTerm2( fm, n, argIndex+1 ); return true; }else{ - return it->second.addTerm2( qe, n, argIndex+1 ); + return it->second.addTerm2( fm, n, argIndex+1 ); } }else{ return false; @@ -99,6 +99,7 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { } } } + //END FOR DEBUGGING }else{ d_curr_model = fm; d_addedLemmas = 0; @@ -162,6 +163,8 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { if( optOneQuantPerRoundInstGen() && addedLemmas>0 ){ break; } + }else if( d_quant_sat.find( f )!=d_quant_sat.end() ){ + d_numQuantSat++; } } Trace("model-engine-debug") << "Quantifiers sat/ig/n-ig/null " << d_numQuantSat << " / " << d_numQuantInstGen << " / "; @@ -267,7 +270,7 @@ void ModelEngineBuilder::analyzeModel( FirstOrderModel* fm ){ if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())==1 ){ if( !n.getAttribute(BasisNoMatchAttribute()) ){ //need to consider if it is not congruent modulo model basis - if( !tabt.addTerm( d_qe, n ) ){ + if( !tabt.addTerm( fm, n ) ){ BasisNoMatchAttribute bnma; n.setAttribute(bnma,true); } @@ -311,7 +314,7 @@ bool ModelEngineBuilder::optOneQuantPerRoundInstGen(){ } bool ModelEngineBuilder::optExhInstNonInstGenQuant(){ - return true; + return options::fmfNewInstGen(); } void ModelEngineBuilder::setEffort( int effort ){ |