Revert "Fix/oom"

sugarlyzer/tester/src/main/scala/sugarlyzer/tester/strategies/ProductStrategy.scala

@@ -32,6 +32,7 @@ object ProductStrategy extends AnalysisStrategy {
       spec: ProgramSpecification,
       tool: AnalysisTool
   ): IO[List[ProductAlarm]] = {
+    given AppConfig = appConfig
     println(s"Running analysis for ${spec.name}")
     if spec.name == "varbugs" then {
       val sharedPath = os.Path(appConfig.sharedPath)

sugarlyzer/tester/src/main/scala/sugarlyzer/tester/strategies/TransformationStrategy.scala

@@ -27,6 +27,7 @@ object TransformationStrategy extends AnalysisStrategy {
       spec: ProgramSpecification,
       tool: AnalysisTool
   ): IO[List[TransformationAlarm]] = {
+    given AppConfig = appConfig
     println(s"Running analysis for ${spec.name}")
     val workingDir = os.Path(appConfig.sharedPath) / os.RelPath(spec.rootDir)
     for {

sugarlyzer/tester/src/main/scala/sugarlyzer/tester/sugarc/PresenceCondition.scala

@@ -3,111 +3,83 @@ package sugarlyzer.tester.sugarc
 import com.microsoft.z3.{BoolExpr, Context, Status}
 import io.circe.Encoder
 import com.typesafe.scalalogging.Logger
-import scala.util.Using
 
-case class PresenceCondition(
-    configs: Set[Map[String, String]],
-    simplifiedCache: Option[String] = None
-) {
+case class PresenceCondition(ctx: Context, expr: BoolExpr) {
 
   def &&(other: PresenceCondition): PresenceCondition = {
-    val newConfigs = for {
-      c1     <- this.configs
-      c2     <- other.configs
-      merged <- mergeConfigs(c1, c2)
-    } yield merged
-    PresenceCondition(newConfigs)
+    val otherExpr =
+      if (other.ctx eq ctx) other.expr else other.expr.translate(ctx)
+    PresenceCondition(ctx, ctx.mkAnd(expr, otherExpr))
   }
 
   def ||(other: PresenceCondition): PresenceCondition = {
-    PresenceCondition(this.configs ++ other.configs)
+    val otherExpr =
+      if (other.ctx eq ctx) other.expr else other.expr.translate(ctx)
+    PresenceCondition(ctx, ctx.mkOr(expr, otherExpr))
   }
 
   def simplify: PresenceCondition = {
-    val simplifiedStr = Using.resource(new Context()) { ctx =>
-      toZ3(ctx).simplify().toString
-    }
-    this.copy(simplifiedCache = Some(simplifiedStr))
+    PresenceCondition(ctx, expr.simplify().asInstanceOf[BoolExpr])
   }
 
-  def isSatisfiable: Boolean = configs.nonEmpty
+  def isSatisfiable: Boolean = {
+    val solver = ctx.mkSolver()
+    solver.add(expr)
+    solver.check() == Status.SATISFIABLE
+  }
 
   def getModel: String = {
-    if (configs.isEmpty) return "Unsatisfiable"
-    Using.resource(new Context()) { ctx =>
-      val solver = ctx.mkSolver()
-      solver.add(toZ3(ctx))
-      if (solver.check() == Status.SATISFIABLE) solver.getModel.toString
-      else "Unsatisfiable"
+    val solver = ctx.mkSolver()
+    solver.add(expr)
+    if (solver.check() == Status.SATISFIABLE) {
+      solver.getModel.toString
+    } else {
+      "Unsatisfiable"
     }
   }
 
   def numConsts: Int = {
-    if (configs.isEmpty) return 0
-    Using.resource(new Context()) { ctx =>
-      val solver = ctx.mkSolver()
-      solver.add(toZ3(ctx))
-      if (solver.check() == Status.SATISFIABLE)
-        solver.getModel.getConstDecls.length
-      else 0
-    }
-  }
-
-  private def mergeConfigs(
-      c1: Map[String, String],
-      c2: Map[String, String]
-  ): Option[Map[String, String]] = {
-    val keys = c1.keySet ++ c2.keySet
-    keys.foldLeft(Option(Map.empty[String, String])) { (accOpt, k) =>
-      accOpt.flatMap { acc =>
-        (c1.get(k), c2.get(k)) match {
-          case (Some(v1), Some(v2)) if v1.toLowerCase != v2.toLowerCase => None
-          case (Some(v1), _) => Some(acc + (k -> v1))
-          case (_, Some(v2)) => Some(acc + (k -> v2))
-          case _             => Some(acc)
-        }
-      }
-    }
-  }
-
-  private def toZ3(ctx: Context): BoolExpr = {
-    if (configs.isEmpty) return ctx.mkFalse()
-    val orClauses = configs.map { config =>
-      if (config.isEmpty) ctx.mkTrue()
-      else {
-        val andClauses = config.map { case (mac, value) =>
-          value.toLowerCase match {
-            case "true" | "y" =>
-              ctx.mkEq(ctx.mkConst(mac, ctx.mkBoolSort()), ctx.mkTrue())
-            case "false" | "n" =>
-              ctx.mkEq(ctx.mkConst(mac, ctx.mkBoolSort()), ctx.mkFalse())
-            case i if i.toIntOption.isDefined =>
-              ctx.mkEq(ctx.mkConst(mac, ctx.mkIntSort()), ctx.mkInt(i.toInt))
-            case s =>
-              ctx.mkEq(ctx.mkConst(mac, ctx.mkStringSort()), ctx.mkString(s))
-          }
-        }
-        if (andClauses.size == 1) andClauses.head
-        else ctx.mkAnd(andClauses.toSeq*)
-      }
+    val solver = ctx.mkSolver()
+    solver.add(expr)
+    if (solver.check() == Status.SATISFIABLE) {
+      solver.getModel.getConstDecls.length
+    } else {
+      0
     }
-    if (orClauses.size == 1) orClauses.head else ctx.mkOr(orClauses.toSeq*)
   }
 }
 
 object PresenceCondition {
   val logger = Logger[PresenceCondition]
-
-  given Encoder[PresenceCondition] = Encoder.instance { pc =>
-    io.circe.Json.fromString(pc.simplifiedCache.getOrElse {
-      Using.resource(new Context()) { ctx => pc.toZ3(ctx).toString }
-    })
+  given Encoder[PresenceCondition] {
+    def apply(pc: PresenceCondition): io.circe.Json = {
+      /* For simplicity, we just encode the string representation of the
+       * expression. */
+      /* In a real implementation, you might want to serialize the expression in
+       * a more structured way. */
+      io.circe.Json.fromString(pc.expr.toString)
+    }
   }
 
-  def vacuouslyTrue(ctx: Context = null): PresenceCondition =
-    PresenceCondition(Set(Map.empty))
+  def vacuouslyTrue(ctx: Context): PresenceCondition =
+    PresenceCondition(ctx, ctx.mkTrue())
 
   def fromTuples(tups: Iterable[(String, String)]): PresenceCondition = {
-    PresenceCondition(Set(tups.toMap))
+    /* Transform the list of tuples, which is of the form [("MACRO_NAME", TRUE)]
+     * into a conjunction of expressions */
+    val ctx = new Context()
+    val exprs = tups.map { case (mac, value) =>
+      value.toLowerCase match {
+        case "true" | "y" =>
+          ctx.mkEq(ctx.mkConst(mac, ctx.mkBoolSort()), ctx.mkTrue())
+        case "false" | "n" =>
+          ctx.mkEq(ctx.mkConst(mac, ctx.mkBoolSort()), ctx.mkFalse())
+        case i if i.toIntOption.isDefined =>
+          ctx.mkEq(ctx.mkConst(mac, ctx.mkIntSort()), ctx.mkInt(i))
+        case s =>
+          ctx.mkEq(ctx.mkConst(mac, ctx.mkStringSort()), ctx.mkString(s))
+      }
+    }
+    PresenceCondition(ctx, ctx.mkAnd(exprs.toSeq*))
   }
 }

sugarlyzer/tester/src/main/scala/sugarlyzer/tester/sugarc/SugarCRunner.scala

@@ -12,8 +12,6 @@ import java.util.concurrent.TimeoutException
 import scala.util.matching.Regex
 import com.microsoft.z3.Context
 import sugarlyzer.tester.tools.ToolAlarm
-import scala.util.Using
-import com.microsoft.z3.Status
 object SugarCRunner {
 
   val logger = Logger[SugarCRunner.type]
@@ -172,55 +170,27 @@ object SugarCRunner {
     // For each presence condition, parse the actual condition expression
     val conditionRegex: Regex =
       """__static_condition_renaming\(\"(.*)\", \"(.*)\"\);""".r
-
-    Using.resource(new Context()) { ctx =>
-      val exprs = for {
-        r <- results
-        l <- lines.filter(_.contains(s"__static_condition_renaming(\"$r\""))
-        expr <- l match {
-          case conditionRegex(oldName, newName) =>
-            logger.debug(
-              s"Found renamed presence condition: $oldName -> $newName"
-            )
-            Some(PresenceConditionParser.parse(ctx, newName))
-          case _ =>
-            logger.debug("Couldn't match regular expression")
-            None
-        }
-      } yield expr
-      val combined = exprs match {
-        case Nil      => ctx.mkTrue()
-        case e :: Nil => e
-        case _        => ctx.mkAnd(exprs*)
+    val ctx = new Context()
+    val exprs = for {
+      r <- results
+      l <- lines.filter(_.contains(s"__static_condition_renaming(\"$r\""))
+      expr <- l match {
+        case conditionRegex(oldName, newName) =>
+          logger.debug(
+            s"Found renamed presence condition: $oldName -> $newName"
+          )
+          Some(PresenceConditionParser.parse(ctx, newName))
+        case _ =>
+          logger.debug("Couldn't match regular expression")
+          None
       }
+    } yield expr
 
-      val solver = ctx.mkSolver()
-      solver.add(combined)
-      var configs = Set.empty[Map[String, String]]
-
-      while (solver.check() == Status.SATISFIABLE) {
-        val model = solver.getModel
-        val decls = model.getConstDecls
-
-        val config = decls.map { d =>
-          d.getName.toString -> model.getConstInterp(d).toString
-        }.toMap
-
-        configs = configs + config
-
-        val blockClauses = decls.map { d =>
-          ctx.mkEq(ctx.mkConst(d.getName, d.getRange), model.getConstInterp(d))
-        }
-
-        if (blockClauses.nonEmpty) {
-          solver.add(ctx.mkNot(ctx.mkAnd(blockClauses*)))
-        } else {
-          solver.add(ctx.mkFalse())
-        }
-      }
-
-      PresenceCondition(configs)
-
+    val combined = exprs match {
+      case Nil      => ctx.mkTrue()
+      case e :: Nil => e
+      case _        => ctx.mkAnd(exprs*)
     }
+    PresenceCondition(ctx, combined)
   }
 }

sugarlyzer/tester_test/src/main/scala/sugarlyzer/tester/test/MainApp.scala

@@ -97,7 +97,7 @@ object MainApp extends IOApp.Simple {
       alarm,
       os.Path("/resources/sample1.desugared.c")
     )
-    IO.println(s"Model: ${model.getModel.toString()}") >>
+    IO.println(s"Model: ${model.expr.toString()}") >>
       IO.println(s"Model feasibility is ${model.isSatisfiable}")
   }