From 861dba0caea6c8bfa54bca58749323c4dbcfb282 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 14 Oct 2021 11:14:02 -0500
Subject: [PATCH] Fix quantifiers variable elimination for parametric datatypes
 (#7358)

Fixes #7353.
---
 .../quantifiers/quantifiers_rewriter.cpp      | 20 ++++++++++++++++---
 test/regress/CMakeLists.txt                   |  1 +
 .../issue7353-var-elim-par-dt.smt2            |  9 +++++++++
 3 files changed, 27 insertions(+), 3 deletions(-)
 create mode 100644 test/regress/regress0/quantifiers/issue7353-var-elim-par-dt.smt2

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 7c7c7aade..52e90e26e 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/quantifiers/quantifiers_rewriter.h"
 
+#include "expr/ascription_type.h"
 #include "expr/bound_var_manager.h"
 #include "expr/dtype.h"
 #include "expr/dtype_cons.h"
@@ -895,12 +896,25 @@ bool QuantifiersRewriter::getVarElimLit(Node body,
       const DType& dt = datatypes::utils::datatypeOf(tester);
       const DTypeConstructor& c = dt[index];
       std::vector<Node> newChildren;
-      newChildren.push_back(c.getConstructor());
+      Node cons = c.getConstructor();
+      TypeNode tspec;
+      // take into account if parametric
+      if (dt.isParametric())
+      {
+        tspec = c.getSpecializedConstructorType(lit[0].getType());
+        cons = nm->mkNode(
+            APPLY_TYPE_ASCRIPTION, nm->mkConst(AscriptionType(tspec)), cons);
+      }
+      else
+      {
+        tspec = cons.getType();
+      }
+      newChildren.push_back(cons);
       std::vector<Node> newVars;
       BoundVarManager* bvm = nm->getBoundVarManager();
-      for (unsigned j = 0, nargs = c.getNumArgs(); j < nargs; j++)
+      for (size_t j = 0, nargs = c.getNumArgs(); j < nargs; j++)
       {
-        TypeNode tn = c[j].getRangeType();
+        TypeNode tn = tspec[j];
         Node rn = nm->mkConst(Rational(j));
         Node cacheVal = BoundVarManager::getCacheValue(body, lit, rn);
         Node v = bvm->mkBoundVar<QRewDtExpandAttribute>(cacheVal, tn);
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 907dc22d1..79a493a1f 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -921,6 +921,7 @@ set(regress_0_tests
   regress0/quantifiers/issue6838-qpdt.smt2
   regress0/quantifiers/issue6996-trivial-elim.smt2
   regress0/quantifiers/issue6999-deq-elim.smt2
+  regress0/quantifiers/issue7353-var-elim-par-dt.smt2
   regress0/quantifiers/lra-triv-gn.smt2
   regress0/quantifiers/macro-back-subs-sat.smt2
   regress0/quantifiers/macros-int-real.smt2
diff --git a/test/regress/regress0/quantifiers/issue7353-var-elim-par-dt.smt2 b/test/regress/regress0/quantifiers/issue7353-var-elim-par-dt.smt2
new file mode 100644
index 000000000..8c9d9eb66
--- /dev/null
+++ b/test/regress/regress0/quantifiers/issue7353-var-elim-par-dt.smt2
@@ -0,0 +1,9 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-datatype Option (par (T) ((none) (some (extractSome T)))))
+(assert
+ (forall ((x (Option Int)))
+         (=> (and ((_ is some) x)
+                  (= (extractSome x) 0))
+             (= x (some 0)))))
+(check-sat)
-- 
2.30.2