From 6a4b16c643d71c9318042ba7b9d42af71c58ac2f Mon Sep 17 00:00:00 2001 From: yoni206 Date: Thu, 25 Feb 2021 12:36:05 -0800 Subject: [PATCH] Datatypes lemmas: share only external types (#5997) Forcing lemmas in datatypes used to be done only for external types. This was changed to consider all types, which is not needed. This PR brings back the restriction to external types. --- src/theory/datatypes/theory_datatypes.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 9d3b5a143..45787ee04 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -1562,11 +1562,15 @@ 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 = true; + bool forceLemma; if (options::dtPoliteOptimize()) { forceLemma = dt[index].hasFiniteExternalArgType(ttn); } + else + { + forceLemma = dt.involvesExternalType(); + } Trace("datatypes-infer-debug") << "DtInstantiate : " << eqc << " " << eq << " forceLemma = " << forceLemma << std::endl; d_im.addPendingInference(eq, InferenceId::DATATYPES_INST, exp, forceLemma); -- 2.30.2