Remove a few options (#4295)

These options are not robust and are not used.

Fixes #4282 and fixes #4291.

2 files changed, 19 insertions, 26 deletions

diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index 3e5d36a7d..af3a94d96 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -321,13 +321,14 @@ bool FullModelChecker::preProcessBuildModel(TheoryModel* m) {
   }
   Trace("fmc") << "Finish preInitialize types" << std::endl;
   //do not have to introduce terms for sorts of domains of quantified formulas if we are allowed to assume empty sorts
-  if( !options::fmfEmptySorts() ){
-    for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
-      Node q = fm->getAssertedQuantifier( i );
-      //make sure all types are set
-      for( unsigned j=0; j<q[0].getNumChildren(); j++ ){
-        preInitializeType( fm, q[0][j].getType() );
-      }
+  for (unsigned i = 0, nquant = fm->getNumAssertedQuantifiers(); i < nquant;
+       i++)
+  {
+    Node q = fm->getAssertedQuantifier(i);
+    // make sure all types are set
+    for (const Node& v : q[0])
+    {
+      preInitializeType(fm, v.getType());
     }
   }
   return true;
diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp
index 5ae05f2a7..a3dc50dd1 100644
--- a/src/theory/quantifiers/fmf/model_builder.cpp
+++ b/src/theory/quantifiers/fmf/model_builder.cpp
@@ -47,7 +47,8 @@ bool QModelBuilder::preProcessBuildModel(TheoryModel* m) {
 bool QModelBuilder::preProcessBuildModelStd(TheoryModel* m) {
   d_addedLemmas = 0;
   d_triedLemmas = 0;
-  if( options::fmfEmptySorts() || options::fmfFunWellDefinedRelevant() ){
+  if (options::fmfFunWellDefinedRelevant())
+  {
     FirstOrderModel * fm = (FirstOrderModel*)m;
     //traverse equality engine
     std::map< TypeNode, bool > eqc_usort;
@@ -63,28 +64,19 @@ bool QModelBuilder::preProcessBuildModelStd(TheoryModel* m) {
       Node q = fm->getAssertedQuantifier( i, true );
       if( fm->isQuantifierActive( q ) ){
         //check if any of these quantified formulas can be set inactive
-        if( options::fmfEmptySorts() ){
-          for (const Node& var : q[0])
+        if (q[0].getNumChildren() == 1)
+        {
+          TypeNode tn = q[0][0].getType();
+          if (tn.getAttribute(AbsTypeFunDefAttribute()))
           {
-            TypeNode tn = var.getType();
-            //we are allowed to assume the type is empty
-            if( tn.isSort() && eqc_usort.find( tn )==eqc_usort.end() ){
-              Trace("model-engine-debug") << "Empty domain quantified formula : " << q << std::endl;
+            // we are allowed to assume the introduced type is empty
+            if (eqc_usort.find(tn) == eqc_usort.end())
+            {
+              Trace("model-engine-debug")
+                  << "Irrelevant function definition : " << q << std::endl;
               fm->setQuantifierActive( q, false );
             }
           }
-        }else if( options::fmfFunWellDefinedRelevant() ){
-          if( q[0].getNumChildren()==1 ){
-            TypeNode tn = q[0][0].getType();
-            if( tn.getAttribute(AbsTypeFunDefAttribute()) ){
-              //Trace("model-engine-debug2") << "...possible irrelevant function def : " << q << ", #rr = " << d_quantEngine->getModel()->d_rep_set.getNumRelevantGroundReps( tn ) << std::endl;
-              //we are allowed to assume the introduced type is empty
-              if( eqc_usort.find( tn )==eqc_usort.end() ){
-                Trace("model-engine-debug") << "Irrelevant function definition : " << q << std::endl;
-                fm->setQuantifierActive( q, false );
-              }
-            }
-          }
         }
       }
     }