d_isRecord = true;
}
-Cardinality Datatype::getCardinality() const throw(IllegalArgumentException) {
+Cardinality Datatype::getCardinality( Type t ) const throw(IllegalArgumentException) {
PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
std::vector< Type > processing;
- computeCardinality( processing );
+ computeCardinality( t, processing );
return d_card;
}
-Cardinality Datatype::computeCardinality( std::vector< Type >& processing ) const throw(IllegalArgumentException){
+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;
processing.push_back( d_self );
Cardinality c = 0;
for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
- c += (*i).computeCardinality( processing );
+ c += (*i).computeCardinality( t, processing );
}
d_card = c;
processing.pop_back();
return d_card;
}
-bool Datatype::isRecursiveSingleton() const throw(IllegalArgumentException) {
+bool Datatype::isRecursiveSingleton( Type t ) const throw(IllegalArgumentException) {
PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
- if( d_card_rec_singleton==0 ){
+ if( d_card_rec_singleton[t]==0 ){
if( isCodatatype() ){
- Assert( d_card_u_assume.empty() );
+ Assert( d_card_u_assume[t].empty() );
std::vector< Type > processing;
- if( computeCardinalityRecSingleton( processing, d_card_u_assume ) ){
- d_card_rec_singleton = 1;
+ if( computeCardinalityRecSingleton( t, processing, d_card_u_assume[t] ) ){
+ d_card_rec_singleton[t] = 1;
}else{
- d_card_rec_singleton = -1;
+ d_card_rec_singleton[t] = -1;
}
- if( d_card_rec_singleton==1 ){
- Trace("dt-card") << "Datatype " << getName() << " is recursive singleton, dependent upon " << d_card_u_assume.size() << " uninterpreted sorts: " << std::endl;
- for( unsigned i=0; i<d_card_u_assume.size(); i++ ){
- Trace("dt-card") << " " << d_card_u_assume [i] << std::endl;
+ 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 = -1;
+ d_card_rec_singleton[t] = -1;
}
}
- return d_card_rec_singleton==1;
+ return d_card_rec_singleton[t]==1;
}
-unsigned Datatype::getNumRecursiveSingletonArgTypes() const throw(IllegalArgumentException) {
- return d_card_u_assume.size();
+unsigned Datatype::getNumRecursiveSingletonArgTypes( Type t ) const throw(IllegalArgumentException) {
+ return d_card_u_assume[t].size();
}
-Type Datatype::getRecursiveSingletonArgType( unsigned i ) const throw(IllegalArgumentException) {
- return d_card_u_assume[i];
+Type Datatype::getRecursiveSingletonArgType( Type t, unsigned i ) const throw(IllegalArgumentException) {
+ return d_card_u_assume[t][i];
}
-bool Datatype::computeCardinalityRecSingleton( std::vector< Type >& processing, std::vector< Type >& u_assume ) const throw(IllegalArgumentException){
+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==0 ){
+ 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 t = ((SelectorType)d_constructors[0][i].getType()).getRangeType();
+ Type tc = ((SelectorType)d_constructors[0][i].getType()).getRangeType();
//if it is an uninterpreted sort, then we depend on it having cardinality one
- if( t.isSort() ){
- if( std::find( u_assume.begin(), u_assume.end(), t )==u_assume.end() ){
- u_assume.push_back( t );
+ 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( t.isDatatype() ){
- const Datatype & dt = ((DatatypeType)t).getDatatype();
- if( !dt.computeCardinalityRecSingleton( processing, u_assume ) ){
+ }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( !t.getCardinality().isOne() ){
+ }else if( !tc.getCardinality().isOne() ){
return false;
}
}
}else{
return false;
}
- }else if( d_card_rec_singleton==-1 ){
+ }else if( d_card_rec_singleton[t]==-1 ){
return false;
}else{
- for( unsigned i=0; i<d_card_u_assume.size(); i++ ){
- if( std::find( u_assume.begin(), u_assume.end(), d_card_u_assume[i] )==u_assume.end() ){
- u_assume.push_back( d_card_u_assume[i] );
+ 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;
}
}
-bool Datatype::isFinite() const throw(IllegalArgumentException) {
+bool Datatype::isFinite( Type t ) const throw(IllegalArgumentException) {
PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
// we're using some internals, so we have to set up this library context
return self.getAttribute(DatatypeFiniteAttr());
}
for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
- if(! (*i).isFinite()) {
+ if(! (*i).isFinite( t )) {
self.setAttribute(DatatypeFiniteComputedAttr(), true);
self.setAttribute(DatatypeFiniteAttr(), false);
return false;
return true;
}
-bool Datatype::isInterpretedFinite() const throw(IllegalArgumentException) {
+bool Datatype::isInterpretedFinite( Type t ) const throw(IllegalArgumentException) {
PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved");
// we're using some internals, so we have to set up this library context
ExprManagerScope ems(d_self);
self.setAttribute(DatatypeUFiniteComputedAttr(), true);
self.setAttribute(DatatypeUFiniteAttr(), false);
for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) {
- if(! (*i).isInterpretedFinite()) {
+ if(! (*i).isInterpretedFinite( t )) {
return false;
}
}
return d_sygus_let_args.size()==1 && d_sygus_let_args[0]==d_sygus_let_body;
}
-Cardinality DatatypeConstructor::getCardinality() const throw(IllegalArgumentException) {
+Cardinality DatatypeConstructor::getCardinality( Type t ) const throw(IllegalArgumentException) {
PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
Cardinality c = 1;
}
/** compute the cardinality of this datatype */
-Cardinality DatatypeConstructor::computeCardinality( std::vector< Type >& processing ) const throw(IllegalArgumentException){
+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 t = SelectorType((*i).getSelector().getType()).getRangeType();
- if( t.isDatatype() ){
- const Datatype& dt = ((DatatypeType)t).getDatatype();
- c *= dt.computeCardinality( processing );
+ 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 *= t.getCardinality();
+ c *= tc.getCardinality();
}
}
return c;
}
-bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) {
+bool DatatypeConstructor::isFinite( Type t ) const throw(IllegalArgumentException) {
PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
// we're using some internals, so we have to set up this library context
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) {
- if(! (*i).getRangeType().getCardinality().isFinite()) {
+ 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;
return true;
}
-bool DatatypeConstructor::isInterpretedFinite() const throw(IllegalArgumentException) {
+bool DatatypeConstructor::isInterpretedFinite( Type t ) const throw(IllegalArgumentException) {
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);
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) {
- TypeNode t = TypeNode::fromType( (*i).getRangeType() );
- if(!t.isInterpretedFinite()) {
+ 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;
const std::vector< DatatypeType >& paramReplacements);
/** compute the cardinality of this datatype */
- Cardinality computeCardinality( std::vector< Type >& processing ) const throw(IllegalArgumentException);
+ Cardinality computeCardinality( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException);
/** compute whether this datatype is well-founded */
bool computeWellFounded( std::vector< Type >& processing ) const throw(IllegalArgumentException);
/** compute ground term */
* Return the cardinality of this constructor (the product of the
* cardinalities of its arguments).
*/
- Cardinality getCardinality() const throw(IllegalArgumentException);
+ Cardinality getCardinality( Type t ) const throw(IllegalArgumentException);
/**
* 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(IllegalArgumentException);
+ bool isFinite( Type t ) const throw(IllegalArgumentException);
/**
* Return true iff this constructor is finite (it is nullary or
* each of its argument types are finite) under assumption
* uninterpreted sorts are finite. This function can
* only be called for resolved constructors.
*/
- bool isInterpretedFinite() const throw(IllegalArgumentException);
+ bool isInterpretedFinite( Type t ) const throw(IllegalArgumentException);
/**
* Returns true iff this Datatype constructor has already been
mutable Cardinality d_card;
// is this type a recursive singleton type
- mutable int d_card_rec_singleton;
+ mutable std::map< Type, int > d_card_rec_singleton;
// if d_card_rec_singleton is true,
// infinite cardinality depends on at least one of the following uninterpreted sorts having cardinality > 1
- mutable std::vector< Type > d_card_u_assume;
+ mutable std::map< Type, std::vector< Type > > d_card_u_assume;
// is this well-founded
mutable int d_well_founded;
// ground term for this datatype
friend class ExprManager;// for access to resolve()
/** compute the cardinality of this datatype */
- Cardinality computeCardinality( std::vector< Type >& processing ) const throw(IllegalArgumentException);
+ Cardinality computeCardinality( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException);
/** compute whether this datatype is a recursive singleton */
- bool computeCardinalityRecSingleton( std::vector< Type >& processing, std::vector< Type >& u_assume ) const throw(IllegalArgumentException);
+ bool computeCardinalityRecSingleton( Type t, std::vector< Type >& processing, std::vector< Type >& u_assume ) const throw(IllegalArgumentException);
/** compute whether this datatype is well-founded */
bool computeWellFounded( std::vector< Type >& processing ) const throw(IllegalArgumentException);
/** compute ground term */
* cardinalities of its constructors). The Datatype must be
* resolved.
*/
- Cardinality getCardinality() const throw(IllegalArgumentException);
+ Cardinality getCardinality( Type t ) const throw(IllegalArgumentException);
/**
* Return true iff this Datatype is finite (all constructors are
* datatype is not well-founded, this function returns false. The
* Datatype must be resolved or an exception is thrown.
*/
- bool isFinite() const throw(IllegalArgumentException);
+ bool isFinite( Type t ) const throw(IllegalArgumentException);
/**
* Return true iff this Datatype is finite (all constructors are
* finite, i.e., there are finitely many ground terms) under the
* datatype is not well-founded, this function returns false. The
* Datatype must be resolved or an exception is thrown.
*/
- bool isInterpretedFinite() const throw(IllegalArgumentException);
+ bool isInterpretedFinite( Type t ) const throw(IllegalArgumentException);
/**
* Return true iff this datatype is well-founded (there exist ground
/**
* Return true iff this datatype is a recursive singleton
*/
- bool isRecursiveSingleton() const throw(IllegalArgumentException);
+ bool isRecursiveSingleton( Type t ) const throw(IllegalArgumentException);
/** get number of recursive singleton argument types */
- unsigned getNumRecursiveSingletonArgTypes() const throw(IllegalArgumentException);
- Type getRecursiveSingletonArgType( unsigned i ) const throw(IllegalArgumentException);
+ unsigned getNumRecursiveSingletonArgTypes( Type t ) const throw(IllegalArgumentException);
+ Type getRecursiveSingletonArgType( Type t, unsigned i ) const throw(IllegalArgumentException);
/**
* Construct and return a ground term of this Datatype. The
d_involvesExt(false),
d_involvesUt(false),
d_card(CardinalityUnknown()),
- d_card_rec_singleton(0),
d_well_founded(0) {
}
d_involvesExt(false),
d_involvesUt(false),
d_card(CardinalityUnknown()),
- d_card_rec_singleton(0),
d_well_founded(0) {
}
/** Is this a datatype type? */
bool Type::isDatatype() const {
NodeManagerScope nms(d_nodeManager);
- return d_typeNode->isDatatype() || d_typeNode->isParametricDatatype();
+ return d_typeNode->isDatatype();
}
/** Is this the Constructor type? */
const Datatype& DatatypeType::getDatatype() const {
NodeManagerScope nms(d_nodeManager);
- if( d_typeNode->isParametricDatatype() ) {
- PrettyCheckArgument( (*d_typeNode)[0].getKind() == kind::DATATYPE_TYPE, this);
- const Datatype& dt = (*d_typeNode)[0].getDatatype();
- return dt;
- } else {
- return d_typeNode->getDatatype();
- }
+ return d_typeNode->getDatatype();
}
bool DatatypeType::isParametric() const {
if( options::finiteModelFind() ){
if( isSort() ){
return true;
- }else if( isDatatype() || isParametricDatatype() ){
+ }else if( isDatatype() ){
+ TypeNode tn = *this;
const Datatype& dt = getDatatype();
- return dt.isInterpretedFinite();
+ return dt.isInterpretedFinite( tn.toType() );
}else if( isArray() ){
return getArrayIndexType().isInterpretedFinite() && getArrayConstituentType().isInterpretedFinite();
}else if( isSet() ) {
/** Is this a datatype type */
inline bool TypeNode::isDatatype() const {
- return getKind() == kind::DATATYPE_TYPE ||
+ return getKind() == kind::DATATYPE_TYPE || getKind() == kind::PARAMETRIC_DATATYPE ||
( isPredicateSubtype() && getSubtypeParentType().isDatatype() );
}
/** Get the datatype specification from a datatype type */
inline const Datatype& TypeNode::getDatatype() const {
Assert(isDatatype());
- //return getConst<Datatype>();
- DatatypeIndexConstant dic = getConst<DatatypeIndexConstant>();
- return NodeManager::currentNM()->getDatatypeForIndex( dic.getIndex() );
+ if( getKind() == kind::DATATYPE_TYPE ){
+ DatatypeIndexConstant dic = getConst<DatatypeIndexConstant>();
+ return NodeManager::currentNM()->getDatatypeForIndex( dic.getIndex() );
+ }else{
+ Assert( getKind() == kind::PARAMETRIC_DATATYPE );
+ return (*this)[0].getDatatype();
+ }
}
/** Get the exponent size of this floating-point type */
TypeNode in_t = in.getType();
if( processing.find( in_t )==processing.end() ){
processing[in_t] = true;
- if(in.getType().isDatatype()) {
- if(as.isBoolean() && in.getType().hasAttribute(BooleanTermAttr())) {
- processing.erase( in_t );
- return NodeManager::currentNM()->mkNode(kind::EQUAL, d_ttDt, in);
+ if(in.getType().isParametricDatatype() &&
+ in.getType().isInstantiatedDatatype()) {
+ // We have something here like (Pair Bool Bool)---need to dig inside
+ // and make it (Pair BV1 BV1)
+ Assert(as.isParametricDatatype() && as.isInstantiatedDatatype());
+ const Datatype* dt2 = &as[0].getDatatype();
+ std::vector<TypeNode> fromParams, toParams;
+ for(unsigned i = 0; i < dt2->getNumParameters(); ++i) {
+ fromParams.push_back(TypeNode::fromType(dt2->getParameter(i)));
+ toParams.push_back(as[i + 1]);
}
- Assert(as.isDatatype());
- const Datatype* dt2 = &as.getDatatype();
const Datatype* dt1;
if(d_datatypeCache.find(dt2) != d_datatypeCache.end()) {
dt1 = d_datatypeCache[dt2];
dt1 = d_datatypeReverseCache[dt2];
}
Assert(dt1 != NULL, "expected datatype in cache");
- Assert(*dt1 == in.getType().getDatatype(), "improper rewriteAs() between datatypes");
+ Assert(*dt1 == in.getType()[0].getDatatype(), "improper rewriteAs() between datatypes");
Node out;
for(size_t i = 0; i < dt1->getNumConstructors(); ++i) {
DatatypeConstructor ctor = (*dt1)[i];
NodeBuilder<> appctorb(kind::APPLY_CONSTRUCTOR);
appctorb << (*dt2)[i].getConstructor();
for(size_t j = 0; j < ctor.getNumArgs(); ++j) {
- appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType()), processing);
+ TypeNode asType = TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType());
+ asType = asType.substitute(fromParams.begin(), fromParams.end(), toParams.begin(), toParams.end());
+ appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), asType, processing);
}
Node appctor = appctorb;
if(i == 0) {
processing.erase( in_t );
return out;
}
- if(in.getType().isArray()) {
- // convert in to in'
- // e.g. in : (Array Int Bool)
- // for in' : (Array Int (_ BitVec 1))
- // then subs in |=> \array_lambda ( \lambda (x:Int) . [convert (read a' x) x]
- Assert(as.isArray());
- Assert(as.getArrayIndexType() == in.getType().getArrayIndexType());
- Assert(as.getArrayConstituentType() != in.getType().getArrayConstituentType());
- Node x = NodeManager::currentNM()->mkBoundVar(as.getArrayIndexType());
- Node boundvars = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, x);
- Node sel = NodeManager::currentNM()->mkNode(kind::SELECT, in, x);
- Node selprime = rewriteAs(sel, as.getArrayConstituentType(), processing);
- Node lam = NodeManager::currentNM()->mkNode(kind::LAMBDA, boundvars, selprime);
- Node out = NodeManager::currentNM()->mkNode(kind::ARRAY_LAMBDA, lam);
- Assert(out.getType() == as);
- processing.erase( in_t );
- return out;
- }
- if(in.getType().isParametricDatatype() &&
- in.getType().isInstantiatedDatatype()) {
- // We have something here like (Pair Bool Bool)---need to dig inside
- // and make it (Pair BV1 BV1)
- Assert(as.isParametricDatatype() && as.isInstantiatedDatatype());
- const Datatype* dt2 = &as[0].getDatatype();
- std::vector<TypeNode> fromParams, toParams;
- for(unsigned i = 0; i < dt2->getNumParameters(); ++i) {
- fromParams.push_back(TypeNode::fromType(dt2->getParameter(i)));
- toParams.push_back(as[i + 1]);
+ if(in.getType().isDatatype()) {
+ if(as.isBoolean() && in.getType().hasAttribute(BooleanTermAttr())) {
+ processing.erase( in_t );
+ return NodeManager::currentNM()->mkNode(kind::EQUAL, d_ttDt, in);
}
+ Assert(as.isDatatype());
+ const Datatype* dt2 = &as.getDatatype();
const Datatype* dt1;
if(d_datatypeCache.find(dt2) != d_datatypeCache.end()) {
dt1 = d_datatypeCache[dt2];
dt1 = d_datatypeReverseCache[dt2];
}
Assert(dt1 != NULL, "expected datatype in cache");
- Assert(*dt1 == in.getType()[0].getDatatype(), "improper rewriteAs() between datatypes");
+ Assert(*dt1 == in.getType().getDatatype(), "improper rewriteAs() between datatypes");
Node out;
for(size_t i = 0; i < dt1->getNumConstructors(); ++i) {
DatatypeConstructor ctor = (*dt1)[i];
NodeBuilder<> appctorb(kind::APPLY_CONSTRUCTOR);
appctorb << (*dt2)[i].getConstructor();
for(size_t j = 0; j < ctor.getNumArgs(); ++j) {
- TypeNode asType = TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType());
- asType = asType.substitute(fromParams.begin(), fromParams.end(), toParams.begin(), toParams.end());
- appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), asType, processing);
+ appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType()), processing);
}
Node appctor = appctorb;
if(i == 0) {
processing.erase( in_t );
return out;
}
+ if(in.getType().isArray()) {
+ // convert in to in'
+ // e.g. in : (Array Int Bool)
+ // for in' : (Array Int (_ BitVec 1))
+ // then subs in |=> \array_lambda ( \lambda (x:Int) . [convert (read a' x) x]
+ Assert(as.isArray());
+ Assert(as.getArrayIndexType() == in.getType().getArrayIndexType());
+ Assert(as.getArrayConstituentType() != in.getType().getArrayConstituentType());
+ Node x = NodeManager::currentNM()->mkBoundVar(as.getArrayIndexType());
+ Node boundvars = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, x);
+ Node sel = NodeManager::currentNM()->mkNode(kind::SELECT, in, x);
+ Node selprime = rewriteAs(sel, as.getArrayConstituentType(), processing);
+ Node lam = NodeManager::currentNM()->mkNode(kind::LAMBDA, boundvars, selprime);
+ Node out = NodeManager::currentNM()->mkNode(kind::ARRAY_LAMBDA, lam);
+ Assert(out.getType() == as);
+ processing.erase( in_t );
+ return out;
+ }
Unhandled(in);
}else{
Message() << "Type " << in_t << " involving Boolean sort is not supported." << std::endl;
//if( !tn.isSort() ){
// useTe = false;
//}
- if( isTypeDatatype( tn ) ){
+ if( tn.isDatatype() ){
const Datatype& dta = ((DatatypeType)(tn).toType()).getDatatype();
useTe = !dta.isCodatatype();
}
}
return true;
}
-
- /** is this term a datatype */
- static bool isTermDatatype( TNode n ){
- TypeNode tn = n.getType();
- return tn.isDatatype() || tn.isParametricDatatype();
- }
- static bool isTypeDatatype( TypeNode tn ){
- return tn.isDatatype() || tn.isParametricDatatype();
- }
private:
static Node collectRef( Node n, std::vector< Node >& sk, std::map< Node, Node >& rf, std::vector< Node >& rf_pending,
std::vector< Node >& terms, std::map< Node, bool >& cdts ){
if( sIndex==1 && pdt[csIndex].getNumArgs()==2 ){
arg1 = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( pdt[csIndex][0].getSelector() ), n[0] );
tn1 = arg1.getType();
- if( !DatatypesRewriter::isTypeDatatype( tn1 ) ){
+ if( !tn1.isDatatype() ){
arg1 = Node::null();
}
}
void SygusSplit::registerSygusType( TypeNode tn ) {
if( d_register.find( tn )==d_register.end() ){
- if( !DatatypesRewriter::isTypeDatatype( tn ) ){
+ if( !tn.isDatatype() ){
d_register[tn] = TypeNode::null();
}else{
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
if( parentKind!=UNDEFINED_KIND && pdt[csIndex].getNumArgs()==2 ){
int osIndex = sIndex==0 ? 1 : 0;
TypeNode tnno = d_tds->getArgType( pdt[csIndex], osIndex );
- if( DatatypesRewriter::isTypeDatatype( tnno ) ){
+ if( tnno.isDatatype() ){
const Datatype& dto = ((DatatypeType)(tnno).toType()).getDatatype();
registerSygusTypeConstructorArg( tnno, dto, tnnp, pdt, csIndex, osIndex );
//compute relationships when doing 0-arg
bool SygusSplit::isArgDatatype( const DatatypeConstructor& c, int i, const Datatype& dt ) {
TypeNode tni = d_tds->getArgType( c, i );
- if( datatypes::DatatypesRewriter::isTypeDatatype( tni ) ){
+ if( tni.isDatatype() ){
const Datatype& adt = ((DatatypeType)(tni).toType()).getDatatype();
if( adt==dt ){
return true;
if( it==d_prog_search.end() ){
//check if sygus type
TypeNode tn = a.getType();
- Assert( DatatypesRewriter::isTypeDatatype( tn ) );
+ Assert( tn.isDatatype() );
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
if( dt.isSygus() ){
ps = new ProgSearch( this, a, d_context );
bool SygusSymBreak::ProgSearch::assignTester( int tindex, Node n, int depth ) {
Trace("sygus-sym-break-debug") << "SymBreak : Assign tester : " << tindex << " " << n << ", depth = " << depth << " of " << d_anchor << std::endl;
TypeNode tn = n.getType();
- Assert( DatatypesRewriter::isTypeDatatype( tn ) );
+ Assert( tn.isDatatype() );
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
std::vector< Node > tst_waiting;
for( unsigned i=0; i<dt[tindex].getNumArgs(); i++ ){
int tindex = DatatypesRewriter::isTester( tst );//Datatype::indexOf( tst.getOperator().toExpr() );
Assert( tindex!=-1 );
TypeNode tn = prog.getType();
- Assert( DatatypesRewriter::isTypeDatatype( tn ) );
+ Assert( tn.isDatatype() );
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
std::map< int, Node > pre;
if( curr_depth<depth ){
"expr/datatype.h" \
"a datatype type index"
cardinality DATATYPE_TYPE \
- "%TYPE%.getDatatype().getCardinality()" \
+ "%TYPE%.getDatatype().getCardinality(%TYPE%.toType())" \
"expr/datatype.h"
well-founded DATATYPE_TYPE \
"%TYPE%.getDatatype().isWellFounded()" \
operator PARAMETRIC_DATATYPE 1: "parametric datatype"
cardinality PARAMETRIC_DATATYPE \
- "DatatypeType(%TYPE%.toType()).getDatatype().getCardinality()" \
+ "DatatypeType(%TYPE%.toType()).getDatatype().getCardinality(%TYPE%.toType())" \
"expr/datatype.h"
well-founded PARAMETRIC_DATATYPE \
"DatatypeType(%TYPE%.toType()).getDatatype().isWellFounded()" \
while( !eqcs_i.isFinished() ){
Node n = (*eqcs_i);
TypeNode tn = n.getType();
- if( DatatypesRewriter::isTypeDatatype( tn ) ){
+ if( tn.isDatatype() ){
Trace("datatypes-debug") << "Process equivalence class " << n << std::endl;
EqcInfo* eqc = getOrMakeEqcInfo( n );
//if there are more than 1 possible constructors for eqc
if( !hasLabel( eqc, n ) ){
Trace("datatypes-debug") << "No constructor..." << std::endl;
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- Trace("datatypes-debug") << "Datatype " << dt << " is " << dt.isFinite() << " " << dt.isInterpretedFinite() << " " << dt.isRecursiveSingleton() << std::endl;
+ Type tt = tn.toType();
+ const Datatype& dt = ((DatatypeType)tt).getDatatype();
+ Trace("datatypes-debug") << "Datatype " << dt << " is " << dt.isFinite( tt ) << " " << dt.isInterpretedFinite( tt ) << " " << dt.isRecursiveSingleton( tt ) << std::endl;
bool continueProc = true;
- if( dt.isRecursiveSingleton() ){
+ if( dt.isRecursiveSingleton( tt ) ){
Trace("datatypes-debug") << "Check recursive singleton..." << std::endl;
//handle recursive singleton case
std::map< TypeNode, Node >::iterator itrs = rec_singletons.find( tn );
// do not infer the equality if at least one sort was processed.
//otherwise, if the logic is quantified, under the assumption that all uninterpreted sorts have cardinality one,
// infer the equality.
- for( unsigned i=0; i<dt.getNumRecursiveSingletonArgTypes(); i++ ){
- TypeNode tn = TypeNode::fromType( dt.getRecursiveSingletonArgType( i ) );
+ for( unsigned i=0; i<dt.getNumRecursiveSingletonArgTypes( tt ); i++ ){
+ TypeNode tn = TypeNode::fromType( dt.getRecursiveSingletonArgType( tt, i ) );
if( getQuantifiersEngine() ){
// under the assumption that the cardinality of this type is one
Node a = getSingletonLemma( tn, true );
if( consIndex==-1 ){
consIndex = j;
}
- if( !dt[ j ].isInterpretedFinite() ) {
+ if( !dt[ j ].isInterpretedFinite( tt ) ) {
if( !eqc || !eqc->d_selectors ){
needSplit = false;
}
/** called when two equivalance classes have merged */
void TheoryDatatypes::eqNotifyPostMerge(TNode t1, TNode t2){
- if( DatatypesRewriter::isTermDatatype( t1 ) ){
+ if( t1.getType().isDatatype() ){
Trace("datatypes-debug") << "NotifyPostMerge : " << t1 << " " << t2 << std::endl;
d_pending_merge.push_back( t1.eqNode( t2 ) );
}
while( !eqccs_i.isFinished() ){
Node eqc = (*eqccs_i);
//for all equivalence classes that are datatypes
- if( DatatypesRewriter::isTermDatatype( eqc ) ){
+ if( eqc.getType().isDatatype() ){
EqcInfo* ei = getOrMakeEqcInfo( eqc );
if( ei && !ei->d_constructor.get().isNull() ){
Node c = ei->d_constructor.get();
Node eqc = nodes[index];
Node neqc;
bool addCons = false;
- const Datatype& dt = ((DatatypeType)(eqc.getType()).toType()).getDatatype();
+ Type tt = eqc.getType().toType();
+ const Datatype& dt = ((DatatypeType)tt).getDatatype();
if( !d_equalityEngine.hasTerm( eqc ) ){
Assert( false );
/*
if( neqc.isNull() ){
for( unsigned i=0; i<pcons.size(); i++ ){
//must try the infinite ones first
- bool cfinite = dt[ i ].isInterpretedFinite();
+ bool cfinite = dt[ i ].isInterpretedFinite( tt );
if( pcons[i] && (r==1)==cfinite ){
neqc = DatatypesRewriter::getInstCons( eqc, dt, i );
//for( unsigned j=0; j<neqc.getNumChildren(); j++ ){
- // //if( sels[i].find( j )==sels[i].end() && DatatypesRewriter::isTermDatatype( neqc[j] ) ){
- // if( !d_equalityEngine.hasTerm( neqc[j] ) && DatatypesRewriter::isTermDatatype( neqc[j] ) ){
+ // //if( sels[i].find( j )==sels[i].end() && neqc[j].getType().isDatatype() ){
+ // if( !d_equalityEngine.hasTerm( neqc[j] ) && neqc[j].getType().isDatatype() ){
// nodes.push_back( neqc[j] );
// }
//}
if( itv!=vmap.end() ){
int debruijn = depth - 1 - itv->second;
return NodeManager::currentNM()->mkConst(UninterpretedConstant(n.getType().toType(), debruijn));
- }else if( DatatypesRewriter::isTermDatatype( n ) ){
+ }else if( n.getType().isDatatype() ){
Node nc = eqc_cons[n];
if( !nc.isNull() ){
vmap[n] = depth;
while( !eqcs_i.isFinished() ){
Node eqc = (*eqcs_i);
TypeNode tn = eqc.getType();
- if( DatatypesRewriter::isTypeDatatype( tn ) ) {
+ if( tn.isDatatype() ) {
if( !tn.isCodatatype() ){
if( options::dtCyclic() ){
//do cycle checks
if( !mkExp ){ Trace("dt-cdt-debug") << " - " << part[j] << " is looping at index " << it_rec->second << std::endl; }
new_part_rec[ it_rec->second ].push_back( part[j] );
}else{
- if( DatatypesRewriter::isTermDatatype( c ) ){
+ if( c.getType().isDatatype() ){
Node ncons = getEqcConstructor( c );
if( ncons.getKind()==APPLY_CONSTRUCTOR ) {
Node cc = ncons.getOperator();
return Node::null();
}else{
TypeNode tn = nn.getType();
- if( DatatypesRewriter::isTypeDatatype( tn ) ) {
+ if( tn.isDatatype() ) {
if( !tn.isCodatatype() ){
return nn;
}
addLemma = true;
}else if( n.getKind()==EQUAL ){
TypeNode tn = n[0].getType();
- if( !DatatypesRewriter::isTypeDatatype( tn ) ){
+ if( !tn.isDatatype() ){
addLemma = true;
}else{
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
while( !eqcs_i.isFinished() ){
Node eqc = (*eqcs_i);
if( !eqc.getType().isBoolean() ){
- if( DatatypesRewriter::isTermDatatype( eqc ) ){
+ if( eqc.getType().isDatatype() ){
Trace( c ) << "DATATYPE : ";
}
Trace( c ) << eqc << " : " << eqc.getType() << " : " << std::endl;
++eqc_i;
}
Trace( c ) << "}" << std::endl;
- if( DatatypesRewriter::isTermDatatype( eqc ) ){
+ if( eqc.getType().isDatatype() ){
EqcInfo* ei = getOrMakeEqcInfo( eqc );
if( ei ){
Trace( c ) << " Instantiated : " << ei->d_inst.get() << std::endl;
Debug("dt-enum") << "datatype is datatype? " << d_type.isDatatype() << std::endl;
Debug("dt-enum") << "datatype is kind " << d_type.getKind() << std::endl;
Debug("dt-enum") << "datatype is " << d_type << std::endl;
- Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " " << d_datatype.isRecursiveSingleton();
- Debug("dt-enum") << " " << d_datatype.isFinite() << std::endl;
- Debug("dt-enum") << " " << d_datatype.isInterpretedFinite() << std::endl;
+ Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " " << d_datatype.isRecursiveSingleton( d_type.toType() );
+ Debug("dt-enum") << " " << d_datatype.isFinite( d_type.toType() ) << std::endl;
+ Debug("dt-enum") << " " << d_datatype.isInterpretedFinite( d_type.toType() ) << std::endl;
if( d_datatype.isCodatatype() && hasCyclesDt( d_datatype ) ){
//start with uninterpreted constant
bool d_child_enum;
bool hasCyclesDt( const Datatype& dt ) {
- return dt.isRecursiveSingleton() || !dt.isFinite();
+ return dt.isRecursiveSingleton( d_type.toType() ) || !dt.isFinite( d_type.toType() );
}
bool hasCycles( TypeNode tn ){
if( tn.isDatatype() ){
}
if( d_ctor>=d_has_debruijn+d_datatype.getNumConstructors() ){
//try next size limit as long as new terms were generated at last size, or other cases
- if( prevSize==d_size_limit || ( d_size_limit==0 && d_datatype.isCodatatype() ) || !d_datatype.isInterpretedFinite() ){
+ if( prevSize==d_size_limit || ( d_size_limit==0 && d_datatype.isCodatatype() ) || !d_datatype.isInterpretedFinite( d_type.toType() ) ){
d_size_limit++;
d_ctor = d_zeroCtor;
for( unsigned i=0; i<d_sel_sum.size(); i++ ){
#include "expr/datatype.h"
#include "options/quantifiers_options.h"
#include "smt/smt_statistics_registry.h"
-#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/term_database.h"
#include "theory/theory_engine.h"
Node pat = q[2][0][0];
if( pat.getKind()==APPLY_UF ){
TypeNode tn = pat[0].getType();
- if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){
+ if( tn.isDatatype() ){
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
if( dt.isSygus() ){
//do unfolding if it induces Boolean structure,
if( n.getKind()==APPLY_UF ){
TypeNode tn = n[0].getType();
Trace("cegqi-eager-debug") << "check " << n[0].getType() << std::endl;
- if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){
+ if( tn.isDatatype() ){
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
if( dt.isSygus() ){
Trace("cegqi-eager") << "Unfold eager : " << n << std::endl;
std::string f(ss.str());
f.erase(f.begin());
TypeNode tn = prog.getType();
- Assert( datatypes::DatatypesRewriter::isTypeDatatype( tn ) );
+ Assert( tn.isDatatype() );
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
Assert( dt.isSygus() );
//get the solution
#include "expr/datatype.h"
#include "options/quantifiers_options.h"
-#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/quantifiers/ce_guided_instantiation.h"
#include "theory/quantifiers/ce_guided_single_inv_ei.h"
#include "theory/quantifiers/first_order_model.h"
d_has_ites = false;
}
}
- Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) );
+ Assert( tn.isDatatype() );
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
Assert( dt.isSygus() );
if( !dt.getSygusAllowAll() ){
#include "expr/datatype.h"
#include "options/quantifiers_options.h"
-#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/quantifiers/ce_guided_instantiation.h"
#include "theory/quantifiers/ce_guided_single_inv.h"
#include "theory/quantifiers/first_order_model.h"
if( Trace.isOn("csi-rcons") ){
for( std::map< TypeNode, std::map< Node, int > >::iterator it = d_rcons_to_id.begin(); it != d_rcons_to_id.end(); ++it ){
TypeNode tn = it->first;
- Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) );
+ Assert( tn.isDatatype() );
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
Trace("csi-rcons") << "Terms to reconstruct of type " << dt.getName() << " : " << std::endl;
for( std::map< Node, int >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
int id = allocate( t, stn );
d_rcons_to_status[stn][t] = -1;
TypeNode tn = t.getType();
- Assert( datatypes::DatatypesRewriter::isTypeDatatype( stn ) );
+ Assert( stn.isDatatype() );
const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
Assert( dt.isSygus() );
Trace("csi-rcons-debug") << "Check reconstruct " << t << ", sygus type " << dt.getName() << ", kind " << t.getKind() << ", id : " << id << std::endl;
TypeNode tn = q[0][i].getType();
if( tn.isDatatype() ){
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- if( dt.isRecursiveSingleton() ){
+ if( dt.isRecursiveSingleton( tn.toType() ) ){
Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is recursive singleton." << std::endl;
}else{
int score = -1;
if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){
- score = dt.isInterpretedFinite() ? 1 : 0;
+ score = dt.isInterpretedFinite( tn.toType() ) ? 1 : 0;
}else if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_DEFAULT ){
- score = dt.isInterpretedFinite() ? 1 : -1;
+ score = dt.isInterpretedFinite( tn.toType() ) ? 1 : -1;
}
- Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is score " << score << " (" << dt.isInterpretedFinite() << " " << dt.isFinite() << ")" << std::endl;
+ Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is score " << score << " (" << dt.isInterpretedFinite( tn.toType() ) << " " << dt.isFinite( tn.toType() ) << ")" << std::endl;
if( score>max_score ){
max_index = i;
max_score = score;
#include "theory/quantifiers/quantifiers_rewriter.h"
#include "options/quantifiers_options.h"
-#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/trigger.h"
#include "expr/datatype.h"
#include "options/base_options.h"
#include "options/quantifiers_options.h"
-#include "theory/datatypes/datatypes_rewriter.h"
#include "theory/quantifiers/ce_guided_instantiation.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/fun_def_engine.h"
}
}
/* TODO: more than weak structural induction
- else if( datatypes::DatatypesRewriter::isTypeDatatype( tn ) && std::find( visited.begin(), visited.end(), tn )==visited.end() ){
+ else if( tn.isDatatype() && std::find( visited.begin(), visited.end(), tn )==visited.end() ){
visited.push_back( tn );
const Datatype& dt = ((DatatypeType)(subs[0].getType()).toType()).getDatatype();
std::vector< Node > disj;
Node nret = ret.substitute( ind_vars[0], k );
//note : everything is under a negation
//the following constructs ~( R( x, k ) => ~P( x ) )
- if( options::dtStcInduction() && datatypes::DatatypesRewriter::isTypeDatatype(tn) ){
+ if( options::dtStcInduction() && tn.isDatatype() ){
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
std::vector< Node > disj;
for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
ret = false;
}else if( tn.isSet() ){
ret = isClosedEnumerableType( tn.getSetElementType() );
- }else if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){
+ }else if( tn.isDatatype() ){
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
}
bool TermDb::isInductionTerm( Node n ) {
- if( options::dtStcInduction() && datatypes::DatatypesRewriter::isTermDatatype( n ) ){
- const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype();
+ TypeNode tn = n.getType();
+ if( options::dtStcInduction() && tn.isDatatype() ){
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
return !dt.isCodatatype();
}
if( options::intWfInduction() && n.getType().isInteger() ){
while( i>=(int)d_fv[tn].size() ){
std::stringstream ss;
TypeNode vtn = tn;
- if( datatypes::DatatypesRewriter::isTypeDatatype( tn ) ){
+ if( tn.isDatatype() ){
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
ss << "fv_" << dt.getName() << "_" << i;
if( !dt.getSygusType().isNull() ){
}
bool TermDbSygus::getMatch( Node t, TypeNode st, int& index_found, std::vector< Node >& args, int index_exc, int index_start ) {
- Assert( datatypes::DatatypesRewriter::isTypeDatatype( st ) );
+ Assert( st.isDatatype() );
const Datatype& dt = ((DatatypeType)(st).toType()).getDatatype();
Assert( dt.isSygus() );
std::map< Kind, std::vector< Node > > kgens;
Node sc;
d_builtin_const_to_sygus[tn][c] = sc;
Assert( c.isConst() );
- Assert( datatypes::DatatypesRewriter::isTypeDatatype( tn ) );
+ Assert( tn.isDatatype() );
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
Trace("csi-rcons-debug") << "Try to reconstruct " << c << " in " << dt.getName() << std::endl;
Assert( dt.isSygus() );
void TermDbSygus::registerSygusType( TypeNode tn ){
if( d_register.find( tn )==d_register.end() ){
- if( !datatypes::DatatypesRewriter::isTypeDatatype( tn ) ){
+ if( !tn.isDatatype() ){
d_register[tn] = TypeNode::null();
}else{
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
if( n.getKind()==APPLY_UF && !n.getType().isBoolean() ){
Trace("sygus-eager") << "TermDbSygus::eager: Register eval term : " << n << std::endl;
TypeNode tn = n[0].getType();
- if( datatypes::DatatypesRewriter::isTypeDatatype(tn) ){
+ if( tn.isDatatype() ){
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
if( dt.isSygus() ){
Node f = n.getOperator();
if( n[0].getKind()!=APPLY_CONSTRUCTOR ){
d_evals[n[0]].push_back( n );
TypeNode tn = n[0].getType();
- Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) );
+ Assert( tn.isDatatype() );
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
Node var_list = Node::fromExpr( dt.getSygusVarList() );
Assert( dt.isSygus() );
unsigned start = d_node_mv_args_proc[n][vn];
Node antec = n.eqNode( vn ).negate();
TypeNode tn = n.getType();
- Assert( datatypes::DatatypesRewriter::isTypeDatatype(tn) );
+ Assert( tn.isDatatype() );
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
Assert( dt.isSygus() );
Trace("sygus-eager") << "TermDbSygus::eager: Register model value : " << vn << " for " << n << std::endl;
bool isCorecursive = false;
if( t.isDatatype() ){
const Datatype& dt = ((DatatypeType)(t).toType()).getDatatype();
- isCorecursive = dt.isCodatatype() && ( !dt.isFinite() || dt.isRecursiveSingleton() );
+ isCorecursive = dt.isCodatatype() && ( !dt.isFinite( t.toType() ) || dt.isRecursiveSingleton( t.toType() ) );
}
#ifdef CVC4_ASSERTIONS
bool isUSortFiniteRestricted = false;
if( parent[0].getType().isDatatype() ){
TypeNode tn = parent[0].getType();
const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- if( dt.isRecursiveSingleton() ){
+ if( dt.isRecursiveSingleton( tn.toType() ) ){
//domain size may be 1
break;
}
sc-cdt1.smt2 \
conqueue-dt-enum-iloop.smt2 \
coda_simp_model.smt2 \
- Test1-tup-mp.cvc
+ Test1-tup-mp.cvc \
+ dt-param-card4-unsat.smt2 \
+ dt-param-card4-bool-sat.smt2
FAILING_TESTS = \
datatype-dump.cvc
--- /dev/null
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status sat)
+(declare-datatypes (T S) ( (Pair (pair (first T) (second S)) ) ) )
+
+(declare-fun p1 () (Pair Bool Bool))
+(declare-fun p2 () (Pair Bool Bool))
+(declare-fun p3 () (Pair Bool Bool))
+(declare-fun p4 () (Pair Bool Bool))
+
+(assert (distinct p1 p2 p3 p4))
+(check-sat)
--- /dev/null
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-datatypes (T S) ( (Pair (pair (first T) (second S)) ) ) )
+
+(declare-datatypes () ((Color (red) (blue))))
+
+(declare-fun p1 () (Pair Color Color))
+(declare-fun p2 () (Pair Color Color))
+(declare-fun p3 () (Pair Color Color))
+(declare-fun p4 () (Pair Color Color))
+(declare-fun p5 () (Pair Color Color))
+
+(assert (distinct p1 p2 p3 p4 p5))
+(check-sat)