Remove a few options (#4295)

These options are not robust and are not used.

Fixes #4282 and fixes #4291.

5 files changed, 54 insertions, 82 deletions

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 5f07e687e..74b3ceca8 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -642,15 +642,6 @@ header = "options/quantifiers_options.h"
   help       = "find models for recursively defined functions, assumes functions are admissible, allows empty type when function is irrelevant"
 
 [[option]]
-  name       = "fmfEmptySorts"
-  category   = "regular"
-  long       = "fmf-empty-sorts"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "allow finite model finding to assume sorts that do not occur in ground assertions are empty"
-
-[[option]]
   name       = "mbqiMode"
   category   = "regular"
   long       = "mbqi=MODE"
diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml
index 49c304bab..44ca2c390 100644
--- a/src/options/strings_options.toml
+++ b/src/options/strings_options.toml
@@ -73,15 +73,6 @@ header = "options/strings_options.h"
   help       = "strings length normalization lemma"
 
 [[option]]
-  name       = "stringSplitEmp"
-  category   = "regular"
-  long       = "strings-sp-emp"
-  type       = "bool"
-  default    = "true"
-  read_only  = true
-  help       = "strings split on empty string"
-
-[[option]]
   name       = "stringInferSym"
   category   = "regular"
   long       = "strings-infer-sym"
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 );
-              }
-            }
-          }
         }
       }
     }
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index f262a2c7d..088bc4a16 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -473,44 +473,41 @@ Node InferenceManager::getRegisterTermAtomicLemma(
   Assert(s == LENGTH_SPLIT);
 
   std::vector<Node> lems;
-  if (options::stringSplitEmp() || !options::stringLenGeqZ())
-  {
-    Node n_len_eq_z = n_len.eqNode(d_zero);
-    Node n_len_eq_z_2 = n.eqNode(d_emptyString);
-    Node case_empty = nm->mkNode(AND, n_len_eq_z, n_len_eq_z_2);
-    case_empty = Rewriter::rewrite(case_empty);
-    Node case_nempty = nm->mkNode(GT, n_len, d_zero);
-    if (!case_empty.isConst())
-    {
-      Node lem = nm->mkNode(OR, case_empty, case_nempty);
-      lems.push_back(lem);
-      Trace("strings-lemma")
-          << "Strings::Lemma LENGTH >= 0 : " << lem << std::endl;
-      // prefer trying the empty case first
-      // notice that requirePhase must only be called on rewritten literals that
-      // occur in the CNF stream.
-      n_len_eq_z = Rewriter::rewrite(n_len_eq_z);
-      Assert(!n_len_eq_z.isConst());
-      reqPhase[n_len_eq_z] = true;
-      n_len_eq_z_2 = Rewriter::rewrite(n_len_eq_z_2);
-      Assert(!n_len_eq_z_2.isConst());
-      reqPhase[n_len_eq_z_2] = true;
-    }
-    else if (!case_empty.getConst<bool>())
-    {
-      // the rewriter knows that n is non-empty
-      Trace("strings-lemma")
-          << "Strings::Lemma LENGTH > 0 (non-empty): " << case_nempty
-          << std::endl;
-      lems.push_back(case_nempty);
-    }
-    else
-    {
-      // If n = "" ---> true or len( n ) = 0 ----> true, then we expect that
-      // n ---> "". Since this method is only called on non-constants n, it must
-      // be that n = "" ^ len( n ) = 0 does not rewrite to true.
-      Assert(false);
-    }
+  // split whether the string is empty
+  Node n_len_eq_z = n_len.eqNode(d_zero);
+  Node n_len_eq_z_2 = n.eqNode(d_emptyString);
+  Node case_empty = nm->mkNode(AND, n_len_eq_z, n_len_eq_z_2);
+  case_empty = Rewriter::rewrite(case_empty);
+  Node case_nempty = nm->mkNode(GT, n_len, d_zero);
+  if (!case_empty.isConst())
+  {
+    Node lem = nm->mkNode(OR, case_empty, case_nempty);
+    lems.push_back(lem);
+    Trace("strings-lemma") << "Strings::Lemma LENGTH >= 0 : " << lem
+                           << std::endl;
+    // prefer trying the empty case first
+    // notice that requirePhase must only be called on rewritten literals that
+    // occur in the CNF stream.
+    n_len_eq_z = Rewriter::rewrite(n_len_eq_z);
+    Assert(!n_len_eq_z.isConst());
+    reqPhase[n_len_eq_z] = true;
+    n_len_eq_z_2 = Rewriter::rewrite(n_len_eq_z_2);
+    Assert(!n_len_eq_z_2.isConst());
+    reqPhase[n_len_eq_z_2] = true;
+  }
+  else if (!case_empty.getConst<bool>())
+  {
+    // the rewriter knows that n is non-empty
+    Trace("strings-lemma") << "Strings::Lemma LENGTH > 0 (non-empty): "
+                           << case_nempty << std::endl;
+    lems.push_back(case_nempty);
+  }
+  else
+  {
+    // If n = "" ---> true or len( n ) = 0 ----> true, then we expect that
+    // n ---> "". Since this method is only called on non-constants n, it must
+    // be that n = "" ^ len( n ) = 0 does not rewrite to true.
+    Assert(false);
   }
 
   // additionally add len( x ) >= 0 ?