From c547bd591891ffd9211ed3859b0a67423a708f25 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 1 Nov 2019 17:06:33 -0500 Subject: [PATCH] Fix non-termination in datatype type enumerator (#3369) --- src/expr/datatype.cpp | 90 ++++--- src/expr/datatype.h | 51 +++- src/expr/type.cpp | 6 + src/expr/type.h | 14 ++ src/expr/type_node.cpp | 7 + src/expr/type_node.h | 8 + src/theory/datatypes/type_enumerator.cpp | 222 +++++++++++++----- src/theory/datatypes/type_enumerator.h | 74 +++--- .../quantifiers/fmf/full_model_check.cpp | 5 + src/theory/theory_model_builder.cpp | 4 + test/regress/CMakeLists.txt | 2 + .../datatypes/issue-variant-dt-zero.smt2 | 16 ++ .../regress1/quantifiers/issue3316.smt2 | 22 ++ 13 files changed, 378 insertions(+), 143 deletions(-) create mode 100644 test/regress/regress1/datatypes/issue-variant-dt-zero.smt2 create mode 100644 test/regress/regress1/quantifiers/issue3316.smt2 diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 2356f74bc..2edb1f53b 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -30,6 +30,7 @@ #include "expr/type.h" #include "options/datatypes_options.h" #include "options/set_language.h" +#include "theory/type_enumerator.h" using namespace std; @@ -479,32 +480,48 @@ bool Datatype::computeWellFounded(std::vector& processing) const Expr Datatype::mkGroundTerm(Type t) const { PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); + return mkGroundTermInternal(t, false); +} + +Expr Datatype::mkGroundValue(Type t) const +{ + PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); + return mkGroundTermInternal(t, true); +} + +Expr Datatype::mkGroundTermInternal(Type t, bool isValue) const +{ ExprManagerScope ems(d_self); - Debug("datatypes") << "mkGroundTerm of type " << t << std::endl; + Debug("datatypes") << "mkGroundTerm of type " << t + << ", isValue = " << isValue << std::endl; // is this already in the cache ? - std::map< Type, Expr >::iterator it = d_ground_term.find( t ); - if( it != d_ground_term.end() ){ + std::map& cache = isValue ? d_ground_value : d_ground_term; + std::map::iterator it = cache.find(t); + if (it != cache.end()) + { Debug("datatypes") << "\nin cache: " << d_self << " => " << it->second << std::endl; return it->second; - } else { - std::vector< Type > processing; - Expr groundTerm = computeGroundTerm( t, processing ); - if(!groundTerm.isNull() ) { - // we found a ground-term-constructing constructor! - d_ground_term[t] = groundTerm; - Debug("datatypes") << "constructed: " << getName() << " => " << groundTerm << std::endl; - } - if( groundTerm.isNull() ){ - if( !d_isCo ){ - // if we get all the way here, we aren't well-founded - IllegalArgument(*this, "datatype is not well-founded, cannot construct a ground term!"); - }else{ - return groundTerm; - } - }else{ - return groundTerm; + } + std::vector processing; + Expr groundTerm = computeGroundTerm(t, processing, isValue); + if (!groundTerm.isNull()) + { + // we found a ground-term-constructing constructor! + cache[t] = groundTerm; + Debug("datatypes") << "constructed: " << getName() << " => " << groundTerm + << std::endl; + } + if (groundTerm.isNull()) + { + if (!d_isCo) + { + // if we get all the way here, we aren't well-founded + IllegalArgument( + *this, + "datatype is not well-founded, cannot construct a ground term!"); } } + return groundTerm; } Expr getSubtermWithType( Expr e, Type t, bool isTop ){ @@ -521,7 +538,9 @@ Expr getSubtermWithType( Expr e, Type t, bool isTop ){ } } -Expr Datatype::computeGroundTerm(Type t, std::vector& processing) const +Expr Datatype::computeGroundTerm(Type t, + std::vector& processing, + bool isValue) const { if( std::find( processing.begin(), processing.end(), t )==processing.end() ){ processing.push_back( t ); @@ -530,7 +549,8 @@ Expr Datatype::computeGroundTerm(Type t, std::vector& processing) const //do nullary constructors first if( ((*i).getNumArgs()==0)==(r==0)){ Debug("datatypes") << "Try constructing for " << (*i).getName() << ", processing = " << processing.size() << std::endl; - Expr e = (*i).computeGroundTerm( t, processing, d_ground_term ); + Expr e = + (*i).computeGroundTerm(t, processing, d_ground_term, isValue); if( !e.isNull() ){ //must check subterms for the same type to avoid infinite loops in type enumeration Expr se = getSubtermWithType( e, t, true ); @@ -1078,7 +1098,8 @@ bool DatatypeConstructor::isInterpretedFinite(Type t) const Expr DatatypeConstructor::computeGroundTerm(Type t, std::vector& processing, - std::map& gt) const + std::map& gt, + bool isValue) const { // we're using some internals, so we have to set up this library context ExprManagerScope ems(d_constructor); @@ -1089,13 +1110,16 @@ Expr DatatypeConstructor::computeGroundTerm(Type t, // for each selector, get a ground term std::vector< Type > instTypes; std::vector< Type > paramTypes; - if( DatatypeType(t).isParametric() ){ + bool isParam = static_cast(t).isParametric(); + if (isParam) + { paramTypes = DatatypeType(t).getDatatype().getParameters(); instTypes = DatatypeType(t).getParamTypes(); } for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { Type selType = SelectorType((*i).getSelector().getType()).getRangeType(); - if( DatatypeType(t).isParametric() ){ + if (isParam) + { selType = selType.substitute( paramTypes, instTypes ); } Expr arg; @@ -1105,10 +1129,13 @@ Expr DatatypeConstructor::computeGroundTerm(Type t, arg = itgt->second; }else{ const Datatype & dt = DatatypeType(selType).getDatatype(); - arg = dt.computeGroundTerm( selType, processing ); + arg = dt.computeGroundTerm(selType, processing, isValue); } - }else{ - arg = selType.mkGroundTerm(); + } + else + { + // call mkGroundValue or mkGroundTerm based on isValue + arg = isValue ? selType.mkGroundValue() : selType.mkGroundTerm(); } if( arg.isNull() ){ Debug("datatypes") << "...unable to construct arg of " << (*i).getName() << std::endl; @@ -1120,9 +1147,10 @@ Expr DatatypeConstructor::computeGroundTerm(Type t, } Expr groundTerm = getConstructor().getExprManager()->mkExpr(kind::APPLY_CONSTRUCTOR, groundTerms); - if( groundTerm.getType()!=t ){ - Assert(Datatype::datatypeOf(d_constructor).isParametric()); - //type is ambiguous, must apply type ascription + if (isParam) + { + Assert( Datatype::datatypeOf( d_constructor ).isParametric() ); + // type is parametric, must apply type ascription Debug("datatypes-gt") << "ambiguous type for " << groundTerm << ", ascribe to " << t << std::endl; groundTerms[0] = getConstructor().getExprManager()->mkExpr(kind::APPLY_TYPE_ASCRIPTION, getConstructor().getExprManager()->mkConst(AscriptionType(getSpecializedConstructorType(t))), diff --git a/src/expr/datatype.h b/src/expr/datatype.h index b7a2721ab..b32001a89 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -528,10 +528,24 @@ class CVC4_PUBLIC DatatypeConstructor { Cardinality computeCardinality(Type t, std::vector& processing) const; /** compute whether this datatype is well-founded */ bool computeWellFounded(std::vector& processing) const; - /** compute ground term */ + /** compute ground term + * + * This method is used for constructing a term that is an application + * of this constructor whose type is t. + * + * The argument processing is the set of datatype types we are currently + * traversing. This is used to avoid infinite loops. + * + * The argument gt caches the ground terms we have computed so far. + * + * The argument isValue is whether we are constructing a constant value. If + * this flag is false, we are constructing a canonical ground term that is + * not necessarily constant. + */ Expr computeGroundTerm(Type t, std::vector& processing, - std::map& gt) const; + std::map& gt, + bool isValue) const; /** compute shared selectors * This computes the maps d_shared_selectors and d_shared_selector_index. */ @@ -821,6 +835,16 @@ public: * type if this datatype is parametric. */ Expr mkGroundTerm(Type t) const; + /** Make ground value + * + * Same as above, but constructs a constant value instead of a ground term. + * These two notions typically coincide. However, for uninterpreted sorts, + * they do not: mkGroundTerm returns a fresh variable whereas mkValue returns + * an uninterpreted constant. The motivation for mkGroundTerm is that + * unintepreted constants should never appear in lemmas. The motivation for + * mkGroundValue is for things like type enumeration and model construction. + */ + Expr mkGroundValue(Type t) const; /** * Get the DatatypeType associated to this Datatype. Can only be @@ -994,6 +1018,8 @@ public: mutable int d_well_founded; /** cache of ground term for this datatype */ mutable std::map d_ground_term; + /** cache of ground values for this datatype */ + mutable std::map d_ground_value; /** cache of shared selectors for this datatype */ mutable std::map > > d_shared_sel; @@ -1043,8 +1069,21 @@ public: std::vector& u_assume) const; /** compute whether this datatype is well-founded */ bool computeWellFounded(std::vector& processing) const; - /** compute ground term */ - Expr computeGroundTerm(Type t, std::vector& processing) const; + /** compute ground term + * + * This method checks if there is a term of this datatype whose type is t + * that is finitely constructable. As needed, it traverses its subfield types. + * + * The argument processing is the set of datatype types we are currently + * traversing. + * + * The argument isValue is whether we are constructing a constant value. If + * this flag is false, we are constructing a canonical ground term that is + * not necessarily constant. + */ + Expr computeGroundTerm(Type t, + std::vector& processing, + bool isValue) const; /** Get the shared selector * * This returns the index^th (constructor-agnostic) @@ -1056,6 +1095,10 @@ public: * this returns the term sel_{dtt}^{t,index}. */ Expr getSharedSelector(Type dtt, Type t, unsigned index) const; + /** + * Helper for mkGroundTerm and mkGroundValue above. + */ + Expr mkGroundTermInternal(Type t, bool isValue) const; };/* class Datatype */ /** diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 76c318b2e..31f21667a 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -101,6 +101,12 @@ Expr Type::mkGroundTerm() const { return d_typeNode->mkGroundTerm().toExpr(); } +Expr Type::mkGroundValue() const +{ + NodeManagerScope nms(d_nodeManager); + return d_typeNode->mkGroundValue().toExpr(); +} + bool Type::isSubtypeOf(Type t) const { NodeManagerScope nms(d_nodeManager); return d_typeNode->isSubtypeOf(*t.d_typeNode); diff --git a/src/expr/type.h b/src/expr/type.h index 587df07ee..529c40930 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -190,6 +190,20 @@ protected: */ Expr mkGroundTerm() const; + /** + * Construct and return a ground value for this Type. Throws an + * exception if this type is not well-founded. + * + * This is the same as mkGroundTerm, but constructs a constant value instead + * of a canonical ground term. These two notions typically coincide. However, + * for uninterpreted sorts, they do not: mkGroundTerm returns a fresh variable + * whereas mkValue returns an uninterpreted constant. The motivation for + * mkGroundTerm is that unintepreted constants should never appear in lemmas. + * The motivation for mkGroundValue is for e.g. type enumeration and model + * construction. + */ + Expr mkGroundValue() const; + /** * Is this type a subtype of the given type? */ diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index b3c8592ed..0a04d7efe 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -23,6 +23,7 @@ #include "options/expr_options.h" #include "options/quantifiers_options.h" #include "options/uf_options.h" +#include "theory/type_enumerator.h" using namespace std; @@ -292,6 +293,12 @@ Node TypeNode::mkGroundTerm() const { return kind::mkGroundTerm(*this); } +Node TypeNode::mkGroundValue() const +{ + theory::TypeEnumerator te(*this); + return *te; +} + bool TypeNode::isSubtypeOf(TypeNode t) const { if(*this == t) { return true; diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 1fcd64fc7..610dd3b62 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -474,6 +474,14 @@ public: */ Node mkGroundTerm() const; + /** + * Construct and return a ground value of this type. If the type is + * not well founded, this function throws an exception. + * + * @return a ground value of the type + */ + Node mkGroundValue() const; + /** * Is this type a subtype of the given type? */ diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp index de97227e0..5de04a9c3 100644 --- a/src/theory/datatypes/type_enumerator.cpp +++ b/src/theory/datatypes/type_enumerator.cpp @@ -97,27 +97,41 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){ } } - Node DatatypesEnumerator::getCurrentTerm( unsigned index ){ - Debug("dt-enum-debug") << "Get current term at " << index << " " << d_type << std::endl; + Node DatatypesEnumerator::getCurrentTerm(unsigned index) + { + Debug("dt-enum-debug") << "Get current term at " << index << " " << d_type + << std::endl; Node ret; - if( indexmkConst(UninterpretedConstant(d_type.toType(), d_size_limit)); - }else{ - //no top-level variables + if (index < d_has_debruijn) + { + if (d_child_enum) + { + ret = NodeManager::currentNM()->mkConst( + UninterpretedConstant(d_type.toType(), d_size_limit)); + } + else + { + // no top-level variables return Node::null(); } - }else{ - Debug("dt-enum-debug") << "Look at constructor " << (index - d_has_debruijn) << std::endl; + } + else + { + Debug("dt-enum-debug") + << "Look at constructor " << (index - d_has_debruijn) << std::endl; DatatypeConstructor ctor = d_datatype[index - d_has_debruijn]; Debug("dt-enum-debug") << "Check last term..." << std::endl; - //we first check if the last argument (which is forced to make sum of iterated arguments equal to d_size_limit) is defined + // we first check if the last argument (which is forced to make sum of + // iterated arguments equal to d_size_limit) is defined Node lc; - if( ctor.getNumArgs()>0 ){ + if (ctor.getNumArgs() > 0) + { Assert(index < d_sel_types.size()); Assert(ctor.getNumArgs() - 1 < d_sel_types[index].size()); - lc = getTermEnum( d_sel_types[index][ctor.getNumArgs()-1], d_size_limit - d_sel_sum[index] ); - if( lc.isNull() ){ + lc = getTermEnum(d_sel_types[index][ctor.getNumArgs() - 1], + d_size_limit - d_sel_sum[index]); + if (lc.isNull()) + { Debug("dt-enum-debug") << "Current infeasible." << std::endl; return Node::null(); } @@ -125,37 +139,49 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){ Debug("dt-enum-debug") << "Get constructor..." << std::endl; NodeBuilder<> b(kind::APPLY_CONSTRUCTOR); Type typ; - if( d_datatype.isParametric() ){ + if (d_datatype.isParametric()) + { typ = ctor.getSpecializedConstructorType(d_type.toType()); - b << NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, - NodeManager::currentNM()->mkConst(AscriptionType(typ)), Node::fromExpr( ctor.getConstructor() ) ); - }else{ + b << NodeManager::currentNM()->mkNode( + kind::APPLY_TYPE_ASCRIPTION, + NodeManager::currentNM()->mkConst(AscriptionType(typ)), + Node::fromExpr(ctor.getConstructor())); + } + else + { b << ctor.getConstructor(); } Debug("dt-enum-debug") << "Get arguments..." << std::endl; - if( ctor.getNumArgs()>0 ){ + if (ctor.getNumArgs() > 0) + { Assert(index < d_sel_types.size()); Assert(index < d_sel_index.size()); Assert(d_sel_types[index].size() == ctor.getNumArgs()); Assert(d_sel_index[index].size() == ctor.getNumArgs() - 1); - for( int i=0; i<(int)(ctor.getNumArgs()-1); i++ ){ - Node c = getTermEnum( d_sel_types[index][i], d_sel_index[index][i] ); + for (int i = 0; i < (int)(ctor.getNumArgs() - 1); i++) + { + Node c = getTermEnum(d_sel_types[index][i], d_sel_index[index][i]); Assert(!c.isNull()); b << c; } b << lc; } Node nnn = Node(b); - Debug("dt-enum-debug") << "Return... " << nnn << std::endl; + Debug("dt-enum-debug") << "Return... " << nnn << std::endl; ret = nnn; } - if( !d_child_enum && d_has_debruijn ){ - Node nret = DatatypesRewriter::normalizeCodatatypeConstant( ret ); - if( nret!=ret ){ - if( nret.isNull() ){ + if (!d_child_enum && d_has_debruijn) + { + Node nret = DatatypesRewriter::normalizeCodatatypeConstant(ret); + if (nret != ret) + { + if (nret.isNull()) + { Trace("dt-enum-nn") << "Invalid constant : " << ret << std::endl; - }else{ + } + else + { Trace("dt-enum-nn") << "Non-normal constant : " << ret << std::endl; Trace("dt-enum-nn") << " ...normal form is : " << nret << std::endl; } @@ -166,59 +192,133 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){ return ret; } - void DatatypesEnumerator::init(){ - //Assert(type.isDatatype()); - Debug("dt-enum") << "datatype is datatype? " << d_type.isDatatype() << std::endl; + void DatatypesEnumerator::init() + { + 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( d_type.toType() ); - Debug("dt-enum") << " " << d_datatype.isInterpretedFinite( d_type.toType() ) << std::endl; + Debug("dt-enum") << "properties : " << d_datatype.isCodatatype() << " " + << d_datatype.isRecursiveSingleton(d_type.toType()); + Debug("dt-enum") << " " << d_datatype.isInterpretedFinite(d_type.toType()) + << std::endl; - if( d_datatype.isCodatatype() && hasCyclesDt( d_datatype ) ){ - //start with uninterpreted constant - d_zeroCtor = 0; + if (d_datatype.isCodatatype() && hasCyclesDt(d_datatype)) + { + // start with uninterpreted constant d_has_debruijn = 1; - d_sel_types.push_back( std::vector< TypeNode >() ); - d_sel_index.push_back( std::vector< unsigned >() ); - d_sel_sum.push_back( -1 ); - }else{ - // find the "zero" constructor via mkGroundTerm + d_sel_types.push_back(std::vector()); + d_sel_index.push_back(std::vector()); + d_sel_sum.push_back(-1); + } + else + { + // find the "zero" term via mkGroundTerm Debug("dt-enum-debug") << "make ground term..." << std::endl; - Node t = d_type.mkGroundTerm(); - Debug("dt-enum-debug") << "done : " << t << std::endl; - Assert(t.getKind() == kind::APPLY_CONSTRUCTOR); - // start with the constructor for which a ground term is constructed - d_zeroCtor = datatypes::utils::indexOf(t.getOperator()); + // Start with the ground term constructed via mkGroundValue, which does + // a traversal over the structure of the datatype to find a finite term. + // Notice that mkGroundValue may be dependent upon extracting the first + // value of type enumerators for *other non-datatype* subfield types of + // this datatype. Since datatypes can not be embedded in non-datatype + // types (e.g. (Array D D) cannot be a subfield type of datatype D), this + // call is guaranteed to avoid infinite recursion. + d_zeroTerm = Node::fromExpr(d_datatype.mkGroundValue(d_type.toType())); + d_zeroTermActive = true; + Debug("dt-enum-debug") << "done : " << d_zeroTerm << std::endl; + Assert(d_zeroTerm.getKind() == kind::APPLY_CONSTRUCTOR); d_has_debruijn = 0; } - Debug("dt-enum") << "zero ctor : " << d_zeroCtor << std::endl; - d_ctor = d_zeroCtor; - for( unsigned i=0; i() ); - d_sel_index.push_back( std::vector< unsigned >() ); - d_sel_sum.push_back( -1 ); + Debug("dt-enum") << "zero term : " << d_zeroTerm << std::endl; + d_ctor = 0; + for (unsigned i = 0, ncons = d_datatype.getNumConstructors(); i < ncons; ++i) + { + d_sel_types.push_back(std::vector()); + d_sel_index.push_back(std::vector()); + d_sel_sum.push_back(-1); DatatypeConstructor ctor = d_datatype[i]; Type typ; - if( d_datatype.isParametric() ){ + if (d_datatype.isParametric()) + { typ = ctor.getSpecializedConstructorType(d_type.toType()); } - for( unsigned a = 0; a < ctor.getNumArgs(); ++a ){ + for (unsigned a = 0; a < ctor.getNumArgs(); ++a) + { TypeNode tn; - if( d_datatype.isParametric() ){ - tn = TypeNode::fromType( typ )[a]; - }else{ + if (d_datatype.isParametric()) + { + tn = TypeNode::fromType(typ)[a]; + } + else + { tn = Node::fromExpr(ctor[a].getSelector()).getType()[1]; } - d_sel_types.back().push_back( tn ); - d_sel_index.back().push_back( 0 ); + d_sel_types.back().push_back(tn); + d_sel_index.back().push_back(0); } - if( !d_sel_index.back().empty() ){ + if (!d_sel_index.back().empty()) + { d_sel_index.back().pop_back(); } } d_size_limit = 0; - //set up initial conditions (should always succeed) - ++*this; //increment( d_ctor ); + if (!d_zeroTermActive) + { + // Set up initial conditions (should always succeed). Here, we are calling + // the increment function of this class, which ensures a term is ready to + // read via a dereference of this class. We use the same method for + // setting up the first term, if it is not already set up + // (d_zeroTermActive) using the increment function, for uniformity. + ++*this; + } AlwaysAssert(!isFinished()); -} + } + + DatatypesEnumerator& DatatypesEnumerator::operator++() + { + Debug("dt-enum-debug") << ": increment " << this << std::endl; + if (d_zeroTermActive) + { + d_zeroTermActive = false; + } + unsigned prevSize = d_size_limit; + while (d_ctor < d_has_debruijn + d_datatype.getNumConstructors()) + { + // increment at index + while (increment(d_ctor)) + { + Node n = getCurrentTerm(d_ctor); + if (!n.isNull()) + { + if (n == d_zeroTerm) + { + d_zeroTerm = Node::null(); + } + else + { + return *this; + } + } + } + // Here, we need to step from the current constructor to the next one + // Go to the next constructor + d_ctor = d_ctor + 1; + 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(d_type.toType())) + { + d_size_limit++; + d_ctor = 0; + for (unsigned i = 0; i < d_sel_sum.size(); i++) + { + d_sel_sum[i] = -1; + } + } + } + } + return *this; + } diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index a294324fa..6f7fc4286 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -41,8 +41,10 @@ class DatatypesEnumerator : public TypeEnumeratorBase { TypeNode d_type; /** The datatype constructor we're currently enumerating */ unsigned d_ctor; - /** The "first" constructor to consider; it's non-recursive */ - unsigned d_zeroCtor; + /** The first term to consider in the enumeration */ + Node d_zeroTerm; + /** Whether we are currently considering the above term */ + bool d_zeroTermActive; /** list of type enumerators (one for each type in a selector argument) */ std::map< TypeNode, unsigned > d_te_index; std::vector< TypeEnumerator > d_children; @@ -85,7 +87,9 @@ class DatatypesEnumerator : public TypeEnumeratorBase { : TypeEnumeratorBase(type), d_tep(tep), d_datatype(DatatypeType(type.toType()).getDatatype()), - d_type(type) + d_type(type), + d_ctor(0), + d_zeroTermActive(false) { d_child_enum = false; init(); @@ -96,19 +100,22 @@ class DatatypesEnumerator : public TypeEnumeratorBase { : TypeEnumeratorBase(type), d_tep(tep), d_datatype(DatatypeType(type.toType()).getDatatype()), - d_type(type) + d_type(type), + d_ctor(0), + d_zeroTermActive(false) { d_child_enum = childEnum; init(); } - DatatypesEnumerator(const DatatypesEnumerator& de) : - TypeEnumeratorBase(de.getType()), - d_tep(de.d_tep), - d_datatype(de.d_datatype), - d_type(de.d_type), - d_ctor(de.d_ctor), - d_zeroCtor(de.d_zeroCtor) { - + DatatypesEnumerator(const DatatypesEnumerator& de) + : TypeEnumeratorBase(de.getType()), + d_tep(de.d_tep), + d_datatype(de.d_datatype), + d_type(de.d_type), + d_ctor(de.d_ctor), + d_zeroTerm(de.d_zeroTerm), + d_zeroTermActive(de.d_zeroTermActive) + { for( std::map< TypeNode, unsigned >::const_iterator it = de.d_te_index.begin(); it != de.d_te_index.end(); ++it ){ d_te_index[it->first] = it->second; } @@ -134,45 +141,18 @@ class DatatypesEnumerator : public TypeEnumeratorBase { Node operator*() override { Debug("dt-enum-debug") << ": get term " << this << std::endl; - if(d_ctor < d_has_debruijn + d_datatype.getNumConstructors()) { + if (d_zeroTermActive) + { + return d_zeroTerm; + } + else if (d_ctor < d_has_debruijn + d_datatype.getNumConstructors()) + { return getCurrentTerm( d_ctor ); - } else { - throw NoMoreValuesException(getType()); } + throw NoMoreValuesException(getType()); } - DatatypesEnumerator& operator++() override - { - Debug("dt-enum-debug") << ": increment " << this << std::endl; - unsigned prevSize = d_size_limit; - while(d_ctor < d_has_debruijn+d_datatype.getNumConstructors()) { - //increment at index - while( increment( d_ctor ) ){ - Node n = getCurrentTerm( d_ctor ); - if( !n.isNull() ){ - return *this; - } - } - // Here, we need to step from the current constructor to the next one - - // Find the next constructor (only complicated by the notion of the "zero" constructor - d_ctor = (d_ctor == d_zeroCtor) ? 0 : d_ctor + 1; - if(d_ctor == d_zeroCtor) { - ++d_ctor; - } - 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( d_type.toType() ) ){ - d_size_limit++; - d_ctor = d_zeroCtor; - for( unsigned i=0; iinitialize(); for( std::map::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) { Node op = it->first; @@ -315,8 +316,10 @@ bool FullModelChecker::preProcessBuildModel(TheoryModel* m) { for( unsigned i=0; igetNumAssertedQuantifiers(); i++ ){ @@ -522,7 +525,9 @@ void FullModelChecker::preInitializeType( FirstOrderModelFmc * fm, TypeNode tn ) d_preinitialized_types[tn] = true; if (!tn.isFunction() || options::ufHo()) { + Trace("fmc") << "Get model basis term " << tn << "..." << std::endl; Node mb = fm->getModelBasisTerm(tn); + Trace("fmc") << "...return " << mb << std::endl; // if the model basis term does not exist in the model, // either add it directly to the model's equality engine if no other terms // of this type exist, or otherwise assert that it is equal to the first diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index b1171f152..47355aa81 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -306,6 +306,8 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) return false; } + Trace("model-builder") + << "TheoryEngineModelBuilder: Preprocess build model..." << std::endl; // model-builder specific initialization if (!preProcessBuildModel(tm)) { @@ -315,6 +317,8 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) return false; } + Trace("model-builder") + << "TheoryEngineModelBuilder: Add assignable subterms..." << std::endl; // Loop through all terms and make sure that assignable sub-terms are in the // equality engine // Also, record #eqc per type (for finite model finding) diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 134f42610..7e52501c2 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1158,6 +1158,7 @@ set(regress_1_tests regress1/datatypes/dt-param-card4-unsat.smt2 regress1/datatypes/error.cvc regress1/datatypes/issue3266-small.smt2 + regress1/datatypes/issue-variant-dt-zero.smt2 regress1/datatypes/manos-model.smt2 regress1/decision/error3.smtv1.smt2 regress1/decision/quant-Arrays_Q1-noinfer.smt2 @@ -1392,6 +1393,7 @@ set(regress_1_tests regress1/quantifiers/isaplanner-goal20.smt2 regress1/quantifiers/issue2970-string-var-elim.smt2 regress1/quantifiers/issue3250-syg-inf-q.smt2 + regress1/quantifiers/issue3316.smt2 regress1/quantifiers/issue3317.smt2 regress1/quantifiers/issue993.smt2 regress1/quantifiers/javafe.ast.StmtVec.009.smt2 diff --git a/test/regress/regress1/datatypes/issue-variant-dt-zero.smt2 b/test/regress/regress1/datatypes/issue-variant-dt-zero.smt2 new file mode 100644 index 000000000..f2a5b81c8 --- /dev/null +++ b/test/regress/regress1/datatypes/issue-variant-dt-zero.smt2 @@ -0,0 +1,16 @@ +; COMMAND-LINE: --fmf-fun-rlv --no-check-models +; EXPECT: sat +(set-info :smt-lib-version 2.5) +(set-option :produce-models true) +(set-logic ALL) +(declare-datatypes () ((a0(c0$0)(c0$1(c0$1$0 String)(c0$1$1 Int))(c0$2(c0$2$0 Bool)(c0$2$1 Int)(c0$2$2 String))) + (a1(c1$0)(c1$1)(c1$2)) + (a2(c2$0(c2$0$0 Int)(c2$0$1 a0)(c2$0$2 String)(c2$0$3 a3)(c2$0$4 String)(c2$0$5 Bool))) + (a3(c3$0(c3$0$0 a7)(c3$0$1 a1)(c3$0$2 a5)(c3$0$3 a6)(c3$0$4 Int)(c3$0$5 Bool)(c3$0$6 Bool))(c3$1(c3$1$0 String))) + (a4(c4$0(c4$0$0 String)(c4$0$1 a2)(c4$0$2 String))(c4$1(c4$1$0 a0)(c4$1$1 a4)(c4$1$2 a4)(c4$1$3 a7))(c4$2)) + (a5(c5$0(c5$0$0 a2))(c5$1)(c5$2)(c5$3(c5$3$0 a0))(c5$4)(c5$5(c5$5$0 a4)(c5$5$1 Int))(c5$6)) + (a6(c6$0(c6$0$0 a7)(c6$0$1 a7)(c6$0$2 String))(c6$1)(c6$2)(c6$3)(c6$4)(c6$5)(c6$6)) + (a7(c7$0(c7$0$0 a2)(c7$0$1 Int))(c7$1(c7$1$0 a4)(c7$1$1 Int)(c7$1$2 Bool))))) +(define-funs-rec ((f0((v0 a6))a4)) + (c4$2)) +(check-sat) diff --git a/test/regress/regress1/quantifiers/issue3316.smt2 b/test/regress/regress1/quantifiers/issue3316.smt2 new file mode 100644 index 000000000..320a57790 --- /dev/null +++ b/test/regress/regress1/quantifiers/issue3316.smt2 @@ -0,0 +1,22 @@ +; COMMAND-LINE: --fmf-fun-rlv --no-check-models +; EXPECT: sat +(set-info :smt-lib-version 2.5) +(set-option :produce-models true) +(set-logic ALL) +(declare-datatypes () ((a0(c0$0)(c0$1(c0$1$0 String)(c0$1$1 Int))(c0$2(c0$2$0 Bool)(c0$2$1 Int)(c0$2$2 String))) + (a1(c1$0)(c1$1)(c1$2)) + (a2(c2$0(c2$0$0 Int)(c2$0$1 a0)(c2$0$2 String)(c2$0$3 a3)(c2$0$4 String)(c2$0$5 Bool))) + (a3(c3$0(c3$0$0 a7)(c3$0$1 a1)(c3$0$2 a5)(c3$0$3 a6)(c3$0$4 Int)(c3$0$5 Bool)(c3$0$6 Bool))(c3$1(c3$1$0 String))) + (a4(c4$0(c4$0$0 String)(c4$0$1 a2)(c4$0$2 String))(c4$1(c4$1$0 a0)(c4$1$1 a4)(c4$1$2 a4)(c4$1$3 a7))(c4$2)) + (a5(c5$0(c5$0$0 a2))(c5$1)(c5$2)(c5$3(c5$3$0 a0))(c5$4)(c5$5(c5$5$0 a4)(c5$5$1 Int))(c5$6)) + (a6(c6$0(c6$0$0 a7)(c6$0$1 a7)(c6$0$2 String))(c6$1)(c6$2)(c6$3)(c6$4)(c6$5)(c6$6)) + (a7(c7$0(c7$0$0 a2)(c7$0$1 Int))(c7$1(c7$1$0 a4)(c7$1$1 Int)(c7$1$2 Bool))))) +(define-funs-rec ((f3((v4 Bool))a7) + (f2()a6) + (f1((v1 a3)(v2 a1)(v3 Bool))String) + (f0((v0 a6))a4)) + ((c7$0 (c2$0 0 c0$0 "" (c3$1 "") "" true) 0) + c6$2 + "" + c4$2)) +(check-sat) -- 2.30.2