diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-03 22:36:55 -0600 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-01-03 22:36:55 -0600 |
commit | 2ce92038d8455637e313a1c2d0ce5d31a3d42b10 (patch) | |
tree | ce599c2e981bbd79d024e90cff6e97468b42712b /src/theory/quantifiers/model_builder.cpp | |
parent | 93f084750d8a76d63fc74d242944bce0635c2194 (diff) |
Removing and consolidating options for uf-ss and quantifiers. Bug fix for inst gen-style MBQI.
Diffstat (limited to 'src/theory/quantifiers/model_builder.cpp')
-rw-r--r-- | src/theory/quantifiers/model_builder.cpp | 21 |
1 files changed, 10 insertions, 11 deletions
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 468c78978..cb63ccd45 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -273,17 +273,15 @@ int QModelBuilderIG::initializeQuantifier( Node f, Node fp ){ ++(d_statistics.d_num_quants_init); } //try to add it - if( optInstGen() ){ - Trace("inst-fmf-init") << "Init: try to add match " << d_quant_basis_match[f] << std::endl; - //add model basis instantiation - if( d_qe->addInstantiation( fp, d_quant_basis_match[f], false, false, false ) ){ - d_quant_basis_match_added[f] = true; - return 1; - }else{ - //shouldn't happen usually, but will occur if x != y is a required literal for f. - //Notice() << "No model basis for " << f << std::endl; - d_quant_basis_match_added[f] = false; - } + Trace("inst-fmf-init") << "Init: try to add match " << d_quant_basis_match[f] << std::endl; + //add model basis instantiation + if( d_qe->addInstantiation( fp, d_quant_basis_match[f], false, false, false ) ){ + d_quant_basis_match_added[f] = true; + return 1; + }else{ + //shouldn't happen usually, but will occur if x != y is a required literal for f. + //Notice() << "No model basis for " << f << std::endl; + d_quant_basis_match_added[f] = false; } } return 0; @@ -418,6 +416,7 @@ bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i //if evaluate(...)==1, then the instantiation is already true in the model // depIndex is the index of the least significant variable that this evaluation relies upon depIndex = riter.getNumTerms()-1; + Debug("fmf-model-eval") << "We will evaluate " << d_qe->getTermDatabase()->getInstConstantBody( f ) << std::endl; eval = fmig->evaluate( d_qe->getTermDatabase()->getInstConstantBody( f ), depIndex, &riter ); if( eval==1 ){ Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl; |