diff options
-rw-r--r-- | src/parser/cvc/Cvc.g | 19 | ||||
-rw-r--r-- | src/parser/parser.cpp | 72 | ||||
-rw-r--r-- | src/parser/parser.h | 24 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 4 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 66 | ||||
-rw-r--r-- | src/parser/smt2/smt2.h | 2 |
6 files changed, 108 insertions, 79 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index dca61fe48..3fde52bbe 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1836,23 +1836,8 @@ postfixTerm[CVC4::Expr& f] { f = (args.size() == 1) ? MK_CONST(bool(true)) : MK_EXPR(CVC4::kind::DISTINCT, args); } ) ( typeAscription[f, t] - { if(f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && t.isDatatype()) { - std::vector<CVC4::Expr> v; - Expr e = f.getOperator(); - const DatatypeConstructor& dtc = Datatype::datatypeOf(e)[Datatype::indexOf(e)]; - v.push_back(MK_EXPR( CVC4::kind::APPLY_TYPE_ASCRIPTION, - MK_CONST(AscriptionType(dtc.getSpecializedConstructorType(t))), f.getOperator() )); - v.insert(v.end(), f.begin(), f.end()); - f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, v); - } else if(f.getKind() == CVC4::kind::EMPTYSET && t.isSet()) { - f = MK_CONST(CVC4::EmptySet(t)); - } else if(f.getKind() == CVC4::kind::UNIVERSE_SET && t.isSet()) { - f = EXPR_MANAGER->mkNullaryOperator(t, kind::UNIVERSE_SET); - } else { - if(f.getType() != t) { - PARSER_STATE->parseError("Type ascription not satisfied."); - } - } + { + f = PARSER_STATE->applyTypeAscription(f,t).getExpr(); } )? ; diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 663be7f1f..d2577433e 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -515,6 +515,78 @@ Expr Parser::mkHoApply(Expr expr, std::vector<Expr>& args) return expr; } +api::Term Parser::applyTypeAscription(api::Term t, api::Sort s) +{ + api::Kind k = t.getKind(); + if (k == api::EMPTYSET) + { + t = d_solver->mkEmptySet(s); + } + else if (k == api::UNIVERSE_SET) + { + t = d_solver->mkUniverseSet(s); + } + else if (k == api::SEP_NIL) + { + t = d_solver->mkSepNil(s); + } + else if (k == api::APPLY_CONSTRUCTOR) + { + std::vector<api::Term> children(t.begin(), t.end()); + // apply type ascription to the operator and reconstruct + children[0] = applyTypeAscription(children[0], s); + t = d_solver->mkTerm(api::APPLY_CONSTRUCTOR, children); + } + // !!! temporary until datatypes are refactored in the new API + api::Sort etype = t.getSort(); + if (etype.isConstructor()) + { + api::Sort etype = t.getSort(); + // 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 = getExprManager(); + // apply type ascription to the operator + Expr e = t.getExpr(); + const DatatypeConstructor& dtc = + Datatype::datatypeOf(e)[Datatype::indexOf(e)]; + t = api::Term(em->mkExpr( + kind::APPLY_TYPE_ASCRIPTION, + em->mkConst( + AscriptionType(dtc.getSpecializedConstructorType(s.getType()))), + e)); + } + // the type of t does not match the sort s by design (constructor type + // vs datatype type), thus we use an alternative check here. + if (t.getSort().getConstructorCodomainSort() != s) + { + std::stringstream ss; + ss << "Type ascription on constructor not satisfied, term " << t + << " expected sort " << s << " but has sort " + << t.getSort().getConstructorCodomainSort(); + parseError(ss.str()); + } + return t; + } + // otherwise, nothing to do + // check that the type is correct + if (t.getSort() != s) + { + std::stringstream ss; + ss << "Type ascription not satisfied, term " << t << " expected sort " << s + << " but has sort " << t.getSort(); + parseError(ss.str()); + } + return t; +} + bool Parser::isDeclared(const std::string& name, SymbolType type) { switch (type) { case SYM_VARIABLE: diff --git a/src/parser/parser.h b/src/parser/parser.h index 8447eb4dc..d40236208 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -678,6 +678,30 @@ public: */ Expr mkHoApply(Expr expr, std::vector<Expr>& args); + /** Apply type ascription + * + * Return term t with a type ascription applied to it. This is used for + * syntax like (as t T) in smt2 and t::T in the CVC language. This includes: + * - (as emptyset (Set T)) + * - (as univset (Set T)) + * - (as sep.nil T) + * - (cons T) + * - ((as cons T) t1 ... tn) where cons is a parametric datatype constructor. + * + * The term to ascribe t is a term whose kind and children (but not type) + * are equivalent to that of the term returned by this method. + * + * Notice that method is not necessarily a cast. In actuality, the above terms + * should be understood as symbols indexed by types. However, SMT-LIB does not + * permit types as indices, so we must use, e.g. (as emptyset (Set T)) + * instead of (_ emptyset (Set T)). + * + * @param t The term to ascribe a type + * @param s The sort to ascribe + * @return Term t with sort s ascribed. + */ + api::Term applyTypeAscription(api::Term t, api::Sort s); + /** * Add an operator to the current legal set. * diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 66831c0c4..eca32cb83 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1931,12 +1931,12 @@ qualIdentifier[CVC4::ParseOp& p] ( CONST_TOK sortSymbol[type, CHECK_DECLARED] { p.d_kind = kind::STORE_ALL; - PARSER_STATE->applyTypeAscription(p, type); + PARSER_STATE->parseOpApplyTypeAscription(p, type); } | identifier[p] sortSymbol[type, CHECK_DECLARED] { - PARSER_STATE->applyTypeAscription(p, type); + PARSER_STATE->parseOpApplyTypeAscription(p, type); } ) RPAREN_TOK diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 8c2b50b04..42111f581 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1578,8 +1578,10 @@ InputLanguage Smt2::getLanguage() const return em->getOptions().getInputLanguage(); } -void Smt2::applyTypeAscription(ParseOp& p, Type type) +void Smt2::parseOpApplyTypeAscription(ParseOp& p, Type type) { + Debug("parser") << "parseOpApplyTypeAscription : " << p << " " << type + << std::endl; // (as const (Array T1 T2)) if (p.d_kind == kind::STORE_ALL) { @@ -1612,66 +1614,12 @@ void Smt2::applyTypeAscription(ParseOp& p, Type type) parseError(ss.str()); } } - ExprManager* em = getExprManager(); - Type etype = p.d_expr.getType(); - Kind ekind = p.d_expr.getKind(); Trace("parser-qid") << "Resolve ascription " << type << " on " << p.d_expr; - Trace("parser-qid") << " " << ekind << " " << etype; + Trace("parser-qid") << " " << p.d_expr.getKind() << " " << p.d_expr.getType(); Trace("parser-qid") << std::endl; - if (ekind == kind::APPLY_CONSTRUCTOR && type.isDatatype()) - { - // nullary constructors with a type ascription - // could be a parametric constructor or just an overloaded constructor - DatatypeType dtype = static_cast<DatatypeType>(type); - if (dtype.isParametric()) - { - std::vector<Expr> v; - Expr e = p.d_expr.getOperator(); - const DatatypeConstructor& dtc = - Datatype::datatypeOf(e)[Datatype::indexOf(e)]; - v.push_back(em->mkExpr( - kind::APPLY_TYPE_ASCRIPTION, - em->mkConst(AscriptionType(dtc.getSpecializedConstructorType(type))), - p.d_expr.getOperator())); - v.insert(v.end(), p.d_expr.begin(), p.d_expr.end()); - p.d_expr = em->mkExpr(kind::APPLY_CONSTRUCTOR, v); - } - } - else if (etype.isConstructor()) - { - // a non-nullary constructor with a type ascription - DatatypeType dtype = static_cast<DatatypeType>(type); - if (dtype.isParametric()) - { - const DatatypeConstructor& dtc = - Datatype::datatypeOf(p.d_expr)[Datatype::indexOf(p.d_expr)]; - p.d_expr = em->mkExpr( - kind::APPLY_TYPE_ASCRIPTION, - em->mkConst(AscriptionType(dtc.getSpecializedConstructorType(type))), - p.d_expr); - } - } - else if (ekind == kind::EMPTYSET) - { - Debug("parser") << "Empty set encountered: " << p.d_expr << " " << type - << std::endl; - p.d_expr = em->mkConst(EmptySet(type)); - } - else if (ekind == kind::UNIVERSE_SET) - { - p.d_expr = em->mkNullaryOperator(type, kind::UNIVERSE_SET); - } - else if (ekind == kind::SEP_NIL) - { - // We don't want the nil reference to be a constant: for instance, it - // could be of type Int but is not a const rational. However, the - // expression has 0 children. So we convert to a SEP_NIL variable. - p.d_expr = em->mkNullaryOperator(type, kind::SEP_NIL); - } - else if (etype != type) - { - parseError("Type ascription not satisfied."); - } + // otherwise, we process the type ascription + p.d_expr = + applyTypeAscription(api::Term(p.d_expr), api::Sort(type)).getExpr(); } Expr Smt2::parseOpToExpr(ParseOp& p) diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 954bca314..35ac781f5 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -516,7 +516,7 @@ class Smt2 : public Parser * - If p's expression field is set, then we leave p unchanged, check if * that expression has the given type and throw a parse error otherwise. */ - void applyTypeAscription(ParseOp& p, Type type); + void parseOpApplyTypeAscription(ParseOp& p, Type type); /** * This converts a ParseOp to expression, assuming it is a standalone term. * |