From: yoni206 <yoni206@users.noreply.github.com>
Date: Thu, 4 Feb 2021 23:46:12 +0000 (-0800)
Subject: Adding an option to optimize polite combination for datatypes (#5856)
X-Git-Tag: cvc5-1.0.0~2320
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7ee5ed0feaaf524237d5e4632948aaa3f1ec3fb6;p=cvc5.git

Adding an option to optimize polite combination for datatypes (#5856)

This PR makes the optimization introduced in bbca987 optional.
---

diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml
index 19434fa33..a43641c73 100644
--- a/src/options/datatypes_options.toml
+++ b/src/options/datatypes_options.toml
@@ -22,6 +22,16 @@ header = "options/datatypes_options.h"
   default    = "false"
   help       = "force the datatypes solver to give specific values to all datatypes terms before answering sat"
 
+[[option]]
+  name       = "dtPoliteOptimize"
+  smt_name   = "dt-polite-optimize"
+  category   = "experimental"
+  long       = "dt-polite-optimize"
+  type       = "bool"
+  default    = "true"
+  read_only  = true
+  help       = "turn on optimization for polite combination"
+
 [[option]]
   name       = "dtBinarySplit"
   category   = "regular"
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 7d5b555c2..cb3198423 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -1558,7 +1558,11 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
   // may contribute to conflicts due to cardinality (good examples of this are
   // regress0/datatypes/dt-param-card4-bool-sat.smt2 and
   // regress0/datatypes/list-bool.smt2).
-  bool forceLemma = dt[index].hasFiniteExternalArgType(ttn);
+  bool forceLemma = true;
+  if (options::dtPoliteOptimize())
+  {
+    forceLemma = dt[index].hasFiniteExternalArgType(ttn);
+  }
   Trace("datatypes-infer-debug") << "DtInstantiate : " << eqc << " " << eq
                                  << " forceLemma = " << forceLemma << std::endl;
   d_im.addPendingInference(eq, exp, forceLemma, InferId::INST);