--- a/src/HOL/Tools/Nitpick/kodkod.scala Wed Aug 19 20:14:41 2020 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.scala Thu Aug 20 14:22:49 2020 +0200
@@ -17,8 +17,13 @@
object Kodkod
{
sealed case class Result(rc: Int, out: String, err: String)
+ {
+ def ok: Boolean = rc == 0
+ def check: String =
+ if (ok) out else error(if (err.isEmpty) "Error" else err)
+ }
- def kodkod(source: String,
+ def execute(source: String,
solve_all: Boolean = false,
prove: Boolean = false,
max_solutions: Int = Integer.MAX_VALUE,
@@ -91,4 +96,7 @@
context.result()
}
+
+ def warmup(): String =
+ execute(File.read(Path.explode("$KODKODI/examples/weber3.kki"))).check
}