generateDatatype now returns new declares for inner types

- Fixes issue #245 - New test
uclid-org · May 11, 2024 · 97e94b0 · 97e94b0
1 parent 25a9174
commit 97e94b0
Show file tree

Hide file tree

Showing 5 changed files with 55 additions and 12 deletions.
diff --git a/src/main/scala/uclid/smt/SMTLIB2Interface.scala b/src/main/scala/uclid/smt/SMTLIB2Interface.scala
@@ -131,18 +131,25 @@ trait SMTLIB2Base {
           case dt : DataType =>
             val typeName = dt.id
             val nameString = "((%s 0))".format(typeName)
-            val constructorsString = Utils.join(dt.cstors.map(c => {
-              val sels = Utils.join(c.inTypes.map(s => {
-                val inner = generateDatatype(s._2) 
-                val sel = "(%s %s)".format(Context.getFieldName(s._1), inner._1)
-                sel
-              }), " ")
-              val constru = "(%s %s)".format(c.id, sels)
-              constru
-            }), " ")
+            val (consNames : String, newTypesNames1 : List[String], newTypes1 : List[String]) = dt.cstors
+              .foldRight("", List.empty[String], List.empty[String]) {
+                (c, acc) => {
+                  val (_consNames : String, _newTypesNames1 : List[String], _newTypes1: List[String]) = c.inTypes
+                    .foldRight("", List.empty[String], List.empty[String]){
+                      (s, _acc) => {
+                      val (fldName, newTypeNames, newTypes) = generateDatatype(s._2)
+                      (_acc._1 + " " + "(%s %s)".format(Context.getFieldName(s._1), fldName),
+                        _acc._2 ++ newTypeNames, _acc._3 ++ newTypes)
+                    }
+                  }
+                  (acc._1 + " " + s"(${c.id} ${_consNames})",  
+                    acc._2 ++ _newTypesNames1, acc._3 ++ _newTypes1)
+                }
+            }
+            val constructorsString = consNames
             val newType = "(declare-datatypes %s ((%s)))".format(nameString, constructorsString)
             typeMap = typeMap.addSynonym(typeName, t)
-            (typeName, typeName :: Nil, newType :: List.empty)
+            (typeName, typeName :: newTypesNames1, newType :: newTypes1)
           case BoolType => 
             typeMap = typeMap.addSynonym("Bool", t)
             ("Bool", List.empty, List.empty)

diff --git a/src/test/scala/ParserSpec.scala b/src/test/scala/ParserSpec.scala
@@ -168,8 +168,8 @@ class ParserSpec extends AnyFlatSpec {
         assert (p.errors.size > 0)
     }
   }
-  "test-adt-23.ucl" should "parse successfully" in {
-    val fileModules = UclidMain.compile(ConfigCons.createConfig("test/test-adt-23.ucl"), lang.Identifier("main"))
+  "test-adt-24.ucl" should "parse successfully" in {
+    val fileModules = UclidMain.compile(ConfigCons.createConfig("test/test-adt-24.ucl"), lang.Identifier("main"))
     val instantiatedModules = UclidMain.instantiateModules(UclidMain.Config(), fileModules, lang.Identifier("main"))
     assert (instantiatedModules.size == 1)
   }

diff --git a/src/test/scala/VerifierSpec.scala b/src/test/scala/VerifierSpec.scala
@@ -128,6 +128,9 @@ class VerifierSanitySpec extends AnyFlatSpec {
   "test-adt-23-datatypegeneration.ucl" should "verify successfully." in {
     VerifierSpec.expectedFails("./test/test-adt-23-datatypegeneration.ucl", 0)
   }
+  "test-adt-25.ucl" should "verify successfully." in {
+    VerifierSpec.expectedFails("./test/test-adt-25.ucl", 0)
+  }
   "test-array-0.ucl" should "verify successfully." in {
     VerifierSpec.expectedFails("./test/test-array-0.ucl", 0)
   }

diff --git a/test/test-adt-23.ucl → test/test-adt-24.ucl b/test/test-adt-23.ucl → test/test-adt-24.ucl
diff --git a/test/test-adt-25.ucl b/test/test-adt-25.ucl
@@ -0,0 +1,33 @@
+
+
+module main {
+
+    type e_t = enum {X, Y, Z};
+
+    datatype adt_t = 
+        A (a: e_t) | B (b : e_t, c: e_t);
+
+
+    var adt1 : adt_t;
+    var adt2 : adt_t;
+
+    init {
+        adt1 = A(Y);
+        adt2 = B(Y, Y);
+    }
+
+    next {
+        adt1' = A(adt2.b);
+        adt2' = B(adt1.a, adt2.c);
+    }
+
+    property match: adt1.a == adt2.b;
+
+    control {
+        v = bmc(2);
+        check;
+        print_results;
+        v.print_cex_json();
+    }
+
+}