summaryrefslogtreecommitdiff
path: root/src/parser
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser')
-rw-r--r--src/parser/cvc/Cvc.g19
-rw-r--r--src/parser/parser.cpp72
-rw-r--r--src/parser/parser.h24
-rw-r--r--src/parser/smt2/Smt2.g4
-rw-r--r--src/parser/smt2/smt2.cpp66
-rw-r--r--src/parser/smt2/smt2.h2
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.
*
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback