From 691ba0e212344f0b73bf23def1bc24f4ecc39874 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Wed, 9 Nov 2016 20:41:58 +0100
Subject: [PATCH] Setup TIP debugging and multi-check inputs
---
src/main/scala/inox/Main.scala | 20 +++++-----
.../inox/solvers/smtlib/SMTLIBDebugger.scala | 4 ++
.../inox/solvers/smtlib/SMTLIBTarget.scala | 3 --
src/main/scala/inox/tip/Parser.scala | 21 +++++-----
src/main/scala/inox/tip/TipDebugger.scala | 38 +++++++++++++++++++
5 files changed, 64 insertions(+), 22 deletions(-)
create mode 100644 src/main/scala/inox/tip/TipDebugger.scala
diff --git a/src/main/scala/inox/Main.scala b/src/main/scala/inox/Main.scala
index c6be43a62..09ac0e7fa 100644
--- a/src/main/scala/inox/Main.scala
+++ b/src/main/scala/inox/Main.scala
@@ -140,34 +140,34 @@ object Main extends MainHelpers {
if (files.isEmpty) {
ctx.reporter.fatalError(s"Input file was not specified.\nTry the --help option for more information.")
} else {
- for (file <- files) {
- val (syms, expr) = new tip.Parser(file).parseScript
+ var error: Boolean = false
+ for (file <- files;
+ (syms, expr) <- new tip.Parser(file).parseScript) {
val program = InoxProgram(ctx, syms)
import program._
import program.ctx._
import SolverResponses._
- val error = SimpleSolverAPI(SolverFactory.default(program)).solveSAT(expr) match {
+ SimpleSolverAPI(SolverFactory.default(program)).solveSAT(expr) match {
case SatWithModel(model) =>
reporter.info(" => SAT")
for ((vd, res) <- model) {
reporter.info(f"${vd.asString}%-15s -> ${res.asString}")
}
- false
case Unsat =>
reporter.info(" => UNSAT")
- false
case Unknown =>
reporter.info(" => UNKNOWN")
- true
+ error = true
}
- reporter.whenDebug(utils.DebugSectionTimers) { debug =>
- timers.outputTable(debug)
- }
+ }
- exit(error = error)
+ ctx.reporter.whenDebug(utils.DebugSectionTimers) { debug =>
+ ctx.timers.outputTable(debug)
}
+
+ exit(error = error)
}
}
}
diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBDebugger.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBDebugger.scala
index 37eaca9f6..2fecf82f6 100644
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBDebugger.scala
+++ b/src/main/scala/inox/solvers/smtlib/SMTLIBDebugger.scala
@@ -4,6 +4,7 @@ package inox
package solvers
package smtlib
+import utils._
import _root_.smtlib.parser.Terms._
trait SMTLIBDebugger extends SMTLIBTarget {
@@ -48,3 +49,6 @@ trait SMTLIBDebugger extends SMTLIBTarget {
super.emit(cmd, rawOut = rawOut)
}
}
+
+// Unique numbers
+private[smtlib] object DebugFileNumbers extends UniqueCounter[String]
diff --git a/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
index 9688bafd5..f02654597 100644
--- a/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/inox/solvers/smtlib/SMTLIBTarget.scala
@@ -729,6 +729,3 @@ trait SMTLIBTarget extends Interruptible with ADTManagers {
fromSMT(s, Some(tpe))
}
}
-
-// Unique numbers
-private[smtlib] object DebugFileNumbers extends UniqueCounter[String]
diff --git a/src/main/scala/inox/tip/Parser.scala b/src/main/scala/inox/tip/Parser.scala
index 6cde5ecec..f73e2f585 100644
--- a/src/main/scala/inox/tip/Parser.scala
+++ b/src/main/scala/inox/tip/Parser.scala
@@ -33,21 +33,24 @@ class Parser(file: File) {
pos.map(p => positions.get(p.line, p.col)).getOrElse(NoPosition)
}
- def parseScript: (Symbols, Expr) = {
+ def parseScript: Seq[(Symbols, Expr)] = {
val parser = new TipParser(new TipLexer(positions.reader))
val script = parser.parseScript
var assertions: Seq[Expr] = Seq.empty
implicit var locals: Locals = NoLocals
- for (cmd <- script.commands) {
- val (newAssertions, newLocals) = extractCommand(cmd)
- assertions ++= newAssertions
- locals = newLocals
- }
-
- val expr: Expr = locals.symbols.andJoin(assertions)
- (locals.symbols, expr)
+ (for (cmd <- script.commands) yield cmd match {
+ case CheckSat() =>
+ val expr: Expr = locals.symbols.andJoin(assertions)
+ Some((locals.symbols, expr))
+
+ case _ =>
+ val (newAssertions, newLocals) = extractCommand(cmd)
+ assertions ++= newAssertions
+ locals = newLocals
+ None
+ }).flatten
}
protected class Locals (
diff --git a/src/main/scala/inox/tip/TipDebugger.scala b/src/main/scala/inox/tip/TipDebugger.scala
new file mode 100644
index 000000000..806d83e98
--- /dev/null
+++ b/src/main/scala/inox/tip/TipDebugger.scala
@@ -0,0 +1,38 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package inox
+package tip
+
+import utils._
+import solvers._
+
+trait TipDebugger extends Solver {
+ import program._
+
+ implicit val debugSection: DebugSection
+
+ abstract override def free(): Unit = {
+ super.free()
+ debugOut.foreach(_.close())
+ }
+
+ protected lazy val debugOut: Option[java.io.FileWriter] = {
+ if (ctx.reporter.isDebugEnabled) {
+ val file = ctx.options.findOptionOrDefault(Main.optFiles).headOption.map(_.getName).getOrElse("NA")
+ val n = DebugFileNumbers.next(file)
+ val fileName = s"tip-sessions/$file-$n.tip"
+
+ val javaFile = new java.io.File(fileName)
+ javaFile.getParentFile.mkdirs()
+
+ ctx.reporter.debug(s"Outputting tip session into $fileName")
+ val fw = new java.io.FileWriter(javaFile, false)
+ Some(fw)
+ } else {
+ None
+ }
+ }
+}
+
+// Unique numbers
+private[tip] object DebugFileNumbers extends UniqueCounter[String]
--
GitLab