adapted to Princess changes

uuverifiers · Apr 26, 2024 · c2880b9 · c2880b9
1 parent 406d7bd
commit c2880b9
Show file tree

Hide file tree

Showing 5 changed files with 29 additions and 25 deletions.
diff --git a/build.sbt b/build.sbt
@@ -173,9 +173,6 @@ lazy val root = (project in file(".")).
     }}).value,
 //
     assembly / test := None,
-//
-    libraryDependencies +=
-      "org.scala-lang.modules" %% "scala-parser-combinators" % "1.0.4",
 //
     libraryDependencies +=
       "net.sf.squirrel-sql.thirdparty-non-maven" % "java-cup" % "0.11a",
@@ -192,10 +189,10 @@ lazy val root = (project in file(".")).
     libraryDependencies +=
       "org.scalatest" %% "scalatest" % "3.2.14" % "test",
 //
-    libraryDependencies += "io.github.uuverifiers" %% "princess" % "2024-03-22"
+//    libraryDependencies += "io.github.uuverifiers" %% "princess" % "2024-03-22"
 //
-//    resolvers += "uuverifiers" at "https://eldarica.org/maven/",
-//    libraryDependencies += "uuverifiers" %% "princess" % "nightly-SNAPSHOT"
+    resolvers += "uuverifiers" at "https://eldarica.org/maven/",
+    libraryDependencies += "uuverifiers" %% "princess" % "nightly-SNAPSHOT"
 
 )
 //
diff --git a/src/main/scala/lazabs/horn/HornWrapper.scala b/src/main/scala/lazabs/horn/HornWrapper.scala
@@ -259,8 +259,10 @@ class HornWrapper(constraints  : Seq[HornClause],
            c.predicates
          }).flatten.toSet.toList
 
-      SMTLineariser("", "HORN", "", Nil, predsToDeclare,
-                    simplifiedClauses.map(_ toFormula))
+      SMTLineariser.printWithDecls(logic          = "HORN",
+                                   predsToDeclare = predsToDeclare,
+                                   formulas       =
+                                     simplifiedClauses.map(_ toFormula))
 
       throw PrintingFinishedException
     }

diff --git a/src/main/scala/lazabs/horn/concurrency/VerificationLoop.scala b/src/main/scala/lazabs/horn/concurrency/VerificationLoop.scala
@@ -219,9 +219,11 @@ class VerificationLoop(system : ParametricEncoder.System,
         val allPredicates =
           HornClauses allPredicates encoder.allClauses
 
-        SMTLineariser("C_VC", "HORN", "unknown",
-                      List(), allPredicates.toSeq.sortBy(_.name),
-                      clauseFors)
+        SMTLineariser.printWithDecls(benchmarkName  = "C_VC",
+                                     logic          = "HORN",
+                                     predsToDeclare =
+                                       allPredicates.toSeq.sortBy(_.name),
+                                     formulas       = clauseFors)
       }
       out.close
     }

diff --git a/src/main/scala/lazabs/horn/predgen/DisjInterpolator.scala b/src/main/scala/lazabs/horn/predgen/DisjInterpolator.scala
@@ -1052,18 +1052,19 @@ object DisjInterpolator {
                                    ("%04d".format(benchmarkCounter)) + ".smt2")
     benchmarkCounter = benchmarkCounter + 1
     Console.withOut(benchmarkFile) {
-      SMTLineariser(clauseFormulas,
-                    Signature(Set(), Set(), Set(), order restrict Set()),
-                    "HORN",
-                    solvable match {
-                      case Some(true) => "sat"
-                      case Some(false) => "unsat"
-                      case None => "unknown"
-                    },
-                    "Horn constraint system (" +
-                      clauseFormulas.size + " clauses, " +
-                      order.orderedPredicates.size + " relation symbols)\n" +
-                    "    Generated by Eldarica (http://lara.epfl.ch/w/eldarica)")
+      SMTLineariser.printWithDeclsSig(
+        formulas      = clauseFormulas,
+        signature     = Signature(Set(), Set(), Set(), order restrict Set()),
+        logic         = "HORN",
+        status        = solvable match {
+                          case Some(true) => "sat"
+                          case Some(false) => "unsat"
+                          case None => "unknown"
+                        },
+        benchmarkName = "Horn constraint system (" +
+                          clauseFormulas.size + " clauses, " +
+                          order.orderedPredicates.size + " relation symbols)\n" +
+                          "    Generated by Eldarica (https://github.com/uuverifiers/eldarica)")
     }
     benchmarkFile.close
   }

diff --git a/src/main/scala/lazabs/prover/PrincessAPI.scala b/src/main/scala/lazabs/prover/PrincessAPI.scala
@@ -353,8 +353,10 @@ abstract class AbstractPrincessAPI extends PrincessAPI {
                          }).getOrElse(false))
 
       Console.withOut(interpolationFile) {
-        SMTLineariser(sortedFormulas, signature,
-                      "Eldarica interpolation query " + interpolationCount)
+        SMTLineariser.printWithDeclsSig(
+          formulas      = sortedFormulas,
+          signature     = signature,
+          benchmarkName = "Eldarica interpolation query " + interpolationCount)
       }
       interpolationFile.close
       interpolationCount = interpolationCount + 1