Minor refactor datatypes sygus (#1673)

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: