diff options
Diffstat (limited to 'src/compat/cvc3_compat.cpp')
-rw-r--r-- | src/compat/cvc3_compat.cpp | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index fa5919e6a..a5d85821d 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -1079,11 +1079,11 @@ void ValidityChecker::dataType(const std::vector<std::string>& names, AlwaysAssert(constructors[i].size() == selectors[i].size()); AlwaysAssert(constructors[i].size() == types[i].size()); for(unsigned j = 0; j < constructors[i].size(); ++j) { - CVC4::Datatype::Constructor ctor(constructors[i][j]); + CVC4::DatatypeConstructor ctor(constructors[i][j]); AlwaysAssert(selectors[i][j].size() == types[i][j].size()); for(unsigned k = 0; k < selectors[i][j].size(); ++k) { if(types[i][j][k].getType().isString()) { - ctor.addArg(selectors[i][j][k], CVC4::Datatype::UnresolvedType(types[i][j][k].getConst<string>())); + ctor.addArg(selectors[i][j][k], CVC4::DatatypeUnresolvedType(types[i][j][k].getConst<string>())); } else { ctor.addArg(selectors[i][j][k], exprToType(types[i][j][k])); } @@ -1106,7 +1106,7 @@ void ValidityChecker::dataType(const std::vector<std::string>& names, // For each constructor, register its name and its selectors names. AlwaysAssert(d_constructors.find((*j).getName()) == d_constructors.end(), "cannot have two constructors with the same name in a ValidityChecker"); d_constructors[(*j).getName()] = &dt; - for(CVC4::Datatype::Constructor::const_iterator k = (*j).begin(); k != (*j).end(); ++k) { + for(CVC4::DatatypeConstructor::const_iterator k = (*j).begin(); k != (*j).end(); ++k) { AlwaysAssert(d_selectors.find((*k).getName()) == d_selectors.end(), "cannot have two selectors with the same name in a ValidityChecker"); d_selectors[(*k).getName()] = make_pair(&dt, (*j).getName()); } @@ -1769,7 +1769,7 @@ Expr ValidityChecker::datatypeConsExpr(const std::string& constructor, const std ConstructorMap::const_iterator i = d_constructors.find(constructor); AlwaysAssert(i != d_constructors.end(), "no such constructor"); const CVC4::Datatype& dt = *(*i).second; - const CVC4::Datatype::Constructor& ctor = dt[constructor]; + const CVC4::DatatypeConstructor& ctor = dt[constructor]; AlwaysAssert(ctor.getNumArgs() == args.size(), "arity mismatch in constructor application"); return d_em->mkExpr(CVC4::kind::APPLY_CONSTRUCTOR, ctor.getConstructor(), vector<CVC4::Expr>(args.begin(), args.end())); } @@ -1779,7 +1779,7 @@ Expr ValidityChecker::datatypeSelExpr(const std::string& selector, const Expr& a AlwaysAssert(i != d_selectors.end(), "no such selector"); const CVC4::Datatype& dt = *(*i).second.first; string constructor = (*i).second.second; - const CVC4::Datatype::Constructor& ctor = dt[constructor]; + const CVC4::DatatypeConstructor& ctor = dt[constructor]; return d_em->mkExpr(CVC4::kind::APPLY_SELECTOR, ctor.getSelector(selector), arg); } @@ -1787,7 +1787,7 @@ Expr ValidityChecker::datatypeTestExpr(const std::string& constructor, const Exp ConstructorMap::const_iterator i = d_constructors.find(constructor); AlwaysAssert(i != d_constructors.end(), "no such constructor"); const CVC4::Datatype& dt = *(*i).second; - const CVC4::Datatype::Constructor& ctor = dt[constructor]; + const CVC4::DatatypeConstructor& ctor = dt[constructor]; return d_em->mkExpr(CVC4::kind::APPLY_TESTER, ctor.getTester(), arg); } |