src/HOL/Tools/Nitpick/kodkod.ML

more NEWS;

(*  Title:      HOL/Tools/Nitpick/kodkod.ML
    Author:     Jasmin Blanchette, TU Muenchen
    Copyright   2008-2014

ML interface for Kodkod.
*)

signature KODKOD =
sig
  type n_ary_index = int * int
  type setting = string * string

  datatype tuple =
    Tuple of int list |
    TupleIndex of n_ary_index |
    TupleReg of n_ary_index

  datatype tuple_set =
    TupleUnion of tuple_set * tuple_set |
    TupleDifference of tuple_set * tuple_set |
    TupleIntersect of tuple_set * tuple_set |
    TupleProduct of tuple_set * tuple_set |
    TupleProject of tuple_set * int |
    TupleSet of tuple list |
    TupleRange of tuple * tuple |
    TupleArea of tuple * tuple |
    TupleAtomSeq of int * int |
    TupleSetReg of n_ary_index

  datatype tuple_assign =
    AssignTuple of n_ary_index * tuple |
    AssignTupleSet of n_ary_index * tuple_set

  type bound = (n_ary_index * string) list * tuple_set list
  type int_bound = int option * tuple_set list

  datatype formula =
    All of decl list * formula |
    Exist of decl list * formula |
    FormulaLet of expr_assign list * formula |
    FormulaIf of formula * formula * formula |
    Or of formula * formula |
    Iff of formula * formula |
    Implies of formula * formula |
    And of formula * formula |
    Not of formula |
    Acyclic of n_ary_index |
    Function of n_ary_index * rel_expr * rel_expr |
    Functional of n_ary_index * rel_expr * rel_expr |
    TotalOrdering of n_ary_index * rel_expr * rel_expr * rel_expr |
    Subset of rel_expr * rel_expr |
    RelEq of rel_expr * rel_expr |
    IntEq of int_expr * int_expr |
    LT of int_expr * int_expr |
    LE of int_expr * int_expr |
    No of rel_expr |
    Lone of rel_expr |
    One of rel_expr |
    Some of rel_expr |
    False |
    True |
    FormulaReg of int
  and rel_expr =
    RelLet of expr_assign list * rel_expr |
    RelIf of formula * rel_expr * rel_expr |
    Union of rel_expr * rel_expr |
    Difference of rel_expr * rel_expr |
    Override of rel_expr * rel_expr |
    Intersect of rel_expr * rel_expr |
    Product of rel_expr * rel_expr |
    IfNo of rel_expr * rel_expr |
    Project of rel_expr * int_expr list |
    Join of rel_expr * rel_expr |
    Closure of rel_expr |
    ReflexiveClosure of rel_expr |
    Transpose of rel_expr |
    Comprehension of decl list * formula |
    Bits of int_expr |
    Int of int_expr |
    Iden |
    Ints |
    None |
    Univ |
    Atom of int |
    AtomSeq of int * int |
    Rel of n_ary_index |
    Var of n_ary_index |
    RelReg of n_ary_index
  and int_expr =
    Sum of decl list * int_expr |
    IntLet of expr_assign list * int_expr |
    IntIf of formula * int_expr * int_expr |
    SHL of int_expr * int_expr |
    SHA of int_expr * int_expr |
    SHR of int_expr * int_expr |
    Add of int_expr * int_expr |
    Sub of int_expr * int_expr |
    Mult of int_expr * int_expr |
    Div of int_expr * int_expr |
    Mod of int_expr * int_expr |
    Cardinality of rel_expr |
    SetSum of rel_expr |
    BitOr of int_expr * int_expr |
    BitXor of int_expr * int_expr |
    BitAnd of int_expr * int_expr |
    BitNot of int_expr |
    Neg of int_expr |
    Absolute of int_expr |
    Signum of int_expr |
    Num of int |
    IntReg of int
  and decl =
    DeclNo of n_ary_index * rel_expr |
    DeclLone of n_ary_index * rel_expr |
    DeclOne of n_ary_index * rel_expr |
    DeclSome of n_ary_index * rel_expr |
    DeclSet of n_ary_index * rel_expr
  and expr_assign =
    AssignFormulaReg of int * formula |
    AssignRelReg of n_ary_index * rel_expr |
    AssignIntReg of int * int_expr

  type 'a fold_expr_funcs =
    {formula_func: formula -> 'a -> 'a,
     rel_expr_func: rel_expr -> 'a -> 'a,
     int_expr_func: int_expr -> 'a -> 'a}

  val fold_formula : 'a fold_expr_funcs -> formula -> 'a -> 'a
  val fold_rel_expr : 'a fold_expr_funcs -> rel_expr -> 'a -> 'a
  val fold_int_expr : 'a fold_expr_funcs -> int_expr -> 'a -> 'a
  val fold_decl : 'a fold_expr_funcs -> decl -> 'a -> 'a
  val fold_expr_assign : 'a fold_expr_funcs -> expr_assign -> 'a -> 'a

  type 'a fold_tuple_funcs =
    {tuple_func: tuple -> 'a -> 'a,
     tuple_set_func: tuple_set -> 'a -> 'a}

  val fold_tuple : 'a fold_tuple_funcs -> tuple -> 'a -> 'a
  val fold_tuple_set : 'a fold_tuple_funcs -> tuple_set -> 'a -> 'a
  val fold_tuple_assign : 'a fold_tuple_funcs -> tuple_assign -> 'a -> 'a
  val fold_bound :
      'a fold_expr_funcs -> 'a fold_tuple_funcs -> bound -> 'a -> 'a
  val fold_int_bound : 'a fold_tuple_funcs -> int_bound -> 'a -> 'a

  type problem =
    {comment: string,
     settings: setting list,
     univ_card: int,
     tuple_assigns: tuple_assign list,
     bounds: bound list,
     int_bounds: int_bound list,
     expr_assigns: expr_assign list,
     formula: formula}

  type raw_bound = n_ary_index * int list list

  datatype outcome =
    Normal of (int * raw_bound list) list * int list * string |
    TimedOut of int list |
    Error of string * int list

  exception SYNTAX of string * string

  val max_arity : int -> int
  val arity_of_rel_expr : rel_expr -> int
  val is_problem_trivially_false : problem -> bool
  val problems_equivalent : problem * problem -> bool
  val solve_any_problem :
    bool -> bool -> bool -> Time.time -> int -> int -> problem list -> outcome
  val kodkod_scala : bool Config.T
