diff --git a/src/main/scala/inox/solvers/Solver.scala b/src/main/scala/inox/solvers/Solver.scala index 6d9632d6a..53c883c67 100644 --- a/src/main/scala/inox/solvers/Solver.scala +++ b/src/main/scala/inox/solvers/Solver.scala @@ -28,6 +28,10 @@ trait AbstractSolver extends Interruptible { // This is ugly, but helpful for smtlib solvers def dbg(msg: => Any): Unit = {} + // Used to report SMT Lib files <-> VCs correspondence + // Therefore it should be overriden in solvers that extends SMTLibDebugger traits + def getSmtLibFileId: Option[Int] = None + object SolverUnsupportedError { def msg(t: Tree, reason: Option[String]) = { s"(of ${t.getClass}) is unsupported by solver $name" + reason.map(":\n " + _ ).getOrElse("") diff --git a/src/main/scala/inox/solvers/SolverFactory.scala b/src/main/scala/inox/solvers/SolverFactory.scala index 7085d14b6..4aa9e2403 100644 --- a/src/main/scala/inox/solvers/SolverFactory.scala +++ b/src/main/scala/inox/solvers/SolverFactory.scala @@ -280,6 +280,9 @@ object SolverFactory { // encoder is from TipDebugger and enc from AbstractUnrollingSolver override protected val encoder = enc + + // Used to report SMT Lib files <-> VCs correspondence + override def getSmtLibFileId: Option[Int] = underlying.getSmtLibFileId } () => new SMTZ3Impl(p)(enc)(ChooseEncoder(p)(enc)) @@ -307,6 +310,9 @@ object SolverFactory { protected val underlying = nonIncrementalWrap(targetProgram)(finalName, targetSemantics, () => new Underlying(targetProgram)) + // Used to report SMT Lib files <-> VCs correspondence + override def getSmtLibFileId: Option[Int] = underlying.getSmtLibFileId + // encoder is from TipDebugger and enc from AbstractUnrollingSolver override protected val encoder = enc } @@ -336,6 +342,9 @@ object SolverFactory { protected val underlying = nonIncrementalWrap(targetProgram)(finalName, targetSemantics, () => new Underlying(targetProgram)) + // Used to report SMT Lib files <-> VCs correspondence + override def getSmtLibFileId: Option[Int] = underlying.getSmtLibFileId + // encoder is from TipDebugger and enc from AbstractUnrollingSolver override protected val encoder = enc } diff --git a/src/main/scala/inox/solvers/combinators/NonIncrementalSolver.scala b/src/main/scala/inox/solvers/combinators/NonIncrementalSolver.scala index e845add8a..c800ba1a7 100644 --- a/src/main/scala/inox/solvers/combinators/NonIncrementalSolver.scala +++ b/src/main/scala/inox/solvers/combinators/NonIncrementalSolver.scala @@ -18,6 +18,11 @@ trait NonIncrementalSolver extends AbstractSolver { self => type Model = self.Model } + // Used to report SMT Lib files <-> VCs correspondence + override def getSmtLibFileId: Option[Int] = currentSolver match + case Some(solver) => solver.getSmtLibFileId + case None => None + val assertions: IncrementalSeq[Trees] = new IncrementalSeq[Trees] var currentSolver: Option[AbstractSolver] = None diff --git a/src/main/scala/inox/solvers/combinators/PortfolioSolver.scala b/src/main/scala/inox/solvers/combinators/PortfolioSolver.scala index 15d7e56b8..04c53ae4f 100644 --- a/src/main/scala/inox/solvers/combinators/PortfolioSolver.scala +++ b/src/main/scala/inox/solvers/combinators/PortfolioSolver.scala @@ -20,6 +20,9 @@ trait PortfolioSolver extends Solver { self => val solvers: Seq[SubSolver] val name = "Pfolio" + // Used to report SMT Lib files <-> VCs correspondence + override def getSmtLibFileId: Option[Int] = if solvers.isEmpty then None else solvers.head.getSmtLibFileId + protected var resultSolver: Option[Solver] = None private[this] var tasks: Future[Unit] = Future(()) diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBDebugger.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBDebugger.scala index 315000c3b..a9c80eacc 100644 --- a/src/main/scala/inox/solvers/smtlib/SMTLIBDebugger.scala +++ b/src/main/scala/inox/solvers/smtlib/SMTLIBDebugger.scala @@ -22,14 +22,26 @@ trait SMTLIBDebugger extends SMTLIBTarget { super.free() debugOut.foreach(_.close()) } + lazy private val file = options.findOptionOrDefault(Main.optFiles).headOption.map(_.getName).getOrElse("NA") + lazy private val smtLibFileId: Int = DebugFileNumbers.next(targetName + file) + /** + * Returns the SMT-lib file query ID if the debug=smt option is activated, otherwise None + * @return + */ + def getSmtLibFileIdIfDebug: Option[Int] = { + given DebugSectionSMT.type = DebugSectionSMT + if (reporter.isDebugEnabled) { + Some(smtLibFileId) + } else { + None + } + } /* Printing VCs */ protected lazy val debugOut: Option[java.io.FileWriter] = { given DebugSectionSMT.type = DebugSectionSMT if (reporter.isDebugEnabled) { - val file = options.findOptionOrDefault(Main.optFiles).headOption.map(_.getName).getOrElse("NA") - val n = DebugFileNumbers.next(targetName + file) - val fileName = s"smt-sessions/$targetName-$file-$n.smt2" + val fileName = s"smt-sessions/$targetName-$file-$smtLibFileId.smt2" val javaFile = new java.io.File(fileName) javaFile.getParentFile.mkdirs() diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBSolver.scala index 609f3d258..5c77da44b 100644 --- a/src/main/scala/inox/solvers/smtlib/SMTLIBSolver.scala +++ b/src/main/scala/inox/solvers/smtlib/SMTLIBSolver.scala @@ -40,6 +40,8 @@ abstract class SMTLIBSolver private(override val program: Program, } } + override def getSmtLibFileId: Option[Int] = this.getSmtLibFileIdIfDebug + /* Public solver interface */ def assertCnstr(expr: Expr): Unit = { variablesOf(expr).foreach(declareVariable) diff --git a/src/main/scala/inox/solvers/z3/NativeZ3Solver.scala b/src/main/scala/inox/solvers/z3/NativeZ3Solver.scala index 758227762..9973433de 100644 --- a/src/main/scala/inox/solvers/z3/NativeZ3Solver.scala +++ b/src/main/scala/inox/solvers/z3/NativeZ3Solver.scala @@ -23,6 +23,8 @@ class NativeZ3Solver(override val program: Program) protected val underlying = NativeZ3Solver.synchronized(new Underlying(targetProgram, self.context)(using targetSemantics)) + + override def free(): Unit = NativeZ3Solver.synchronized(super.free())