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]));
}
// 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());
}
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()));
}
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);
}
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);
}
for(Datatype::const_iterator i = dt.begin(), i_end = dt.end();
i != i_end;
++i) {
- const Datatype::Constructor& c = *i;
+ const DatatypeConstructor& c = *i;
Type testerType CVC4_UNUSED = c.getTester().getType();
Assert(c.isResolved() &&
testerType.isTester() &&
ConstructorType(ctorType).getRangeType() == dtt,
"malformed constructor in datatype post-resolution");
// for all selectors...
- for(Datatype::Constructor::const_iterator j = c.begin(), j_end = c.end();
+ for(DatatypeConstructor::const_iterator j = c.begin(), j_end = c.end();
j != j_end;
++j) {
- const Datatype::Constructor::Arg& a = *j;
+ const DatatypeConstructorArg& a = *j;
Type selectorType = a.getSelector().getType();
Assert(a.isResolved() &&
selectorType.isSelector() &&
}
}
-ConstructorType ExprManager::mkConstructorType(const Datatype::Constructor& constructor, Type range) const {
+ConstructorType ExprManager::mkConstructorType(const DatatypeConstructor& constructor, Type range) const {
NodeManagerScope nms(d_nodeManager);
return Type(d_nodeManager, new TypeNode(d_nodeManager->mkConstructorType(constructor, *range.d_typeNode)));
}
/**
* Make a type representing a constructor with the given parameterization.
*/
- ConstructorType mkConstructorType(const Datatype::Constructor& constructor, Type range) const;
+ ConstructorType mkConstructorType(const DatatypeConstructor& constructor, Type range) const;
/** Make a type representing a selector with the given parameterization. */
SelectorType mkSelectorType(Type domain, Type range) const;
return typeNode;
}
-TypeNode NodeManager::mkConstructorType(const Datatype::Constructor& constructor,
+TypeNode NodeManager::mkConstructorType(const DatatypeConstructor& constructor,
TypeNode range) {
std::vector<TypeNode> sorts;
Debug("datatypes") << "ctor name: " << constructor.getName() << std::endl;
- for(Datatype::Constructor::const_iterator i = constructor.begin();
+ for(DatatypeConstructor::const_iterator i = constructor.begin();
i != constructor.end();
++i) {
TypeNode selectorType = *(*i).getSelector().getType().d_typeNode;
inline TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType);
/** Make a type representing a constructor with the given parameterization */
- TypeNode mkConstructorType(const Datatype::Constructor& constructor, TypeNode range);
+ TypeNode mkConstructorType(const DatatypeConstructor& constructor, TypeNode range);
/** Make a type representing a selector with the given parameterization */
inline TypeNode mkSelectorType(TypeNode domain, TypeNode range);
{ 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());
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]
}
;
-selector[CVC4::Datatype::Constructor& ctor]
+selector[CVC4::DatatypeConstructor& ctor]
@init {
std::string id;
Type t, t2;
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;
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) {
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
}
;
-selector[CVC4::Datatype::Constructor& ctor]
+selector[CVC4::DatatypeConstructor& ctor]
@init {
std::string id;
Type t, t2;
size_t selectorIndex = Datatype::indexOf(selectorExpr);
size_t constructorIndex = Datatype::indexOf(constructorExpr);
const Datatype& dt = Datatype::datatypeOf(constructorExpr);
- const Datatype::Constructor& c = dt[constructorIndex];
+ const DatatypeConstructor& c = dt[constructorIndex];
if(c.getNumArgs() > selectorIndex &&
c[selectorIndex].getSelector() == selectorExpr) {
Debug("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
using namespace CVC4::theory;
using namespace CVC4::theory::datatypes;
-const Datatype::Constructor& TheoryDatatypes::getConstructor( Node cons )
+const DatatypeConstructor& TheoryDatatypes::getConstructor( Node cons )
{
Expr consExpr = cons.toExpr();
return Datatype::datatypeOf(consExpr)[ Datatype::indexOf(consExpr) ];
}
}
if( !cons.isNull() ) {
- const Datatype::Constructor& cn = getConstructor( cons );
+ const DatatypeConstructor& cn = getConstructor( cons );
Debug("datatypes-split") << "*************Split for possible constructor " << cons << endl;
Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( cn.getTester() ), (*i).first );
NodeBuilder<> nb(kind::OR);
vector< Node > selectorVals;
selectorVals.push_back( cons );
bool foundSel = false;
- const Datatype::Constructor& cn = getConstructor( cons );
+ const DatatypeConstructor& cn = getConstructor( cons );
for( unsigned int i=0; i<cn.getNumArgs(); i++ ) {
Node s = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( cn[i].getSelector() ), te );
if( d_selectors.find( s ) != d_selectors.end() ) {
if( val.getType()!=te.getType() ){ //IDT-param
Assert( Datatype::datatypeOf( cons.toExpr() ).isParametric() );
Debug("datatypes-gt") << "Inst: ambiguous type for " << cons << ", ascribe to " << te.getType() << std::endl;
- const Datatype::Constructor& dtc = Datatype::datatypeOf(cons.toExpr())[Datatype::indexOf(cons.toExpr())];
+ const DatatypeConstructor& dtc = Datatype::datatypeOf(cons.toExpr())[Datatype::indexOf(cons.toExpr())];
Debug("datatypes-gt") << "constructor is " << dtc << std::endl;
Type tspec = dtc.getSpecializedConstructorType(te.getType().toType());
Debug("datatypes-gt") << "tpec is " << tspec << std::endl;
Node sel = t.getOperator();
TypeNode selType = sel.getType();
Node cons = getConstructorForSelector( sel );
- const Datatype::Constructor& cn = getConstructor( cons );
+ const DatatypeConstructor& cn = getConstructor( cons );
Node tmp = find( t[0] );
Node retNode = t;
if( tmp.getKind() == APPLY_CONSTRUCTOR ) {
/** has seen cycle */
context::CDO< bool > d_hasSeenCycle;
/** get the constructor for the node */
- const Datatype::Constructor& getConstructor( Node cons );
+ const DatatypeConstructor& getConstructor( Node cons );
/** get the constructor for the selector */
Node getConstructorForSelector( Node sel );
"Datatype::resolve(): resolutions doesn't contain me!");
AssertArgument(placeholders.size() == replacements.size(), placeholders,
"placeholders and replacements must be the same size");
+ AssertArgument(paramTypes.size() == paramReplacements.size(), paramTypes,
+ "paramTypes and paramReplacements must be the same size");
CheckArgument(getNumConstructors() > 0, *this, "cannot resolve a Datatype that has no constructors");
DatatypeType self = (*resolutions.find(d_name)).second;
AssertArgument(&self.getDatatype() == this, "Datatype::resolve(): resolutions doesn't contain me!");
Assert(index == getNumConstructors());
}
-void Datatype::addConstructor(const Constructor& c) {
+void Datatype::addConstructor(const DatatypeConstructor& c) {
CheckArgument(!d_resolved, this,
"cannot add a constructor to a finalized Datatype");
d_constructors.push_back(c);
i != i_end;
++i) {
if( groundTerm.isNull() ){
- Constructor::const_iterator j = (*i).begin(), j_end = (*i).end();
+ DatatypeConstructor::const_iterator j = (*i).begin(), j_end = (*i).end();
for(; j != j_end; ++j) {
SelectorType stype((*j).getSelector().getType());
if(stype.getDomain() == stype.getRangeType()) {
if(j == j_end && (*i).isWellFounded()) {
groundTerm = (*i).mkGroundTerm( t );
- // Constructor::mkGroundTerm() doesn't ever return null when
+ // DatatypeConstructor::mkGroundTerm() doesn't ever return null when
// called from the outside. But in recursive invocations, it
// can: say you have dt = a(one:dt) | b(two:INT), and you ask
// the "a" constructor for a ground term. It asks "dt" for a
// ground term! Thus, even though "a" is a well-founded
// constructor, it cannot construct a ground-term by itself. We
// have to skip past it, and we do that with a
- // RecursionBreaker<> in Constructor::mkGroundTerm(). In the
+ // RecursionBreaker<> in DatatypeConstructor::mkGroundTerm(). In the
// case of recursion, it returns null.
if(!groundTerm.isNull()) {
// we found a ground-term-constructing constructor!
if(!(*i).d_tester.isNull() && (*i).d_tester != (*j).d_tester) {
return false;
}
- for(Constructor::const_iterator k = (*i).begin(), l = (*j).begin(); k != (*i).end(); ++k, ++l) {
+ for(DatatypeConstructor::const_iterator k = (*i).begin(), l = (*j).begin(); k != (*i).end(); ++k, ++l) {
Assert(l != (*j).end());
if((*k).getName() != (*l).getName()) {
return false;
return true;
}
-const Datatype::Constructor& Datatype::operator[](size_t index) const {
+const DatatypeConstructor& Datatype::operator[](size_t index) const {
CheckArgument(index < getNumConstructors(), index, "index out of bounds");
return d_constructors[index];
}
-const Datatype::Constructor& Datatype::operator[](std::string name) const {
+const DatatypeConstructor& Datatype::operator[](std::string name) const {
for(const_iterator i = begin(); i != end(); ++i) {
if((*i).getName() == name) {
return *i;
return (*this)[name].getConstructor();
}
-void Datatype::Constructor::resolve(ExprManager* em, DatatypeType self,
- const std::map<std::string, DatatypeType>& resolutions,
- const std::vector<Type>& placeholders,
- const std::vector<Type>& replacements,
- const std::vector< SortConstructorType >& paramTypes,
- const std::vector< DatatypeType >& paramReplacements)
+void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self,
+ const std::map<std::string, DatatypeType>& resolutions,
+ const std::vector<Type>& placeholders,
+ const std::vector<Type>& replacements,
+ const std::vector< SortConstructorType >& paramTypes,
+ const std::vector< DatatypeType >& paramReplacements)
throw(AssertionException, DatatypeResolutionException) {
AssertArgument(em != NULL, "cannot resolve a Datatype with a NULL expression manager");
Assert(index == getNumArgs());
- // Set constructor/tester last, since Constructor::isResolved()
+ // Set constructor/tester last, since DatatypeConstructor::isResolved()
// returns true when d_tester is not the null Expr. If something
// fails above, we want Constuctor::isResolved() to remain "false".
// Further, mkConstructorType() iterates over the selectors, so
}
}
-Type Datatype::Constructor::doParametricSubstitution( Type range,
+Type DatatypeConstructor::doParametricSubstitution( Type range,
const std::vector< SortConstructorType >& paramTypes,
const std::vector< DatatypeType >& paramReplacements ) {
TypeNode typn = TypeNode::fromType( range );
origChildren.push_back( (*i).toType() );
children.push_back( doParametricSubstitution( (*i).toType(), paramTypes, paramReplacements ) );
}
- for( int i=0; i<(int)paramTypes.size(); i++ ) {
- if( paramTypes[i].getArity()==origChildren.size() ) {
+ for( unsigned i = 0; i < paramTypes.size(); ++i ) {
+ if( paramTypes[i].getArity() == origChildren.size() ) {
Type tn = paramTypes[i].instantiate( origChildren );
- if( range==tn ) {
+ if( range == tn ) {
return paramReplacements[i].instantiate( children );
}
}
}
NodeBuilder<> nb(typn.getKind());
- for( int i=0; i<(int)children.size(); i++ ) {
+ for( unsigned i = 0; i < children.size(); ++i ) {
nb << TypeNode::fromType( children[i] );
}
return nb.constructTypeNode().toType();
}
}
-Datatype::Constructor::Constructor(std::string name) :
+DatatypeConstructor::DatatypeConstructor(std::string name) :
// We don't want to introduce a new data member, because eventually
// we're going to be a constant stuffed inside a node. So we stow
// the tester name away inside the constructor name until
CheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
}
-Datatype::Constructor::Constructor(std::string name, std::string tester) :
+DatatypeConstructor::DatatypeConstructor(std::string name, std::string tester) :
// We don't want to introduce a new data member, because eventually
// we're going to be a constant stuffed inside a node. So we stow
// the tester name away inside the constructor name until
CheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester");
}
-void Datatype::Constructor::addArg(std::string selectorName, Type selectorType) {
+void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) {
// We don't want to introduce a new data member, because eventually
// we're going to be a constant stuffed inside a node. So we stow
// the selector type away inside a var until resolution (when we can
CheckArgument(!selectorType.isNull(), selectorType, "cannot add a null selector type");
Expr type = selectorType.getExprManager()->mkVar(selectorType);
Debug("datatypes") << type << endl;
- d_args.push_back(Arg(selectorName, type));
+ d_args.push_back(DatatypeConstructorArg(selectorName, type));
}
-void Datatype::Constructor::addArg(std::string selectorName, Datatype::UnresolvedType selectorType) {
+void DatatypeConstructor::addArg(std::string selectorName, DatatypeUnresolvedType selectorType) {
// We don't want to introduce a new data member, because eventually
// we're going to be a constant stuffed inside a node. So we stow
// the selector type away after a NUL in the name string until
// resolution (when we can create the proper selector type)
CheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor");
CheckArgument(selectorType.getName() != "", selectorType, "cannot add a null selector type");
- d_args.push_back(Arg(selectorName + '\0' + selectorType.getName(), Expr()));
+ d_args.push_back(DatatypeConstructorArg(selectorName + '\0' + selectorType.getName(), Expr()));
}
-void Datatype::Constructor::addArg(std::string selectorName, Datatype::SelfType) {
+void DatatypeConstructor::addArg(std::string selectorName, DatatypeSelfType) {
// We don't want to introduce a new data member, because eventually
// we're going to be a constant stuffed inside a node. So we mark
// the name string with a NUL to indicate that we have a
// self-selecting selector until resolution (when we can create the
// proper selector type)
CheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor");
- d_args.push_back(Arg(selectorName + '\0', Expr()));
+ d_args.push_back(DatatypeConstructorArg(selectorName + '\0', Expr()));
}
-std::string Datatype::Constructor::getName() const throw() {
+std::string DatatypeConstructor::getName() const throw() {
string name = d_name;
if(!isResolved()) {
name.resize(name.find('\0'));
return name;
}
-Expr Datatype::Constructor::getConstructor() const {
+Expr DatatypeConstructor::getConstructor() const {
CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
return d_constructor;
}
-Type Datatype::Constructor::getSpecializedConstructorType(Type returnType) const {
+Type DatatypeConstructor::getSpecializedConstructorType(Type returnType) const {
CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
const Datatype& dt = Datatype::datatypeOf(d_constructor);
CheckArgument(dt.isParametric(), this, "this datatype constructor is not yet resolved");
- DatatypeType dtt = DatatypeType(dt.d_self);
+ DatatypeType dtt = dt.getDatatypeType();
Matcher m(dtt);
m.doMatching( TypeNode::fromType(dtt), TypeNode::fromType(returnType) );
vector<Type> subst;
return d_constructor.getType().substitute(params, subst);
}
-Expr Datatype::Constructor::getTester() const {
+Expr DatatypeConstructor::getTester() const {
CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
return d_tester;
}
-Cardinality Datatype::Constructor::getCardinality() const throw(AssertionException) {
+Cardinality DatatypeConstructor::getCardinality() const throw(AssertionException) {
CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
Cardinality c = 1;
return c;
}
-bool Datatype::Constructor::isFinite() const throw(AssertionException) {
+bool DatatypeConstructor::isFinite() const throw(AssertionException) {
CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
// we're using some internals, so we have to set up this library context
return true;
}
-bool Datatype::Constructor::isWellFounded() const throw(AssertionException) {
+bool DatatypeConstructor::isWellFounded() const throw(AssertionException) {
CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
// we're using some internals, so we have to set up this library context
return self.getAttribute(DatatypeWellFoundedAttr());
}
- RecursionBreaker<const Datatype::Constructor*, DatatypeHashFunction> breaker(__PRETTY_FUNCTION__, this);
+ RecursionBreaker<const DatatypeConstructor*, DatatypeHashFunction> breaker(__PRETTY_FUNCTION__, this);
if(breaker.isRecursion()) {
// This *path* is cyclic, sso may not be well-founded. The
// constructor itself might still be well-founded, though (we'll
return true;
}
-Expr Datatype::Constructor::mkGroundTerm( Type t ) const throw(AssertionException) {
+Expr DatatypeConstructor::mkGroundTerm( Type t ) const throw(AssertionException) {
CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
// we're using some internals, so we have to set up this library context
return groundTerm;
}
- RecursionBreaker<const Datatype::Constructor*, DatatypeHashFunction> breaker(__PRETTY_FUNCTION__, this);
+ RecursionBreaker<const DatatypeConstructor*, DatatypeHashFunction> breaker(__PRETTY_FUNCTION__, this);
if(breaker.isRecursion()) {
// Recursive path, we should skip and go to the next constructor;
// see lengthy comments in Datatype::mkGroundTerm().
return groundTerm;
}
-const Datatype::Constructor::Arg& Datatype::Constructor::operator[](size_t index) const {
+const DatatypeConstructorArg& DatatypeConstructor::operator[](size_t index) const {
CheckArgument(index < getNumArgs(), index, "index out of bounds");
return d_args[index];
}
-const Datatype::Constructor::Arg& Datatype::Constructor::operator[](std::string name) const {
+const DatatypeConstructorArg& DatatypeConstructor::operator[](std::string name) const {
for(const_iterator i = begin(); i != end(); ++i) {
if((*i).getName() == name) {
return *i;
CheckArgument(false, name, "No such arg `%s' of constructor `%s'", name.c_str(), d_name.c_str());
}
-Expr Datatype::Constructor::getSelector(std::string name) const {
+Expr DatatypeConstructor::getSelector(std::string name) const {
return (*this)[name].getSelector();
}
-Datatype::Constructor::Arg::Arg(std::string name, Expr selector) :
+DatatypeConstructorArg::DatatypeConstructorArg(std::string name, Expr selector) :
d_name(name),
d_selector(selector),
d_resolved(false) {
CheckArgument(name != "", name, "cannot construct a datatype constructor arg without a name");
}
-std::string Datatype::Constructor::Arg::getName() const throw() {
+std::string DatatypeConstructorArg::getName() const throw() {
string name = d_name;
const size_t nul = name.find('\0');
if(nul != string::npos) {
return name;
}
-Expr Datatype::Constructor::Arg::getSelector() const {
+Expr DatatypeConstructorArg::getSelector() const {
CheckArgument(isResolved(), this, "cannot get a selector for an unresolved datatype constructor");
return d_selector;
}
-Expr Datatype::Constructor::Arg::getConstructor() const {
+Expr DatatypeConstructorArg::getConstructor() const {
CheckArgument(isResolved(), this,
"cannot get a associated constructor for argument of an unresolved datatype constructor");
return d_constructor;
}
-Type Datatype::Constructor::Arg::getSelectorType() const {
+Type DatatypeConstructorArg::getType() const {
return getSelector().getType();
}
-bool Datatype::Constructor::Arg::isUnresolvedSelf() const throw() {
+bool DatatypeConstructorArg::isUnresolvedSelf() const throw() {
return d_selector.isNull() && d_name.size() == d_name.find('\0') + 1;
}
static const int s_printDatatypeNamesOnly = std::ios_base::xalloc();
-std::string Datatype::Constructor::Arg::getSelectorTypeName() const {
+std::string DatatypeConstructorArg::getTypeName() const {
Type t;
if(isResolved()) {
t = SelectorType(d_selector.getType()).getRangeType();
return os;
}
-std::ostream& operator<<(std::ostream& os, const Datatype::Constructor& ctor) {
+std::ostream& operator<<(std::ostream& os, const DatatypeConstructor& ctor) {
// can only output datatypes in the CVC4 native language
Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4);
os << ctor.getName();
- Datatype::Constructor::const_iterator i = ctor.begin(), i_end = ctor.end();
+ DatatypeConstructor::const_iterator i = ctor.begin(), i_end = ctor.end();
if(i != i_end) {
os << "(";
do {
return os;
}
-std::ostream& operator<<(std::ostream& os, const Datatype::Constructor::Arg& arg) {
+std::ostream& operator<<(std::ostream& os, const DatatypeConstructorArg& arg) {
// can only output datatypes in the CVC4 native language
Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4);
- os << arg.getName() << ": " << arg.getSelectorTypeName();
+ os << arg.getName() << ": " << arg.getTypeName();
return os;
}
inline DatatypeResolutionException(std::string msg);
};/* class DatatypeResolutionException */
+/**
+ * A holder type (used in calls to DatatypeConstructor::addArg())
+ * to allow a Datatype to refer to itself. Self-typed fields of
+ * Datatypes will be properly typed when a Type is created for the
+ * Datatype by the ExprManager (which calls Datatype::resolve()).
+ */
+class CVC4_PUBLIC DatatypeSelfType {
+};/* class DatatypeSelfType */
+
+/**
+ * An unresolved type (used in calls to
+ * DatatypeConstructor::addArg()) to allow a Datatype to refer to
+ * itself or to other mutually-recursive Datatypes. Unresolved-type
+ * fields of Datatypes will be properly typed when a Type is created
+ * for the Datatype by the ExprManager (which calls
+ * Datatype::resolve()).
+ */
+class CVC4_PUBLIC DatatypeUnresolvedType {
+ std::string d_name;
+public:
+ inline DatatypeUnresolvedType(std::string name);
+ inline std::string getName() const throw();
+};/* class DatatypeUnresolvedType */
+
+/**
+ * A Datatype constructor argument (i.e., a Datatype field).
+ */
+class CVC4_PUBLIC DatatypeConstructorArg {
+
+ std::string d_name;
+ Expr d_selector;
+ /** the constructor associated with this selector */
+ Expr d_constructor;
+ bool d_resolved;
+
+ DatatypeConstructorArg(std::string name, Expr selector);
+ friend class DatatypeConstructor;
+ friend class Datatype;
+
+ bool isUnresolvedSelf() const throw();
+
+public:
+
+ /** Get the name of this constructor argument. */
+ std::string getName() const throw();
+
+ /**
+ * Get the selector for this constructor argument; this call is
+ * only permitted after resolution.
+ */
+ Expr getSelector() const;
+
+ /**
+ * Get the associated constructor for this constructor argument;
+ * this call is only permitted after resolution.
+ */
+ Expr getConstructor() const;
+
+ /**
+ * Get the type of the selector for this constructor argument;
+ * this call is only permitted after resolution.
+ */
+ Type getType() const;
+
+ /**
+ * Get the name of the type of this constructor argument
+ * (Datatype field). Can be used for not-yet-resolved Datatypes
+ * (in which case the name of the unresolved type, or "[self]"
+ * for a self-referential type is returned).
+ */
+ std::string getTypeName() const;
+
+ /**
+ * Returns true iff this constructor argument has been resolved.
+ */
+ bool isResolved() const throw();
+
+};/* class DatatypeConstructorArg */
+
+/**
+ * A constructor for a Datatype.
+ */
+class CVC4_PUBLIC DatatypeConstructor {
+public:
+
+ /** The type for iterators over constructor arguments. */
+ typedef std::vector<DatatypeConstructorArg>::iterator iterator;
+ /** The (const) type for iterators over constructor arguments. */
+ typedef std::vector<DatatypeConstructorArg>::const_iterator const_iterator;
+
+private:
+
+ std::string d_name;
+ Expr d_constructor;
+ Expr d_tester;
+ std::vector<DatatypeConstructorArg> d_args;
+
+ void resolve(ExprManager* em, DatatypeType self,
+ const std::map<std::string, DatatypeType>& resolutions,
+ const std::vector<Type>& placeholders,
+ const std::vector<Type>& replacements,
+ const std::vector< SortConstructorType >& paramTypes,
+ const std::vector< DatatypeType >& paramReplacements)
+ throw(AssertionException, DatatypeResolutionException);
+ friend class Datatype;
+
+ /** @FIXME document this! */
+ Type doParametricSubstitution(Type range,
+ const std::vector< SortConstructorType >& paramTypes,
+ const std::vector< DatatypeType >& paramReplacements);
+public:
+ /**
+ * Create a new Datatype constructor with the given name for the
+ * constructor and the same name (prefixed with "is_") for the
+ * tester. The actual constructor and tester (meaning, the Exprs
+ * representing operators for these entities) aren't created until
+ * resolution time.
+ */
+ explicit DatatypeConstructor(std::string name);
+
+ /**
+ * Create a new Datatype constructor with the given name for the
+ * constructor and the given name for the tester. The actual
+ * constructor and tester aren't created until resolution time.
+ */
+ DatatypeConstructor(std::string name, std::string tester);
+
+ /**
+ * Add an argument (i.e., a data field) of the given name and type
+ * to this Datatype constructor. Selector names need not be unique;
+ * they are for convenience and pretty-printing only.
+ */
+ void addArg(std::string selectorName, Type selectorType);
+
+ /**
+ * Add an argument (i.e., a data field) of the given name to this
+ * Datatype constructor that refers to an as-yet-unresolved
+ * Datatype (which may be mutually-recursive). Selector names need
+ * not be unique; they are for convenience and pretty-printing only.
+ */
+ void addArg(std::string selectorName, DatatypeUnresolvedType selectorType);
+
+ /**
+ * Add a self-referential (i.e., a data field) of the given name
+ * to this Datatype constructor that refers to the enclosing
+ * Datatype. For example, using the familiar "nat" Datatype, to
+ * create the "pred" field for "succ" constructor, one uses
+ * succ::addArg("pred", DatatypeSelfType())---the actual Type
+ * cannot be passed because the Datatype is still under
+ * construction. Selector names need not be unique; they are for
+ * convenience and pretty-printing only.
+ *
+ * This is a special case of
+ * DatatypeConstructor::addArg(std::string, DatatypeUnresolvedType).
+ */
+ void addArg(std::string selectorName, DatatypeSelfType);
+
+ /** Get the name of this Datatype constructor. */
+ std::string getName() const throw();
+
+ /**
+ * Get the constructor operator of this Datatype constructor. The
+ * Datatype must be resolved.
+ */
+ Expr getConstructor() const;
+
+ /**
+ * Get the tester operator of this Datatype constructor. The
+ * Datatype must be resolved.
+ */
+ Expr getTester() const;
+
+ /**
+ * Get the number of arguments (so far) of this Datatype constructor.
+ */
+ inline size_t getNumArgs() const throw();
+
+ /**
+ * Get the specialized constructor type for a parametric
+ * constructor; this call is only permitted after resolution.
+ * Given a (concrete) returnType, the constructor's concrete
+ * type in this parametric datatype is returned.
+ *
+ * For instance, if the datatype is list[T], with constructor
+ * "cons[T]" of type "T -> list[T] -> list[T]", then calling
+ * this function with "list[int]" will return the concrete
+ * "cons" constructor type for lists of int---namely,
+ * "int -> list[int] -> list[int]".
+ */
+ Type getSpecializedConstructorType(Type returnType) const;
+
+ /**
+ * Return the cardinality of this constructor (the product of the
+ * cardinalities of its arguments).
+ */
+ Cardinality getCardinality() const throw(AssertionException);
+
+ /**
+ * Return true iff this constructor is finite (it is nullary or
+ * each of its argument types are finite). This function can
+ * only be called for resolved constructors.
+ */
+ bool isFinite() const throw(AssertionException);
+
+ /**
+ * Return true iff this constructor is well-founded (there exist
+ * ground terms). The constructor must be resolved or an
+ * exception is thrown.
+ */
+ bool isWellFounded() const throw(AssertionException);
+
+ /**
+ * Construct and return a ground term of this constructor. The
+ * constructor must be both resolved and well-founded, or else an
+ * exception is thrown.
+ */
+ Expr mkGroundTerm( Type t ) const throw(AssertionException);
+
+ /**
+ * Returns true iff this Datatype constructor has already been
+ * resolved.
+ */
+ inline bool isResolved() const throw();
+
+ /** Get the beginning iterator over DatatypeConstructor args. */
+ inline iterator begin() throw();
+ /** Get the ending iterator over DatatypeConstructor args. */
+ inline iterator end() throw();
+ /** Get the beginning const_iterator over DatatypeConstructor args. */
+ inline const_iterator begin() const throw();
+ /** Get the ending const_iterator over DatatypeConstructor args. */
+ inline const_iterator end() const throw();
+
+ /** Get the ith DatatypeConstructor arg. */
+ const DatatypeConstructorArg& operator[](size_t index) const;
+
+ /**
+ * Get the DatatypeConstructor arg named. This is a linear search
+ * through the arguments, so in the case of multiple,
+ * similarly-named arguments, the first is returned.
+ */
+ const DatatypeConstructorArg& operator[](std::string name) const;
+
+ /**
+ * Get the selector named. This is a linear search
+ * through the arguments, so in the case of multiple,
+ * similarly-named arguments, the selector for the first
+ * is returned.
+ */
+ Expr getSelector(std::string name) const;
+
+};/* class DatatypeConstructor */
+
/**
* The representation of an inductive datatype.
*
* You cannot define "nat" until you have a Type for it, but you
* cannot have a Type for it until you fill in the type of the "pred"
* selector, which needs the Type. So we have a chicken-and-egg
- * problem. It's even more complicated when we have mutual recusion
+ * problem. It's even more complicated when we have mutual recursion
* between datatypes, since the CVC presentation language does not
* require forward-declarations. Here, we define trees of lists that
* contain trees of lists (etc):
* on the task of generating its own selectors and testers, for
* instance. That means that, after reifying the Datatype with the
* ExprManager, the parser needs to go through the (now-resolved)
- * Datatype and request ; see src/parser/parser.cpp for how this is
- * done. For API usage ideas, see test/unit/util/datatype_black.h.
+ * Datatype and request the constructor, selector, and tester terms.
+ * See src/parser/parser.cpp for how this is done. For API usage
+ * ideas, see test/unit/util/datatype_black.h.
*/
class CVC4_PUBLIC Datatype {
public:
*/
static size_t indexOf(Expr item) CVC4_PUBLIC;
- /**
- * A holder type (used in calls to Datatype::Constructor::addArg())
- * to allow a Datatype to refer to itself. Self-typed fields of
- * Datatypes will be properly typed when a Type is created for the
- * Datatype by the ExprManager (which calls Datatype::resolve()).
- */
- class CVC4_PUBLIC SelfType {
- };/* class Datatype::SelfType */
-
- /**
- * An unresolved type (used in calls to
- * Datatype::Constructor::addArg()) to allow a Datatype to refer to
- * itself or to other mutually-recursive Datatypes. Unresolved-type
- * fields of Datatypes will be properly typed when a Type is created
- * for the Datatype by the ExprManager (which calls
- * Datatype::resolve()).
- */
- class CVC4_PUBLIC UnresolvedType {
- std::string d_name;
- public:
- inline UnresolvedType(std::string name);
- inline std::string getName() const throw();
- };/* class Datatype::UnresolvedType */
-
- /**
- * A constructor for a Datatype.
- */
- class CVC4_PUBLIC Constructor {
- public:
- /**
- * A Datatype constructor argument (i.e., a Datatype field).
- */
- class CVC4_PUBLIC Arg {
-
- std::string d_name;
- Expr d_selector;
- /** the constructor associated with this selector */
- Expr d_constructor;
- bool d_resolved;
-
- explicit Arg(std::string name, Expr selector);
- friend class Constructor;
- friend class Datatype;
-
- bool isUnresolvedSelf() const throw();
-
- public:
-
- /** Get the name of this constructor argument. */
- std::string getName() const throw();
-
- /**
- * Get the selector for this constructor argument; this call is
- * only permitted after resolution.
- */
- Expr getSelector() const;
-
- /**
- * Get the associated constructor for this constructor argument;
- * this call is only permitted after resolution.
- */
- Expr getConstructor() const;
-
- /**
- * Get the selector for this constructor argument; this call is
- * only permitted after resolution.
- */
- Type getSelectorType() const;
-
- /**
- * Get the name of the type of this constructor argument
- * (Datatype field). Can be used for not-yet-resolved Datatypes
- * (in which case the name of the unresolved type, or "[self]"
- * for a self-referential type is returned).
- */
- std::string getSelectorTypeName() const;
-
- /**
- * Returns true iff this constructor argument has been resolved.
- */
- bool isResolved() const throw();
-
- };/* class Datatype::Constructor::Arg */
-
- /** The type for iterators over constructor arguments. */
- typedef std::vector<Arg>::iterator iterator;
- /** The (const) type for iterators over constructor arguments. */
- typedef std::vector<Arg>::const_iterator const_iterator;
-
- private:
-
- std::string d_name;
- Expr d_constructor;
- Expr d_tester;
- std::vector<Arg> d_args;
-
- void resolve(ExprManager* em, DatatypeType self,
- const std::map<std::string, DatatypeType>& resolutions,
- const std::vector<Type>& placeholders,
- const std::vector<Type>& replacements,
- const std::vector< SortConstructorType >& paramTypes,
- const std::vector< DatatypeType >& paramReplacements)
- throw(AssertionException, DatatypeResolutionException);
- friend class Datatype;
-
- /** @FIXME document this! */
- Type doParametricSubstitution(Type range,
- const std::vector< SortConstructorType >& paramTypes,
- const std::vector< DatatypeType >& paramReplacements);
- public:
- /**
- * Create a new Datatype constructor with the given name for the
- * constructor and the same name (prefixed with "is_") for the
- * tester. The actual constructor and tester aren't created until
- * resolution time.
- */
- explicit Constructor(std::string name);
-
- /**
- * Create a new Datatype constructor with the given name for the
- * constructor and the given name for the tester. The actual
- * constructor and tester aren't created until resolution time.
- */
- explicit Constructor(std::string name, std::string tester);
-
- /**
- * Add an argument (i.e., a data field) of the given name and type
- * to this Datatype constructor.
- */
- void addArg(std::string selectorName, Type selectorType);
-
- /**
- * Add an argument (i.e., a data field) of the given name to this
- * Datatype constructor that refers to an as-yet-unresolved
- * Datatype (which may be mutually-recursive).
- */
- void addArg(std::string selectorName, Datatype::UnresolvedType selectorType);
-
- /**
- * Add a self-referential (i.e., a data field) of the given name
- * to this Datatype constructor that refers to the enclosing
- * Datatype. For example, using the familiar "nat" Datatype, to
- * create the "pred" field for "succ" constructor, one uses
- * succ::addArg("pred", Datatype::SelfType())---the actual Type
- * cannot be passed because the Datatype is still under
- * construction.
- *
- * This is a special case of
- * Constructor::addArg(std::string, Datatype::UnresolvedType).
- */
- void addArg(std::string selectorName, Datatype::SelfType);
-
- /** Get the name of this Datatype constructor. */
- std::string getName() const throw();
-
- /**
- * Get the constructor operator of this Datatype constructor. The
- * Datatype must be resolved.
- */
- Expr getConstructor() const;
-
- /**
- * Get the tester operator of this Datatype constructor. The
- * Datatype must be resolved.
- */
- Expr getTester() const;
-
- /**
- * Get the number of arguments (so far) of this Datatype constructor.
- */
- inline size_t getNumArgs() const throw();
-
- /**
- * Get the specialized constructor type for a parametric
- * constructor; this call is only permitted after resolution.
- */
- Type getSpecializedConstructorType(Type returnType) const;
-
- /**
- * Return the cardinality of this constructor (the product of the
- * cardinalities of its arguments).
- */
- Cardinality getCardinality() const throw(AssertionException);
-
- /**
- * Return true iff this constructor is finite (it is nullary or
- * each of its argument types are finite). This function can
- * only be called for resolved constructors.
- */
- bool isFinite() const throw(AssertionException);
-
- /**
- * Return true iff this constructor is well-founded (there exist
- * ground terms). The constructor must be resolved or an
- * exception is thrown.
- */
- bool isWellFounded() const throw(AssertionException);
-
- /**
- * Construct and return a ground term of this constructor. The
- * constructor must be both resolved and well-founded, or else an
- * exception is thrown.
- */
- Expr mkGroundTerm( Type t ) const throw(AssertionException);
-
- /**
- * Returns true iff this Datatype constructor has already been
- * resolved.
- */
- inline bool isResolved() const throw();
-
- /** Get the beginning iterator over Constructor args. */
- inline iterator begin() throw();
- /** Get the ending iterator over Constructor args. */
- inline iterator end() throw();
- /** Get the beginning const_iterator over Constructor args. */
- inline const_iterator begin() const throw();
- /** Get the ending const_iterator over Constructor args. */
- inline const_iterator end() const throw();
-
- /** Get the ith Constructor arg. */
- const Arg& operator[](size_t index) const;
-
- /**
- * Get the Constructor arg named. This is a linear search
- * through the arguments, so in the case of multiple,
- * similarly-named arguments, the first is returned.
- */
- const Arg& operator[](std::string name) const;
-
- /**
- * Get the selector named. This is a linear search
- * through the arguments, so in the case of multiple,
- * similarly-named arguments, the selector for the first
- * is returned.
- */
- Expr getSelector(std::string name) const;
-
- };/* class Datatype::Constructor */
-
/** The type for iterators over constructors. */
- typedef std::vector<Constructor>::iterator iterator;
+ typedef std::vector<DatatypeConstructor>::iterator iterator;
/** The (const) type for iterators over constructors. */
- typedef std::vector<Constructor>::const_iterator const_iterator;
+ typedef std::vector<DatatypeConstructor>::const_iterator const_iterator;
private:
std::string d_name;
std::vector<Type> d_params;
- std::vector<Constructor> d_constructors;
+ std::vector<DatatypeConstructor> d_constructors;
bool d_resolved;
Type d_self;
* chicken-and-egg problem. The DatatypeType around the Datatype
* cannot exist until the Datatype is finalized, and the Datatype
* cannot refer to the DatatypeType representing itself until it
- * exists. resolve() is called by the ExprManager when a Type. Has
- * the effect of freezing the object, too; that is, addConstructor()
- * will fail after a call to resolve().
+ * exists. resolve() is called by the ExprManager when a Type is
+ * ultimately requested of the Datatype specification (that is, when
+ * ExprManager::mkDatatypeType() or ExprManager::mkMutualDatatypeTypes()
+ * is called). Has the effect of freezing the object, too; that is,
+ * addConstructor() will fail after a call to resolve().
+ *
+ * The basic goal of resolution is to assign constructors, selectors,
+ * and testers. To do this, any UnresolvedType/SelfType references
+ * must be cleared up. This is the purpose of the "resolutions" map;
+ * it includes any mutually-recursive datatypes that are currently
+ * under resolution. The four vectors come in two pairs (so, really
+ * they are two maps). placeholders->replacements give type variables
+ * that should be resolved in the case of parametric datatypes.
+ *
+ * @param em the ExprManager at play
+ * @param resolutions a map of strings to DatatypeTypes currently under resolution
+ * @param placeholders the types in these Datatypes under resolution that must be replaced
+ * @param replacements the corresponding replacements
+ * @param paramTypes the sort constructors in these Datatypes under resolution that must be replaced
+ * @param paramReplacements the corresponding (parametric) DatatypeTypes
*/
void resolve(ExprManager* em,
const std::map<std::string, DatatypeType>& resolutions,
* Create a new Datatype of the given name, with the given
* parameterization.
*/
- inline explicit Datatype(std::string name, std::vector<Type>& params);
+ inline Datatype(std::string name, std::vector<Type>& params);
- /** Add a constructor to this Datatype. */
- void addConstructor(const Constructor& c);
+ /**
+ * Add a constructor to this Datatype. Constructor names need not
+ * be unique; they are for convenience and pretty-printing only.
+ */
+ void addConstructor(const DatatypeConstructor& c);
/** Get the name of this Datatype. */
inline std::string getName() const throw();
/** Return true iff this Datatype has already been resolved. */
inline bool isResolved() const throw();
- /** Get the beginning iterator over Constructors. */
- inline std::vector<Constructor>::iterator begin() throw();
- /** Get the ending iterator over Constructors. */
- inline std::vector<Constructor>::iterator end() throw();
- /** Get the beginning const_iterator over Constructors. */
- inline std::vector<Constructor>::const_iterator begin() const throw();
- /** Get the ending const_iterator over Constructors. */
- inline std::vector<Constructor>::const_iterator end() const throw();
+ /** Get the beginning iterator over DatatypeConstructors. */
+ inline std::vector<DatatypeConstructor>::iterator begin() throw();
+ /** Get the ending iterator over DatatypeConstructors. */
+ inline std::vector<DatatypeConstructor>::iterator end() throw();
+ /** Get the beginning const_iterator over DatatypeConstructors. */
+ inline std::vector<DatatypeConstructor>::const_iterator begin() const throw();
+ /** Get the ending const_iterator over DatatypeConstructors. */
+ inline std::vector<DatatypeConstructor>::const_iterator end() const throw();
- /** Get the ith Constructor. */
- const Constructor& operator[](size_t index) const;
+ /** Get the ith DatatypeConstructor. */
+ const DatatypeConstructor& operator[](size_t index) const;
/**
- * Get the Constructor named. This is a linear search
+ * Get the DatatypeConstructor named. This is a linear search
* through the constructors, so in the case of multiple,
* similarly-named constructors, the first is returned.
*/
- const Constructor& operator[](std::string name) const;
+ const DatatypeConstructor& operator[](std::string name) const;
/**
* Get the constructor operator for the named constructor.
+ * This is a linear search through the constructors, so in
+ * the case of multiple, similarly-named constructors, the
+ * first is returned.
+ *
* This Datatype must be resolved.
*/
Expr getConstructor(std::string name) const;
};/* class Datatype */
-
/**
* A hash strategy for Datatypes. Needed because Datatypes are used
* as the constant payload in CONSTANT-kinded TypeNodes (for
inline size_t operator()(const Datatype* dt) const {
return StringHashFunction()(dt->getName());
}
- inline size_t operator()(const Datatype::Constructor& dtc) const {
+ inline size_t operator()(const DatatypeConstructor& dtc) const {
return StringHashFunction()(dtc.getName());
}
- inline size_t operator()(const Datatype::Constructor* dtc) const {
+ inline size_t operator()(const DatatypeConstructor* dtc) const {
return StringHashFunction()(dtc->getName());
}
};/* struct DatatypeHashFunction */
// FUNCTION DECLARATIONS FOR OUTPUT STREAMS
std::ostream& operator<<(std::ostream& os, const Datatype& dt) CVC4_PUBLIC;
-std::ostream& operator<<(std::ostream& os, const Datatype::Constructor& ctor) CVC4_PUBLIC;
-std::ostream& operator<<(std::ostream& os, const Datatype::Constructor::Arg& arg) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& os, const DatatypeConstructor& ctor) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& os, const DatatypeConstructorArg& arg) CVC4_PUBLIC;
// INLINE FUNCTIONS
Exception(msg) {
}
-inline Datatype::UnresolvedType::UnresolvedType(std::string name) :
+inline DatatypeUnresolvedType::DatatypeUnresolvedType(std::string name) :
d_name(name) {
}
-inline std::string Datatype::UnresolvedType::getName() const throw() {
+inline std::string DatatypeUnresolvedType::getName() const throw() {
return d_name;
}
return d_constructors.end();
}
-inline bool Datatype::Constructor::isResolved() const throw() {
+inline bool DatatypeConstructor::isResolved() const throw() {
return !d_tester.isNull();
}
-inline size_t Datatype::Constructor::getNumArgs() const throw() {
+inline size_t DatatypeConstructor::getNumArgs() const throw() {
return d_args.size();
}
-inline bool Datatype::Constructor::Arg::isResolved() const throw() {
+inline bool DatatypeConstructorArg::isResolved() const throw() {
// We could just write:
//
// return !d_selector.isNull() && d_selector.getType().isSelector();
return d_resolved;
}
-inline Datatype::Constructor::iterator Datatype::Constructor::begin() throw() {
+inline DatatypeConstructor::iterator DatatypeConstructor::begin() throw() {
return d_args.begin();
}
-inline Datatype::Constructor::iterator Datatype::Constructor::end() throw() {
+inline DatatypeConstructor::iterator DatatypeConstructor::end() throw() {
return d_args.end();
}
-inline Datatype::Constructor::const_iterator Datatype::Constructor::begin() const throw() {
+inline DatatypeConstructor::const_iterator DatatypeConstructor::begin() const throw() {
return d_args.begin();
}
-inline Datatype::Constructor::const_iterator Datatype::Constructor::end() const throw() {
+inline DatatypeConstructor::const_iterator DatatypeConstructor::end() const throw() {
return d_args.end();
}
#include "util/datatype.h"
%}
-namespace CVC4 {
-%rename(DatatypeConstructor) CVC4::Datatype::Constructor;
-%rename(DatatypeConstructor) CVC4::Constructor;
-}
-
%extend std::vector< CVC4::Datatype > {
/* These member functions have slightly different signatures in
* different swig language packages. The underlying issue is that
- * Datatype::Constructor doesn't have a default constructor */
+ * DatatypeConstructor doesn't have a default constructor */
%ignore vector(unsigned int size = 0);// ocaml
%ignore set( int i, const CVC4::Datatype &x );// ocaml
%ignore to_array();// ocaml
};
%template(vectorDatatype) std::vector< CVC4::Datatype >;
-%extend std::vector< CVC4::Datatype::Constructor > {
+%extend std::vector< CVC4::DatatypeConstructor > {
/* These member functions have slightly different signatures in
* different swig language packages. The underlying issue is that
- * Datatype::Constructor doesn't have a default constructor */
+ * DatatypeConstructor doesn't have a default constructor */
%ignore vector(unsigned int size = 0);// ocaml
- %ignore set( int i, const CVC4::Datatype::Constructor &x );// ocaml
+ %ignore set( int i, const CVC4::DatatypeConstructor &x );// ocaml
%ignore to_array();// ocaml
%ignore vector(size_type);// java/python
%ignore resize(size_type);// java/python
};
-%template(vectorDatatypeConstructor) std::vector< CVC4::Datatype::Constructor >;
+%template(vectorDatatypeConstructor) std::vector< CVC4::DatatypeConstructor >;
%rename(equals) CVC4::Datatype::operator==(const Datatype&) const;
%ignore CVC4::Datatype::operator!=(const Datatype&) const;
%rename(apply) CVC4::DatatypeHashFunction::operator()(const Datatype&) const;
%ignore CVC4::DatatypeHashFunction::operator()(const Datatype*) const;
-%rename(apply) CVC4::DatatypeHashFunction::operator()(const Datatype::Constructor&) const;
-%ignore CVC4::DatatypeHashFunction::operator()(const Datatype::Constructor*) const;
+%rename(apply) CVC4::DatatypeHashFunction::operator()(const DatatypeConstructor&) const;
+%ignore CVC4::DatatypeHashFunction::operator()(const DatatypeConstructor*) const;
-%rename(beginConst) CVC4::Constructor::begin() const;
-%rename(endConst) CVC4::Constructor::end() const;
+%rename(beginConst) CVC4::DatatypeConstructor::begin() const;
+%rename(endConst) CVC4::DatatypeConstructor::end() const;
-%rename(getArg) CVC4::Constructor::operator[](size_t) const;
+%rename(getArg) CVC4::DatatypeConstructor::operator[](size_t) const;
%ignore CVC4::operator<<(std::ostream&, const Datatype&);
-%ignore CVC4::operator<<(std::ostream&, const Datatype::Constructor&);
-%ignore CVC4::operator<<(std::ostream&, const Datatype::Constructor::Arg&);
+%ignore CVC4::operator<<(std::ostream&, const DatatypeConstructor&);
+%ignore CVC4::operator<<(std::ostream&, const DatatypeConstructorArg&);
-%feature("valuewrapper") CVC4::Datatype::UnresolvedType;
-%feature("valuewrapper") CVC4::Datatype::Constructor;
+%feature("valuewrapper") CVC4::DatatypeUnresolvedType;
+%feature("valuewrapper") CVC4::DatatypeConstructor;
%include "util/datatype.h"
-namespace CVC4 {
- class CVC4_PUBLIC Arg {
-
- std::string d_name;
- Expr d_selector;
- /** the constructor associated with this selector */
- Expr d_constructor;
- bool d_resolved;
-
- explicit Arg(std::string name, Expr selector);
- friend class Constructor;
- friend class Datatype;
-
- bool isUnresolvedSelf() const throw();
-
- public:
-
- /** Get the name of this constructor argument. */
- std::string getName() const throw();
-
- /**
- * Get the selector for this constructor argument; this call is
- * only permitted after resolution.
- */
- Expr getSelector() const;
-
- /**
- * Get the associated constructor for this constructor argument;
- * this call is only permitted after resolution.
- */
- Expr getConstructor() const;
-
- /**
- * Get the selector for this constructor argument; this call is
- * only permitted after resolution.
- */
- Type getSelectorType() const;
-
- /**
- * Get the name of the type of this constructor argument
- * (Datatype field). Can be used for not-yet-resolved Datatypes
- * (in which case the name of the unresolved type, or "[self]"
- * for a self-referential type is returned).
- */
- std::string getSelectorTypeName() const;
-
- /**
- * Returns true iff this constructor argument has been resolved.
- */
- bool isResolved() const throw();
-
- };/* class Datatype::Constructor::Arg */
-
- class Constructor {
- public:
-
- /** The type for iterators over constructor arguments. */
- typedef std::vector<Arg>::iterator iterator;
- /** The (const) type for iterators over constructor arguments. */
- typedef std::vector<Arg>::const_iterator const_iterator;
-
- private:
-
- std::string d_name;
- Expr d_constructor;
- Expr d_tester;
- std::vector<Arg> d_args;
-
- void resolve(ExprManager* em, DatatypeType self,
- const std::map<std::string, DatatypeType>& resolutions,
- const std::vector<Type>& placeholders,
- const std::vector<Type>& replacements,
- const std::vector< SortConstructorType >& paramTypes,
- const std::vector< DatatypeType >& paramReplacements)
- throw(AssertionException, DatatypeResolutionException);
- friend class Datatype;
-
- /** @FIXME document this! */
- Type doParametricSubstitution(Type range,
- const std::vector< SortConstructorType >& paramTypes,
- const std::vector< DatatypeType >& paramReplacements);
- public:
- /**
- * Create a new Datatype constructor with the given name for the
- * constructor and the given name for the tester. The actual
- * constructor and tester aren't created until resolution time.
- */
- explicit Constructor(std::string name, std::string tester);
-
- /**
- * Add an argument (i.e., a data field) of the given name and type
- * to this Datatype constructor.
- */
- void addArg(std::string selectorName, Type selectorType);
-
- /**
- * Add an argument (i.e., a data field) of the given name to this
- * Datatype constructor that refers to an as-yet-unresolved
- * Datatype (which may be mutually-recursive).
- */
- void addArg(std::string selectorName, Datatype::UnresolvedType selectorType);
-
- /**
- * Add a self-referential (i.e., a data field) of the given name
- * to this Datatype constructor that refers to the enclosing
- * Datatype. For example, using the familiar "nat" Datatype, to
- * create the "pred" field for "succ" constructor, one uses
- * succ::addArg("pred", Datatype::SelfType())---the actual Type
- * cannot be passed because the Datatype is still under
- * construction.
- *
- * This is a special case of
- * Constructor::addArg(std::string, Datatype::UnresolvedType).
- */
- void addArg(std::string selectorName, Datatype::SelfType);
-
- /** Get the name of this Datatype constructor. */
- std::string getName() const throw();
- /**
- * Get the constructor operator of this Datatype constructor. The
- * Datatype must be resolved.
- */
- Expr getConstructor() const;
- /**
- * Get the tester operator of this Datatype constructor. The
- * Datatype must be resolved.
- */
- Expr getTester() const;
- /**
- * Get the number of arguments (so far) of this Datatype constructor.
- */
- inline size_t getNumArgs() const throw();
-
- /**
- * Get the specialized constructor type for a parametric
- * constructor; this call is only permitted after resolution.
- */
- Type getSpecializedConstructorType(Type returnType) const;
-
- /**
- * Return the cardinality of this constructor (the product of the
- * cardinalities of its arguments).
- */
- Cardinality getCardinality() const throw(AssertionException);
-
- /**
- * Return true iff this constructor is finite (it is nullary or
- * each of its argument types are finite). This function can
- * only be called for resolved constructors.
- */
- bool isFinite() const throw(AssertionException);
-
- /**
- * Return true iff this constructor is well-founded (there exist
- * ground terms). The constructor must be resolved or an
- * exception is thrown.
- */
- bool isWellFounded() const throw(AssertionException);
-
- /**
- * Construct and return a ground term of this constructor. The
- * constructor must be both resolved and well-founded, or else an
- * exception is thrown.
- */
- Expr mkGroundTerm( Type t ) const throw(AssertionException);
-
- /**
- * Returns true iff this Datatype constructor has already been
- * resolved.
- */
- inline bool isResolved() const throw();
-
- /** Get the beginning iterator over Constructor args. */
- inline iterator begin() throw();
- /** Get the ending iterator over Constructor args. */
- inline iterator end() throw();
- /** Get the beginning const_iterator over Constructor args. */
- inline const_iterator begin() const throw();
- /** Get the ending const_iterator over Constructor args. */
- inline const_iterator end() const throw();
-
- /** Get the ith Constructor arg. */
- const Arg& operator[](size_t index) const;
-
- };/* class Datatype::Constructor */
-
- class SelfType {
- };/* class Datatype::SelfType */
-
- /**
- * An unresolved type (used in calls to
- * Datatype::Constructor::addArg()) to allow a Datatype to refer to
- * itself or to other mutually-recursive Datatypes. Unresolved-type
- * fields of Datatypes will be properly typed when a Type is created
- * for the Datatype by the ExprManager (which calls
- * Datatype::resolve()).
- */
- class UnresolvedType {
- std::string d_name;
- public:
- inline UnresolvedType(std::string name);
- inline std::string getName() const throw();
- };/* class Datatype::UnresolvedType */
-}
-
-%{
-namespace CVC4 {
-typedef Datatype::Constructor Constructor;
-typedef Datatype::Constructor::Arg Arg;
-typedef Datatype::SelfType SelfType;
-typedef Datatype::UnresolvedType UnresolvedType;
-}
-%}
-
void testEnumeration() {
Datatype colors("colors");
- Datatype::Constructor yellow("yellow", "is_yellow");
- Datatype::Constructor blue("blue", "is_blue");
- Datatype::Constructor green("green", "is_green");
- Datatype::Constructor red("red", "is_red");
+ DatatypeConstructor yellow("yellow", "is_yellow");
+ DatatypeConstructor blue("blue", "is_blue");
+ DatatypeConstructor green("green", "is_green");
+ DatatypeConstructor red("red", "is_red");
colors.addConstructor(yellow);
colors.addConstructor(blue);
void testNat() {
Datatype nat("nat");
- Datatype::Constructor succ("succ", "is_succ");
- succ.addArg("pred", Datatype::SelfType());
+ DatatypeConstructor succ("succ", "is_succ");
+ succ.addArg("pred", DatatypeSelfType());
nat.addConstructor(succ);
- Datatype::Constructor zero("zero", "is_zero");
+ DatatypeConstructor zero("zero", "is_zero");
nat.addConstructor(zero);
Debug("datatypes") << nat << std::endl;
Datatype tree("tree");
Type integerType = d_em->integerType();
- Datatype::Constructor node("node", "is_node");
- node.addArg("left", Datatype::SelfType());
- node.addArg("right", Datatype::SelfType());
+ DatatypeConstructor node("node", "is_node");
+ node.addArg("left", DatatypeSelfType());
+ node.addArg("right", DatatypeSelfType());
tree.addConstructor(node);
- Datatype::Constructor leaf("leaf", "is_leaf");
+ DatatypeConstructor leaf("leaf", "is_leaf");
leaf.addArg("leaf", integerType);
tree.addConstructor(leaf);
Datatype list("list");
Type integerType = d_em->integerType();
- Datatype::Constructor cons("cons", "is_cons");
+ DatatypeConstructor cons("cons", "is_cons");
cons.addArg("car", integerType);
- cons.addArg("cdr", Datatype::SelfType());
+ cons.addArg("cdr", DatatypeSelfType());
list.addConstructor(cons);
- Datatype::Constructor nil("nil", "is_nil");
+ DatatypeConstructor nil("nil", "is_nil");
list.addConstructor(nil);
Debug("datatypes") << list << std::endl;
Datatype list("list");
Type realType = d_em->realType();
- Datatype::Constructor cons("cons", "is_cons");
+ DatatypeConstructor cons("cons", "is_cons");
cons.addArg("car", realType);
- cons.addArg("cdr", Datatype::SelfType());
+ cons.addArg("cdr", DatatypeSelfType());
list.addConstructor(cons);
- Datatype::Constructor nil("nil", "is_nil");
+ DatatypeConstructor nil("nil", "is_nil");
list.addConstructor(nil);
Debug("datatypes") << list << std::endl;
Datatype list("list");
Type booleanType = d_em->booleanType();
- Datatype::Constructor cons("cons", "is_cons");
+ DatatypeConstructor cons("cons", "is_cons");
cons.addArg("car", booleanType);
- cons.addArg("cdr", Datatype::SelfType());
+ cons.addArg("cdr", DatatypeSelfType());
list.addConstructor(cons);
- Datatype::Constructor nil("nil", "is_nil");
+ DatatypeConstructor nil("nil", "is_nil");
list.addConstructor(nil);
Debug("datatypes") << list << std::endl;
* END;
*/
Datatype tree("tree");
- Datatype::Constructor node("node", "is_node");
- node.addArg("left", Datatype::SelfType());
- node.addArg("right", Datatype::SelfType());
+ DatatypeConstructor node("node", "is_node");
+ node.addArg("left", DatatypeSelfType());
+ node.addArg("right", DatatypeSelfType());
tree.addConstructor(node);
- Datatype::Constructor leaf("leaf", "is_leaf");
- leaf.addArg("leaf", Datatype::UnresolvedType("list"));
+ DatatypeConstructor leaf("leaf", "is_leaf");
+ leaf.addArg("leaf", DatatypeUnresolvedType("list"));
tree.addConstructor(leaf);
Debug("datatypes") << tree << std::endl;
Datatype list("list");
- Datatype::Constructor cons("cons", "is_cons");
- cons.addArg("car", Datatype::UnresolvedType("tree"));
- cons.addArg("cdr", Datatype::SelfType());
+ DatatypeConstructor cons("cons", "is_cons");
+ cons.addArg("car", DatatypeUnresolvedType("tree"));
+ cons.addArg("cdr", DatatypeSelfType());
list.addConstructor(cons);
- Datatype::Constructor nil("nil", "is_nil");
+ DatatypeConstructor nil("nil", "is_nil");
list.addConstructor(nil);
Debug("datatypes") << list << std::endl;
// add another constructor to list datatype resulting in an
// "otherNil-list"
- Datatype::Constructor otherNil("otherNil", "is_otherNil");
+ DatatypeConstructor otherNil("otherNil", "is_otherNil");
dts[1].addConstructor(otherNil);
// remake the types
void testNotSoWellFounded() {
Datatype tree("tree");
- Datatype::Constructor node("node", "is_node");
- node.addArg("left", Datatype::SelfType());
- node.addArg("right", Datatype::SelfType());
+ DatatypeConstructor node("node", "is_node");
+ node.addArg("left", DatatypeSelfType());
+ node.addArg("right", DatatypeSelfType());
tree.addConstructor(node);
Debug("datatypes") << tree << std::endl;
projects / cvc5.git / commitdiff