Print clauses with -logSimplified[SMT]

uuverifiers · Jun 22, 2024 · 8bdd86a · 8bdd86a
1 parent 42e39ad
commit 8bdd86a
Showing 1 changed file with 50 additions and 27 deletions.
diff --git a/src/main/scala/hornconcurrency/VerificationLoop.scala b/src/main/scala/hornconcurrency/VerificationLoop.scala
@@ -202,41 +202,64 @@ class VerificationLoop(system : ParametricEncoder.System,
     var res : Either[Option[HornPreprocessor.Solution], Counterexample] = null
 
     while (res == null) {
+      println
+      println("Using invariants " + (invariants mkString ", "))
+      println
 
-    println
-    println("Using invariants " + (invariants mkString ", "))
-    println
+      val encoder =  new ParametricEncoder (system, invariants)
 
-    val encoder =  new ParametricEncoder (system, invariants)
+      ////////////////////////////////////////////////////////////////////////////
 
-    ////////////////////////////////////////////////////////////////////////////
+      val printAndExit =
+        printIntermediateClauseSets ||
+        lazabs.GlobalParameters.get.printHornSimplified ||
+        lazabs.GlobalParameters.get.printHornSimplifiedSMT
 
-    if (printIntermediateClauseSets) {
-      //val basename = fileName
-      //val suffix =
-      //  (for (inv <- invariants) yield (inv mkString "_")) mkString "--"
-      //val filename = basename + "-" + suffix + ".smt2"
+      if (printAndExit) {
+        if (printIntermediateClauseSets) {
+          println
+          println("Writing Horn clauses to " + fileName)
 
-      println
-      println("Writing Horn clauses to " + fileName)
-
-      val out = new java.io.FileOutputStream(fileName)
-      Console.withOut(out) {
-        val clauseFors =
-          for (c <- encoder.allClauses) yield {
-            val f = c.normalize.toFormula
-            // eliminate remaining operators like eps
-            Transform2Prenex(EquivExpander(PartialEvaluator(f)))
-          }
+          val out = new java.io.FileOutputStream(fileName)
+          Console.withOut(out){
+            val clauseFors =
+              for (c <- encoder.allClauses) yield {
+                val f = c.normalize.toFormula
+                // eliminate remaining operators like eps
+                Transform2Prenex(EquivExpander(PartialEvaluator(f)))
+              }
 
-        val allPredicates =
-          HornClauses allPredicates encoder.allClauses
+            val allPredicates =
+              HornClauses allPredicates encoder.allClauses
 
-          SMTLineariser("C_VC", "HORN", expectedStatus,
-            List(), allPredicates.toSeq.sortBy(_.name),
-            clauseFors)
+            SMTLineariser("C_VC", "HORN", expectedStatus,
+                          List(), allPredicates.toSeq.sortBy(_.name),
+                          clauseFors)
+          }
+          out.close
+        }
+        if (GlobalParameters.get.printHornSimplified ||
+            GlobalParameters.get.printHornSimplifiedSMT) {
+          val preprocessor = new DefaultPreprocessor
+          val (simpClauses, _, _) =
+            Console.withErr(Console.out) {
+              preprocessor.process(encoder.allClauses, encoder.globalHints)
+            }
+          if (GlobalParameters.get.printHornSimplified) {
+            println("Clauses after preprocessing:")
+            for (c <- simpClauses)
+              println(c.toPrologString)
+          } else {
+            val predsToDeclare =
+              (for (c <- simpClauses
+                    if c.head.pred != FALSE) yield {
+                c.predicates
+              }).flatten.toSet.toList
+
+            SMTLineariser("", "HORN", "", Nil, predsToDeclare,
+                          simpClauses.map(_ toFormula))
+          }
         }
-        out.close
         res = Left(None) // return dummy result
       } else {