Skip to content
Snippets Groups Projects
Commit c1bf0cbe authored by Etienne Kneuss's avatar Etienne Kneuss
Browse files

Rework vcs output of SMT-Lib solvers

parent 62ed1089
Branches
Tags
No related merge requests found
......@@ -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
}
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment