diff options
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
-rw-r--r-- | src/parser/smt2/smt2.cpp | 66 |
1 files changed, 7 insertions, 59 deletions
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) |