Skip to content

Commit

Permalink
must be an exact word match to determine type dependency
Browse files Browse the repository at this point in the history
  • Loading branch information
FedericoAureliano committed Jul 4, 2024
1 parent 0cad476 commit 7b5a91e
Showing 1 changed file with 9 additions and 2 deletions.
11 changes: 9 additions & 2 deletions src/main/scala/uclid/smt/SMTLIB2Interface.scala
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,7 @@ import scala.collection.mutable.{Set => MutableSet}
import scala.collection.mutable.ListBuffer
import com.typesafe.scalalogging.Logger
import lang.Identifier

import org.json4s._
import lang.Scope
import lang.ExpressionEnvironment
Expand Down Expand Up @@ -549,10 +550,16 @@ class SMTLIB2Interface(args: List[String], var disableLetify: Boolean=false) ext
}
}

def dependsOn(d1: (String, String), d2: (String, String)) : Boolean = {
// 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 dependsGraph = new mutable.HashMap[String, List[String]]()
declCommands.foreach(d1 => declCommands.foreach(d2 => {
if (d1._1 != d2._1 && d1._2.contains(d2._1)) {
// d1 depends on d2
if (dependsOn(d1, d2)) {
val d1deps = dependsGraph.getOrElse(d1._1, List())
dependsGraph.update(d1._1, d2._1 :: d1deps)
}
Expand Down

0 comments on commit 7b5a91e

Please sign in to comment.