src/HOL/Tools/Nitpick/kodkod.scala

preload library;

/*  Title:      HOL/Tools/Nitpick/kodkod.scala
    Author:     Makarius

Scala interface for Kodkod.
*/

package isabelle.nitpick

import isabelle._

import java.util.concurrent.Executors

import org.antlr.runtime.{ANTLRInputStream, RecognitionException}
import de.tum.in.isabelle.Kodkodi.{Context, KodkodiLexer, KodkodiParser}


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 execute(source: String,
    solve_all: Boolean = false,
    prove: Boolean = false,
    max_solutions: Int = Integer.MAX_VALUE,
    cleanup_inst: Boolean = false,
    timeout: Time = Time.zero,
    max_threads: Int = 1): Result =
  {
    val executor = Executors.newFixedThreadPool(max_threads)

    def executor_kill(): Unit =
      if (!executor.isShutdown) Isabelle_Thread.fork() { executor.shutdownNow() }

    class Exit extends Exception

    val context =
      new Context {
        private var rc = 0
        private val out = new StringBuilder
        private val err = new StringBuilder

        def return_code(i: Int): Unit = synchronized { rc = rc max i}
        override def output(s: String): Unit = synchronized { out ++= s; out += '\n' }
        override def error(s: String): Unit = synchronized { err ++= s; err += '\n' }
        override def exit(i: Int): Unit =
          synchronized {
            return_code(i)
            executor_kill()
            throw new Exit
          }

        def result(): Result = synchronized { Result(rc, out.toString, err.toString) }
      }

    try {
      val lexer = new KodkodiLexer(new ANTLRInputStream(Bytes(source).stream))
      val parser =
        KodkodiParser.create(context, executor,
          false, solve_all, prove, max_solutions, cleanup_inst, lexer)

      val timeout_request =
        if (timeout.is_zero) None
        else {
          Some(Event_Timer.request(Time.now() + timeout) {
            context.error("Ran out of time")
            context.return_code(2)
            executor_kill()
          })
        }

      try { parser.problems() }
      catch { case exn: RecognitionException => parser.reportError(exn) }

      timeout_request.foreach(_.cancel)

      if (parser.getTokenStream.LA(1) != KodkodiParser.EOF) {
        context.error("Error: trailing tokens")
        context.exit(1)
      }
      if (lexer.getNumberOfSyntaxErrors + parser.getNumberOfSyntaxErrors > 0) {
        context.exit(1)
      }
    }
    catch {
      case _: Exit =>
      case exn: Throwable =>
        val message = exn.getMessage
        context.error(if (message.isEmpty) exn.toString else "Error: " + message)
        context.return_code(1)
    }

    context.result()
  }

  def warmup(): String =
    execute(
      """solver: "MiniSat\n"""" +
      File.read(Path.explode("$KODKODI/examples/weber3.kki"))).check
}