diff options
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/datatype.cpp | 118 | ||||
-rw-r--r-- | src/expr/datatype.h | 31 | ||||
-rw-r--r-- | src/expr/node.cpp | 7 |
3 files changed, 152 insertions, 4 deletions
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 39bdddbad..4f1fc82b1 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -28,6 +28,7 @@ #include "expr/node_manager.h" #include "expr/type.h" #include "options/set_language.h" +#include "options/datatypes_options.h" using namespace std; @@ -161,7 +162,7 @@ void Datatype::resolve(ExprManager* em, evalType.push_back(TypeNode::fromType(d_sygus_type)); TypeNode eval_func_type = nm->mkFunctionType(evalType); d_sygus_eval = nm->mkSkolem(name, eval_func_type, "sygus evaluation function").toExpr(); - } + } } void Datatype::addConstructor(const DatatypeConstructor& c) { @@ -180,6 +181,41 @@ void Datatype::setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ){ d_sygus_allow_all = allow_all; } +void Datatype::addSygusConstructor( CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs, + CVC4::Expr& let_body, std::vector< CVC4::Expr >& let_args, unsigned let_num_input_args ) { + Debug("dt-sygus") << "--> Add constructor " << cname << " to " << getName() << std::endl; + if( !let_body.isNull() ){ + Debug("dt-sygus") << " let body = " << let_body << ", args = " << let_args.size() << "," << let_num_input_args << std::endl; + //TODO : remove arguments not occurring in body + //if this is a self identity function, ignore + if( let_args.size()==0 && let_args[0]==let_body ){ + Debug("dt-sygus") << " identity function " << cargs[0] << " to " << getName() << std::endl; + //TODO + } + } + std::string name = getName() + "_" + cname; + std::string testerId("is-"); + testerId.append(name); + //checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); + //checkDeclaration(testerId, CHECK_UNDECLARED, SYM_VARIABLE); + CVC4::DatatypeConstructor c(name, testerId ); + c.setSygus( op, let_body, let_args, let_num_input_args ); + for( unsigned j=0; j<cargs.size(); j++ ){ + Debug("parser-sygus-debug") << " arg " << j << " : " << cargs[j] << std::endl; + std::stringstream sname; + sname << name << "_" << j; + c.addArg(sname.str(), cargs[j]); + } + addConstructor(c); +} + +void Datatype::addSygusConstructor( CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs ) { + CVC4::Expr let_body; + std::vector< CVC4::Expr > let_args; + unsigned let_num_input_args = 0; + addSygusConstructor( op, cname, cargs, let_body, let_args, let_num_input_args ); +} + void Datatype::setTuple() { PrettyCheckArgument(!d_resolved, this, "cannot set tuple to a finalized Datatype"); d_isTuple = true; @@ -584,6 +620,30 @@ const DatatypeConstructor& Datatype::operator[](std::string name) const { IllegalArgument(name, "No such constructor `%s' of datatype `%s'", name.c_str(), d_name.c_str()); } + +Expr Datatype::getSharedSelector( Type dtt, Type t, unsigned index ) const{ + PrettyCheckArgument(isResolved(), this, "this datatype is not yet resolved"); + std::map< Type, std::map< Type, std::map< unsigned, Expr > > >::iterator itd = d_shared_sel.find( dtt ); + if( itd!=d_shared_sel.end() ){ + std::map< Type, std::map< unsigned, Expr > >::iterator its = itd->second.find( t ); + if( its!=itd->second.end() ){ + std::map< unsigned, Expr >::iterator it = its->second.find( index ); + if( it!=its->second.end() ){ + return it->second; + } + } + } + //make the shared selector + Expr s; + NodeManager* nm = NodeManager::fromExprManager( d_self.getExprManager() ); + std::stringstream ss; + ss << "sel_" << index; + s = nm->mkSkolem(ss.str(), nm->mkSelectorType(TypeNode::fromType(dtt), TypeNode::fromType(t)), "is a shared selector", NodeManager::SKOLEM_NO_NOTIFY).toExpr(); + d_shared_sel[dtt][t][index] = s; + Trace("dt-shared-sel") << "Made " << s << " of type " << dtt << " -> " << t << std::endl; + return s; +} + Expr Datatype::getConstructor(std::string name) const { return (*this)[name].getConstructor(); } @@ -797,6 +857,7 @@ Expr DatatypeConstructor::getConstructor() const { Type DatatypeConstructor::getSpecializedConstructorType(Type returnType) const { PrettyCheckArgument(isResolved(), this, "this datatype constructor is not yet resolved"); + PrettyCheckArgument(returnType.isDatatype(), this, "cannot get specialized constructor type for non-datatype type"); ExprManagerScope ems(d_constructor); const Datatype& dt = Datatype::datatypeOf(d_constructor); PrettyCheckArgument(dt.isParametric(), this, "this datatype constructor is not parametric"); @@ -1011,6 +1072,30 @@ Expr DatatypeConstructor::computeGroundTerm( Type t, std::vector< Type >& proces return groundTerm; } +void DatatypeConstructor::computeSharedSelectors( Type domainType ) const { + if( d_shared_selectors[domainType].size()<getNumArgs() ){ + TypeNode ctype; + if( DatatypeType(domainType).isParametric() ){ + ctype = TypeNode::fromType( getSpecializedConstructorType( domainType ) ); + }else{ + ctype = TypeNode::fromType( d_constructor.getType() ); + } + Assert( ctype.isConstructor() ); + Assert( ctype.getNumChildren()-1==getNumArgs() ); + //compute the shared selectors + const Datatype& dt = Datatype::datatypeOf(d_constructor); + std::map< TypeNode, unsigned > counter; + for( unsigned j=0; j<ctype.getNumChildren()-1; j++ ){ + TypeNode t = ctype[j]; + Expr ss = dt.getSharedSelector( domainType, t.toType(), counter[t] ); + d_shared_selectors[domainType].push_back( ss ); + Assert( d_shared_selector_index[domainType].find( ss )==d_shared_selector_index[domainType].end() ); + d_shared_selector_index[domainType][ss] = j; + counter[t]++; + } + } +} + const DatatypeConstructorArg& DatatypeConstructor::operator[](size_t index) const { PrettyCheckArgument(index < getNumArgs(), index, "index out of bounds"); @@ -1069,6 +1154,37 @@ Expr DatatypeConstructorArg::getSelector() const { return d_selector; } +Expr DatatypeConstructor::getSelectorInternal( Type domainType, size_t index ) const { + PrettyCheckArgument(isResolved(), this, "cannot get an internal selector for an unresolved datatype constructor"); + PrettyCheckArgument(index < getNumArgs(), index, "index out of bounds"); + if( options::dtSharedSelectors() ){ + computeSharedSelectors( domainType ); + Assert( d_shared_selectors[domainType].size()==getNumArgs() ); + return d_shared_selectors[domainType][index]; + }else{ + return d_args[index].getSelector(); + } +} + +int DatatypeConstructor::getSelectorIndexInternal( Expr sel ) const { + PrettyCheckArgument(isResolved(), this, "cannot get an internal selector index for an unresolved datatype constructor"); + if( options::dtSharedSelectors() ){ + Assert( sel.getType().isSelector() ); + Type domainType = ((SelectorType)sel.getType()).getDomain(); + computeSharedSelectors( domainType ); + std::map< Expr, unsigned >::iterator its = d_shared_selector_index[domainType].find( sel ); + if( its!=d_shared_selector_index[domainType].end() ){ + return (int)its->second; + } + }else{ + unsigned sindex = Datatype::indexOf(sel); + if( getNumArgs() > sindex && d_args[sindex].getSelector() == sel ){ + return (int)sindex; + } + } + return -1; +} + Expr DatatypeConstructorArg::getConstructor() const { PrettyCheckArgument(isResolved(), this, "cannot get a associated constructor for argument of an unresolved datatype constructor"); diff --git a/src/expr/datatype.h b/src/expr/datatype.h index 456e70fd5..84588fef0 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -197,6 +197,10 @@ private: Expr d_sygus_let_body; std::vector< Expr > d_sygus_let_args; unsigned d_sygus_num_let_input_args; + + /** shared selectors */ + mutable std::map< Type, std::vector< Expr > > d_shared_selectors; + mutable std::map< Type, std::map< Expr, unsigned > > d_shared_selector_index; void resolve(ExprManager* em, DatatypeType self, const std::map<std::string, DatatypeType>& resolutions, @@ -226,6 +230,8 @@ private: bool computeWellFounded( std::vector< Type >& processing ) const throw(IllegalArgumentException); /** compute ground term */ Expr computeGroundTerm( Type t, std::vector< Type >& processing, std::map< Type, Expr >& gt ) const throw(IllegalArgumentException); + /** compute shared selectors */ + void computeSharedSelectors( Type domainType ) const; public: /** * Create a new Datatype constructor with the given name for the @@ -378,6 +384,17 @@ public: */ Expr getSelector(std::string name) const; + + /** + * Get the internal selector for a constructor argument. + */ + Expr getSelectorInternal( Type domainType, size_t index ) const; + + /** + * Get the index for the selector + */ + int getSelectorIndexInternal( Expr sel ) const; + /** * Get whether this datatype involves an external type. If so, * then we will pose additional requirements for sharing. @@ -506,6 +523,8 @@ private: mutable int d_well_founded; // ground term for this datatype mutable std::map< Type, Expr > d_ground_term; + // shared selectors + mutable std::map< Type, std::map< Type, std::map< unsigned, Expr > > > d_shared_sel; /** * Datatypes refer to themselves, recursively, and we have a @@ -549,7 +568,9 @@ private: /** compute whether this datatype is well-founded */ bool computeWellFounded( std::vector< Type >& processing ) const throw(IllegalArgumentException); /** compute ground term */ - Expr computeGroundTerm( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException); + Expr computeGroundTerm( Type t, std::vector< Type >& processing ) const throw(IllegalArgumentException); + /** Get the shared selector */ + Expr getSharedSelector( Type dtt, Type t, unsigned index ) const; public: /** Create a new Datatype of the given name. */ @@ -575,7 +596,11 @@ public: * allow_const : whether all constants are (implicitly) included in the grammar */ void setSygus( Type st, Expr bvl, bool allow_const, bool allow_all ); - + /** add sygus constructor */ + void addSygusConstructor( CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs ); + void addSygusConstructor( CVC4::Expr op, std::string& cname, std::vector< CVC4::Type >& cargs, + CVC4::Expr& let_body, std::vector< CVC4::Expr >& let_args, unsigned let_num_input_args ); + /** set tuple */ void setTuple(); @@ -726,7 +751,7 @@ public: * similarly-named constructors, the first is returned. */ const DatatypeConstructor& operator[](std::string name) const; - + /** * Get the constructor operator for the named constructor. * This is a linear search through the constructors, so in diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 262085a23..e45ca49e0 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -22,6 +22,8 @@ #include "base/output.h" #include "expr/attribute.h" +#include "theory/quantifiers/term_database.h" + using namespace std; @@ -111,6 +113,11 @@ bool NodeTemplate<ref_count>::hasBoundVar() { for(iterator i = begin(); i != end() && !hasBv; ++i) { hasBv = (*i).hasBoundVar(); } + if( !hasBv ){ + if( getKind()==kind::APPLY_UF && getOperator().hasAttribute(theory::SygusSynthFunVarListAttribute()) ){ + hasBv = true; + } + } } setAttribute(HasBoundVarAttr(), hasBv); setAttribute(HasBoundVarComputedAttr(), true); |