diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-11-01 17:06:33 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-11-01 17:06:33 -0500 |
commit | c547bd591891ffd9211ed3859b0a67423a708f25 (patch) | |
tree | b6a046cdc9cc474102640067fe1d9d67a012ae25 /src/expr | |
parent | 86c541cdf83e0b98def5a479d1da966f2e959408 (diff) |
Fix non-termination in datatype type enumerator (#3369)
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/datatype.cpp | 90 | ||||
-rw-r--r-- | src/expr/datatype.h | 51 | ||||
-rw-r--r-- | src/expr/type.cpp | 6 | ||||
-rw-r--r-- | src/expr/type.h | 14 | ||||
-rw-r--r-- | src/expr/type_node.cpp | 7 | ||||
-rw-r--r-- | src/expr/type_node.h | 8 |
6 files changed, 141 insertions, 35 deletions
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<Type>& 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<Type, Expr>& cache = isValue ? d_ground_value : d_ground_term; + std::map<Type, Expr>::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<Type> 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<Type>& processing) const +Expr Datatype::computeGroundTerm(Type t, + std::vector<Type>& 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<Type>& 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<Type>& processing, - std::map<Type, Expr>& gt) const + std::map<Type, Expr>& 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<DatatypeType>(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<Type>& processing) const; /** compute whether this datatype is well-founded */ bool computeWellFounded(std::vector<Type>& 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<Type>& processing, - std::map<Type, Expr>& gt) const; + std::map<Type, Expr>& 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<Type, Expr> d_ground_term; + /** cache of ground values for this datatype */ + mutable std::map<Type, Expr> d_ground_value; /** cache of shared selectors for this datatype */ mutable std::map<Type, std::map<Type, std::map<unsigned, Expr> > > d_shared_sel; @@ -1043,8 +1069,21 @@ public: std::vector<Type>& u_assume) const; /** compute whether this datatype is well-founded */ bool computeWellFounded(std::vector<Type>& processing) const; - /** compute ground term */ - Expr computeGroundTerm(Type t, std::vector<Type>& 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<Type>& 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 @@ -191,6 +191,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? */ bool isSubtypeOf(Type t) const; 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 @@ -475,6 +475,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? */ bool isSubtypeOf(TypeNode t) const; |