From 7ee5ed0feaaf524237d5e4632948aaa3f1ec3fb6 Mon Sep 17 00:00:00 2001 From: yoni206 Date: Thu, 4 Feb 2021 15:46:12 -0800 Subject: [PATCH] Adding an option to optimize polite combination for datatypes (#5856) This PR makes the optimization introduced in bbca987 optional. --- src/options/datatypes_options.toml | 10 ++++++++++ src/theory/datatypes/theory_datatypes.cpp | 6 +++++- 2 files changed, 15 insertions(+), 1 deletion(-) 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); -- 2.30.2