end;

structure Kodkod : KODKOD =
struct

type n_ary_index = int * int

type setting = string * string

datatype tuple =
  Tuple of int list |
  TupleIndex of n_ary_index |
  TupleReg of n_ary_index

datatype tuple_set =
  TupleUnion of tuple_set * tuple_set |
  TupleDifference of tuple_set * tuple_set |
  TupleIntersect of tuple_set * tuple_set |
  TupleProduct of tuple_set * tuple_set |
  TupleProject of tuple_set * int |
  TupleSet of tuple list |
  TupleRange of tuple * tuple |
  TupleArea of tuple * tuple |
  TupleAtomSeq of int * int |
  TupleSetReg of n_ary_index

datatype tuple_assign =
  AssignTuple of n_ary_index * tuple |
  AssignTupleSet of n_ary_index * tuple_set

type bound = (n_ary_index * string) list * tuple_set list
type int_bound = int option * tuple_set list

datatype formula =
  All of decl list * formula |
  Exist of decl list * formula |
  FormulaLet of expr_assign list * formula |
  FormulaIf of formula * formula * formula |
  Or of formula * formula |
  Iff of formula * formula |
  Implies of formula * formula |
  And of formula * formula |
  Not of formula |
  Acyclic of n_ary_index |
  Function of n_ary_index * rel_expr * rel_expr |
  Functional of n_ary_index * rel_expr * rel_expr |
  TotalOrdering of n_ary_index * rel_expr * rel_expr * rel_expr |
  Subset of rel_expr * rel_expr |
  RelEq of rel_expr * rel_expr |
  IntEq of int_expr * int_expr |
  LT of int_expr * int_expr |
  LE of int_expr * int_expr |
  No of rel_expr |
  Lone of rel_expr |
  One of rel_expr |
  Some of rel_expr |
  False |
  True |
  FormulaReg of int
and rel_expr =
  RelLet of expr_assign list * rel_expr |
  RelIf of formula * rel_expr * rel_expr |
  Union of rel_expr * rel_expr |
  Difference of rel_expr * rel_expr |
  Override of rel_expr * rel_expr |
  Intersect of rel_expr * rel_expr |
  Product of rel_expr * rel_expr |
  IfNo of rel_expr * rel_expr |
  Project of rel_expr * int_expr list |
  Join of rel_expr * rel_expr |
  Closure of rel_expr |
  ReflexiveClosure of rel_expr |
  Transpose of rel_expr |
  Comprehension of decl list * formula |
  Bits of int_expr |
  Int of int_expr |
  Iden |
  Ints |
  None |
  Univ |
  Atom of int |
  AtomSeq of int * int |
  Rel of n_ary_index |
  Var of n_ary_index |
  RelReg of n_ary_index
and int_expr =
  Sum of decl list * int_expr |
  IntLet of expr_assign list * int_expr |
  IntIf of formula * int_expr * int_expr |
  SHL of int_expr * int_expr |
  SHA of int_expr * int_expr |
  SHR of int_expr * int_expr |
  Add of int_expr * int_expr |
  Sub of int_expr * int_expr |
  Mult of int_expr * int_expr |
  Div of int_expr * int_expr |
  Mod of int_expr * int_expr |
  Cardinality of rel_expr |
  SetSum of rel_expr |
  BitOr of int_expr * int_expr |
  BitXor of int_expr * int_expr |
  BitAnd of int_expr * int_expr |
  BitNot of int_expr |
  Neg of int_expr |
  Absolute of int_expr |
  Signum of int_expr |
  Num of int |
  IntReg of int
and decl =
  DeclNo of n_ary_index * rel_expr |
  DeclLone of n_ary_index * rel_expr |
  DeclOne of n_ary_index * rel_expr |
  DeclSome of n_ary_index * rel_expr |
  DeclSet of n_ary_index * rel_expr
and expr_assign =
  AssignFormulaReg of int * formula |
  AssignRelReg of n_ary_index * rel_expr |
  AssignIntReg of int * int_expr

type problem =
  {comment: string,
   settings: setting list,
   univ_card: int,
   tuple_assigns: tuple_assign list,
   bounds: bound list,
   int_bounds: int_bound list,
   expr_assigns: expr_assign list,
   formula: formula}

type raw_bound = n_ary_index * int list list

datatype outcome =
  Normal of (int * raw_bound list) list * int list * string |
  TimedOut of int list |
  Error of string * int list

exception SYNTAX of string * string

type 'a fold_expr_funcs =
  {formula_func: formula -> 'a -> 'a,
   rel_expr_func: rel_expr -> 'a -> 'a,
   int_expr_func: int_expr -> 'a -> 'a}


(** Auxiliary functions on Kodkod problems **)

