Removing a few deprecated options (#4052)

4 files changed, 6 insertions, 17 deletions

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"