From c3c8d013d2a879eaa1d205e57af32a7f8bb8c0b7 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 2 Dec 2016 14:25:07 -0600 Subject: [PATCH] Bug fixes and refactoring of parametric datatypes, add some regressions. --- src/expr/datatype.cpp | 129 +++++++++++------- src/expr/datatype.h | 30 ++-- src/expr/type.cpp | 10 +- src/expr/type_node.cpp | 5 +- src/expr/type_node.h | 12 +- src/smt/boolean_terms.cpp | 80 +++++------ src/theory/datatypes/datatypes_rewriter.h | 11 +- src/theory/datatypes/datatypes_sygus.cpp | 14 +- src/theory/datatypes/kinds | 4 +- src/theory/datatypes/theory_datatypes.cpp | 42 +++--- src/theory/datatypes/type_enumerator.cpp | 6 +- src/theory/datatypes/type_enumerator.h | 4 +- .../quantifiers/ce_guided_instantiation.cpp | 7 +- .../quantifiers/ce_guided_single_inv.cpp | 3 +- .../quantifiers/ce_guided_single_inv_sol.cpp | 5 +- src/theory/quantifiers/quant_split.cpp | 8 +- .../quantifiers/quantifiers_rewriter.cpp | 1 - src/theory/quantifiers/term_database.cpp | 26 ++-- src/theory/theory_model.cpp | 2 +- src/theory/unconstrained_simplifier.cpp | 2 +- test/regress/regress0/datatypes/Makefile.am | 4 +- .../datatypes/dt-param-card4-bool-sat.smt2 | 11 ++ .../datatypes/dt-param-card4-unsat.smt2 | 14 ++ 23 files changed, 236 insertions(+), 194 deletions(-) create mode 100644 test/regress/regress0/datatypes/dt-param-card4-bool-sat.smt2 create mode 100644 test/regress/regress0/datatypes/dt-param-card4-unsat.smt2 diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 537fc2b1a..bc39ced13 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -173,14 +173,14 @@ void Datatype::setRecord() { 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; @@ -188,7 +188,7 @@ Cardinality Datatype::computeCardinality( std::vector< Type >& processing ) cons 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(); @@ -196,64 +196,64 @@ Cardinality Datatype::computeCardinality( std::vector< Type >& processing ) cons 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& 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& processing, }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& processing, } } -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 @@ -286,7 +286,7 @@ bool Datatype::isFinite() const throw(IllegalArgumentException) { 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; @@ -297,7 +297,7 @@ bool Datatype::isFinite() const throw(IllegalArgumentException) { 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); @@ -310,7 +310,7 @@ bool Datatype::isInterpretedFinite() const throw(IllegalArgumentException) { 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; } } @@ -787,7 +787,7 @@ bool DatatypeConstructor::isSygusIdFunc() const { 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; @@ -800,15 +800,24 @@ Cardinality DatatypeConstructor::getCardinality() const throw(IllegalArgumentExc } /** 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; @@ -828,7 +837,7 @@ bool DatatypeConstructor::computeWellFounded( std::vector< Type >& processing ) } -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 @@ -838,8 +847,18 @@ bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) { 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; @@ -850,7 +869,7 @@ bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) { 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); @@ -859,9 +878,19 @@ bool DatatypeConstructor::isInterpretedFinite() const throw(IllegalArgumentExcep 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; diff --git a/src/expr/datatype.h b/src/expr/datatype.h index f81d2358d..49189959b 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -221,7 +221,7 @@ private: 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 */ @@ -329,21 +329,21 @@ public: * 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 @@ -497,10 +497,10 @@ private: 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 @@ -542,9 +542,9 @@ private: 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 */ @@ -619,7 +619,7 @@ public: * 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 @@ -627,7 +627,7 @@ public: * 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 @@ -635,7 +635,7 @@ public: * 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 @@ -646,12 +646,12 @@ public: /** * 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 @@ -836,7 +836,6 @@ inline Datatype::Datatype(std::string name, bool isCo) : d_involvesExt(false), d_involvesUt(false), d_card(CardinalityUnknown()), - d_card_rec_singleton(0), d_well_founded(0) { } @@ -853,7 +852,6 @@ inline Datatype::Datatype(std::string name, const std::vector& params, boo d_involvesExt(false), d_involvesUt(false), d_card(CardinalityUnknown()), - d_card_rec_singleton(0), d_well_founded(0) { } diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 11a45db79..5f62317ee 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -250,7 +250,7 @@ bool Type::isFloatingPoint() const { /** 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? */ @@ -564,13 +564,7 @@ std::vector ConstructorType::getArgTypes() const { 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 { diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index ede710dad..f11aa019e 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -72,9 +72,10 @@ bool TypeNode::isInterpretedFinite() 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() ) { diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 9fffbdeb2..0abbc9a1b 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -969,7 +969,7 @@ inline bool TypeNode::isBitVector() const { /** 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() ); } @@ -1023,9 +1023,13 @@ inline bool TypeNode::isBitVector(unsigned size) const { /** Get the datatype specification from a datatype type */ inline const Datatype& TypeNode::getDatatype() const { Assert(isDatatype()); - //return getConst(); - DatatypeIndexConstant dic = getConst(); - return NodeManager::currentNM()->getDatatypeForIndex( dic.getIndex() ); + if( getKind() == kind::DATATYPE_TYPE ){ + DatatypeIndexConstant dic = getConst(); + 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 */ diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index 51ae0fd11..ba7902d32 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -137,13 +137,17 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode, 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 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]; @@ -151,14 +155,16 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode, 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) { @@ -171,35 +177,13 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode, 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 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]; @@ -207,16 +191,14 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode, 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) { @@ -229,6 +211,24 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode, 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; diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index dd2803d30..e58289568 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -134,7 +134,7 @@ public: //if( !tn.isSort() ){ // useTe = false; //} - if( isTypeDatatype( tn ) ){ + if( tn.isDatatype() ){ const Datatype& dta = ((DatatypeType)(tn).toType()).getDatatype(); useTe = !dta.isCodatatype(); } @@ -376,15 +376,6 @@ public: } 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 ){ diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 0ecc6e547..fe07e44da 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -57,7 +57,7 @@ void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node > 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(); } } @@ -193,7 +193,7 @@ void SygusSplit::getSygusSplits( Node n, const Datatype& dt, std::vector< Node > 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(); @@ -319,7 +319,7 @@ void SygusSplit::registerSygusTypeConstructorArg( TypeNode tnn, const Datatype& 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 @@ -700,7 +700,7 @@ int SygusSplit::getFirstArgOccurrence( const DatatypeConstructor& c, const Datat 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; @@ -784,7 +784,7 @@ void SygusSymBreak::addTester( int tindex, Node n, Node exp ) { 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 ); @@ -837,7 +837,7 @@ void SygusSymBreak::ProgSearch::addTester( int tindex, Node n, Node exp ) { 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 pre; if( curr_depth::iterator itrs = rec_singletons.find( tn ); @@ -209,8 +210,8 @@ void TheoryDatatypes::check(Effort e) { // 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; id_selectors ){ needSplit = false; } @@ -773,7 +774,7 @@ void TheoryDatatypes::eqNotifyPreMerge(TNode t1, TNode t2){ /** 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 ) ); } @@ -1441,7 +1442,7 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ 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(); @@ -1467,7 +1468,8 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ 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 ); /* @@ -1533,12 +1535,12 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ if( neqc.isNull() ){ for( unsigned i=0; i& eqc_c 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; @@ -1789,7 +1791,7 @@ void TheoryDatatypes::checkCycles() { 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 @@ -1895,7 +1897,7 @@ void TheoryDatatypes::separateBisimilar( std::vector< Node >& part, std::vector< 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(); @@ -2021,7 +2023,7 @@ Node TheoryDatatypes::searchForCycle( TNode n, TNode on, return Node::null(); }else{ TypeNode tn = nn.getType(); - if( DatatypesRewriter::isTypeDatatype( tn ) ) { + if( tn.isDatatype() ) { if( !tn.isCodatatype() ){ return nn; } @@ -2045,7 +2047,7 @@ bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){ 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(); @@ -2109,7 +2111,7 @@ void TheoryDatatypes::printModelDebug( const char* c ){ 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; @@ -2123,7 +2125,7 @@ void TheoryDatatypes::printModelDebug( const char* c ){ ++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; diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp index c0539743f..60d319da3 100644 --- a/src/theory/datatypes/type_enumerator.cpp +++ b/src/theory/datatypes/type_enumerator.cpp @@ -170,9 +170,9 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){ 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 diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index 8473b5d69..83c938299 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -61,7 +61,7 @@ class DatatypesEnumerator : public TypeEnumeratorBase { 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() ){ @@ -159,7 +159,7 @@ public: } 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& visited ) 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; @@ -769,7 +768,7 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) { 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 diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index e0bbbf8ac..44ac135a7 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -16,7 +16,6 @@ #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" @@ -147,7 +146,7 @@ void CegConjectureSingleInv::initialize( Node q ) { 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() ){ diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp index 240c2ed12..5cc46d163 100644 --- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp @@ -16,7 +16,6 @@ #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" @@ -655,7 +654,7 @@ Node CegConjectureSingleInvSol::reconstructSolution( Node sol, TypeNode stn, int 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 ){ @@ -732,7 +731,7 @@ int CegConjectureSingleInvSol::collectReconstructNodes( Node t, TypeNode stn, in 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; diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index 5f73fe6d0..c88430dbf 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -43,16 +43,16 @@ void QuantDSplit::preRegisterQuantifier( Node q ) { 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; diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index de8875ae3..fcd8d1829 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -15,7 +15,6 @@ #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" diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 2c6bfb7d3..0bdfa2d24 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -17,7 +17,6 @@ #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" @@ -1088,7 +1087,7 @@ void getSelfSel( const Datatype& dt, const DatatypeConstructor& dc, Node n, Type } } /* 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; @@ -1160,7 +1159,7 @@ Node TermDb::mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& argTypes 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=(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() ){ @@ -2373,7 +2373,7 @@ bool TermDbSygus::getMatch2( Node p, Node n, std::map< int, Node >& s, std::vect } 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; @@ -2530,7 +2530,7 @@ Node TermDbSygus::builtinToSygusConst( Node c, TypeNode tn, int rcons_depth ) { 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() ); @@ -2839,7 +2839,7 @@ struct sortConstants { 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(); @@ -3234,7 +3234,7 @@ void TermDbSygus::registerEvalTerm( Node n ) { 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(); @@ -3242,7 +3242,7 @@ void TermDbSygus::registerEvalTerm( Node n ) { 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() ); @@ -3281,7 +3281,7 @@ void TermDbSygus::registerModelValue( Node a, Node v, std::vector< Node >& lems 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; diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 71d82d5e4..8579ad55f 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -819,7 +819,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel) 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; diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp index d13cc1f03..8284f6ff4 100644 --- a/src/theory/unconstrained_simplifier.cpp +++ b/src/theory/unconstrained_simplifier.cpp @@ -202,7 +202,7 @@ void UnconstrainedSimplifier::processUnconstrained() 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; } diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index 8631a4f32..a8a637377 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -69,7 +69,9 @@ TESTS = \ 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 diff --git a/test/regress/regress0/datatypes/dt-param-card4-bool-sat.smt2 b/test/regress/regress0/datatypes/dt-param-card4-bool-sat.smt2 new file mode 100644 index 000000000..ca5791ce2 --- /dev/null +++ b/test/regress/regress0/datatypes/dt-param-card4-bool-sat.smt2 @@ -0,0 +1,11 @@ +(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) diff --git a/test/regress/regress0/datatypes/dt-param-card4-unsat.smt2 b/test/regress/regress0/datatypes/dt-param-card4-unsat.smt2 new file mode 100644 index 000000000..9676745b4 --- /dev/null +++ b/test/regress/regress0/datatypes/dt-param-card4-unsat.smt2 @@ -0,0 +1,14 @@ +(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) -- 2.30.2