diff options
Diffstat (limited to 'src/theory/quantifiers/full_model_check.cpp')
-rw-r--r-- | src/theory/quantifiers/full_model_check.cpp | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 174e26a5a..c7d7b7415 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -60,9 +60,9 @@ bool EntryTrie::hasGeneralization( FirstOrderModelFmc * m, Node c, int index ) { return true; } } - if( !options::fmfFmcInterval() || !c[index].getType().isInteger() ){ + if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !c[index].getType().isInteger() ){ //for star: check if all children are defined and have generalizations - if( options::fmfFmcCoverSimplify() && c[index]==st ){ + if( c[index]==st ){ ///options::fmfFmcCoverSimplify() //check if all children exist and are complete int num_child_def = d_child.size() - (d_child.find(st)!=d_child.end() ? 1 : 0); if( num_child_def==m->d_rep_set.getNumRepresentatives(tn) ){ @@ -92,7 +92,7 @@ int EntryTrie::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node> return d_data; }else{ int minIndex = -1; - if( options::fmfFmcInterval() && inst[index].getType().isInteger() ){ + if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && inst[index].getType().isInteger() ){ for( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){ //if( !m->isInterval( it->first ) ){ // std::cout << "Not an interval during getGenIndex " << it->first << std::endl; @@ -327,7 +327,7 @@ QModelBuilder( c, qe ){ bool FullModelChecker::optBuildAtFullModel() { //need to build after full model has taken effect if we are constructing interval models // this is because we need to have a constant in all integer equivalence classes - return options::fmfFmcInterval(); + return options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL; } void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ @@ -443,7 +443,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ Trace("fmc-warn") << "Warning : model has non-constant argument in model " << ri << std::endl; } children.push_back(ri); - if( !options::fmfFmcInterval() || !ri.getType().isInteger() ){ + if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !ri.getType().isInteger() ){ if (fm->isModelBasisTerm(ri) ) { ri = fm->getStar( ri.getType() ); }else{ @@ -485,7 +485,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ } - if( options::fmfFmcInterval() ){ + if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL ){ convertIntervalModel( fm, op ); } @@ -1103,7 +1103,7 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f, } }else{ if( !v.isNull() ){ - if( options::fmfFmcInterval() && v.getType().isInteger() ){ + if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && v.getType().isInteger() ){ for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) { if( fm->isInRange( v, it->first ) ){ doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second); @@ -1165,7 +1165,7 @@ int FullModelChecker::isCompat( FirstOrderModelFmc * fm, std::vector< Node > & c Trace("fmc-debug3") << "isCompat " << c << std::endl; Assert(cond.size()==c.getNumChildren()+1); for (unsigned i=1; i<cond.size(); i++) { - if( options::fmfFmcInterval() && cond[i].getType().isInteger() ){ + if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && cond[i].getType().isInteger() ){ Node iv = doIntervalMeet( fm, cond[i], c[i-1], false ); if( iv.isNull() ){ return 0; @@ -1184,7 +1184,7 @@ bool FullModelChecker::doMeet( FirstOrderModelFmc * fm, std::vector< Node > & co Assert(cond.size()==c.getNumChildren()+1); for (unsigned i=1; i<cond.size(); i++) { if( cond[i]!=c[i-1] ) { - if( options::fmfFmcInterval() && cond[i].getType().isInteger() ){ + if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && cond[i].getType().isInteger() ){ Node iv = doIntervalMeet( fm, cond[i], c[i-1] ); if( !iv.isNull() ){ cond[i] = iv; @@ -1254,7 +1254,7 @@ Node FullModelChecker::mkCondDefault( FirstOrderModelFmc * fm, Node f) { } void FullModelChecker::mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond ) { - Trace("fmc-debug") << "Make default vec, intervals = " << options::fmfFmcInterval() << std::endl; + Trace("fmc-debug") << "Make default vec, intervals = " << (options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL) << std::endl; //get function symbol for f cond.push_back(d_quant_cond[f]); for (unsigned i=0; i<f[0].getNumChildren(); i++) { |