From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 9 Dec 2020 04:08:52 +0000 (-0600)
Subject: Ensure CEGQI is applied for parametric datatypes when applicable (#5628)
X-Git-Tag: cvc5-1.0.0~2472
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e0846857d7f0a926203695315b565b3541175525;p=cvc5.git

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 0a5deb480..4e00a08e7 100644
--- 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 590c2fef2..0bb5c9ef7 100644
--- 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
index 000000000..1b72d3ba8
--- /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)