Removing and consolidating options for uf-ss and quantifiers. Bug fix for inst gen-style MBQI.

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++) {