fun fold_formula (F : 'a fold_expr_funcs) formula =
  case formula of
    All (ds, f) => fold (fold_decl F) ds #> fold_formula F f
  | Exist (ds, f) => fold (fold_decl F) ds #> fold_formula F f
  | FormulaLet (bs, f) => fold (fold_expr_assign F) bs #> fold_formula F f
  | FormulaIf (f, f1, f2) =>
    fold_formula F f #> fold_formula F f1 #> fold_formula F f2
  | Or (f1, f2) => fold_formula F f1 #> fold_formula F f2
  | Iff (f1, f2) => fold_formula F f1 #> fold_formula F f2
  | Implies (f1, f2) => fold_formula F f1 #> fold_formula F f2
  | And (f1, f2) => fold_formula F f1 #> fold_formula F f2
  | Not f => fold_formula F f
  | Acyclic x => fold_rel_expr F (Rel x)
  | Function (x, r1, r2) =>
    fold_rel_expr F (Rel x) #> fold_rel_expr F r1 #> fold_rel_expr F r2
  | Functional (x, r1, r2) =>
    fold_rel_expr F (Rel x) #> fold_rel_expr F r1 #> fold_rel_expr F r2
  | TotalOrdering (x, r1, r2, r3) =>
    fold_rel_expr F (Rel x) #> fold_rel_expr F r1 #> fold_rel_expr F r2
    #> fold_rel_expr F r3
  | Subset (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
  | RelEq (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
  | IntEq (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
  | LT (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
  | LE (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
  | No r => fold_rel_expr F r
  | Lone r => fold_rel_expr F r
  | One r => fold_rel_expr F r
  | Some r => fold_rel_expr F r
  | False => #formula_func F formula
  | True => #formula_func F formula
  | FormulaReg _ => #formula_func F formula
and fold_rel_expr F rel_expr =
  case rel_expr of
    RelLet (bs, r) => fold (fold_expr_assign F) bs #> fold_rel_expr F r
  | RelIf (f, r1, r2) =>
    fold_formula F f #> fold_rel_expr F r1 #> fold_rel_expr F r2
  | Union (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
  | Difference (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
  | Override (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
  | Intersect (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
  | Product (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
  | IfNo (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
  | Project (r1, is) => fold_rel_expr F r1 #> fold (fold_int_expr F) is
  | Join (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
  | Closure r => fold_rel_expr F r
  | ReflexiveClosure r => fold_rel_expr F r
  | Transpose r => fold_rel_expr F r
  | Comprehension (ds, f) => fold (fold_decl F) ds #> fold_formula F f
  | Bits i => fold_int_expr F i
  | Int i => fold_int_expr F i
  | Iden => #rel_expr_func F rel_expr
  | Ints => #rel_expr_func F rel_expr
  | None => #rel_expr_func F rel_expr
  | Univ => #rel_expr_func F rel_expr
  | Atom _ => #rel_expr_func F rel_expr
  | AtomSeq _ => #rel_expr_func F rel_expr
  | Rel _ => #rel_expr_func F rel_expr
  | Var _ => #rel_expr_func F rel_expr
  | RelReg _ => #rel_expr_func F rel_expr
and fold_int_expr F int_expr =
  case int_expr of
    Sum (ds, i) => fold (fold_decl F) ds #> fold_int_expr F i
  | IntLet (bs, i) => fold (fold_expr_assign F) bs #> fold_int_expr F i
  | IntIf (f, i1, i2) =>
    fold_formula F f #> fold_int_expr F i1 #> fold_int_expr F i2
  | SHL (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
  | SHA (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
  | SHR (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
  | Add (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
  | Sub (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
  | Mult (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
  | Div (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
  | Mod (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
  | Cardinality r => fold_rel_expr F r
  | SetSum r => fold_rel_expr F r
  | BitOr (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
  | BitXor (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
  | BitAnd (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
  | BitNot i => fold_int_expr F i
  | Neg i => fold_int_expr F i
  | Absolute i => fold_int_expr F i
  | Signum i => fold_int_expr F i
  | Num _ => #int_expr_func F int_expr
  | IntReg _ => #int_expr_func F int_expr
and fold_decl F decl =
  case decl of
    DeclNo (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r
  | DeclLone (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r
  | DeclOne (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r
  | DeclSome (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r
  | DeclSet (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r
and fold_expr_assign F assign =
  case assign of
    AssignFormulaReg (x, f) => fold_formula F (FormulaReg x) #> fold_formula F f
  | AssignRelReg (x, r) => fold_rel_expr F (RelReg x) #> fold_rel_expr F r
  | AssignIntReg (x, i) => fold_int_expr F (IntReg x) #> fold_int_expr F i

type 'a fold_tuple_funcs =
  {tuple_func: tuple -> 'a -> 'a,
   tuple_set_func: tuple_set -> 'a -> 'a}

fun fold_tuple (F : 'a fold_tuple_funcs) = #tuple_func F

fun fold_tuple_set F tuple_set =
  case tuple_set of
    TupleUnion (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2
  | TupleDifference (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2
  | TupleIntersect (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2
  | TupleProduct (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2
  | TupleProject (ts, _) => fold_tuple_set F ts
  | TupleSet ts => fold (fold_tuple F) ts
  | TupleRange (t1, t2) => fold_tuple F t1 #> fold_tuple F t2
  | TupleArea (t1, t2) => fold_tuple F t1 #> fold_tuple F t2
  | TupleAtomSeq _ => #tuple_set_func F tuple_set
  | TupleSetReg _ => #tuple_set_func F tuple_set

fun fold_tuple_assign F assign =
  case assign of
    AssignTuple (x, t) => fold_tuple F (TupleReg x) #> fold_tuple F t
  | AssignTupleSet (x, ts) =>
    fold_tuple_set F (TupleSetReg x) #> fold_tuple_set F ts

fun fold_bound expr_F tuple_F (zs, tss) =
  fold (fold_rel_expr expr_F) (map (Rel o fst) zs)
  #> fold (fold_tuple_set tuple_F) tss

fun fold_int_bound F (_, tss) = fold (fold_tuple_set F) tss

fun max_arity univ_card = floor (Math.ln 2147483647.0
                                 / Math.ln (Real.fromInt univ_card))

fun arity_of_rel_expr (RelLet (_, r)) = arity_of_rel_expr r
  | arity_of_rel_expr (RelIf (_, r1, _)) = arity_of_rel_expr r1
  | arity_of_rel_expr (Union (r1, _)) = arity_of_rel_expr r1
  | arity_of_rel_expr (Difference (r1, _)) = arity_of_rel_expr r1
  | arity_of_rel_expr (Override (r1, _)) = arity_of_rel_expr r1
  | arity_of_rel_expr (Intersect (r1, _)) = arity_of_rel_expr r1
  | arity_of_rel_expr (Product (r1, r2)) = sum_arities_of_rel_exprs r1 r2
  | arity_of_rel_expr (IfNo (r1, _)) = arity_of_rel_expr r1
  | arity_of_rel_expr (Project (_, is)) = length is
  | arity_of_rel_expr (Join (r1, r2)) = sum_arities_of_rel_exprs r1 r2 - 2
  | arity_of_rel_expr (Closure _) = 2
  | arity_of_rel_expr (ReflexiveClosure _) = 2
  | arity_of_rel_expr (Transpose _) = 2
  | arity_of_rel_expr (Comprehension (ds, _)) =
    fold (curry op + o arity_of_decl) ds 0
  | arity_of_rel_expr (Bits _) = 1
  | arity_of_rel_expr (Int _) = 1
  | arity_of_rel_expr Iden = 2
  | arity_of_rel_expr Ints = 1
  | arity_of_rel_expr None = 1
  | arity_of_rel_expr Univ = 1
  | arity_of_rel_expr (Atom _) = 1
  | arity_of_rel_expr (AtomSeq _) = 1
  | arity_of_rel_expr (Rel (n, _)) = n
  | arity_of_rel_expr (Var (n, _)) = n
  | arity_of_rel_expr (RelReg (n, _)) = n
and sum_arities_of_rel_exprs r1 r2 = arity_of_rel_expr r1 + arity_of_rel_expr r2
and arity_of_decl (DeclNo ((n, _), _)) = n
  | arity_of_decl (DeclLone ((n, _), _)) = n
  | arity_of_decl (DeclOne ((n, _), _)) = n
  | arity_of_decl (DeclSome ((n, _), _)) = n
  | arity_of_decl (DeclSet ((n, _), _)) = n

fun is_problem_trivially_false ({formula = False, ...} : problem) = true
  | is_problem_trivially_false _ = false

val chop_solver = take 2 o space_explode ","

fun settings_equivalent ([], []) = true
  | settings_equivalent ((key1, value1) :: settings1,
                         (key2, value2) :: settings2) =
    key1 = key2 andalso
    (value1 = value2 orelse key1 = "delay" orelse
     (key1 = "solver" andalso chop_solver value1 = chop_solver value2)) andalso
    settings_equivalent (settings1, settings2)
  | settings_equivalent _ = false

fun problems_equivalent (p1 : problem, p2 : problem) =
  #univ_card p1 = #univ_card p2 andalso
  #formula p1 = #formula p2 andalso
  #bounds p1 = #bounds p2 andalso
  #expr_assigns p1 = #expr_assigns p2 andalso
  #tuple_assigns p1 = #tuple_assigns p2 andalso
  #int_bounds p1 = #int_bounds p2 andalso
  settings_equivalent (#settings p1, #settings p2)

(** Serialization of problem **)

fun base_name j =
  if j < 0 then string_of_int (~j - 1) ^ "'" else string_of_int j

fun n_ary_name (1, j) prefix _ _ = prefix ^ base_name j
  | n_ary_name (2, j) _ prefix _ = prefix ^ base_name j
  | n_ary_name (n, j) _ _ prefix = prefix ^ string_of_int n ^ "_" ^ base_name j

fun atom_name j = "A" ^ base_name j
fun atom_seq_name (k, 0) = "u" ^ base_name k
  | atom_seq_name (k, j0) = "u" ^ base_name k ^ "@" ^ base_name j0
fun formula_reg_name j = "$f" ^ base_name j
fun rel_reg_name j = "$e" ^ base_name j
fun int_reg_name j = "$i" ^ base_name j

fun tuple_name x = n_ary_name x "A" "P" "T"
fun rel_name x = n_ary_name x "s" "r" "m"
fun var_name x = n_ary_name x "S" "R" "M"
fun tuple_reg_name x = n_ary_name x "$A" "$P" "$T"
fun tuple_set_reg_name x = n_ary_name x "$a" "$p" "$t"

fun inline_comment "" = ""
  | inline_comment comment =
    " /* " ^ translate_string (fn "\n" => " " | "*" => "* " | s => s) comment ^
    " */"

fun block_comment "" = ""
  | block_comment comment = prefix_lines "// " comment ^ "\n"

fun commented_rel_name (x, s) = rel_name x ^ inline_comment s

fun string_for_tuple (Tuple js) = "[" ^ commas (map atom_name js) ^ "]"
  | string_for_tuple (TupleIndex x) = tuple_name x
  | string_for_tuple (TupleReg x) = tuple_reg_name x

val no_prec = 100
val prec_TupleUnion = 1
val prec_TupleIntersect = 2
val prec_TupleProduct = 3
val prec_TupleProject = 4

fun precedence_ts (TupleUnion _) = prec_TupleUnion
  | precedence_ts (TupleDifference _) = prec_TupleUnion
  | precedence_ts (TupleIntersect _) = prec_TupleIntersect
  | precedence_ts (TupleProduct _) = prec_TupleProduct
  | precedence_ts (TupleProject _) = prec_TupleProject
  | precedence_ts _ = no_prec

fun string_for_tuple_set tuple_set =
  let
    fun sub tuple_set outer_prec =
      let
        val prec = precedence_ts tuple_set
        val need_parens = (prec < outer_prec)
      in
        (if need_parens then "(" else "") ^
        (case tuple_set of
           TupleUnion (ts1, ts2) => sub ts1 prec ^ " + " ^ sub ts2 (prec + 1)
         | TupleDifference (ts1, ts2) =>
           sub ts1 prec ^ " - " ^ sub ts2 (prec + 1)
         | TupleIntersect (ts1, ts2) => sub ts1 prec ^ " & " ^ sub ts2 prec
         | TupleProduct (ts1, ts2) => sub ts1 prec ^ "->" ^ sub ts2 prec
         | TupleProject (ts, c) => sub ts prec ^ "[" ^ string_of_int c ^ "]"
         | TupleSet ts => "{" ^ commas (map string_for_tuple ts) ^ "}"
         | TupleRange (t1, t2) =>
           "{" ^ string_for_tuple t1 ^
           (if t1 = t2 then "" else " .. " ^ string_for_tuple t2) ^ "}"
         | TupleArea (t1, t2) =>
           "{" ^ string_for_tuple t1 ^ " # " ^ string_for_tuple t2 ^ "}"
         | TupleAtomSeq x => atom_seq_name x
         | TupleSetReg x => tuple_set_reg_name x) ^
        (if need_parens then ")" else "")
      end
  in sub tuple_set 0 end

fun string_for_tuple_assign (AssignTuple (x, t)) =
    tuple_reg_name x ^ " := " ^ string_for_tuple t ^ "\n"
  | string_for_tuple_assign (AssignTupleSet (x, ts)) =
    tuple_set_reg_name x ^ " := " ^ string_for_tuple_set ts ^ "\n"

fun string_for_bound (zs, tss) =
  "bounds " ^ commas (map commented_rel_name zs) ^ ": " ^
  (if length tss = 1 then "" else "[") ^ commas (map string_for_tuple_set tss) ^
  (if length tss = 1 then "" else "]") ^ "\n"

fun int_string_for_bound (opt_n, tss) =
  (case opt_n of
     SOME n => signed_string_of_int n ^ ": "
   | NONE => "") ^ "[" ^ commas (map string_for_tuple_set tss) ^ "]"

val prec_All = 1
val prec_Or = 2
val prec_Iff = 3
val prec_Implies = 4
val prec_And = 5
val prec_Not = 6
val prec_Eq = 7
val prec_Some = 8
val prec_SHL = 9
val prec_Add = 10
val prec_Mult = 11
val prec_Override = 12
val prec_Intersect = 13
val prec_Product = 14
val prec_IfNo = 15
val prec_Project = 17
val prec_Join = 18
val prec_BitNot = 19

fun precedence_f (All _) = prec_All
  | precedence_f (Exist _) = prec_All
  | precedence_f (FormulaLet _) = prec_All
  | precedence_f (FormulaIf _) = prec_All
  | precedence_f (Or _) = prec_Or
  | precedence_f (Iff _) = prec_Iff
  | precedence_f (Implies _) = prec_Implies
  | precedence_f (And _) = prec_And
  | precedence_f (Not _) = prec_Not
  | precedence_f (Acyclic _) = no_prec
  | precedence_f (Function _) = no_prec
  | precedence_f (Functional _) = no_prec
  | precedence_f (TotalOrdering _) = no_prec
  | precedence_f (Subset _) = prec_Eq
  | precedence_f (RelEq _) = prec_Eq
  | precedence_f (IntEq _) = prec_Eq
  | precedence_f (LT _) = prec_Eq
  | precedence_f (LE _) = prec_Eq
  | precedence_f (No _) = prec_Some
  | precedence_f (Lone _) = prec_Some
  | precedence_f (One _) = prec_Some
  | precedence_f (Some _) = prec_Some
  | precedence_f False = no_prec
  | precedence_f True = no_prec
  | precedence_f (FormulaReg _) = no_prec
and precedence_r (RelLet _) = prec_All
  | precedence_r (RelIf _) = prec_All
  | precedence_r (Union _) = prec_Add
  | precedence_r (Difference _) = prec_Add
  | precedence_r (Override _) = prec_Override
  | precedence_r (Intersect _) = prec_Intersect
  | precedence_r (Product _) = prec_Product
  | precedence_r (IfNo _) = prec_IfNo
  | precedence_r (Project _) = prec_Project
  | precedence_r (Join _) = prec_Join
  | precedence_r (Closure _) = prec_BitNot
  | precedence_r (ReflexiveClosure _) = prec_BitNot
  | precedence_r (Transpose _) = prec_BitNot
  | precedence_r (Comprehension _) = no_prec
  | precedence_r (Bits _) = no_prec
  | precedence_r (Int _) = no_prec
  | precedence_r Iden = no_prec
  | precedence_r Ints = no_prec
  | precedence_r None = no_prec
  | precedence_r Univ = no_prec
  | precedence_r (Atom _) = no_prec
  | precedence_r (AtomSeq _) = no_prec
  | precedence_r (Rel _) = no_prec
  | precedence_r (Var _) = no_prec
  | precedence_r (RelReg _) = no_prec
and precedence_i (Sum _) = prec_All
  | precedence_i (IntLet _) = prec_All
  | precedence_i (IntIf _) = prec_All
  | precedence_i (SHL _) = prec_SHL
  | precedence_i (SHA _) = prec_SHL
  | precedence_i (SHR _) = prec_SHL
  | precedence_i (Add _) = prec_Add
  | precedence_i (Sub _) = prec_Add
  | precedence_i (Mult _) = prec_Mult
  | precedence_i (Div _) = prec_Mult
  | precedence_i (Mod _) = prec_Mult
  | precedence_i (Cardinality _) = no_prec
  | precedence_i (SetSum _) = no_prec
  | precedence_i (BitOr _) = prec_Intersect
  | precedence_i (BitXor _) = prec_Intersect
  | precedence_i (BitAnd _) = prec_Intersect
  | precedence_i (BitNot _) = prec_BitNot
  | precedence_i (Neg _) = prec_BitNot
  | precedence_i (Absolute _) = prec_BitNot
  | precedence_i (Signum _) = prec_BitNot
  | precedence_i (Num _) = no_prec
  | precedence_i (IntReg _) = no_prec

fun write_problem out problems =
  let
    fun out_outmost_f (And (f1, f2)) =
        (out_outmost_f f1; out "\n   && "; out_outmost_f f2)
      | out_outmost_f f = out_f f prec_And
    and out_f formula outer_prec =
      let
        val prec = precedence_f formula
        val need_parens = (prec < outer_prec)
      in
        (if need_parens then out "(" else ());
        (case formula of
           All (ds, f) => (out "all ["; out_decls ds; out "] | "; out_f f prec)
         | Exist (ds, f) =>
           (out "some ["; out_decls ds; out "] | "; out_f f prec)
         | FormulaLet (bs, f) =>
           (out "let ["; out_assigns bs; out "] | "; out_f f prec)
         | FormulaIf (f, f1, f2) =>
           (out "if "; out_f f prec; out " then "; out_f f1 prec; out " else ";
            out_f f2 prec)
         | Or (f1, f2) => (out_f f1 prec; out " || "; out_f f2 prec)
         | Iff (f1, f2) => (out_f f1 prec; out " <=> "; out_f f2 prec)
         | Implies (f1, f2) => (out_f f1 (prec + 1); out " => "; out_f f2 prec)
         | And (f1, f2) => (out_f f1 prec; out " && "; out_f f2 prec)
         | Not f => (out "! "; out_f f prec)
         | Acyclic x => out ("ACYCLIC(" ^ rel_name x ^ ")")
         | Function (x, r1, r2) =>
           (out ("FUNCTION(" ^ rel_name x ^ ", "); out_r r1 0; out " -> one ";
            out_r r2 0; out ")")
         | Functional (x, r1, r2) =>
           (out ("FUNCTION(" ^ rel_name x ^ ", "); out_r r1 0; out " -> lone ";
            out_r r2 0; out ")")
         | TotalOrdering (x, r1, r2, r3) =>
           (out ("TOTAL_ORDERING(" ^ rel_name x ^ ", "); out_r r1 0; out ", ";
            out_r r2 0; out ", "; out_r r3 0; out ")")
         | Subset (r1, r2) => (out_r r1 prec; out " in "; out_r r2 prec)
         | RelEq (r1, r2) => (out_r r1 prec; out " = "; out_r r2 prec)
         | IntEq (i1, i2) => (out_i i1 prec; out " = "; out_i i2 prec)
         | LT (i1, i2) => (out_i i1 prec; out " < "; out_i i2 prec)
         | LE (i1, i2) => (out_i i1 prec; out " <= "; out_i i2 prec)
         | No r => (out "no "; out_r r prec)
         | Lone r => (out "lone "; out_r r prec)
         | One r => (out "one "; out_r r prec)
         | Some r => (out "some "; out_r r prec)
         | False => out "false"
         | True => out "true"
         | FormulaReg j => out (formula_reg_name j));
        (if need_parens then out ")" else ())
      end
    and out_r rel_expr outer_prec =
      let
        val prec = precedence_r rel_expr
        val need_parens = (prec < outer_prec)
      in
        (if need_parens then out "(" else ());
        (case rel_expr of
           RelLet (bs, r) =>
           (out "let ["; out_assigns bs; out "] | "; out_r r prec)
         | RelIf (f, r1, r2) =>
           (out "if "; out_f f prec; out " then "; out_r r1 prec;
            out " else "; out_r r2 prec)
         | Union (r1, r2) => (out_r r1 prec; out " + "; out_r r2 (prec + 1))
         | Difference (r1, r2) =>
           (out_r r1 prec; out " - "; out_r r2 (prec + 1))
         | Override (r1, r2) => (out_r r1 prec; out " ++ "; out_r r2 prec)
         | Intersect (r1, r2) => (out_r r1 prec; out " & "; out_r r2 prec)
         | Product (r1, r2) => (out_r r1 prec; out "->"; out_r r2 prec)
         | IfNo (r1, r2) => (out_r r1 prec; out "\\"; out_r r2 prec)
         | Project (r1, is) => (out_r r1 prec; out "["; out_columns is; out "]")
         | Join (r1, r2) => (out_r r1 prec; out "."; out_r r2 (prec + 1))
         | Closure r => (out "^"; out_r r prec)
         | ReflexiveClosure r => (out "*"; out_r r prec)
         | Transpose r => (out "~"; out_r r prec)
         | Comprehension (ds, f) =>
           (out "{["; out_decls ds; out "] | "; out_f f 0; out "}")
         | Bits i => (out "Bits["; out_i i 0; out "]")
         | Int i => (out "Int["; out_i i 0; out "]")
         | Iden => out "iden"
         | Ints => out "ints"
         | None => out "none"
         | Univ => out "univ"
         | Atom j => out (atom_name j)
         | AtomSeq x => out (atom_seq_name x)
         | Rel x => out (rel_name x)
         | Var x => out (var_name x)
         | RelReg (_, j) => out (rel_reg_name j));
        (if need_parens then out ")" else ())
      end
    and out_i int_expr outer_prec =
      let
        val prec = precedence_i int_expr
        val need_parens = (prec < outer_prec)
      in
        (if need_parens then out "(" else ());
        (case int_expr of
           Sum (ds, i) => (out "sum ["; out_decls ds; out "] | "; out_i i prec)
         | IntLet (bs, i) =>
           (out "let ["; out_assigns bs; out "] | "; out_i i prec)
         | IntIf (f, i1, i2) =>
           (out "if "; out_f f prec; out " then "; out_i i1 prec;
            out " else "; out_i i2 prec)
         | SHL (i1, i2) => (out_i i1 prec; out " << "; out_i i2 (prec + 1))
         | SHA (i1, i2) => (out_i i1 prec; out " >> "; out_i i2 (prec + 1))
         | SHR (i1, i2) => (out_i i1 prec; out " >>> "; out_i i2 (prec + 1))
         | Add (i1, i2) => (out_i i1 prec; out " + "; out_i i2 (prec + 1))
         | Sub (i1, i2) => (out_i i1 prec; out " - "; out_i i2 (prec + 1))
         | Mult (i1, i2) => (out_i i1 prec; out " * "; out_i i2 (prec + 1))
         | Div (i1, i2) => (out_i i1 prec; out " / "; out_i i2 (prec + 1))
         | Mod (i1, i2) => (out_i i1 prec; out " % "; out_i i2 (prec + 1))
         | Cardinality r => (out "#("; out_r r 0; out ")")
         | SetSum r => (out "sum("; out_r r 0; out ")")
         | BitOr (i1, i2) => (out_i i1 prec; out " | "; out_i i2 prec)
         | BitXor (i1, i2) => (out_i i1 prec; out " ^ "; out_i i2 prec)
         | BitAnd (i1, i2) => (out_i i1 prec; out " & "; out_i i2 prec)
         | BitNot i => (out "~"; out_i i prec)
         | Neg i => (out "-"; out_i i prec)
         | Absolute i => (out "abs "; out_i i prec)
         | Signum i => (out "sgn "; out_i i prec)
         | Num k => out (signed_string_of_int k)
         | IntReg j => out (int_reg_name j));
        (if need_parens then out ")" else ())
      end
    and out_decls [] = ()
      | out_decls [d] = out_decl d
      | out_decls (d :: ds) = (out_decl d; out ", "; out_decls ds)
    and out_decl (DeclNo (x, r)) =
        (out (var_name x); out " : no "; out_r r 0)
      | out_decl (DeclLone (x, r)) =
        (out (var_name x); out " : lone "; out_r r 0)
      | out_decl (DeclOne (x, r)) =
        (out (var_name x); out " : one "; out_r r 0)
      | out_decl (DeclSome (x, r)) =
        (out (var_name x); out " : some "; out_r r 0)
      | out_decl (DeclSet (x, r)) =
        (out (var_name x); out " : set "; out_r r 0)
    and out_assigns [] = ()
      | out_assigns [b] = out_assign b
      | out_assigns (b :: bs) = (out_assign b; out ", "; out_assigns bs)
    and out_assign (AssignFormulaReg (j, f)) =
        (out (formula_reg_name j); out " := "; out_f f 0)
      | out_assign (AssignRelReg ((_, j), r)) =
        (out (rel_reg_name j); out " := "; out_r r 0)
      | out_assign (AssignIntReg (j, i)) =
        (out (int_reg_name j); out " := "; out_i i 0)
    and out_columns [] = ()
      | out_columns [i] = out_i i 0
      | out_columns (i :: is) = (out_i i 0; out ", "; out_columns is)
    and out_problem {comment, settings, univ_card, tuple_assigns, bounds,
                     int_bounds, expr_assigns, formula} =
        (out ("\n" ^ block_comment comment ^
              implode (map (fn (key, value) => key ^ ": " ^ value ^ "\n")
                            settings) ^
              "univ: " ^ atom_seq_name (univ_card, 0) ^ "\n" ^
              implode (map string_for_tuple_assign tuple_assigns) ^
              implode (map string_for_bound bounds) ^
              (if int_bounds = [] then
                 ""
               else
                 "int_bounds: " ^
                 commas (map int_string_for_bound int_bounds) ^ "\n"));
         List.app (fn b => (out_assign b; out ";")) expr_assigns;
         out "solve "; out_outmost_f formula; out ";\n")
  in
    out ("// This file was generated by Isabelle (most likely Nitpick)\n" ^
         "// " ^ ATP_Util.timestamp () ^ "\n");
    List.app out_problem problems
  end

(** Parsing of solution **)

fun is_ident_char s =
  Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse
  s = "_" orelse s = "'" orelse s = "$"

fun strip_blanks [] = []
  | strip_blanks (" " :: ss) = strip_blanks ss
  | strip_blanks [s1, " "] = [s1]
  | strip_blanks (s1 :: " " :: s2 :: ss) =
    if is_ident_char s1 andalso is_ident_char s2 then
      s1 :: " " :: strip_blanks (s2 :: ss)
    else
      strip_blanks (s1 :: s2 :: ss)
  | strip_blanks (s :: ss) = s :: strip_blanks ss

val scan_nat =
  Scan.repeat1 (Scan.one Symbol.is_ascii_digit)
  >> (the o Int.fromString o implode)
val scan_rel_name =
  ($$ "s" |-- scan_nat >> pair 1
   || $$ "r" |-- scan_nat >> pair 2
   || ($$ "m" |-- scan_nat --| $$ "_") -- scan_nat) -- Scan.option ($$ "'")
  >> (fn ((n, j), SOME _) => (n, ~j - 1)
       | ((n, j), NONE) => (n, j))
val scan_atom = $$ "A" |-- scan_nat
fun parse_non_empty_list scan = scan ::: Scan.repeat ($$ "," |-- scan)
fun parse_list scan = parse_non_empty_list scan || Scan.succeed []
val parse_tuple = $$ "[" |-- parse_list scan_atom --| $$ "]"
val parse_tuple_set = $$ "[" |-- parse_list parse_tuple --| $$ "]"
val parse_assignment = (scan_rel_name --| $$ "=") -- parse_tuple_set
val parse_instance =
  Scan.this_string "relations:"
  |-- $$ "{" |-- parse_list parse_assignment --| $$ "}"

val extract_instance =
  fst o Scan.finite Symbol.stopper
            (Scan.error (!! (fn _ =>
                                raise SYNTAX ("Kodkod.extract_instance",
                                              "ill-formed Kodkodi output"))
                            parse_instance))
  o strip_blanks o raw_explode

val problem_marker = "*** PROBLEM "
val outcome_marker = "---OUTCOME---\n"
val instance_marker = "---INSTANCE---\n"

fun read_section_body marker =
  Substring.string o fst o Substring.position "\n\n"
  o Substring.triml (size marker)

fun read_next_instance s =
  let val s = Substring.position instance_marker s |> snd in
    if Substring.isEmpty s then
      raise SYNTAX ("Kodkod.read_next_instance", "expected \"INSTANCE\" marker")
    else
      read_section_body instance_marker s |> extract_instance
  end

fun read_next_outcomes j (s, ps, js) =
  let val (s1, s2) = Substring.position outcome_marker s in
    if Substring.isEmpty s2 orelse
       not (Substring.isEmpty (Substring.position problem_marker s1
                               |> snd)) then
      (s, ps, js)
    else
      let
        val outcome = read_section_body outcome_marker s2
        val s = Substring.triml (size outcome_marker) s2
      in
        if String.isSuffix "UNSATISFIABLE" outcome then
          read_next_outcomes j (s, ps, j :: js)
        else if String.isSuffix "SATISFIABLE" outcome then
          read_next_outcomes j (s, (j, read_next_instance s2) :: ps, js)
        else
          raise SYNTAX ("Kodkod.read_next_outcomes",
                        "unknown outcome " ^ quote outcome)
      end
  end

fun read_next_problems (s, ps, js) =
  let val s = Substring.position problem_marker s |> snd in
    if Substring.isEmpty s then
      (ps, js)
    else
      let
        val s = Substring.triml (size problem_marker) s
        val j_plus_1 = s |> Substring.takel (not_equal #" ") |> Substring.string
                         |> Int.fromString |> the
        val j = j_plus_1 - 1
      in read_next_problems (read_next_outcomes j (s, ps, js)) end
  end
  handle Option.Option => raise SYNTAX ("Kodkod.read_next_problems",
                                        "expected number after \"PROBLEM\"")


(** Main Kodkod entry point **)

fun serial_string_and_temporary_dir overlord =
  if overlord then ("", getenv "ISABELLE_HOME_USER")
  else (serial_string (), getenv "ISABELLE_TMP")

(* The fudge term below is to account for Kodkodi's slow start-up time, which
   is partly due to the JVM and partly due to the ML "bash" function. *)
val fudge_ms = 250

fun uncached_solve_any_problem kodkod_scala overlord deadline max_threads0 max_solutions problems =
  let
    val j = find_index (curry (op =) True o #formula) problems
    val indexed_problems = if j >= 0 then
                             [(j, nth problems j)]
                           else
                             filter_out (is_problem_trivially_false o snd)
                                        (0 upto length problems - 1 ~~ problems)
    val triv_js = filter_out (AList.defined (op =) indexed_problems)
                             (0 upto length problems - 1)
    val reindex = fst o nth indexed_problems

    val max_threads =
      if max_threads0 = 0
      then Options.default_int \<^system_option>\<open>kodkod_max_threads\<close>
      else max_threads0

    val external_process = not kodkod_scala orelse overlord
    val timeout0 = Time.toMilliseconds (deadline - Time.now ())
    val timeout = if external_process then timeout0 - fudge_ms else timeout0

    val solve_all = max_solutions > 1
  in
    if null indexed_problems then
      Normal ([], triv_js, "")
    else if timeout <= 0 then TimedOut triv_js
    else
      let
        val kki =
          let
            val buf = Unsynchronized.ref Buffer.empty
            fun out s = Unsynchronized.change buf (Buffer.add s)
            val _ = write_problem out (map snd indexed_problems)
          in Buffer.content (! buf) end
        val (rc, out, err) =
          if external_process then
            let
              val (serial_str, temp_dir) = serial_string_and_temporary_dir overlord
              fun path_for suf = Path.explode (temp_dir ^ "/kodkodi" ^ serial_str ^ "." ^ suf)
              val kki_path = path_for "kki"
              val out_path = path_for "out"
              val err_path = path_for "err"

              fun remove_temporary_files () =
                if overlord then ()
                else List.app (ignore o try File.rm) [kki_path, out_path, err_path]
            in
              \<^try>\<open>
                let
                  val _ = File.write kki_path kki
                  val rc =
                    Isabelle_System.bash ("cd " ^ Bash.string temp_dir ^ ";\n\
                      \\"$KODKODI/bin/kodkodi\"" ^
                      (" -max-msecs " ^ string_of_int timeout) ^
                      (if solve_all then " -solve-all" else "") ^
                      " -max-solutions " ^ string_of_int max_solutions ^
                      (if max_threads > 0 then " -max-threads " ^ string_of_int max_threads else "") ^
                      " < " ^ File.bash_path kki_path ^
                      " > " ^ File.bash_path out_path ^
                      " 2> " ^ File.bash_path err_path)
                  val out = File.read out_path
                  val err = File.read err_path
                  val _ = remove_temporary_files ()
                in (rc, out, err) end
                finally remove_temporary_files ()
              \<close>
            end
          else
            (timeout, (solve_all, (max_solutions, (max_threads, kki))))
            |> let open XML.Encode in pair int (pair bool (pair int (pair int string))) end
            |> YXML.string_of_body
            |> \<^scala>\<open>kodkod\<close>
            |> YXML.parse_body
            |> let open XML.Decode in triple int string string end

        val (ps, nontriv_js) =
          read_next_problems (Substring.full out, [], [])
          |>> rev ||> rev
          |> apfst (map (apfst reindex)) |> apsnd (map reindex)
        val js = triv_js @ nontriv_js

        val first_error =
          trim_split_lines err
          |> map
           (perhaps (try (unsuffix ".")) #>
            perhaps (try (unprefix "Solve error: ")) #>
            perhaps (try (unprefix "Error: ")))
          |> find_first (fn line => line <> "" andalso line <> "EXIT")
          |> the_default ""
      in
        if not (null ps) orelse rc = 0 then Normal (ps, js, first_error)
        else if rc = 2 then TimedOut js
        else if rc = 130 then Isabelle_Thread.raise_interrupt ()
        else Error (if first_error = "" then "Unknown error" else first_error, js)
      end
  end

val cached_outcome =
  Synchronized.var "Kodkod.cached_outcome"
                   (NONE : ((int * problem list) * outcome) option)

fun solve_any_problem kodkod_scala debug overlord deadline max_threads max_solutions
                      problems =
  let
    fun do_solve () =
      uncached_solve_any_problem kodkod_scala overlord deadline max_threads max_solutions
                                 problems
  in
    if debug orelse overlord then
      do_solve ()
    else
      case AList.lookup (fn ((max1, ps1), (max2, ps2)) =>
                            max1 = max2 andalso length ps1 = length ps2 andalso
                            forall problems_equivalent (ps1 ~~ ps2))
                        (the_list (Synchronized.value cached_outcome))
                        (max_solutions, problems) of
        SOME outcome => outcome
      | NONE =>
        let val outcome = do_solve () in
          (case outcome of
             Normal (_, _, "") =>
             Synchronized.change cached_outcome
                                 (K (SOME ((max_solutions, problems), outcome)))
           | _ => ());
          outcome
        end
  end

val kodkod_scala = Attrib.setup_option_bool (\<^system_option>\<open>kodkod_scala\<close>, \<^here>)

end;