diff options
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/cvc/Cvc.g | 8 | ||||
-rw-r--r-- | src/parser/parser.cpp | 4 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 6 |
3 files changed, 9 insertions, 9 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 22cf368eb..2d659cfe3 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1486,7 +1486,7 @@ postfixTerm[CVC4::Expr& f] { if(f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && t.isDatatype()) { std::vector<CVC4::Expr> v; Expr e = f.getOperator(); - const Datatype::Constructor& dtc = Datatype::datatypeOf(e)[Datatype::indexOf(e)]; + 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()); @@ -1783,14 +1783,14 @@ datatypeDef[std::vector<CVC4::Datatype>& datatypes] constructorDef[CVC4::Datatype& type] @init { std::string id; - CVC4::Datatype::Constructor* ctor = NULL; + CVC4::DatatypeConstructor* ctor = NULL; } : identifier[id,CHECK_UNDECLARED,SYM_SORT] { // make the tester std::string testerId("is_"); testerId.append(id); PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_SORT); - ctor = new CVC4::Datatype::Constructor(id, testerId); + ctor = new CVC4::DatatypeConstructor(id, testerId); } ( LPAREN selector[*ctor] @@ -1804,7 +1804,7 @@ constructorDef[CVC4::Datatype& type] } ; -selector[CVC4::Datatype::Constructor& ctor] +selector[CVC4::DatatypeConstructor& ctor] @init { std::string id; Type t, t2; diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index f1ad4b330..4418ea18f 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -286,7 +286,7 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) { j_end = dt.end(); j != j_end; ++j) { - const Datatype::Constructor& ctor = *j; + const DatatypeConstructor& ctor = *j; Expr::printtypes::Scope pts(Debug("parser-idt"), true); Expr constructor = ctor.getConstructor(); Debug("parser-idt") << "+ define " << constructor << std::endl; @@ -302,7 +302,7 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) { throw ParserException(testerName + " already declared"); } defineVar(testerName, tester); - for(Datatype::Constructor::const_iterator k = ctor.begin(), + for(DatatypeConstructor::const_iterator k = ctor.begin(), k_end = ctor.end(); k != k_end; ++k) { diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 974de29b2..a093aa1ef 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -824,14 +824,14 @@ datatypeDef[std::vector<CVC4::Datatype>& datatypes] constructorDef[CVC4::Datatype& type] @init { std::string id; - CVC4::Datatype::Constructor* ctor = NULL; + CVC4::DatatypeConstructor* ctor = NULL; } : symbol[id,CHECK_UNDECLARED,SYM_SORT] { // make the tester std::string testerId("is_"); testerId.append(id); PARSER_STATE->checkDeclaration(testerId, CHECK_UNDECLARED, SYM_SORT); - ctor = new CVC4::Datatype::Constructor(id, testerId); + ctor = new CVC4::DatatypeConstructor(id, testerId); } ( LPAREN_TOK selector[*ctor] RPAREN_TOK )* { // make the constructor @@ -841,7 +841,7 @@ constructorDef[CVC4::Datatype& type] } ; -selector[CVC4::Datatype::Constructor& ctor] +selector[CVC4::DatatypeConstructor& ctor] @init { std::string id; Type t, t2; |