Add API interface for specialized constructor term (#4817)

This is an interface to get the instantiated parametric datatype constructor operator to apply when the type of this operator cannot be inferred without a cast.

This is required for eliminating the Expr-level datatype and calls to ExprManager from the parsers.

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 61d180fe4b9439da3eb81b97e9d7e45b92914894..a1effec91cb64022cc6b0757e357b27a9f6f1071 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -2142,6 +2142,27 @@ Term DatatypeConstructor::getConstructorTerm() const
   return ctor;
 }
 
+Term DatatypeConstructor::getSpecializedConstructorTerm(Sort retSort) const
+{
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  
+  NodeManager* nm = d_solver->getNodeManager();
+  Node ret = nm->mkNode(kind::APPLY_TYPE_ASCRIPTION,
+                           nm->mkConst(AscriptionType(
+                               d_ctor
+                                   ->getSpecializedConstructorType(
+                                       retSort.getType()))),
+                           d_ctor->getConstructor());
+  (void)ret.getType(true); /* kick off type checking */
+  // apply type ascription to the operator
+  Term sctor =
+      api::Term(d_solver,
+                ret);
+  return sctor;
+  
+  CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
 Term DatatypeConstructor::getTesterTerm() const
 {
   Term tst = Term(d_solver, d_ctor->getTester());

diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index bba6542006c9185226300dfd73842e8bea8abc6b..30a0ad0a7214a51ea722687eed24ca6079d33d6b 100644 (file)
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -1490,6 +1490,31 @@ class CVC4_PUBLIC DatatypeConstructor
    */
   Term getConstructorTerm() const;
 
+  /**
+   * Get the constructor operator of this datatype constructor whose return
+   * type is retSort. This method is intended to be used on constructors of
+   * parametric datatypes and can be seen as returning the constructor
+   * term that has been explicitly cast to the given sort.
+   *
+   * This method is required for constructors of parametric datatypes whose
+   * return type cannot be determined by type inference. For example, given:
+   *   (declare-datatype List (par (T) ((nil) (cons (head T) (tail (List T))))))
+   * The type of nil terms need to be provided by the user. In SMT version 2.6,
+   * this is done via the syntax for qualified identifiers:
+   *   (as nil (List Int))
+   * This method is equivalent of applying the above, where this
+   * DatatypeConstructor is the one corresponding to nil, and retSort is
+   * (List Int).
+   *
+   * Furthermore note that the returned constructor term t is an operator,
+   * while Solver::mkTerm(APPLY_CONSTRUCTOR, t) is used to construct the above
+   * (nullary) application of nil.
+   *
+   * @param retSort the desired return sort of the constructor
+   * @return the constructor term
+   */
+  Term getSpecializedConstructorTerm(Sort retSort) const;
+
   /**
    * Get the tester operator of this datatype constructor.
    * @return the tester operator

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index bf12ee87df285f5e7272059497beb1b501e8b81d..71a9d47ebacd06dcff6a14199ce7a1a1918d0727 100644 (file)
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -596,27 +596,17 @@ api::Term Parser::applyTypeAscription(api::Term t, api::Sort s)
   api::Sort etype = t.getSort();
   if (etype.isConstructor())
   {
-    // get the datatype that t belongs to
-    api::Sort etyped = etype.getConstructorCodomainSort();
-    api::Datatype d = etyped.getDatatype();
-    // lookup by name
-    api::DatatypeConstructor dc = d.getConstructor(t.toString());
-
     // Type ascriptions only have an effect on the node structure if this is a
     // parametric datatype.
     if (s.isParametricDatatype())
     {
-      ExprManager* em = d_solver->getExprManager();
-      // apply type ascription to the operator
-      Expr e = t.getExpr();
-      const DatatypeConstructor& dtc =
-          Datatype::datatypeOf(e)[Datatype::indexOf(e)];
-      t = api::Term(
-          d_solver,
-          em->mkExpr(kind::APPLY_TYPE_ASCRIPTION,
-                     em->mkConst(AscriptionType(
-                         dtc.getSpecializedConstructorType(s.getType()))),
-                     e));
+      // get the datatype that t belongs to
+      api::Sort etyped = etype.getConstructorCodomainSort();
+      api::Datatype d = etyped.getDatatype();
+      // lookup by name
+      api::DatatypeConstructor dc = d.getConstructor(t.toString());
+      // ask the constructor for the specialized constructor term
+      t = dc.getSpecializedConstructorTerm(s);
     }
     // the type of t does not match the sort s by design (constructor type
     // vs datatype type), thus we use an alternative check here.

diff --git a/test/unit/api/datatype_api_black.h b/test/unit/api/datatype_api_black.h
index bc2516474ed4056573634d4753549a0ceb5d6694..a9d0638a6baa8f0ae10bb67eadbf165e4e76033d 100644 (file)
--- a/test/unit/api/datatype_api_black.h
+++ b/test/unit/api/datatype_api_black.h
@@ -36,6 +36,8 @@ class DatatypeBlack : public CxxTest::TestSuite
 
   void testDatatypeSimplyRec();
 
+  void testDatatypeSpecializedCons();
+
  private:
   Solver d_solver;
 };
@@ -519,3 +521,56 @@ void DatatypeBlack::testDatatypeSimplyRec()
   TS_ASSERT(dtsorts[0].getDatatype().isWellFounded());
   TS_ASSERT(dtsorts[0].getDatatype().hasNestedRecursion());
 }
+
+void DatatypeBlack::testDatatypeSpecializedCons()
+{
+  /* Create mutual datatypes corresponding to this definition block:
+   *   DATATYPE
+   *     plist[X] = pcons(car: X, cdr: plist[X]) | pnil
+   *   END;
+   */
+  // Make unresolved types as placeholders
+  std::set<Sort> unresTypes;
+  Sort unresList = d_solver.mkSortConstructorSort("plist", 1);
+  unresTypes.insert(unresList);
+
+  std::vector<Sort> v;
+  Sort x = d_solver.mkParamSort("X");
+  v.push_back(x);
+  DatatypeDecl plist = d_solver.mkDatatypeDecl("plist", v);
+
+  std::vector<Sort> args;
+  args.push_back(x);
+  Sort urListX = unresList.instantiate(args);
+
+  DatatypeConstructorDecl pcons = d_solver.mkDatatypeConstructorDecl("pcons");
+  pcons.addSelector("car", x);
+  pcons.addSelector("cdr", urListX);
+  plist.addConstructor(pcons);
+  DatatypeConstructorDecl nil5 = d_solver.mkDatatypeConstructorDecl("pnil");
+  plist.addConstructor(nil5);
+
+  std::vector<DatatypeDecl> dtdecls;
+  dtdecls.push_back(plist);
+
+  std::vector<Sort> dtsorts;
+  // make the datatype sorts
+  TS_ASSERT_THROWS_NOTHING(dtsorts =
+                               d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+  TS_ASSERT(dtsorts.size() == 1);
+  Datatype d = dtsorts[0].getDatatype();
+  DatatypeConstructor nilc = d[0];
+
+  Sort isort = d_solver.getIntegerSort();
+  std::vector<Sort> iargs;
+  iargs.push_back(isort);
+  Sort listInt = dtsorts[0].instantiate(iargs);
+
+  Term testConsTerm;
+  // get the specialized constructor term for list[Int]
+  TS_ASSERT_THROWS_NOTHING(testConsTerm =
+                               nilc.getSpecializedConstructorTerm(listInt));
+  TS_ASSERT(testConsTerm != nilc.getConstructorTerm());
+  // error to get the specialized constructor term for Int
+  TS_ASSERT_THROWS(nilc.getSpecializedConstructorTerm(isort), CVC4ApiException&);
+}