diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.cpp | 69 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.h | 2 |
2 files changed, 40 insertions, 31 deletions
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index e8bdf2083..40183fe9c 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -161,42 +161,53 @@ Node TermDbSygus::mkGeneric(const Datatype& dt, int c, std::map<int, Node>& pre) return mkGeneric(dt, c, var_count, pre); } +struct SygusToBuiltinAttributeId +{ +}; +typedef expr::Attribute<SygusToBuiltinAttributeId, Node> + SygusToBuiltinAttribute; + Node TermDbSygus::sygusToBuiltin( Node n, TypeNode tn ) { Assert( n.getType()==tn ); Assert( tn.isDatatype() ); - std::map< Node, Node >::iterator it = d_sygus_to_builtin[tn].find( n ); - if( it==d_sygus_to_builtin[tn].end() ){ - Trace("sygus-db-debug") << "SygusToBuiltin : compute for " << n << ", type = " << tn << std::endl; - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - if( n.getKind()==APPLY_CONSTRUCTOR ){ - unsigned i = Datatype::indexOf( n.getOperator().toExpr() ); - Assert( n.getNumChildren()==dt[i].getNumArgs() ); - std::map< TypeNode, int > var_count; - std::map< int, Node > pre; - for (unsigned j = 0, size = n.getNumChildren(); j < size; j++) - { - pre[j] = sygusToBuiltin( n[j], getArgType( dt[i], j ) ); - } - Node ret = mkGeneric(dt, i, var_count, pre); - Trace("sygus-db-debug") << "SygusToBuiltin : Generic is " << ret << std::endl; - d_sygus_to_builtin[tn][n] = ret; - return ret; - } - if (n.hasAttribute(SygusPrintProxyAttribute())) + + // has it already been computed? + if (n.hasAttribute(SygusToBuiltinAttribute())) + { + return n.getAttribute(SygusToBuiltinAttribute()); + } + + Trace("sygus-db-debug") << "SygusToBuiltin : compute for " << n + << ", type = " << tn << std::endl; + const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype(); + if (n.getKind() == APPLY_CONSTRUCTOR) + { + unsigned i = Datatype::indexOf(n.getOperator().toExpr()); + Assert(n.getNumChildren() == dt[i].getNumArgs()); + std::map<TypeNode, int> var_count; + std::map<int, Node> pre; + for (unsigned j = 0, size = n.getNumChildren(); j < size; j++) { - // this variable was associated by an attribute to a builtin node - return n.getAttribute(SygusPrintProxyAttribute()); + pre[j] = sygusToBuiltin(n[j], getArgType(dt[i], j)); } - Assert(isFreeVar(n)); - // map to builtin variable type - int fv_num = getVarNum(n); - Assert(!dt.getSygusType().isNull()); - TypeNode vtn = TypeNode::fromType(dt.getSygusType()); - Node ret = getFreeVar(vtn, fv_num); + Node ret = mkGeneric(dt, i, var_count, pre); + Trace("sygus-db-debug") + << "SygusToBuiltin : Generic is " << ret << std::endl; + n.setAttribute(SygusToBuiltinAttribute(), ret); return ret; - }else{ - return it->second; } + if (n.hasAttribute(SygusPrintProxyAttribute())) + { + // this variable was associated by an attribute to a builtin node + return n.getAttribute(SygusPrintProxyAttribute()); + } + Assert(isFreeVar(n)); + // map to builtin variable type + int fv_num = getVarNum(n); + Assert(!dt.getSygusType().isNull()); + TypeNode vtn = TypeNode::fromType(dt.getSygusType()); + Node ret = getFreeVar(vtn, fv_num); + return ret; } Node TermDbSygus::sygusSubstituted( TypeNode tn, Node n, std::vector< Node >& args ) { diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index 7ef9e6151..57a127d8d 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -187,8 +187,6 @@ class TermDbSygus { //------------------------------end enumerators //-----------------------------conversion from sygus to builtin - /** cache for sygusToBuiltin */ - std::map<TypeNode, std::map<Node, Node> > d_sygus_to_builtin; /** a cache of fresh variables for each type * * We store two versions of this list: |