Eliminate unecessary datatype options (#8280)

diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml
index 0bb0edba6639f781225121867791a7f299913e14..58c20c6189d4b6fca35f5fb97c6ee8e5c9dce39d 100644 (file)
--- a/src/options/datatypes_options.toml
+++ b/src/options/datatypes_options.toml
@@ -1,26 +1,6 @@
 id     = "DATATYPES"
 name   = "Datatypes Theory"
 
-# How to handle selectors applied to incorrect constructors.  If this option is set,
-# then we do not rewrite such a selector term to an arbitrary ground term.  
-# For example, by default cvc5 considers cdr( nil ) = nil.  If this option is set, then
-# cdr( nil ) has no set value.
-[[option]]
-  name       = "dtRewriteErrorSel"
-  category   = "expert"
-  long       = "dt-rewrite-error-sel"
-  type       = "bool"
-  default    = "false"
-  help       = "rewrite incorrectly applied selectors to arbitrary ground term"
-
-[[option]]
-  name       = "dtForceAssignment"
-  category   = "regular"
-  long       = "dt-force-assignment"
-  type       = "bool"
-  default    = "false"
-  help       = "force the datatypes solver to give specific values to all datatypes terms before answering sat"
-
 [[option]]
   name       = "dtPoliteOptimize"
   category   = "expert"

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 1461889b1f68d22e9d2b1c938edb1bbe498dc35e..f3b1e0fba86d7a2d840c97df71f51373b9b5d3aa 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -69,7 +69,6 @@ TheoryDatatypes::TheoryDatatypes(Env& env,
 
   d_true = NodeManager::currentNM()->mkConst( true );
   d_zero = NodeManager::currentNM()->mkConstInt(Rational(0));
-  d_dtfCounter = 0;
 
   // indicate we are using the default theory state object
   d_theoryState = &d_state;
@@ -308,15 +307,6 @@ void TheoryDatatypes::postCheck(Effort level)
                   }
                 }
               }
-              //if we want to force an assignment of constructors to all ground eqc
-              //d_dtfCounter++;
-              if (!needSplit && options().datatypes.dtForceAssignment
-                  && d_dtfCounter % 2 == 0)
-              {
-                Trace("datatypes-force-assign") << "Force assignment for " << n << std::endl;
-                needSplit = true;
-                consIndex = fconsIndex!=-1 ? fconsIndex : consIndex;
-              }
 
               if( needSplit ) {
                 if( dt.getNumConstructors()==1 ){

diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 68dedb6f319baa59c3c8c6ca3d00d41b381f94b8..ad3ced16580f049a6c54e7c400aa80cfab048e16 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -149,8 +149,6 @@ private:
   BoolMap d_collectTermsCacheU;
   /** All the function terms that the theory has seen */
   context::CDList<TNode> d_functionTerms;
-  /** counter for forcing assignments (ensures fairness) */
-  unsigned d_dtfCounter;
   /** uninterpreted constant to variable map */
   std::map< Node, Node > d_uc_to_fresh_var;
 private:

diff --git a/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2 b/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2
index c48593a36379c942e26844662cfec28fdfc45748..3db6b223a14d2977728e5a91508bc0de3fc8273b 100644 (file)
--- a/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2
+++ b/test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi --dt-rewrite-error-sel
+; COMMAND-LINE: --cegqi
 ; EXPECT: unsat
 (set-logic ALL)
 (declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil))))

diff --git a/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2 b/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2
index 432a3fdf641f308201801711608032e4473389be..4c06908dd5da0d24f70dc8391896a7ee5df65df7 100644 (file)
--- a/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2
+++ b/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --dt-rewrite-error-sel -q
+; COMMAND-LINE: --finite-model-find -q
 ; EXPECT: sat
 (set-logic ALL)
 (declare-datatypes ((Nat 0) (Lst 0)) (((succ (pred Nat)) (zero)) ((cons (hd Nat) (tl Lst)) (nil))))