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 19434fa33af9b28faeb88a9e94e44eea3b0c849d..a43641c7393f7847945e2e129381932e5f84ba5b 100644 (file)
--- 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 7d5b555c23db4961c8a55bbfde990768a0d3efee..cb3198423a283d83ac362f7b911ce4e500c0f450 100644 (file)
--- 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);