From c1bf0cbe4a2b7ee126020f2366e8346239d0a783 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Wed, 17 Sep 2014 16:04:38 +0200
Subject: [PATCH] Rework vcs output of SMT-Lib solvers
---
.../leon/solvers/smtlib/SMTLIBTarget.scala | 23 +++++++++++++++++--
1 file changed, 21 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index fe1149bb0..da8533fc4 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -30,9 +30,19 @@ trait SMTLIBTarget {
val interpreter = getNewInterpreter()
- val out = new java.io.FileWriter(s"vcs-$targetName.smt2", true)
+ var out: java.io.FileWriter = _
+
reporter.ifDebug { debug =>
- out.write("; -----------------------------------------------------\n")
+ val file = context.files.headOption.map(_.getName).getOrElse("NA")
+ val n = VCNumbers.getNext(targetName+file)
+
+ val dir = new java.io.File("vcs");
+
+ if (!dir.isDirectory) {
+ dir.mkdir
+ }
+
+ out = new java.io.FileWriter(s"vcs/$targetName-$file-$n.smt2", true)
}
def id2sym(id: Identifier): SSymbol = SSymbol(id.name+"!"+id.globalId)
@@ -490,3 +500,12 @@ trait SMTLIBTarget {
}
}
+
+object VCNumbers {
+ private var nexts = Map[String, Int]().withDefaultValue(0)
+ def getNext(id: String) = {
+ val n = nexts(id)+1
+ nexts += id -> n
+ n
+ }
+}
--
GitLab