Fix processing of nested Variable construct in sygus let bodies (#2351)

1 files changed, 13 insertions, 16 deletions

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 778766a61..dfeaca62b 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -676,7 +676,10 @@ void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index,
                               std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr,
                               CVC4::Type& ret, bool isNested ){
   if( sgt.d_gterm_type==SygusGTerm::gterm_op || sgt.d_gterm_type==SygusGTerm::gterm_let ){
-    Debug("parser-sygus") << "Add " << sgt.d_expr << " to datatype " << index << std::endl;
+    Debug("parser-sygus") << "Add " << sgt.d_expr << " to datatype " << index
+                          << ", isLet = "
+                          << (sgt.d_gterm_type == SygusGTerm::gterm_let)
+                          << std::endl;
     Kind oldKind;
     Kind newKind = kind::UNDEFINED_KIND;
     //convert to UMINUS if one child of MINUS
@@ -684,17 +687,6 @@ void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index,
       oldKind = kind::MINUS;
       newKind = kind::UMINUS;
     }
-    /*
-    //convert to IFF if boolean EQUAL
-    if( sgt.d_expr==getExprManager()->operatorOf(kind::EQUAL) ){
-      Type ctn = sgt.d_children[0].d_type;
-      std::map< CVC4::Type, CVC4::Type >::iterator it = sygus_to_builtin.find( ctn );
-      if( it != sygus_to_builtin.end() && it->second.isBoolean() ){
-        oldKind = kind::EQUAL;
-        newKind = kind::IFF;
-      }
-    }
-    */
     if( newKind!=kind::UNDEFINED_KIND ){
       Expr newExpr = getExprManager()->operatorOf(newKind);
       Debug("parser-sygus") << "Replace " << sgt.d_expr << " with " << newExpr << std::endl;
@@ -842,10 +834,15 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st
     if( sop.getKind() != kind::BUILTIN && ( sop.isConst() || cargs[sub_dt_index][0].empty() ) ){
       curr_t = sop.getType();
       Debug("parser-sygus") << ": it is constant/0-arg cons " << sop << " with type " << sop.getType() << ", debug=" << sop.isConst() << " " << cargs[sub_dt_index][0].size() << std::endl;
-      sygus_to_builtin_expr[t] = sop;
-      //store that term sop has dedicated sygus type t
-      if( d_sygus_bound_var_type.find( sop )==d_sygus_bound_var_type.end() ){
-        d_sygus_bound_var_type[sop] = t;
+      // only cache if it is a singleton datatype (has unique expr)
+      if (ops[sub_dt_index].size() == 1)
+      {
+        sygus_to_builtin_expr[t] = sop;
+        // store that term sop has dedicated sygus type t
+        if (d_sygus_bound_var_type.find(sop) == d_sygus_bound_var_type.end())
+        {
+          d_sygus_bound_var_type[sop] = t;
+        }
       }
     }else{
       std::vector< Expr > children;