Fix parsing of overloaded parametric datatype selectors (#2819)

diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp
index 32126cf4eeee7a63d657df0a94a81381804cf931..9401e772cbe44e71b336ca36ceea2865a682cdc6 100644 (file)
--- a/src/expr/symbol_table.cpp
+++ b/src/expr/symbol_table.cpp
@@ -203,8 +203,31 @@ Expr OverloadedTypeTrie::getOverloadedFunctionForTypes(
       if (itc != tat->d_children.end()) {
         tat = &itc->second;
       } else {
-        // no functions match
-        return d_nullExpr;
+        Trace("parser-overloading")
+            << "Could not find overloaded function " << name << std::endl;
+        // it may be a parametric datatype
+        TypeNode tna = TypeNode::fromType(argTypes[i]);
+        if (tna.isParametricDatatype())
+        {
+          Trace("parser-overloading")
+              << "Parametric overloaded datatype selector " << name << " "
+              << tna << std::endl;
+          DatatypeType tnd = static_cast<DatatypeType>(argTypes[i]);
+          const Datatype& dt = tnd.getDatatype();
+          // tng is the "generalized" version of the instantiated parametric
+          // type tna
+          Type tng = dt.getDatatypeType();
+          itc = tat->d_children.find(tng);
+          if (itc != tat->d_children.end())
+          {
+            tat = &itc->second;
+          }
+        }
+        if (tat == nullptr)
+        {
+          // no functions match
+          return d_nullExpr;
+        }
       }
     }
     // we ensure that there is *only* one active symbol at this node

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index c8b052265f48561b22a2b35ce0c31655294e8f21..77f68aa456f0574b4ef5f4951294e405c2dffedd 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -371,6 +371,7 @@ set(regress_0_tests
   regress0/datatypes/rec1.cvc
   regress0/datatypes/rec2.cvc
   regress0/datatypes/rec4.cvc
+  regress0/datatypes/repeated-selectors-2769.smt2
   regress0/datatypes/rewriter.cvc
   regress0/datatypes/sc-cdt1.smt2
   regress0/datatypes/some-boolean-tests.cvc

diff --git a/test/regress/regress0/datatypes/repeated-selectors-2769.smt2 b/test/regress/regress0/datatypes/repeated-selectors-2769.smt2
new file mode 100644 (file)
index 0000000..827b17e
--- /dev/null
+++ b/test/regress/regress0/datatypes/repeated-selectors-2769.smt2
@@ -0,0 +1,10 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-datatypes ((t1 1)) ((par (T1) ((mkt1 (p1 T1))))))
+(declare-datatypes ((t2 1)) ((par (T1) ((mkt2 (p1 T1))))))
+(define-fun s1 () (t1 Int) (mkt1 3))
+(define-fun s2 () (t2 Int) (mkt2 3))
+(define-fun s3 () Int (p1 s1))
+(define-fun s4 () Int (p1 s2))
+(assert (= s3 s4))
+(check-sat)