Ensure CEGQI is applied for parametric datatypes when applicable (#5628)

Previously was a bug computing the argument types of parametric datatypes.

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 0a5deb4802ccd783af590c3dc8f4ea94284866b0..4e00a08e7114cf5b33d78625aabe7ac23f73fd77 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -344,12 +344,24 @@ CegHandledStatus CegInstantiator::isCbqiSort(
     const DType& dt = tn.getDType();
     for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
     {
-      for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
+      // get the constructor type
+      TypeNode consType;
+      if (dt.isParametric())
+      {
+        // if parametric, must instantiate the argument types
+        consType = dt[i].getSpecializedConstructorType(tn);
+      }
+      else
+      {
+        consType = dt[i].getConstructor().getType();
+      }
+      for (const TypeNode& crange : consType)
       {
-        TypeNode crange = dt[i].getArgType(j);
         CegHandledStatus cret = isCbqiSort(crange, visited, qe);
         if (cret == CEG_UNHANDLED)
         {
+          Trace("cegqi-debug2")
+              << "Non-cbqi sort : " << tn << " due to " << crange << std::endl;
           visited[tn] = CEG_UNHANDLED;
           return CEG_UNHANDLED;
         }

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 590c2fef2eb12126c49f58f1ffa61c879620c2f9..0bb5c9ef7faff9390c8783d0041c23de8ef0781f 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -765,6 +765,7 @@ set(regress_0_tests
   regress0/quantifiers/cbqi-lia-dt-simp.smt2
   regress0/quantifiers/cegqi-nl-simp.cvc
   regress0/quantifiers/cegqi-nl-sq.smt2
+  regress0/quantifiers/cegqi-par-dt-simple.smt2
   regress0/quantifiers/clock-10.smt2
   regress0/quantifiers/clock-3.smt2
   regress0/quantifiers/cond-var-elim-binary.smt2

diff --git a/test/regress/regress0/quantifiers/cegqi-par-dt-simple.smt2 b/test/regress/regress0/quantifiers/cegqi-par-dt-simple.smt2
new file mode 100644 (file)
index 0000000..1b72d3b
--- /dev/null
+++ b/test/regress/regress0/quantifiers/cegqi-par-dt-simple.smt2
@@ -0,0 +1,7 @@
+; EXPECT: unsat
+(set-logic ALL)
+(declare-datatype List (par (T) ((nil) (cons (head T) (tail (List T))))))
+
+(declare-const x (List Int))
+(assert (not (exists ((y (List Int))) (= x (tail y)))))
+(check-sat)