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

4 files changed, 98 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;
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index e773bf698..f766396a1 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1513,6 +1513,7 @@ REG1_TESTS = \
 	regress1/strings/type003.smt2 \
 	regress1/strings/username_checker_min.smt2 \
 	regress1/sygus/VC22_a.sy \
+	regress1/sygus/abv.sy \
 	regress1/sygus/array_search_2.sy \
 	regress1/sygus/array_search_5-Q-easy.sy \
 	regress1/sygus/array_sum_2_5.sy \
@@ -1546,6 +1547,7 @@ REG1_TESTS = \
 	regress1/sygus/inv-example.sy \
 	regress1/sygus/inv-unused.sy \
 	regress1/sygus/large-const-simp.sy \
+	regress1/sygus/let-bug-simp.sy \
 	regress1/sygus/list-head-x.sy \
 	regress1/sygus/logiccell_help.sy \
 	regress1/sygus/max.sy \
diff --git a/test/regress/regress1/sygus/abv.sy b/test/regress/regress1/sygus/abv.sy
new file mode 100644
index 000000000..6ce1a011a
--- /dev/null
+++ b/test/regress/regress1/sygus/abv.sy
@@ -0,0 +1,61 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic ABV)
+
+(define-sort AddrSort () (BitVec 32))
+(define-sort ValSort () (BitVec 8))
+(define-sort MemSort () (Array AddrSort ValSort))
+
+; Write the value y to index x
+(define-fun WriteArr 
+	; Args
+	((x AddrSort) (y ValSort) (arrIn MemSort)) 
+	
+	; Return value
+	MemSort
+	
+	; Function Body
+	(store arrIn x y)
+)
+
+; Read from index x
+(define-fun ReadArr 
+	; Args
+	((x AddrSort) (arrIn MemSort)) 
+	
+	; Return value
+	ValSort
+	
+	; Function Body
+	(select arrIn x)
+)
+
+
+(synth-fun f 
+	; Args
+	((x0 ValSort) (x1 ValSort) (idx0 AddrSort) (idx1 AddrSort) (mem MemSort))
+	
+	; Return value
+	ValSort
+    
+    	; Grammar
+    	(
+	(StartArray MemSort (
+		(WriteArr (Variable AddrSort) (Variable ValSort) StartArray)
+		(WriteArr (Variable AddrSort) (Variable ValSort) mem)))
+
+	(Start ValSort (
+		(let 
+			((m MemSort StartArray)) 
+			(bvadd 
+				(ReadArr (Variable AddrSort) m) 
+				(ReadArr (Variable AddrSort) m))))))
+)
+
+(declare-var a (BitVec 8))
+(declare-var b (BitVec 8))
+(declare-var c (BitVec 32))
+(declare-var d (BitVec 32))
+(declare-var e (Array (BitVec 32) (BitVec 8)))
+(constraint (=> (not (= c d)) (= (bvadd a b) (f a b c d e))))
+(check-synth)
diff --git a/test/regress/regress1/sygus/let-bug-simp.sy b/test/regress/regress1/sygus/let-bug-simp.sy
new file mode 100644
index 000000000..d570d5a21
--- /dev/null
+++ b/test/regress/regress1/sygus/let-bug-simp.sy
@@ -0,0 +1,22 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic LIA)
+
+(synth-fun f ((x0 Int) (x1 Int)) Bool
+(
+	(StartInt Int (5))
+
+	(Start Bool (
+		(let 
+			((z Int StartInt)) 
+			(or 
+				(= (Variable Int) z) 
+				(= (Variable Int) z)))))
+)
+)
+
+(declare-var a Int)
+(declare-var b Int)
+(constraint (=> (= a 5) (f a b)))
+(constraint (=> (= b 5) (f a b)))
+(check-synth)