Skip to content

Commit

Permalink
Adapt to changes in Eldarica
Browse files Browse the repository at this point in the history
  • Loading branch information
zafer-esen committed Mar 5, 2024
1 parent f0a67a1 commit 860ff13
Show file tree
Hide file tree
Showing 2 changed files with 4 additions and 6 deletions.
2 changes: 1 addition & 1 deletion src/tricera/Util.scala
Original file line number Diff line number Diff line change
Expand Up @@ -223,7 +223,7 @@ object Util {
}

////////////////////////////////////////////////////////////////////////////////
import lazabs.horn.bottomup.Util.{Dag, DagNode, DagEmpty}
import lazabs.horn.Util.{Dag, DagNode, DagEmpty}

/**
* Methods to print lazabs.horn.bottomup.Util.Dag
Expand Down
8 changes: 3 additions & 5 deletions src/tricera/concurrency/ParameterisedExamples.scala
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ package tricera.concurrency

import ap.parser._
import ap.theories.nia.GroebnerMultiplication
import lazabs.horn.bottomup.{DagInterpolator, HornClauses, HornPredAbs, Util}
import lazabs.horn.bottomup.{HornClauses, HornPredAbs}
import hornconcurrency.{ParametricEncoder, VerificationLoop}
import tricera.params.TriCeraParameters

Expand Down Expand Up @@ -70,15 +70,13 @@ object ParameterisedExamples extends App {
def solve(enc : ParametricEncoder) = {
println("Solving ...")

val predAbs =
new HornPredAbs(enc.allClauses, Map(),
DagInterpolator.interpolatingPredicateGenCEXAndOr _)
val predAbs = new HornPredAbs(enc.allClauses)

println
predAbs.result match {
case Right(cex) => {
println("NOT SOLVABLE")
Util.show(for (p <- cex) yield p._1, "horn-cex")
lazabs.horn.Util.show(for (p <- cex) yield p._1, "horn-cex")
cex.prettyPrint
}
case Left(solution) =>
Expand Down

0 comments on commit 860ff13

Please sign in to comment.