Merge pull request #256 from uclid-org/fix-255

Declare types in the correct order

src/main/scala/uclid/smt/SMTLIB2Interface.scala

@@ -50,6 +50,9 @@ import org.json4s._
 import lang.Scope
 import lang.ExpressionEnvironment
 
+import scala.annotation.tailrec
+import scala.collection.mutable
+
 trait SMTLIB2Base {
   val smtlib2BaseLogger = Logger(classOf[SMTLIB2Base])
 
@@ -539,24 +542,52 @@ class SMTLIB2Interface(args: List[String], var disableLetify: Boolean=false) ext
   }
 
   override def preassert(e: Expr) {
-    val declCommands = new ListBuffer[(String, String)]()
+    val declCommands = new mutable.HashMap[String, String]()
     Context.findTypes(e).filter(typ => !typeMap.contains(typ)).foreach {
       newType => {
         val (name, newTypeNames, newTypes) = generateDatatype(newType)
-        (newTypeNames zip newTypes).foreach({case (n, typ) => declCommands.append((n, typ))})
+        (newTypeNames zip newTypes).foreach({case (n, typ) => declCommands += (n -> typ)})
       }
     }
 
-    // Figure out which type depends on which other type and then declare them in the right order.
     def dependsOn(d1: (String, String), d2: (String, String)) : Boolean = {
-      return d2._2.contains(d1._1)
+      // if the exact name is found in the body of the declaration, then it depends on it.
+      val body1 = d1._2.replaceAll("[()]", " ")
+      val name2 = s" ${d2._1} "
+      d1 != d2 && body1.contains(name2)
     }
-    val declCommandsSorted = declCommands.toList.sortWith(dependsOn)
-    declCommandsSorted.foreach{
-      decl => {
-        writeCommand(decl._2)
+
+    val dependsGraph = new mutable.HashMap[String, List[String]]()
+    declCommands.foreach(d1 => declCommands.foreach(d2 => {
+      if (dependsOn(d1, d2)) {
+        val d1deps = dependsGraph.getOrElse(d1._1, List())
+        dependsGraph.update(d1._1, d2._1 :: d1deps)
+      }
+    }))
+
+    @tailrec
+    def reduce(toWrite: Map[String, String], written: Set[String]): Unit = {
+      if (toWrite.isEmpty) {
+        return
       }
+      val change = new ListBuffer[String]()
+      toWrite.foreach(d => {
+        val depends = dependsGraph.getOrElse(d._1, List())
+        val dependsFiltered = depends.filter(d => !written.contains(d))
+        if (dependsFiltered == List()) {
+          writeCommand(d._2)
+          change.append(d._1)
+        }
+      })
+      if (change.isEmpty) {
+        throw new Utils.AssertionError(s"Didn't make progress writing declarations. The following are not declared: ${toWrite.keys}")
+      }
+      val newToWrite = toWrite.filter(d => !change.contains(d._1));
+      val newWritten = written ++ change
+      reduce(newToWrite, newWritten)
     }
+
+    reduce(declCommands.toMap, Set.empty)
   }
 
   override def check(produceModel: Boolean = true) : SolverResult = {

src/test/scala/SMTLIB2Spec.scala

@@ -445,6 +445,9 @@ class SMTLIB2Spec extends AnyFlatSpec {
   "issue-187b.ucl" should "verify all assertions." in {
     SMTLIB2Spec.expectedFails("./test/issue-187b.ucl", 0)
   }
+  "issue-255.ucl" should "faill single assertion." in {
+    SMTLIB2Spec.expectedFails("./test/issue-255.ucl", 1)
+  }
   "test-redundant-assign.ucl" should "verify all assertions." in {
     SMTLIB2Spec.expectedFails("./test/test-redundant-assign.ucl", 0)
   }

test/issue-255.ucl

@@ -0,0 +1,17 @@
+module main {
+    type t;
+    datatype a = A(x: t);
+
+    var y: a;
+    var z: t;
+
+    init {
+        assert y.x == z;
+    }
+
+    control {
+        bmc(0);
+        check;
+        print_results;
+    }
+}