From 33c1c517f6d4a052cc669f8e11cb80bf63fae2c9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 10 Mar 2022 13:20:35 -0600 Subject: [PATCH] Eliminate unecessary datatype options (#8280) --- src/options/datatypes_options.toml | 20 ------------------- src/theory/datatypes/theory_datatypes.cpp | 10 ---------- src/theory/datatypes/theory_datatypes.h | 2 -- .../quantifiers/cbqi-lia-dt-simp.smt2 | 2 +- .../regress1/fmf/lst-no-self-rev-exp.smt2 | 2 +- 5 files changed, 2 insertions(+), 34 deletions(-) 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 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)))) -- 2.30.2