From 75003d97ad485f8840310e652a74872f5950538d Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 22 Dec 2015 13:44:05 +0100 Subject: Always split on constructor types for datatypes involving uninterpreted sorts when finite model finding is enabled, add regressions. --- src/expr/datatype.cpp | 78 ++++++++++++++++++++++++++++++++++++++++++--------- src/expr/datatype.h | 46 +++++++++++++++++++++--------- 2 files changed, 98 insertions(+), 26 deletions(-) (limited to 'src/expr') diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 09fe2cdc3..4ebc5071f 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -39,6 +39,8 @@ namespace expr { struct DatatypeConsIndexTag {}; struct DatatypeFiniteTag {}; struct DatatypeFiniteComputedTag {}; + struct DatatypeUFiniteTag {}; + struct DatatypeUFiniteComputedTag {}; }/* CVC4::expr::attr namespace */ }/* CVC4::expr namespace */ @@ -46,6 +48,8 @@ typedef expr::Attribute DatatypeIndexAtt typedef expr::Attribute DatatypeConsIndexAttr; typedef expr::Attribute DatatypeFiniteAttr; typedef expr::Attribute DatatypeFiniteComputedAttr; +typedef expr::Attribute DatatypeUFiniteAttr; +typedef expr::Attribute DatatypeUFiniteComputedAttr; const Datatype& Datatype::datatypeOf(Expr item) { ExprManagerScope ems(item); @@ -120,10 +124,13 @@ void Datatype::resolve(ExprManager* em, d_self = self; d_involvesExt = false; + d_involvesUt = false; for(const_iterator i = begin(); i != end(); ++i) { if( (*i).involvesExternalType() ){ d_involvesExt = true; - break; + } + if( (*i).involvesUninterpretedType() ){ + d_involvesUt = true; } } } @@ -245,18 +252,13 @@ bool Datatype::computeCardinalityRecSingleton( std::vector< Type >& processing, bool Datatype::isFinite() const throw(IllegalArgumentException) { CheckArgument(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); - TypeNode self = TypeNode::fromType(d_self); - // is this already in the cache ? if(self.getAttribute(DatatypeFiniteComputedAttr())) { return self.getAttribute(DatatypeFiniteAttr()); } - - Cardinality c = 0; for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { if(! (*i).isFinite()) { self.setAttribute(DatatypeFiniteComputedAttr(), true); @@ -269,6 +271,27 @@ bool Datatype::isFinite() const throw(IllegalArgumentException) { return true; } +bool Datatype::isUFinite() const throw(IllegalArgumentException) { + CheckArgument(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); + TypeNode self = TypeNode::fromType(d_self); + // is this already in the cache ? + if(self.getAttribute(DatatypeUFiniteComputedAttr())) { + return self.getAttribute(DatatypeUFiniteAttr()); + } + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + if(! (*i).isUFinite()) { + self.setAttribute(DatatypeUFiniteComputedAttr(), true); + self.setAttribute(DatatypeUFiniteAttr(), false); + return false; + } + } + self.setAttribute(DatatypeUFiniteComputedAttr(), true); + self.setAttribute(DatatypeUFiniteAttr(), true); + return true; +} + bool Datatype::isWellFounded() const throw(IllegalArgumentException) { CheckArgument(isResolved(), this, "this datatype is not yet resolved"); if( d_well_founded==0 ){ @@ -505,6 +528,10 @@ bool Datatype::involvesExternalType() const{ return d_involvesExt; } +bool Datatype::involvesUninterpretedType() const{ + return d_involvesUt; +} + void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self, const std::map& resolutions, const std::vector& placeholders, @@ -722,7 +749,7 @@ unsigned DatatypeConstructor::getNumSygusLetArgs() const { Expr DatatypeConstructor::getSygusLetArg( unsigned i ) const { CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); return d_sygus_let_args[i]; -} +} unsigned DatatypeConstructor::getNumSygusLetInputArgs() const { CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); @@ -733,7 +760,7 @@ bool DatatypeConstructor::isSygusIdFunc() const { CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); return d_sygus_let_args.size()==1 && d_sygus_let_args[0]==d_sygus_let_body; } - + Cardinality DatatypeConstructor::getCardinality() const throw(IllegalArgumentException) { CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); @@ -777,17 +804,13 @@ bool DatatypeConstructor::computeWellFounded( std::vector< Type >& processing ) bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) { CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); - // we're using some internals, so we have to set up this library context ExprManagerScope ems(d_constructor); - TNode self = Node::fromExpr(d_constructor); - // is this already in the cache ? if(self.getAttribute(DatatypeFiniteComputedAttr())) { return self.getAttribute(DatatypeFiniteAttr()); } - for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { if(! SelectorType((*i).getSelector().getType()).getRangeType().getCardinality().isFinite()) { self.setAttribute(DatatypeFiniteComputedAttr(), true); @@ -795,11 +818,31 @@ bool DatatypeConstructor::isFinite() const throw(IllegalArgumentException) { return false; } } - self.setAttribute(DatatypeFiniteComputedAttr(), true); self.setAttribute(DatatypeFiniteAttr(), true); return true; } +bool DatatypeConstructor::isUFinite() const throw(IllegalArgumentException) { + CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + // we're using some internals, so we have to set up this library context + ExprManagerScope ems(d_constructor); + TNode self = Node::fromExpr(d_constructor); + // is this already in the cache ? + if(self.getAttribute(DatatypeUFiniteComputedAttr())) { + return self.getAttribute(DatatypeUFiniteAttr()); + } + for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { + Type t = SelectorType((*i).getSelector().getType()).getRangeType(); + if(!t.isSort() && !t.getCardinality().isFinite()) { + self.setAttribute(DatatypeUFiniteComputedAttr(), true); + self.setAttribute(DatatypeUFiniteAttr(), false); + return false; + } + } + self.setAttribute(DatatypeUFiniteComputedAttr(), true); + self.setAttribute(DatatypeUFiniteAttr(), true); + return true; +} Expr DatatypeConstructor::computeGroundTerm( Type t, std::vector< Type >& processing, std::map< Type, Expr >& gt ) const throw(IllegalArgumentException) { // we're using some internals, so we have to set up this library context @@ -882,6 +925,15 @@ bool DatatypeConstructor::involvesExternalType() const{ return false; } +bool DatatypeConstructor::involvesUninterpretedType() const{ + for(const_iterator i = begin(); i != end(); ++i) { + if(SelectorType((*i).getSelector().getType()).getRangeType().isSort()) { + return true; + } + } + return false; +} + DatatypeConstructorArg::DatatypeConstructorArg(std::string name, Expr selector) : d_name(name), d_selector(selector), diff --git a/src/expr/datatype.h b/src/expr/datatype.h index c1ec475e5..1ea9fd6be 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -213,7 +213,7 @@ private: Type doParametricSubstitution(Type range, const std::vector< SortConstructorType >& paramTypes, const std::vector< DatatypeType >& paramReplacements); - + /** compute the cardinality of this datatype */ Cardinality computeCardinality( std::vector< Type >& processing ) const throw(IllegalArgumentException); /** compute whether this datatype is well-founded */ @@ -236,7 +236,7 @@ public: * constructor and tester aren't created until resolution time. */ DatatypeConstructor(std::string name, std::string tester); - + /** set sygus */ void setSygus( Expr op, Expr let_body, std::vector< Expr >& let_args, unsigned num_let_input_argus ); @@ -284,7 +284,7 @@ public: * Datatype must be resolved. */ Expr getTester() const; - + /** get sygus op */ Expr getSygusOp() const; /** get sygus let body */ @@ -297,7 +297,7 @@ public: unsigned getNumSygusLetInputArgs() const; /** is this a sygus identity function */ bool isSygusIdFunc() const; - + /** * Get the tester name for this Datatype constructor. */ @@ -334,6 +334,13 @@ public: * only be called for resolved constructors. */ bool isFinite() 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 isUFinite() const throw(IllegalArgumentException); /** * Returns true iff this Datatype constructor has already been @@ -373,6 +380,7 @@ public: * then we will pose additional requirements for sharing. */ bool involvesExternalType() const; + bool involvesUninterpretedType() const; };/* class DatatypeConstructor */ @@ -469,16 +477,17 @@ private: bool d_resolved; Type d_self; bool d_involvesExt; + bool d_involvesUt; /** information for sygus */ Type d_sygus_type; - Expr d_sygus_bvl; + Expr d_sygus_bvl; bool d_sygus_allow_const; bool d_sygus_allow_all; // "mutable" because computing the cardinality can be expensive, // and so it's computed just once, on demand---this is the cache mutable Cardinality d_card; - + // is this type a recursive singleton type mutable int d_card_rec_singleton; // if d_card_rec_singleton is true, @@ -555,7 +564,7 @@ public: * allow_const : whether all constants are (implicitly) included in the grammar */ void setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ); - + /** Get the name of this Datatype. */ inline std::string getName() const throw(); @@ -576,7 +585,7 @@ public: /** is this a co-datatype? */ inline bool isCodatatype() const; - + /** is this a sygus datatype? */ inline bool isSygus() const; @@ -594,6 +603,14 @@ public: * Datatype must be resolved or an exception is thrown. */ bool isFinite() const throw(IllegalArgumentException); + /** + * Return true iff this Datatype is finite (all constructors are + * finite, i.e., there are finitely many ground terms) under the + * assumption unintepreted sorts are finite. If the + * datatype is not well-founded, this function returns false. The + * Datatype must be resolved or an exception is thrown. + */ + bool isUFinite() const throw(IllegalArgumentException); /** * Return true iff this datatype is well-founded (there exist ground @@ -601,16 +618,16 @@ public: */ bool isWellFounded() const throw(IllegalArgumentException); - /** + /** * Return true iff this datatype is a recursive singleton */ bool isRecursiveSingleton() const throw(IllegalArgumentException); - - + + /** get number of recursive singleton argument types */ unsigned getNumRecursiveSingletonArgTypes() const throw(IllegalArgumentException); Type getRecursiveSingletonArgType( unsigned i ) const throw(IllegalArgumentException); - + /** * Construct and return a ground term of this Datatype. The * Datatype must be both resolved and well-founded, or else an @@ -678,7 +695,7 @@ public: * This Datatype must be resolved. */ Expr getConstructor(std::string name) const; - + /** get sygus type */ Type getSygusType() const; /** get sygus var list */ @@ -693,6 +710,7 @@ public: * then we will pose additional requirements for sharing. */ bool involvesExternalType() const; + bool involvesUninterpretedType() const; };/* class Datatype */ @@ -743,6 +761,7 @@ inline Datatype::Datatype(std::string name, bool isCo) : d_resolved(false), d_self(), d_involvesExt(false), + d_involvesUt(false), d_card(CardinalityUnknown()), d_card_rec_singleton(0), d_well_founded(0) { @@ -756,6 +775,7 @@ inline Datatype::Datatype(std::string name, const std::vector& params, boo d_resolved(false), d_self(), d_involvesExt(false), + d_involvesUt(false), d_card(CardinalityUnknown()), d_card_rec_singleton(0), d_well_founded(0) { -- cgit v1.2.3