Removing a few deprecated options (#4052)

9 files changed, 25 insertions, 157 deletions

diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml
index 7eb9d30c5..82e833506 100644
--- a/src/options/datatypes_options.toml
+++ b/src/options/datatypes_options.toml
@@ -119,15 +119,6 @@ header = "options/datatypes_options.h"
   type       = "bool"
   default    = "true"
   help       = "sygus symmetry breaking lemmas based on pbe conjectures"
-  
-[[option]]
-  name       = "sygusOpt1"
-  category   = "regular"
-  long       = "sygus-opt1"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "sygus experimental option"
 
 [[option]]
   name       = "sygusSymBreakLazy"
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 6e0460ae9..12549152d 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -677,15 +677,6 @@ header = "options/quantifiers_options.h"
   help       = "only add one instantiation per quantifier per round for mbqi"
 
 [[option]]
-  name       = "fmfOneQuantPerRound"
-  category   = "regular"
-  long       = "mbqi-one-quant-per-round"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "only add instantiations for one quantifier per round for mbqi"
-
-[[option]]
   name       = "mbqiInterleave"
   category   = "regular"
   long       = "mbqi-interleave"
@@ -703,24 +694,6 @@ header = "options/quantifiers_options.h"
   help       = "use instantiation engine in conjunction with finite model finding"
 
 [[option]]
-  name       = "fmfInstGen"
-  category   = "regular"
-  long       = "fmf-inst-gen"
-  type       = "bool"
-  default    = "true"
-  read_only  = true
-  help       = "enable Inst-Gen instantiation techniques for finite model finding"
-
-[[option]]
-  name       = "fmfInstGenOneQuantPerRound"
-  category   = "regular"
-  long       = "fmf-inst-gen-one-quant-per-round"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "only perform Inst-Gen instantiation techniques on one quantifier per round"
-
-[[option]]
   name       = "fmfFreshDistConst"
   category   = "regular"
   long       = "fmf-fresh-dc"
@@ -871,14 +844,6 @@ header = "options/quantifiers_options.h"
   help       = "do not consider instances of quantified formulas that are currently true in model, if it is available"
 
 [[option]]
-  name       = "instPropagate"
-  category   = "regular"
-  long       = "inst-prop"
-  type       = "bool"
-  default    = "false"
-  help       = "internal propagation for instantiations for selecting relevant instances"
-
-[[option]]
   name       = "qcfEagerTest"
   category   = "regular"
   long       = "qcf-eager-test"
@@ -905,17 +870,6 @@ header = "options/quantifiers_options.h"
   read_only  = true
   help       = "optimization, skip instances based on possibly irrelevant portions of quantified formulas"
 
-### Rewrite rules options
-
-[[option]]
-  name       = "rrOneInstPerRound"
-  category   = "regular"
-  long       = "rr-one-inst-per-round"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "add one instance of rewrite rule per round"
-
 ### Induction options
 
 [[option]]
@@ -1378,15 +1332,6 @@ header = "options/quantifiers_options.h"
   help       = "do unfolding of Boolean evaluation functions that appear in refinement lemmas"
 
 [[option]]
-  name       = "sygusRefEval"
-  category   = "regular"
-  long       = "sygus-ref-eval"
-  type       = "bool"
-  default    = "true"
-  read_only  = true
-  help       = "direct evaluation of refinement lemmas for conflict analysis"
-
-[[option]]
   name       = "sygusStream"
   category   = "regular"
   long       = "sygus-stream"
@@ -1429,14 +1374,6 @@ header = "options/quantifiers_options.h"
   help = "Trust that when a solution for a conjecture is always true under sampling, then it is indeed a solution. Note this option may print out spurious solutions for synthesis conjectures."
 
 [[option]]
-  name       = "minSynthSol"
-  category   = "regular"
-  long       = "min-synth-sol"
-  type       = "bool"
-  default    = "true"
-  help       = "Minimize synthesis solutions"
-
-[[option]]
   name       = "sygusEvalOpt"
   category   = "regular"
   long       = "sygus-eval-opt"
diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml
index f51c4ce67..49c304bab 100644
--- a/src/options/strings_options.toml
+++ b/src/options/strings_options.toml
@@ -11,17 +11,6 @@ header = "options/strings_options.h"
   help       = "experimental features in the theory of strings"
 
 [[option]]
-  name       = "stringLB"
-  smt_name   = "strings-lb"
-  category   = "regular"
-  long       = "strings-lb=N"
-  type       = "unsigned"
-  default    = "0"
-  predicates = ["unsignedLessEqual2"]
-  read_only  = true
-  help       = "the strategy of LB rule application: 0-lazy, 1-eager, 2-no"
-
-[[option]]
   name       = "stdPrintASCII"
   category   = "regular"
   long       = "strings-print-ascii"
@@ -48,15 +37,6 @@ header = "options/strings_options.h"
   help       = "strings eager check"
 
 [[option]]
-  name       = "stringEIT"
-  category   = "regular"
-  long       = "strings-eit"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "the eager intersection used by the theory of strings"
-
-[[option]]
   name       = "stringIgnNegMembership"
   category   = "regular"
   long       = "strings-inm"
diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index 24288216f..d962ad189 100644
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -130,39 +130,10 @@ void SygusExtension::assertFact( Node n, bool polarity, std::vector< Node >& lem
 Node SygusExtension::getTermOrderPredicate( Node n1, Node n2 ) {
   NodeManager* nm = NodeManager::currentNM();
   std::vector< Node > comm_disj;
-  // (1) size of left is greater than size of right
-  Node sz_less =
-      nm->mkNode(GT, nm->mkNode(DT_SIZE, n1), nm->mkNode(DT_SIZE, n2));
-  comm_disj.push_back( sz_less );
-  // (2) ...or sizes are equal and first child is less by term order
-  std::vector<Node> sz_eq_cases;
-  Node sz_eq =
-      nm->mkNode(EQUAL, nm->mkNode(DT_SIZE, n1), nm->mkNode(DT_SIZE, n2));
-  sz_eq_cases.push_back( sz_eq );
-  if( options::sygusOpt1() ){
-    TypeNode tnc = n1.getType();
-    const DType& cdt = tnc.getDType();
-    for( unsigned j=0; j<cdt.getNumConstructors(); j++ ){
-      std::vector<Node> case_conj;
-      for (unsigned k = 0; k < j; k++)
-      {
-        case_conj.push_back(utils::mkTester(n2, k, cdt).negate());
-      }
-      if (!case_conj.empty())
-      {
-        Node corder = nm->mkNode(
-            OR,
-            utils::mkTester(n1, j, cdt).negate(),
-            case_conj.size() == 1 ? case_conj[0] : nm->mkNode(AND, case_conj));
-        sz_eq_cases.push_back(corder);
-      }
-    }
-  }
-  Node sz_eqc = sz_eq_cases.size() == 1 ? sz_eq_cases[0]
-                                        : nm->mkNode(kind::AND, sz_eq_cases);
-  comm_disj.push_back( sz_eqc );
-
-  return nm->mkNode(kind::OR, comm_disj);
+  // size of left is greater than or equal to the size of right
+  Node szGeq =
+      nm->mkNode(GEQ, nm->mkNode(DT_SIZE, n1), nm->mkNode(DT_SIZE, n2));
+  return szGeq;
 }
 
 void SygusExtension::registerTerm( Node n, std::vector< Node >& lemmas ) {
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index 5b2931e42..4012f687f 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -163,11 +163,6 @@ void ModelEngine::assertNode( Node f ){
 
 }
 
-bool ModelEngine::optOneQuantPerRound(){
-  return options::fmfOneQuantPerRound();
-}
-
-
 int ModelEngine::checkModel(){
   FirstOrderModel* fm = d_quantEngine->getModel();
 
@@ -230,7 +225,8 @@ int ModelEngine::checkModel(){
       //determine if we should check this quantifier
       if( d_quantEngine->getModel()->isQuantifierActive( q ) && d_quantEngine->hasOwnership( q, this ) ){
         exhaustiveInstantiate( q, e );
-        if( d_quantEngine->inConflict() || ( optOneQuantPerRound() && d_addedLemmas>0 ) ){
+        if (d_quantEngine->inConflict())
+        {
           break;
         }
       }else{
diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h
index b39dd03f8..3165b01db 100644
--- a/src/theory/quantifiers/fmf/model_engine.h
+++ b/src/theory/quantifiers/fmf/model_engine.h
@@ -29,9 +29,6 @@ class ModelEngine : public QuantifiersModule
 {
   friend class RepSetIterator;
 private:
-  //options
-  bool optOneQuantPerRound();
-private:
   //check model
   int checkModel();
   //exhaustively instantiate quantifier (possibly using mbqi)
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
index f81d2455c..2e5a834b1 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
@@ -556,12 +556,9 @@ Node CegSingleInv::reconstructToSyntax(Node s,
   }else{
     Trace("csi-sol") << "Post-process solution..." << std::endl;
     Node prev = d_solution;
-    if (options::minSynthSol())
-    {
-      d_solution =
-          d_qe->getTermDatabaseSygus()->getExtRewriter()->extendedRewrite(
-              d_solution);
-    }
+    d_solution =
+        d_qe->getTermDatabaseSygus()->getExtRewriter()->extendedRewrite(
+            d_solution);
     if( prev!=d_solution ){
       Trace("csi-sol") << "Solution (after post process) : " << d_solution << std::endl;
     }
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index 3ef3a3edc..57fe40517 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -136,8 +136,7 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates,
   bool addedEvalLemmas = false;
   // Refinement evaluation should not be done for grammars with symbolic
   // constructors.
-  bool doRefEval = options::sygusRefEval() && !d_usingSymCons;
-  if (doRefEval)
+  if (!d_usingSymCons)
   {
     Trace("cegqi-engine") << "  *** Do refinement lemma evaluation"
                           << (doGen ? " with conjecture-specific refinement"
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index e2cafa4d3..723a8c08e 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -1484,22 +1484,22 @@ bool CoreSolver::detectLoop(NormalForm& nfi,
                                unsigned rproc)
 {
   int has_loop[2] = { -1, -1 };
-  if( options::stringLB() != 2 ) {
-    for( unsigned r=0; r<2; r++ ) {
-      NormalForm& nf = r == 0 ? nfi : nfj;
-      NormalForm& nfo = r == 0 ? nfj : nfi;
-      std::vector<Node>& nfv = nf.d_nf;
-      std::vector<Node>& nfov = nfo.d_nf;
-      if (!nfov[index].isConst())
+  for (unsigned r = 0; r < 2; r++)
+  {
+    NormalForm& nf = r == 0 ? nfi : nfj;
+    NormalForm& nfo = r == 0 ? nfj : nfi;
+    std::vector<Node>& nfv = nf.d_nf;
+    std::vector<Node>& nfov = nfo.d_nf;
+    if (nfov[index].isConst())
+    {
+      continue;
+    }
+    for (unsigned lp = index + 1, lpEnd = nfv.size() - rproc; lp < lpEnd; lp++)
+    {
+      if (nfv[lp] == nfov[index])
       {
-        for (unsigned lp = index + 1; lp < nfv.size() - rproc; lp++)
-        {
-          if (nfv[lp] == nfov[index])
-          {
-            has_loop[r] = lp;
-            break;
-          }
-        }
+        has_loop[r] = lp;
+        break;
       }
     }
   }