/*! \file datatype.cpp
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Andrew Reynolds, Tim King
+ ** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
#include <string>
#include <sstream>
-#include "base/cvc4_assert.h"
+#include "base/check.h"
#include "expr/attribute.h"
+#include "expr/dtype.h"
#include "expr/expr_manager.h"
#include "expr/expr_manager_scope.h"
-#include "expr/matcher.h"
#include "expr/node.h"
+#include "expr/node_algorithm.h"
#include "expr/node_manager.h"
#include "expr/type.h"
+#include "expr/type_matcher.h"
+#include "options/datatypes_options.h"
#include "options/set_language.h"
+#include "theory/type_enumerator.h"
using namespace std;
namespace CVC4 {
-namespace expr {
- namespace attr {
- struct DatatypeIndexTag {};
- struct DatatypeConsIndexTag {};
- struct DatatypeFiniteTag {};
- struct DatatypeFiniteComputedTag {};
- struct DatatypeUFiniteTag {};
- struct DatatypeUFiniteComputedTag {};
- }/* CVC4::expr::attr namespace */
-}/* CVC4::expr namespace */
-
-typedef expr::Attribute<expr::attr::DatatypeIndexTag, uint64_t> DatatypeIndexAttr;
-typedef expr::Attribute<expr::attr::DatatypeConsIndexTag, uint64_t> DatatypeConsIndexAttr;
-typedef expr::Attribute<expr::attr::DatatypeFiniteTag, bool> DatatypeFiniteAttr;
-typedef expr::Attribute<expr::attr::DatatypeFiniteComputedTag, bool> DatatypeFiniteComputedAttr;
-typedef expr::Attribute<expr::attr::DatatypeUFiniteTag, bool> DatatypeUFiniteAttr;
-typedef expr::Attribute<expr::attr::DatatypeUFiniteComputedTag, bool> DatatypeUFiniteComputedAttr;
-
-Datatype::~Datatype(){
+Datatype::~Datatype()
+{
+ ExprManagerScope ems(*d_em);
+ d_internal.reset();
+ d_constructors.clear();
delete d_record;
}
+Datatype::Datatype(ExprManager* em, std::string name, bool isCo)
+ : d_em(em),
+ d_internal(nullptr),
+ d_record(NULL),
+ d_isRecord(false),
+ d_constructors()
+{
+ ExprManagerScope ems(*d_em);
+ d_internal = std::make_shared<DType>(name, isCo);
+}
+
+Datatype::Datatype(ExprManager* em,
+ std::string name,
+ const std::vector<Type>& params,
+ bool isCo)
+ : d_em(em),
+ d_internal(nullptr),
+ d_record(NULL),
+ d_isRecord(false),
+ d_constructors()
+{
+ ExprManagerScope ems(*d_em);
+ std::vector<TypeNode> paramsn;
+ for (const Type& t : params)
+ {
+ paramsn.push_back(TypeNode::fromType(t));
+ }
+ d_internal = std::make_shared<DType>(name, paramsn, isCo);
+}
+
const Datatype& Datatype::datatypeOf(Expr item) {
ExprManagerScope ems(item);
TypeNode t = Node::fromExpr(item).getType();
case kind::TESTER_TYPE:
return DatatypeType(t[0].toType()).getDatatype();
default:
- Unhandled("arg must be a datatype constructor, selector, or tester");
+ Unhandled() << "arg must be a datatype constructor, selector, or tester";
}
}
item.getType().isSelector(),
item,
"arg must be a datatype constructor, selector, or tester");
+ return indexOfInternal(item);
+}
+
+size_t Datatype::indexOfInternal(Expr item)
+{
TNode n = Node::fromExpr(item);
if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){
return indexOf( item[0] );
}else{
- Assert(n.hasAttribute(DatatypeIndexAttr()));
- return n.getAttribute(DatatypeIndexAttr());
+ Assert(n.hasAttribute(DTypeIndexAttr()));
+ return n.getAttribute(DTypeIndexAttr());
}
}
PrettyCheckArgument(item.getType().isSelector(),
item,
"arg must be a datatype selector");
+ return cindexOfInternal(item);
+}
+size_t Datatype::cindexOfInternal(Expr item)
+{
TNode n = Node::fromExpr(item);
if( item.getKind()==kind::APPLY_TYPE_ASCRIPTION ){
return cindexOf( item[0] );
}else{
- Assert(n.hasAttribute(DatatypeConsIndexAttr()));
- return n.getAttribute(DatatypeConsIndexAttr());
+ Assert(n.hasAttribute(DTypeConsIndexAttr()));
+ return n.getAttribute(DTypeConsIndexAttr());
}
}
-void Datatype::resolve(ExprManager* em,
- const std::map<std::string, DatatypeType>& resolutions,
+void Datatype::resolve(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(IllegalArgumentException, DatatypeResolutionException) {
-
- PrettyCheckArgument(em != NULL, em, "cannot resolve a Datatype with a NULL expression manager");
- PrettyCheckArgument(!d_resolved, this, "cannot resolve a Datatype twice");
- PrettyCheckArgument(resolutions.find(d_name) != resolutions.end(), resolutions,
- "Datatype::resolve(): resolutions doesn't contain me!");
+ const std::vector<SortConstructorType>& paramTypes,
+ const std::vector<DatatypeType>& paramReplacements)
+{
+ PrettyCheckArgument(!isResolved(), this, "cannot resolve a Datatype twice");
+ PrettyCheckArgument(resolutions.find(getName()) != resolutions.end(),
+ resolutions,
+ "Datatype::resolve(): resolutions doesn't contain me!");
PrettyCheckArgument(placeholders.size() == replacements.size(), placeholders,
"placeholders and replacements must be the same size");
PrettyCheckArgument(paramTypes.size() == paramReplacements.size(), paramTypes,
"paramTypes and paramReplacements must be the same size");
PrettyCheckArgument(getNumConstructors() > 0, *this, "cannot resolve a Datatype that has no constructors");
- DatatypeType self = (*resolutions.find(d_name)).second;
- PrettyCheckArgument(&self.getDatatype() == this, resolutions, "Datatype::resolve(): resolutions doesn't contain me!");
- d_resolved = true;
- size_t index = 0;
- for(std::vector<DatatypeConstructor>::iterator i = d_constructors.begin(), i_end = d_constructors.end(); i != i_end; ++i) {
- (*i).resolve(em, self, resolutions, placeholders, replacements, paramTypes, paramReplacements, index);
- Node::fromExpr((*i).d_constructor).setAttribute(DatatypeIndexAttr(), index);
- Node::fromExpr((*i).d_tester).setAttribute(DatatypeIndexAttr(), index++);
- }
- d_self = self;
- d_involvesExt = false;
- d_involvesUt = false;
- for(const_iterator i = begin(); i != end(); ++i) {
- if( (*i).involvesExternalType() ){
- d_involvesExt = true;
- }
- if( (*i).involvesUninterpretedType() ){
- d_involvesUt = true;
+ // we're using some internals, so we have to make sure that the Datatype's
+ // ExprManager is active
+ ExprManagerScope ems(*d_em);
+
+ Trace("datatypes") << "Datatype::resolve: " << getName()
+ << ", #placeholders=" << placeholders.size() << std::endl;
+
+ std::map<std::string, TypeNode> resolutionsn;
+ std::vector<TypeNode> placeholdersn;
+ std::vector<TypeNode> replacementsn;
+ std::vector<TypeNode> paramTypesn;
+ std::vector<TypeNode> paramReplacementsn;
+ for (const std::pair<const std::string, DatatypeType>& r : resolutions)
+ {
+ resolutionsn[r.first] = TypeNode::fromType(r.second);
+ }
+ for (const Type& t : placeholders)
+ {
+ placeholdersn.push_back(TypeNode::fromType(t));
+ }
+ for (const Type& t : replacements)
+ {
+ replacementsn.push_back(TypeNode::fromType(t));
+ }
+ for (const Type& t : paramTypes)
+ {
+ paramTypesn.push_back(TypeNode::fromType(t));
+ }
+ for (const Type& t : paramReplacements)
+ {
+ paramReplacementsn.push_back(TypeNode::fromType(t));
+ }
+ bool res = d_internal->resolve(resolutionsn,
+ placeholdersn,
+ replacementsn,
+ paramTypesn,
+ paramReplacementsn);
+ if (!res)
+ {
+ IllegalArgument(*this,
+ "could not resolve datatype that is not well formed");
+ }
+ Trace("dt-debug") << "Datatype::resolve: finished " << getName() << " "
+ << d_constructors.size() << std::endl;
+ AlwaysAssert(isResolved());
+ //
+ d_self = d_internal->getTypeNode().toType();
+ for (DatatypeConstructor& c : d_constructors)
+ {
+ AlwaysAssert(c.isResolved());
+ c.d_constructor = c.d_internal->getConstructor().toExpr();
+ for (size_t i = 0, nargs = c.getNumArgs(); i < nargs; i++)
+ {
+ AlwaysAssert(c.d_args[i].isResolved());
+ c.d_args[i].d_selector = c.d_args[i].d_internal->getSelector().toExpr();
}
}
}
d_record = new Record(fields);
}
-
- //make the sygus evaluation function
- if( isSygus() ){
- PrettyCheckArgument(d_params.empty(), this, "sygus types cannot be parametric");
- NodeManager* nm = NodeManager::fromExprManager(em);
- std::string name = "eval_" + getName();
- std::vector<TypeNode> evalType;
- evalType.push_back(TypeNode::fromType(d_self));
- if( !d_sygus_bvl.isNull() ){
- for(size_t j = 0; j < d_sygus_bvl.getNumChildren(); ++j) {
- evalType.push_back(TypeNode::fromType(d_sygus_bvl[j].getType()));
- }
- }
- evalType.push_back(TypeNode::fromType(d_sygus_type));
- TypeNode eval_func_type = nm->mkFunctionType(evalType);
- d_sygus_eval = nm->mkSkolem(name, eval_func_type, "sygus evaluation function").toExpr();
- }
}
void Datatype::addConstructor(const DatatypeConstructor& c) {
- PrettyCheckArgument(!d_resolved, this,
- "cannot add a constructor to a finalized Datatype");
+ Trace("dt-debug") << "Datatype::addConstructor" << std::endl;
+ PrettyCheckArgument(
+ !isResolved(), this, "cannot add a constructor to a finalized Datatype");
d_constructors.push_back(c);
+ d_internal->addConstructor(c.d_internal);
+ Trace("dt-debug") << "Datatype::addConstructor: finished" << std::endl;
}
void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){
- PrettyCheckArgument(!d_resolved, this,
- "cannot set sygus type to a finalized Datatype");
- d_sygus_type = st;
- d_sygus_bvl = bvl;
- d_sygus_allow_const = allow_const || allow_all;
- d_sygus_allow_all = allow_all;
+ PrettyCheckArgument(
+ !isResolved(), this, "cannot set sygus type to a finalized Datatype");
+ TypeNode stn = TypeNode::fromType(st);
+ Node bvln = Node::fromExpr(bvl);
+ d_internal->setSygus(stn, bvln, allow_const, allow_all);
+}
+
+void Datatype::addSygusConstructor(Expr op,
+ const std::string& cname,
+ const std::vector<Type>& cargs,
+ std::shared_ptr<SygusPrintCallback> spc,
+ int weight)
+{
+ // avoid name clashes
+ std::stringstream ss;
+ ss << getName() << "_" << getNumConstructors() << "_" << cname;
+ std::string name = ss.str();
+ std::string testerId("is-");
+ testerId.append(name);
+ unsigned cweight = weight >= 0 ? weight : (cargs.empty() ? 0 : 1);
+ DatatypeConstructor c(name, testerId, cweight);
+ c.setSygus(op, spc);
+ for( unsigned j=0; j<cargs.size(); j++ ){
+ Debug("parser-sygus-debug") << " arg " << j << " : " << cargs[j] << std::endl;
+ std::stringstream sname;
+ sname << name << "_" << j;
+ c.addArg(sname.str(), cargs[j]);
+ }
+ addConstructor(c);
+}
+
+void Datatype::addSygusConstructor(Kind k,
+ const std::string& cname,
+ const std::vector<Type>& cargs,
+ std::shared_ptr<SygusPrintCallback> spc,
+ int weight)
+{
+ ExprManagerScope ems(*d_em);
+ Expr op = d_em->operatorOf(k);
+ addSygusConstructor(op, cname, cargs, spc, weight);
}
void Datatype::setTuple() {
- PrettyCheckArgument(!d_resolved, this, "cannot set tuple to a finalized Datatype");
- d_isTuple = true;
+ PrettyCheckArgument(
+ !isResolved(), this, "cannot set tuple to a finalized Datatype");
+ d_internal->setTuple();
}
void Datatype::setRecord() {
- PrettyCheckArgument(!d_resolved, this, "cannot set record to a finalized Datatype");
+ PrettyCheckArgument(
+ !isResolved(), this, "cannot set record to a finalized Datatype");
d_isRecord = true;
}
-Cardinality Datatype::getCardinality( Type t ) const throw(IllegalArgumentException) {
+Cardinality Datatype::getCardinality(Type t) const
+{
PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
- Assert( t.isDatatype() && ((DatatypeType)t).getDatatype()==*this );
- std::vector< Type > processing;
- computeCardinality( t, processing );
- return d_card;
+ Assert(t.isDatatype() && ((DatatypeType)t).getDatatype() == *this);
+ ExprManagerScope ems(d_self);
+ TypeNode tn = TypeNode::fromType(t);
+ return d_internal->getCardinality(tn);
}
-Cardinality Datatype::getCardinality() const throw(IllegalArgumentException) {
+Cardinality Datatype::getCardinality() const
+{
PrettyCheckArgument(!isParametric(), this, "for getCardinality, this datatype cannot be parametric");
- return getCardinality( d_self );
-}
-
-Cardinality Datatype::computeCardinality( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException){
- PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
- if( std::find( processing.begin(), processing.end(), d_self )!=processing.end() ){
- d_card = Cardinality::INTEGERS;
- }else{
- processing.push_back( d_self );
- Cardinality c = 0;
- for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
- c += (*i).computeCardinality( t, processing );
- }
- d_card = c;
- processing.pop_back();
- }
- return d_card;
+ ExprManagerScope ems(d_self);
+ return d_internal->getCardinality();
}
-bool Datatype::isRecursiveSingleton( Type t ) const throw(IllegalArgumentException) {
+bool Datatype::isRecursiveSingleton(Type t) const
+{
PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
- Assert( t.isDatatype() && ((DatatypeType)t).getDatatype()==*this );
- if( d_card_rec_singleton.find( t )==d_card_rec_singleton.end() ){
- if( isCodatatype() ){
- Assert( d_card_u_assume[t].empty() );
- std::vector< Type > processing;
- if( computeCardinalityRecSingleton( t, processing, d_card_u_assume[t] ) ){
- d_card_rec_singleton[t] = 1;
- }else{
- d_card_rec_singleton[t] = -1;
- }
- if( d_card_rec_singleton[t]==1 ){
- Trace("dt-card") << "Datatype " << getName() << " is recursive singleton, dependent upon " << d_card_u_assume[t].size() << " uninterpreted sorts: " << std::endl;
- for( unsigned i=0; i<d_card_u_assume[t].size(); i++ ){
- Trace("dt-card") << " " << d_card_u_assume[t][i] << std::endl;
- }
- Trace("dt-card") << std::endl;
- }
- }else{
- d_card_rec_singleton[t] = -1;
- }
- }
- return d_card_rec_singleton[t]==1;
+ Assert(t.isDatatype() && ((DatatypeType)t).getDatatype() == *this);
+ ExprManagerScope ems(d_self);
+ TypeNode tn = TypeNode::fromType(t);
+ return d_internal->isRecursiveSingleton(tn);
}
-bool Datatype::isRecursiveSingleton() const throw(IllegalArgumentException) {
+bool Datatype::isRecursiveSingleton() const
+{
PrettyCheckArgument(!isParametric(), this, "for isRecursiveSingleton, this datatype cannot be parametric");
- return isRecursiveSingleton( d_self );
+ ExprManagerScope ems(d_self);
+ return d_internal->isRecursiveSingleton();
}
-unsigned Datatype::getNumRecursiveSingletonArgTypes( Type t ) const throw(IllegalArgumentException) {
- Assert( d_card_rec_singleton.find( t )!=d_card_rec_singleton.end() );
- Assert( isRecursiveSingleton( t ) );
- return d_card_u_assume[t].size();
+unsigned Datatype::getNumRecursiveSingletonArgTypes(Type t) const
+{
+ Assert(isRecursiveSingleton(t));
+ ExprManagerScope ems(d_self);
+ TypeNode tn = TypeNode::fromType(t);
+ return d_internal->getNumRecursiveSingletonArgTypes(tn);
}
-unsigned Datatype::getNumRecursiveSingletonArgTypes() const throw(IllegalArgumentException) {
+unsigned Datatype::getNumRecursiveSingletonArgTypes() const
+{
PrettyCheckArgument(!isParametric(), this, "for getNumRecursiveSingletonArgTypes, this datatype cannot be parametric");
- return getNumRecursiveSingletonArgTypes( d_self );
+ ExprManagerScope ems(d_self);
+ return d_internal->getNumRecursiveSingletonArgTypes();
}
-Type Datatype::getRecursiveSingletonArgType( Type t, unsigned i ) const throw(IllegalArgumentException) {
- Assert( d_card_rec_singleton.find( t )!=d_card_rec_singleton.end() );
- Assert( isRecursiveSingleton( t ) );
- return d_card_u_assume[t][i];
+Type Datatype::getRecursiveSingletonArgType(Type t, unsigned i) const
+{
+ Assert(isRecursiveSingleton(t));
+ ExprManagerScope ems(d_self);
+ TypeNode tn = TypeNode::fromType(t);
+ return d_internal->getRecursiveSingletonArgType(tn, i).toType();
}
-Type Datatype::getRecursiveSingletonArgType( unsigned i ) const throw(IllegalArgumentException) {
+Type Datatype::getRecursiveSingletonArgType(unsigned i) const
+{
PrettyCheckArgument(!isParametric(), this, "for getRecursiveSingletonArgType, this datatype cannot be parametric");
- return getRecursiveSingletonArgType( d_self, i );
-}
-
-bool Datatype::computeCardinalityRecSingleton( Type t, std::vector< Type >& processing, std::vector< Type >& u_assume ) const throw(IllegalArgumentException){
- if( std::find( processing.begin(), processing.end(), d_self )!=processing.end() ){
- return true;
- }else{
- if( d_card_rec_singleton[t]==0 ){
- //if not yet computed
- if( d_constructors.size()==1 ){
- bool success = false;
- processing.push_back( d_self );
- for(unsigned i = 0; i<d_constructors[0].getNumArgs(); i++ ) {
- Type tc = ((SelectorType)d_constructors[0][i].getType()).getRangeType();
- //if it is an uninterpreted sort, then we depend on it having cardinality one
- if( tc.isSort() ){
- if( std::find( u_assume.begin(), u_assume.end(), tc )==u_assume.end() ){
- u_assume.push_back( tc );
- }
- //if it is a datatype, recurse
- }else if( tc.isDatatype() ){
- const Datatype & dt = ((DatatypeType)tc).getDatatype();
- if( !dt.computeCardinalityRecSingleton( t, processing, u_assume ) ){
- return false;
- }else{
- success = true;
- }
- //if it is a builtin type, it must have cardinality one
- }else if( !tc.getCardinality().isOne() ){
- return false;
- }
- }
- processing.pop_back();
- return success;
- }else{
- return false;
- }
- }else if( d_card_rec_singleton[t]==-1 ){
- return false;
- }else{
- for( unsigned i=0; i<d_card_u_assume[t].size(); i++ ){
- if( std::find( u_assume.begin(), u_assume.end(), d_card_u_assume[t][i] )==u_assume.end() ){
- u_assume.push_back( d_card_u_assume[t][i] );
- }
- }
- return true;
- }
- }
+ ExprManagerScope ems(d_self);
+ return d_internal->getRecursiveSingletonArgType(i).toType();
}
-bool Datatype::isFinite( Type t ) const throw(IllegalArgumentException) {
+bool Datatype::isFinite(Type t) const
+{
PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
- Assert( t.isDatatype() && ((DatatypeType)t).getDatatype()==*this );
-
- // we're using some internals, so we have to set up this library context
+ Assert(t.isDatatype() && ((DatatypeType)t).getDatatype() == *this);
ExprManagerScope ems(d_self);
- TypeNode self = TypeNode::fromType(d_self);
- // is this already in the cache ?
- if(self.getAttribute(DatatypeFiniteComputedAttr())) {
- return self.getAttribute(DatatypeFiniteAttr());
- }
- for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
- if(! (*i).isFinite( t )) {
- self.setAttribute(DatatypeFiniteComputedAttr(), true);
- self.setAttribute(DatatypeFiniteAttr(), false);
- return false;
- }
- }
- self.setAttribute(DatatypeFiniteComputedAttr(), true);
- self.setAttribute(DatatypeFiniteAttr(), true);
- return true;
+ TypeNode tn = TypeNode::fromType(t);
+ return d_internal->isFinite(tn);
}
-bool Datatype::isFinite() const throw(IllegalArgumentException) {
+bool Datatype::isFinite() const
+{
PrettyCheckArgument(isResolved() && !isParametric(), this, "this datatype must be resolved and not parametric");
- return isFinite( d_self );
+ ExprManagerScope ems(d_self);
+ return d_internal->isFinite();
}
-bool Datatype::isInterpretedFinite( Type t ) const throw(IllegalArgumentException) {
+bool Datatype::isInterpretedFinite(Type t) const
+{
PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
- Assert( t.isDatatype() && ((DatatypeType)t).getDatatype()==*this );
- // we're using some internals, so we have to set up this library context
+ Assert(t.isDatatype() && ((DatatypeType)t).getDatatype() == *this);
ExprManagerScope ems(d_self);
- TypeNode self = TypeNode::fromType(d_self);
- // is this already in the cache ?
- if(self.getAttribute(DatatypeUFiniteComputedAttr())) {
- return self.getAttribute(DatatypeUFiniteAttr());
- }
- //start by assuming it is not
- self.setAttribute(DatatypeUFiniteComputedAttr(), true);
- self.setAttribute(DatatypeUFiniteAttr(), false);
- for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
- if(! (*i).isInterpretedFinite( t )) {
- return false;
- }
- }
- self.setAttribute(DatatypeUFiniteComputedAttr(), true);
- self.setAttribute(DatatypeUFiniteAttr(), true);
- return true;
+ TypeNode tn = TypeNode::fromType(t);
+ return d_internal->isInterpretedFinite(tn);
}
-bool Datatype::isInterpretedFinite() const throw(IllegalArgumentException) {
+bool Datatype::isInterpretedFinite() const
+{
PrettyCheckArgument(isResolved() && !isParametric(), this, "this datatype must be resolved and not parametric");
- return isInterpretedFinite( d_self );
+ ExprManagerScope ems(d_self);
+ return d_internal->isInterpretedFinite();
}
-bool Datatype::isWellFounded() const throw(IllegalArgumentException) {
- PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
- if( d_well_founded==0 ){
- // we're using some internals, so we have to set up this library context
- ExprManagerScope ems(d_self);
- std::vector< Type > processing;
- if( computeWellFounded( processing ) ){
- d_well_founded = 1;
- }else{
- d_well_founded = -1;
- }
- }
- return d_well_founded==1;
+bool Datatype::isWellFounded() const
+{
+ ExprManagerScope ems(d_self);
+ return d_internal->isWellFounded();
}
-bool Datatype::computeWellFounded( std::vector< Type >& processing ) const throw(IllegalArgumentException) {
+Expr Datatype::mkGroundTerm(Type t) const
+{
PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
- if( std::find( processing.begin(), processing.end(), d_self )!=processing.end() ){
- return d_isCo;
- }else{
- processing.push_back( d_self );
- for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
- if( (*i).computeWellFounded( processing ) ){
- processing.pop_back();
- return true;
- }else{
- Trace("dt-wf") << "Constructor " << (*i).getName() << " is not well-founded." << std::endl;
- }
- }
- processing.pop_back();
- Trace("dt-wf") << "Datatype " << getName() << " is not well-founded." << std::endl;
- return false;
- }
+ ExprManagerScope ems(d_self);
+ TypeNode tn = TypeNode::fromType(t);
+ Node gterm = d_internal->mkGroundTerm(tn);
+ PrettyCheckArgument(
+ !gterm.isNull(),
+ this,
+ "datatype is not well-founded, cannot construct a ground term!");
+ return gterm.toExpr();
}
-Expr Datatype::mkGroundTerm( Type t ) const throw(IllegalArgumentException) {
+Expr Datatype::mkGroundValue(Type t) const
+{
PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
ExprManagerScope ems(d_self);
- Debug("datatypes") << "mkGroundTerm of type " << t << std::endl;
- // is this already in the cache ?
- std::map< Type, Expr >::iterator it = d_ground_term.find( t );
- if( it != d_ground_term.end() ){
- Debug("datatypes") << "\nin cache: " << d_self << " => " << it->second << std::endl;
- return it->second;
- } else {
- std::vector< Type > processing;
- Expr groundTerm = computeGroundTerm( t, processing );
- if(!groundTerm.isNull() ) {
- // we found a ground-term-constructing constructor!
- d_ground_term[t] = groundTerm;
- Debug("datatypes") << "constructed: " << getName() << " => " << groundTerm << std::endl;
- }
- if( groundTerm.isNull() ){
- if( !d_isCo ){
- // if we get all the way here, we aren't well-founded
- IllegalArgument(*this, "datatype is not well-founded, cannot construct a ground term!");
- }else{
- return groundTerm;
- }
- }else{
- return groundTerm;
- }
- }
+ TypeNode tn = TypeNode::fromType(t);
+ Node gvalue = d_internal->mkGroundValue(tn);
+ PrettyCheckArgument(
+ !gvalue.isNull(),
+ this,
+ "datatype is not well-founded, cannot construct a ground value!");
+ return gvalue.toExpr();
}
-Expr getSubtermWithType( Expr e, Type t, bool isTop ){
- if( !isTop && e.getType()==t ){
- return e;
- }else{
- for( unsigned i=0; i<e.getNumChildren(); i++ ){
- Expr se = getSubtermWithType( e[i], t, false );
- if( !se.isNull() ){
- return se;
- }
- }
- return Expr();
- }
-}
-
-Expr Datatype::computeGroundTerm( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException) {
- if( std::find( processing.begin(), processing.end(), t )==processing.end() ){
- processing.push_back( t );
- for( unsigned r=0; r<2; r++ ){
- for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
- //do nullary constructors first
- if( ((*i).getNumArgs()==0)==(r==0)){
- Debug("datatypes") << "Try constructing for " << (*i).getName() << ", processing = " << processing.size() << std::endl;
- Expr e = (*i).computeGroundTerm( t, processing, d_ground_term );
- if( !e.isNull() ){
- //must check subterms for the same type to avoid infinite loops in type enumeration
- Expr se = getSubtermWithType( e, t, true );
- if( !se.isNull() ){
- Debug("datatypes") << "Take subterm " << se << std::endl;
- e = se;
- }
- processing.pop_back();
- return e;
- }else{
- Debug("datatypes") << "...failed." << std::endl;
- }
- }
- }
- }
- processing.pop_back();
- }else{
- Debug("datatypes") << "...already processing " << t << " " << d_self << std::endl;
- }
- return Expr();
-}
-
-DatatypeType Datatype::getDatatypeType() const throw(IllegalArgumentException) {
+DatatypeType Datatype::getDatatypeType() const
+{
PrettyCheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType");
- PrettyCheckArgument(!d_self.isNull(), *this);
- return DatatypeType(d_self);
+ ExprManagerScope ems(d_self);
+ Type self = d_internal->getTypeNode().toType();
+ PrettyCheckArgument(!self.isNull(), *this);
+ return DatatypeType(self);
}
-DatatypeType Datatype::getDatatypeType(const std::vector<Type>& params)
- const throw(IllegalArgumentException) {
+DatatypeType Datatype::getDatatypeType(const std::vector<Type>& params) const
+{
PrettyCheckArgument(isResolved(), *this, "Datatype must be resolved to get its DatatypeType");
- PrettyCheckArgument(!d_self.isNull() && DatatypeType(d_self).isParametric(), this);
- return DatatypeType(d_self).instantiate(params);
+ ExprManagerScope ems(d_self);
+ Type self = d_internal->getTypeNode().toType();
+ PrettyCheckArgument(!self.isNull() && DatatypeType(self).isParametric(),
+ this);
+ return DatatypeType(self).instantiate(params);
}
-bool Datatype::operator==(const Datatype& other) const throw() {
+bool Datatype::operator==(const Datatype& other) const
+{
// two datatypes are == iff the name is the same and they have
// exactly matching constructors (in the same order)
if(this == &other) {
return true;
}
-
- if(isResolved() != other.isResolved()) {
- return false;
- }
-
- if( d_name != other.d_name ||
- getNumConstructors() != other.getNumConstructors() ) {
- return false;
- }
- for(const_iterator i = begin(), j = other.begin(); i != end(); ++i, ++j) {
- Assert(j != other.end());
- // two constructors are == iff they have the same name, their
- // constructors and testers are equal and they have exactly
- // matching args (in the same order)
- if((*i).getName() != (*j).getName() ||
- (*i).getNumArgs() != (*j).getNumArgs()) {
- return false;
- }
- // testing equivalence of constructors and testers is harder b/c
- // this constructor might not be resolved yet; only compare them
- // if they are both resolved
- Assert(isResolved() == !(*i).d_constructor.isNull() &&
- isResolved() == !(*i).d_tester.isNull() &&
- (*i).d_constructor.isNull() == (*j).d_constructor.isNull() &&
- (*i).d_tester.isNull() == (*j).d_tester.isNull());
- if(!(*i).d_constructor.isNull() && (*i).d_constructor != (*j).d_constructor) {
- return false;
- }
- if(!(*i).d_tester.isNull() && (*i).d_tester != (*j).d_tester) {
- return false;
- }
- 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;
- }
- // testing equivalence of selectors is harder b/c args might not
- // be resolved yet
- Assert(isResolved() == (*k).isResolved() &&
- (*k).isResolved() == (*l).isResolved());
- if((*k).isResolved()) {
- // both are resolved, so simply compare the selectors directly
- if((*k).d_selector != (*l).d_selector) {
- return false;
- }
- } else {
- // neither is resolved, so compare their (possibly unresolved)
- // types; we don't know if they'll be resolved the same way,
- // so we can't ever say unresolved types are equal
- if(!(*k).d_selector.isNull() && !(*l).d_selector.isNull()) {
- if((*k).d_selector.getType() != (*l).d_selector.getType()) {
- return false;
- }
- } else {
- if((*k).isUnresolvedSelf() && (*l).isUnresolvedSelf()) {
- // Fine, the selectors are equal if the rest of the
- // enclosing datatypes are equal...
- } else {
- return false;
- }
- }
- }
- }
- }
return true;
}
return *i;
}
}
- IllegalArgument(name, "No such constructor `%s' of datatype `%s'", name.c_str(), d_name.c_str());
+ std::string dname = getName();
+ IllegalArgument(name,
+ "No such constructor `%s' of datatype `%s'",
+ name.c_str(),
+ dname.c_str());
}
Expr Datatype::getConstructor(std::string name) const {
}
Type Datatype::getSygusType() const {
- return d_sygus_type;
+ return d_internal->getSygusType().toType();
}
Expr Datatype::getSygusVarList() const {
- return d_sygus_bvl;
+ return d_internal->getSygusVarList().toExpr();
}
bool Datatype::getSygusAllowConst() const {
- return d_sygus_allow_const;
+ return d_internal->getSygusAllowConst();
}
bool Datatype::getSygusAllowAll() const {
- return d_sygus_allow_all;
-}
-
-Expr Datatype::getSygusEvaluationFunc() const {
- return d_sygus_eval;
+ return d_internal->getSygusAllowAll();
}
bool Datatype::involvesExternalType() const{
- return d_involvesExt;
+ return d_internal->involvesExternalType();
}
bool Datatype::involvesUninterpretedType() const{
- return d_involvesUt;
+ return d_internal->involvesUninterpretedType();
}
-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, size_t cindex)
- throw(IllegalArgumentException, DatatypeResolutionException) {
-
- PrettyCheckArgument(em != NULL, em, "cannot resolve a Datatype with a NULL expression manager");
- PrettyCheckArgument(!isResolved(),
- "cannot resolve a Datatype constructor twice; "
- "perhaps the same constructor was added twice, "
- "or to two datatypes?");
-
- // we're using some internals, so we have to set up this library context
- ExprManagerScope ems(*em);
-
- NodeManager* nm = NodeManager::fromExprManager(em);
- TypeNode selfTypeNode = TypeNode::fromType(self);
- size_t index = 0;
- for(std::vector<DatatypeConstructorArg>::iterator i = d_args.begin(), i_end = d_args.end(); i != i_end; ++i) {
- if((*i).d_selector.isNull()) {
- // the unresolved type wasn't created here; do name resolution
- string typeName = (*i).d_name.substr((*i).d_name.find('\0') + 1);
- (*i).d_name.resize((*i).d_name.find('\0'));
- if(typeName == "") {
- (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, selfTypeNode), "is a selector", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
- } else {
- map<string, DatatypeType>::const_iterator j = resolutions.find(typeName);
- if(j == resolutions.end()) {
- stringstream msg;
- msg << "cannot resolve type \"" << typeName << "\" "
- << "in selector \"" << (*i).d_name << "\" "
- << "of constructor \"" << d_name << "\"";
- throw DatatypeResolutionException(msg.str());
- } else {
- (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, TypeNode::fromType((*j).second)), "is a selector", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
- }
- }
- } else {
- // the type for the selector already exists; may need
- // complex-type substitution
- Type range = (*i).d_selector.getType();
- if(!placeholders.empty()) {
- range = range.substitute(placeholders, replacements);
- }
- if(!paramTypes.empty() ) {
- range = doParametricSubstitution( range, paramTypes, paramReplacements );
- }
- (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, TypeNode::fromType(range)), "is a selector", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
- }
- Node::fromExpr((*i).d_selector).setAttribute(DatatypeConsIndexAttr(), cindex);
- Node::fromExpr((*i).d_selector).setAttribute(DatatypeIndexAttr(), index++);
- (*i).d_resolved = true;
- }
-
- Assert(index == getNumArgs());
-
- // 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
- // should get the results of any resolutions we did above.
- d_tester = nm->mkSkolem(getTesterName(), nm->mkTesterType(selfTypeNode), "is a tester", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
- d_constructor = nm->mkSkolem(getName(), nm->mkConstructorType(*this, selfTypeNode), "is a constructor", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
- // associate constructor with all selectors
- for(std::vector<DatatypeConstructorArg>::iterator i = d_args.begin(), i_end = d_args.end(); i != i_end; ++i) {
- (*i).d_constructor = d_constructor;
- }
+const std::vector<DatatypeConstructor>* Datatype::getConstructors() const
+{
+ return &d_constructors;
}
-Type DatatypeConstructor::doParametricSubstitution( Type range,
- const std::vector< SortConstructorType >& paramTypes,
- const std::vector< DatatypeType >& paramReplacements ) {
- TypeNode typn = TypeNode::fromType( range );
- if(typn.getNumChildren() == 0) {
- return range;
- } else {
- std::vector< Type > origChildren;
- std::vector< Type > children;
- for(TypeNode::const_iterator i = typn.begin(), iend = typn.end();i != iend; ++i) {
- origChildren.push_back( (*i).toType() );
- children.push_back( doParametricSubstitution( (*i).toType(), paramTypes, paramReplacements ) );
- }
- for( unsigned i = 0; i < paramTypes.size(); ++i ) {
- if( paramTypes[i].getArity() == origChildren.size() ) {
- Type tn = paramTypes[i].instantiate( origChildren );
- if( range == tn ) {
- return paramReplacements[i].instantiate( children );
- }
- }
- }
- NodeBuilder<> nb(typn.getKind());
- for( unsigned i = 0; i < children.size(); ++i ) {
- nb << TypeNode::fromType( children[i] );
- }
- return nb.constructTypeNode().toType();
- }
-}
-
-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
- // resolution.
- d_name(name + '\0' + "is_" + name), // default tester name is "is_FOO"
- d_tester(),
- d_args() {
+DatatypeConstructor::DatatypeConstructor(std::string name)
+ : d_internal(nullptr),
+ d_testerName("is_" + name) // default tester name is "is_FOO"
+{
PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
+ d_internal = std::make_shared<DTypeConstructor>(name, 1);
}
-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
- // resolution.
- d_name(name + '\0' + tester),
- d_tester(),
- d_args() {
+DatatypeConstructor::DatatypeConstructor(std::string name,
+ std::string tester,
+ unsigned weight)
+ : d_internal(nullptr), d_testerName(tester)
+{
PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor without a name");
PrettyCheckArgument(!tester.empty(), tester, "cannot construct a datatype constructor without a tester");
+ d_internal = std::make_shared<DTypeConstructor>(name, weight);
+}
+
+void DatatypeConstructor::setSygus(Expr op,
+ std::shared_ptr<SygusPrintCallback> spc)
+{
+ PrettyCheckArgument(
+ !isResolved(), this, "cannot modify a finalized Datatype constructor");
+ Node opn = Node::fromExpr(op);
+ d_internal->setSygus(op);
+ // print callback lives at the expression level currently
+ d_sygus_pc = spc;
}
-void DatatypeConstructor::setSygus( Expr op, Expr let_body, std::vector< Expr >& let_args, unsigned num_let_input_args ){
- d_sygus_op = op;
- d_sygus_let_body = let_body;
- d_sygus_let_args.insert( d_sygus_let_args.end(), let_args.begin(), let_args.end() );
- d_sygus_num_let_input_args = num_let_input_args;
+const std::vector<DatatypeConstructorArg>* DatatypeConstructor::getArgs()
+ const
+{
+ return &d_args;
}
void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) {
Expr type = NodeManager::currentNM()->mkSkolem("unresolved_" + selectorName, TypeNode::fromType(selectorType), "is an unresolved selector type placeholder", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
Debug("datatypes") << type << endl;
d_args.push_back(DatatypeConstructorArg(selectorName, type));
+ d_internal->addArg(d_args.back().d_internal);
}
void DatatypeConstructor::addArg(std::string selectorName, DatatypeUnresolvedType selectorType) {
PrettyCheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor");
PrettyCheckArgument(selectorType.getName() != "", selectorType, "cannot add a null selector type");
d_args.push_back(DatatypeConstructorArg(selectorName + '\0' + selectorType.getName(), Expr()));
+ d_internal->addArg(d_args.back().d_internal);
}
void DatatypeConstructor::addArg(std::string selectorName, DatatypeSelfType) {
// proper selector type)
PrettyCheckArgument(!isResolved(), this, "cannot modify a finalized Datatype constructor");
d_args.push_back(DatatypeConstructorArg(selectorName + '\0', Expr()));
+ d_internal->addArg(d_args.back().d_internal);
}
-std::string DatatypeConstructor::getName() const throw() {
- return d_name.substr(0, d_name.find('\0'));
+std::string DatatypeConstructor::getName() const
+{
+ return d_internal->getName();
}
-std::string DatatypeConstructor::getTesterName() const throw() {
- return d_name.substr(d_name.find('\0') + 1);
+std::string DatatypeConstructor::getTesterName() const
+{
+ // not stored internally, since tester names only pertain to parsing
+ return d_testerName;
}
Expr DatatypeConstructor::getConstructor() const {
Type DatatypeConstructor::getSpecializedConstructorType(Type returnType) const {
PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+ PrettyCheckArgument(returnType.isDatatype(), this, "cannot get specialized constructor type for non-datatype type");
ExprManagerScope ems(d_constructor);
- const Datatype& dt = Datatype::datatypeOf(d_constructor);
- PrettyCheckArgument(dt.isParametric(), this, "this datatype constructor is not parametric");
- DatatypeType dtt = dt.getDatatypeType();
- Matcher m(dtt);
- m.doMatching( TypeNode::fromType(dtt), TypeNode::fromType(returnType) );
- vector<Type> subst;
- m.getMatches(subst);
- vector<Type> params = dt.getParameters();
- return d_constructor.getType().substitute(params, subst);
+ TypeNode tn = TypeNode::fromType(returnType);
+ return d_internal->getSpecializedConstructorType(tn).toType();
}
Expr DatatypeConstructor::getTester() const {
PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
- return d_tester;
+ ExprManagerScope ems(d_constructor);
+ return d_internal->getTester().toExpr();
}
Expr DatatypeConstructor::getSygusOp() const {
PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
- return d_sygus_op;
-}
-
-Expr DatatypeConstructor::getSygusLetBody() const {
- PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
- return d_sygus_let_body;
-}
-
-unsigned DatatypeConstructor::getNumSygusLetArgs() const {
- PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
- return d_sygus_let_args.size();
-}
-
-Expr DatatypeConstructor::getSygusLetArg( unsigned i ) const {
- PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
- return d_sygus_let_args[i];
-}
-
-unsigned DatatypeConstructor::getNumSygusLetInputArgs() const {
- PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
- return d_sygus_num_let_input_args;
+ ExprManagerScope ems(d_constructor);
+ return d_internal->getSygusOp().toExpr();
}
bool DatatypeConstructor::isSygusIdFunc() const {
PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
- return d_sygus_let_args.size()==1 && d_sygus_let_args[0]==d_sygus_let_body;
+ ExprManagerScope ems(d_constructor);
+ return d_internal->isSygusIdFunc();
}
-Cardinality DatatypeConstructor::getCardinality( Type t ) const throw(IllegalArgumentException) {
- PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
-
- Cardinality c = 1;
-
- for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
- c *= SelectorType((*i).getSelector().getType()).getRangeType().getCardinality();
- }
-
- return c;
-}
-
-/** compute the cardinality of this datatype */
-Cardinality DatatypeConstructor::computeCardinality( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException){
- Cardinality c = 1;
- std::vector< Type > instTypes;
- std::vector< Type > paramTypes;
- if( DatatypeType(t).isParametric() ){
- paramTypes = DatatypeType(t).getDatatype().getParameters();
- instTypes = DatatypeType(t).getParamTypes();
- }
- for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
- Type tc = SelectorType((*i).getSelector().getType()).getRangeType();
- if( DatatypeType(t).isParametric() ){
- tc = tc.substitute( paramTypes, instTypes );
- }
- if( tc.isDatatype() ){
- const Datatype& dt = ((DatatypeType)tc).getDatatype();
- c *= dt.computeCardinality( t, processing );
- }else{
- c *= tc.getCardinality();
- }
- }
- return c;
+unsigned DatatypeConstructor::getWeight() const
+{
+ PrettyCheckArgument(
+ isResolved(), this, "this datatype constructor is not yet resolved");
+ ExprManagerScope ems(d_constructor);
+ return d_internal->getWeight();
}
-bool DatatypeConstructor::computeWellFounded( std::vector< Type >& processing ) const throw(IllegalArgumentException){
- for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
- Type t = SelectorType((*i).getSelector().getType()).getRangeType();
- if( t.isDatatype() ){
- const Datatype& dt = ((DatatypeType)t).getDatatype();
- if( !dt.computeWellFounded( processing ) ){
- return false;
- }
- }
- }
- return true;
+std::shared_ptr<SygusPrintCallback> DatatypeConstructor::getSygusPrintCallback() const
+{
+ PrettyCheckArgument(
+ isResolved(), this, "this datatype constructor is not yet resolved");
+ return d_sygus_pc;
}
-
-bool DatatypeConstructor::isFinite( Type t ) const throw(IllegalArgumentException) {
+Cardinality DatatypeConstructor::getCardinality(Type t) const
+{
PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
-
- // we're using some internals, so we have to set up this library context
ExprManagerScope ems(d_constructor);
- TNode self = Node::fromExpr(d_constructor);
- // is this already in the cache ?
- if(self.getAttribute(DatatypeFiniteComputedAttr())) {
- return self.getAttribute(DatatypeFiniteAttr());
- }
- std::vector< Type > instTypes;
- std::vector< Type > paramTypes;
- if( DatatypeType(t).isParametric() ){
- paramTypes = DatatypeType(t).getDatatype().getParameters();
- instTypes = DatatypeType(t).getParamTypes();
- }
- for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
- Type tc = (*i).getRangeType();
- if( DatatypeType(t).isParametric() ){
- tc = tc.substitute( paramTypes, instTypes );
- }
- if(! tc.getCardinality().isFinite()) {
- self.setAttribute(DatatypeFiniteComputedAttr(), true);
- self.setAttribute(DatatypeFiniteAttr(), false);
- return false;
- }
- }
- self.setAttribute(DatatypeFiniteComputedAttr(), true);
- self.setAttribute(DatatypeFiniteAttr(), true);
- return true;
+ TypeNode tn = TypeNode::fromType(t);
+ return d_internal->getCardinality(tn);
}
-bool DatatypeConstructor::isInterpretedFinite( Type t ) const throw(IllegalArgumentException) {
+bool DatatypeConstructor::isFinite(Type t) const
+{
PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
- // we're using some internals, so we have to set up this library context
ExprManagerScope ems(d_constructor);
- TNode self = Node::fromExpr(d_constructor);
- // is this already in the cache ?
- if(self.getAttribute(DatatypeUFiniteComputedAttr())) {
- return self.getAttribute(DatatypeUFiniteAttr());
- }
- std::vector< Type > instTypes;
- std::vector< Type > paramTypes;
- if( DatatypeType(t).isParametric() ){
- paramTypes = DatatypeType(t).getDatatype().getParameters();
- instTypes = DatatypeType(t).getParamTypes();
- }
- for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
- Type tc = (*i).getRangeType();
- if( DatatypeType(t).isParametric() ){
- tc = tc.substitute( paramTypes, instTypes );
- }
- TypeNode tcn = TypeNode::fromType( tc );
- if(!tcn.isInterpretedFinite()) {
- self.setAttribute(DatatypeUFiniteComputedAttr(), true);
- self.setAttribute(DatatypeUFiniteAttr(), false);
- return false;
- }
- }
- self.setAttribute(DatatypeUFiniteComputedAttr(), true);
- self.setAttribute(DatatypeUFiniteAttr(), true);
- return true;
+ TypeNode tn = TypeNode::fromType(t);
+ return d_internal->isFinite(tn);
}
-Expr DatatypeConstructor::computeGroundTerm( Type t, std::vector< Type >& processing, std::map< Type, Expr >& gt ) const throw(IllegalArgumentException) {
-// we're using some internals, so we have to set up this library context
+bool DatatypeConstructor::isInterpretedFinite(Type t) const
+{
+ PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
ExprManagerScope ems(d_constructor);
-
- std::vector<Expr> groundTerms;
- groundTerms.push_back(getConstructor());
-
- // for each selector, get a ground term
- std::vector< Type > instTypes;
- std::vector< Type > paramTypes;
- if( DatatypeType(t).isParametric() ){
- paramTypes = DatatypeType(t).getDatatype().getParameters();
- instTypes = DatatypeType(t).getParamTypes();
- }
- for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
- Type selType = SelectorType((*i).getSelector().getType()).getRangeType();
- if( DatatypeType(t).isParametric() ){
- selType = selType.substitute( paramTypes, instTypes );
- }
- Expr arg;
- if( selType.isDatatype() ){
- std::map< Type, Expr >::iterator itgt = gt.find( selType );
- if( itgt != gt.end() ){
- arg = itgt->second;
- }else{
- const Datatype & dt = DatatypeType(selType).getDatatype();
- arg = dt.computeGroundTerm( selType, processing );
- }
- }else{
- arg = selType.mkGroundTerm();
- }
- if( arg.isNull() ){
- Debug("datatypes") << "...unable to construct arg of " << (*i).getName() << std::endl;
- return Expr();
- }else{
- Debug("datatypes") << "...constructed arg " << arg.getType() << std::endl;
- groundTerms.push_back(arg);
- }
- }
-
- Expr groundTerm = getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, groundTerms);
- if( groundTerm.getType()!=t ){
- Assert( Datatype::datatypeOf( d_constructor ).isParametric() );
- //type is ambiguous, must apply type ascription
- Debug("datatypes-gt") << "ambiguous type for " << groundTerm << ", ascribe to " << t << std::endl;
- groundTerms[0] = getConstructor().getExprManager()->mkExpr(kind::APPLY_TYPE_ASCRIPTION,
- getConstructor().getExprManager()->mkConst(AscriptionType(getSpecializedConstructorType(t))),
- groundTerms[0]);
- groundTerm = getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, groundTerms);
- }
- return groundTerm;
+ TypeNode tn = TypeNode::fromType(t);
+ return d_internal->isInterpretedFinite(tn);
}
-
const DatatypeConstructorArg& DatatypeConstructor::operator[](size_t index) const {
PrettyCheckArgument(index < getNumArgs(), index, "index out of bounds");
return d_args[index];
return *i;
}
}
- IllegalArgument(name, "No such arg `%s' of constructor `%s'", name.c_str(), d_name.c_str());
+ std::string dname = getName();
+ IllegalArgument(name,
+ "No such arg `%s' of constructor `%s'",
+ name.c_str(),
+ dname.c_str());
}
Expr DatatypeConstructor::getSelector(std::string name) const {
- return (*this)[name].getSelector();
+ return (*this)[name].d_selector;
+}
+
+Type DatatypeConstructor::getArgType(unsigned index) const
+{
+ PrettyCheckArgument(index < getNumArgs(), index, "index out of bounds");
+ ExprManagerScope ems(d_constructor);
+ return d_internal->getArgType(index).toType();
}
bool DatatypeConstructor::involvesExternalType() const{
- for(const_iterator i = begin(); i != end(); ++i) {
- if(! SelectorType((*i).getSelector().getType()).getRangeType().isDatatype()) {
- return true;
- }
- }
- return false;
+ ExprManagerScope ems(d_constructor);
+ return d_internal->involvesExternalType();
}
bool DatatypeConstructor::involvesUninterpretedType() const{
- for(const_iterator i = begin(); i != end(); ++i) {
- if(SelectorType((*i).getSelector().getType()).getRangeType().isSort()) {
- return true;
- }
- }
- return false;
+ ExprManagerScope ems(d_constructor);
+ return d_internal->involvesUninterpretedType();
}
-DatatypeConstructorArg::DatatypeConstructorArg(std::string name, Expr selector) :
- d_name(name),
- d_selector(selector),
- d_resolved(false) {
+DatatypeConstructorArg::DatatypeConstructorArg(std::string name, Expr selector)
+ : d_internal(nullptr)
+{
PrettyCheckArgument(name != "", name, "cannot construct a datatype constructor arg without a name");
+ d_internal = std::make_shared<DTypeSelector>(name, Node::fromExpr(selector));
}
-std::string DatatypeConstructorArg::getName() const throw() {
- string name = d_name;
+std::string DatatypeConstructorArg::getName() const
+{
+ string name = d_internal->getName();
const size_t nul = name.find('\0');
if(nul != string::npos) {
name.resize(nul);
return d_selector;
}
+Expr DatatypeConstructor::getSelectorInternal( Type domainType, size_t index ) const {
+ PrettyCheckArgument(isResolved(), this, "cannot get an internal selector for an unresolved datatype constructor");
+ PrettyCheckArgument(index < getNumArgs(), index, "index out of bounds");
+ ExprManagerScope ems(d_constructor);
+ TypeNode dtn = TypeNode::fromType(domainType);
+ return d_internal->getSelectorInternal(dtn, index).toExpr();
+}
+
+int DatatypeConstructor::getSelectorIndexInternal( Expr sel ) const {
+ PrettyCheckArgument(isResolved(), this, "cannot get an internal selector index for an unresolved datatype constructor");
+ ExprManagerScope ems(d_constructor);
+ Node seln = Node::fromExpr(sel);
+ return d_internal->getSelectorIndexInternal(seln);
+}
+
Expr DatatypeConstructorArg::getConstructor() const {
PrettyCheckArgument(isResolved(), this,
"cannot get a associated constructor for argument of an unresolved datatype constructor");
- return d_constructor;
+ ExprManagerScope ems(d_selector);
+ return d_internal->getConstructor().toExpr();
}
SelectorType DatatypeConstructorArg::getType() const {
- return getSelector().getType();
+ return d_selector.getType();
}
Type DatatypeConstructorArg::getRangeType() const {
return getType().getRangeType();
}
-bool DatatypeConstructorArg::isUnresolvedSelf() const throw() {
- return d_selector.isNull() && d_name.size() == d_name.find('\0') + 1;
+bool DatatypeConstructorArg::isUnresolvedSelf() const
+{
+ return d_selector.isNull();
}
-static const int s_printDatatypeNamesOnly = std::ios_base::xalloc();
-
-std::string DatatypeConstructorArg::getTypeName() const {
- Type t;
- if(isResolved()) {
- t = SelectorType(d_selector.getType()).getRangeType();
- } else {
- if(d_selector.isNull()) {
- string typeName = d_name.substr(d_name.find('\0') + 1);
- return (typeName == "") ? "[self]" : typeName;
- } else {
- t = d_selector.getType();
- }
- }
-
- // Unfortunately, in the case of complex selector types, we can
- // enter nontrivial recursion here. Make sure that doesn't happen.
- stringstream ss;
- ss << language::SetLanguage(language::output::LANG_CVC4);
- ss.iword(s_printDatatypeNamesOnly) = 1;
- t.toStream(ss);
- return ss.str();
-}
-
-std::ostream& operator<<(std::ostream& os, const Datatype& dt) {
- // These datatype things are recursive! Be very careful not to
- // print an infinite chain of them.
- long& printNameOnly = os.iword(s_printDatatypeNamesOnly);
- Debug("datatypes-output") << "printNameOnly is " << printNameOnly << std::endl;
- if(printNameOnly) {
- return os << dt.getName();
- }
-
- class Scope {
- long& d_ref;
- long d_oldValue;
- public:
- Scope(long& ref, long value) : d_ref(ref), d_oldValue(ref) { d_ref = value; }
- ~Scope() { d_ref = d_oldValue; }
- } scope(printNameOnly, 1);
- // when scope is destructed, the value pops back
-
- Debug("datatypes-output") << "printNameOnly is now " << printNameOnly << std::endl;
+bool DatatypeConstructorArg::isResolved() const
+{
+ // We could just write:
+ //
+ // return !d_selector.isNull() && d_selector.getType().isSelector();
+ //
+ // HOWEVER, this causes problems in ExprManager tear-down, because
+ // the attributes are removed before the pool is purged. When the
+ // pool is purged, this triggers an equality test between Datatypes,
+ // and this triggers a call to isResolved(), which breaks because
+ // d_selector has no type after attributes are stripped.
+ //
+ // This problem, coupled with the fact that this function is called
+ // _often_, means we should just use a boolean flag.
+ //
+ return d_internal->isResolved();
+}
+std::ostream& operator<<(std::ostream& os, const Datatype& dt)
+{
// can only output datatypes in the CVC4 native language
language::SetLanguage::Scope ls(os, language::output::LANG_CVC4);
+ dt.toStream(os);
+ return os;
+}
- os << "DATATYPE " << dt.getName();
- if(dt.isParametric()) {
- os << '[';
- for(size_t i = 0; i < dt.getNumParameters(); ++i) {
+void Datatype::toStream(std::ostream& out) const
+{
+ out << "DATATYPE " << getName();
+ if (isParametric())
+ {
+ out << '[';
+ for (size_t i = 0; i < getNumParameters(); ++i)
+ {
if(i > 0) {
- os << ',';
+ out << ',';
}
- os << dt.getParameter(i);
+ out << getParameter(i);
}
- os << ']';
+ out << ']';
}
- os << " =" << endl;
- Datatype::const_iterator i = dt.begin(), i_end = dt.end();
+ out << " =" << endl;
+ Datatype::const_iterator i = begin(), i_end = end();
if(i != i_end) {
- os << " ";
+ out << " ";
do {
- os << *i << endl;
+ out << *i << endl;
if(++i != i_end) {
- os << "| ";
+ out << "| ";
}
} while(i != i_end);
}
- os << "END;" << endl;
-
- return os;
+ out << "END;" << endl;
}
std::ostream& operator<<(std::ostream& os, const DatatypeConstructor& ctor) {
// can only output datatypes in the CVC4 native language
language::SetLanguage::Scope ls(os, language::output::LANG_CVC4);
+ ctor.toStream(os);
+ return os;
+}
- os << ctor.getName();
+void DatatypeConstructor::toStream(std::ostream& out) const
+{
+ out << getName();
- DatatypeConstructor::const_iterator i = ctor.begin(), i_end = ctor.end();
+ DatatypeConstructor::const_iterator i = begin(), i_end = end();
if(i != i_end) {
- os << "(";
+ out << "(";
do {
- os << *i;
+ out << *i;
if(++i != i_end) {
- os << ", ";
+ out << ", ";
}
} while(i != i_end);
- os << ")";
+ out << ")";
}
-
- return os;
}
std::ostream& operator<<(std::ostream& os, const DatatypeConstructorArg& arg) {
// can only output datatypes in the CVC4 native language
language::SetLanguage::Scope ls(os, language::output::LANG_CVC4);
-
- os << arg.getName() << ": " << arg.getTypeName();
-
+ arg.toStream(os);
return os;
}
-DatatypeIndexConstant::DatatypeIndexConstant(unsigned index) throw(IllegalArgumentException) : d_index(index){
+void DatatypeConstructorArg::toStream(std::ostream& out) const
+{
+ std::string name = getName();
+ out << name << ": ";
+ Type t;
+ if (isResolved())
+ {
+ t = getRangeType();
+ }
+ else if (d_selector.isNull())
+ {
+ string typeName = name.substr(name.find('\0') + 1);
+ out << ((typeName == "") ? "[self]" : typeName);
+ return;
+ }
+ else
+ {
+ t = d_selector.getType();
+ }
+ out << t;
}
+DatatypeIndexConstant::DatatypeIndexConstant(unsigned index) : d_index(index) {}
std::ostream& operator<<(std::ostream& out, const DatatypeIndexConstant& dic) {
return out << "index_" << dic.getIndex();
}
+
+std::string Datatype::getName() const
+{
+ ExprManagerScope ems(*d_em);
+ return d_internal->getName();
+}
+size_t Datatype::getNumConstructors() const { return d_constructors.size(); }
+
+bool Datatype::isParametric() const
+{
+ ExprManagerScope ems(*d_em);
+ return d_internal->isParametric();
+}
+size_t Datatype::getNumParameters() const
+{
+ ExprManagerScope ems(*d_em);
+ return d_internal->getNumParameters();
+}
+Type Datatype::getParameter(unsigned int i) const
+{
+ CheckArgument(isParametric(),
+ this,
+ "Cannot get type parameter of a non-parametric datatype.");
+ CheckArgument(i < getNumParameters(),
+ i,
+ "Type parameter index out of range for datatype.");
+ ExprManagerScope ems(*d_em);
+ return d_internal->getParameter(i).toType();
+}
+
+std::vector<Type> Datatype::getParameters() const
+{
+ CheckArgument(isParametric(),
+ this,
+ "Cannot get type parameters of a non-parametric datatype.");
+ std::vector<Type> params;
+ std::vector<TypeNode> paramsn = d_internal->getParameters();
+ // convert to type
+ for (unsigned i = 0, nparams = paramsn.size(); i < nparams; i++)
+ {
+ params.push_back(paramsn[i].toType());
+ }
+ return params;
+}
+
+bool Datatype::isCodatatype() const
+{
+ ExprManagerScope ems(*d_em);
+ return d_internal->isCodatatype();
+}
+
+bool Datatype::isSygus() const
+{
+ ExprManagerScope ems(*d_em);
+ return d_internal->isSygus();
+}
+
+bool Datatype::isTuple() const
+{
+ ExprManagerScope ems(*d_em);
+ return d_internal->isTuple();
+}
+
+bool Datatype::isRecord() const { return d_isRecord; }
+
+Record* Datatype::getRecord() const { return d_record; }
+bool Datatype::operator!=(const Datatype& other) const
+{
+ return !(*this == other);
+}
+
+bool Datatype::isResolved() const
+{
+ ExprManagerScope ems(*d_em);
+ return d_internal->isResolved();
+}
+Datatype::iterator Datatype::begin() { return iterator(d_constructors, true); }
+
+Datatype::iterator Datatype::end() { return iterator(d_constructors, false); }
+
+Datatype::const_iterator Datatype::begin() const
+{
+ return const_iterator(d_constructors, true);
+}
+
+Datatype::const_iterator Datatype::end() const
+{
+ return const_iterator(d_constructors, false);
+}
+
+bool DatatypeConstructor::isResolved() const
+{
+ return d_internal->isResolved();
+}
+
+size_t DatatypeConstructor::getNumArgs() const { return d_args.size(); }
+
+DatatypeConstructor::iterator DatatypeConstructor::begin()
+{
+ return iterator(d_args, true);
+}
+
+DatatypeConstructor::iterator DatatypeConstructor::end()
+{
+ return iterator(d_args, false);
+}
+
+DatatypeConstructor::const_iterator DatatypeConstructor::begin() const
+{
+ return const_iterator(d_args, true);
+}
+
+DatatypeConstructor::const_iterator DatatypeConstructor::end() const
+{
+ return const_iterator(d_args, false);
+}
}/* CVC4 namespace */
projects / cvc5.git / blobdiff