From: Andrew Reynolds Date: Tue, 4 Aug 2020 19:01:47 +0000 (-0500) Subject: Add API interface for specialized constructor term (#4817) X-Git-Tag: cvc5-1.0.0~3044 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0cbcf1f835f74c304e2ac3884143b7df9c7f75b6;p=cvc5.git 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 61d180fe4..a1effec91 100644 --- 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 bba654200..30a0ad0a7 100644 --- 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 bf12ee87d..71a9d47eb 100644 --- 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 bc2516474..a9d0638a6 100644 --- 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 unresTypes; + Sort unresList = d_solver.mkSortConstructorSort("plist", 1); + unresTypes.insert(unresList); + + std::vector v; + Sort x = d_solver.mkParamSort("X"); + v.push_back(x); + DatatypeDecl plist = d_solver.mkDatatypeDecl("plist", v); + + std::vector 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 dtdecls; + dtdecls.push_back(plist); + + std::vector 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 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&); +}