From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 10 Mar 2022 19:20:35 +0000 (-0600)
Subject: Eliminate unecessary datatype options (#8280)
X-Git-Tag: cvc5-1.0.0~286
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=33c1c517f6d4a052cc669f8e11cb80bf63fae2c9;p=cvc5.git

Eliminate unecessary datatype options (#8280)
---

diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml
index 0bb0edba6..58c20c618 100644
--- 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 1461889b1..f3b1e0fba 100644
--- 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 68dedb6f3..ad3ced165 100644
--- 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 c48593a36..3db6b223a 100644
--- 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 432a3fdf6..4c06908dd 100644
--- 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))))