src/HOL/Tools/Nitpick/kodkod.ML
author wenzelm
Sat Apr 02 23:29:05 2016 +0200 (2016-04-02 ago)
changeset 62826 eb94e570c1a4
parent 62549 9498623b27f0
child 64304 96bc94c87a81
permissions -rw-r--r--
prefer infix operations;
     1 (*  Title:      HOL/Tools/Nitpick/kodkod.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2008-2014
     4 
     5 ML interface for Kodkod.
     6 *)
     7 
     8 signature KODKOD =
     9 sig
    10   type n_ary_index = int * int
    11   type setting = string * string
    12 
    13   datatype tuple =
    14     Tuple of int list |
    15     TupleIndex of n_ary_index |
    16     TupleReg of n_ary_index
    17 
    18   datatype tuple_set =
    19     TupleUnion of tuple_set * tuple_set |
    20     TupleDifference of tuple_set * tuple_set |
    21     TupleIntersect of tuple_set * tuple_set |
    22     TupleProduct of tuple_set * tuple_set |
    23     TupleProject of tuple_set * int |
    24     TupleSet of tuple list |
    25     TupleRange of tuple * tuple |
    26     TupleArea of tuple * tuple |
    27     TupleAtomSeq of int * int |
    28     TupleSetReg of n_ary_index
    29 
    30   datatype tuple_assign =
    31     AssignTuple of n_ary_index * tuple |
    32     AssignTupleSet of n_ary_index * tuple_set
    33 
    34   type bound = (n_ary_index * string) list * tuple_set list
    35   type int_bound = int option * tuple_set list
    36 
    37   datatype formula =
    38     All of decl list * formula |
    39     Exist of decl list * formula |
    40     FormulaLet of expr_assign list * formula |
    41     FormulaIf of formula * formula * formula |
    42     Or of formula * formula |
    43     Iff of formula * formula |
    44     Implies of formula * formula |
    45     And of formula * formula |
    46     Not of formula |
    47     Acyclic of n_ary_index |
    48     Function of n_ary_index * rel_expr * rel_expr |
    49     Functional of n_ary_index * rel_expr * rel_expr |
    50     TotalOrdering of n_ary_index * rel_expr * rel_expr * rel_expr |
    51     Subset of rel_expr * rel_expr |
    52     RelEq of rel_expr * rel_expr |
    53     IntEq of int_expr * int_expr |
    54     LT of int_expr * int_expr |
    55     LE of int_expr * int_expr |
    56     No of rel_expr |
    57     Lone of rel_expr |
    58     One of rel_expr |
    59     Some of rel_expr |
    60     False |
    61     True |
    62     FormulaReg of int
    63   and rel_expr =
    64     RelLet of expr_assign list * rel_expr |
    65     RelIf of formula * rel_expr * rel_expr |
    66     Union of rel_expr * rel_expr |
    67     Difference of rel_expr * rel_expr |
    68     Override of rel_expr * rel_expr |
    69     Intersect of rel_expr * rel_expr |
    70     Product of rel_expr * rel_expr |
    71     IfNo of rel_expr * rel_expr |
    72     Project of rel_expr * int_expr list |
    73     Join of rel_expr * rel_expr |
    74     Closure of rel_expr |
    75     ReflexiveClosure of rel_expr |
    76     Transpose of rel_expr |
    77     Comprehension of decl list * formula |
    78     Bits of int_expr |
    79     Int of int_expr |
    80     Iden |
    81     Ints |
    82     None |
    83     Univ |
    84     Atom of int |
    85     AtomSeq of int * int |
    86     Rel of n_ary_index |
    87     Var of n_ary_index |
    88     RelReg of n_ary_index
    89   and int_expr =
    90     Sum of decl list * int_expr |
    91     IntLet of expr_assign list * int_expr |
    92     IntIf of formula * int_expr * int_expr |
    93     SHL of int_expr * int_expr |
    94     SHA of int_expr * int_expr |
    95     SHR of int_expr * int_expr |
    96     Add of int_expr * int_expr |
    97     Sub of int_expr * int_expr |
    98     Mult of int_expr * int_expr |
    99     Div of int_expr * int_expr |
   100     Mod of int_expr * int_expr |
   101     Cardinality of rel_expr |
   102     SetSum of rel_expr |
   103     BitOr of int_expr * int_expr |
   104     BitXor of int_expr * int_expr |
   105     BitAnd of int_expr * int_expr |
   106     BitNot of int_expr |
   107     Neg of int_expr |
   108     Absolute of int_expr |
   109     Signum of int_expr |
   110     Num of int |
   111     IntReg of int
   112   and decl =
   113     DeclNo of n_ary_index * rel_expr |
   114     DeclLone of n_ary_index * rel_expr |
   115     DeclOne of n_ary_index * rel_expr |
   116     DeclSome of n_ary_index * rel_expr |
   117     DeclSet of n_ary_index * rel_expr
   118   and expr_assign =
   119     AssignFormulaReg of int * formula |
   120     AssignRelReg of n_ary_index * rel_expr |
   121     AssignIntReg of int * int_expr
   122 
   123   type 'a fold_expr_funcs =
   124     {formula_func: formula -> 'a -> 'a,
   125      rel_expr_func: rel_expr -> 'a -> 'a,
   126      int_expr_func: int_expr -> 'a -> 'a}
   127 
   128   val kodkodi_version : unit -> int list
   129 
   130   val fold_formula : 'a fold_expr_funcs -> formula -> 'a -> 'a
   131   val fold_rel_expr : 'a fold_expr_funcs -> rel_expr -> 'a -> 'a
   132   val fold_int_expr : 'a fold_expr_funcs -> int_expr -> 'a -> 'a
   133   val fold_decl : 'a fold_expr_funcs -> decl -> 'a -> 'a
   134   val fold_expr_assign : 'a fold_expr_funcs -> expr_assign -> 'a -> 'a
   135 
   136   type 'a fold_tuple_funcs =
   137     {tuple_func: tuple -> 'a -> 'a,
   138      tuple_set_func: tuple_set -> 'a -> 'a}
   139 
   140   val fold_tuple : 'a fold_tuple_funcs -> tuple -> 'a -> 'a
   141   val fold_tuple_set : 'a fold_tuple_funcs -> tuple_set -> 'a -> 'a
   142   val fold_tuple_assign : 'a fold_tuple_funcs -> tuple_assign -> 'a -> 'a
   143   val fold_bound :
   144       'a fold_expr_funcs -> 'a fold_tuple_funcs -> bound -> 'a -> 'a
   145   val fold_int_bound : 'a fold_tuple_funcs -> int_bound -> 'a -> 'a
   146 
   147   type problem =
   148     {comment: string,
   149      settings: setting list,
   150      univ_card: int,
   151      tuple_assigns: tuple_assign list,
   152      bounds: bound list,
   153      int_bounds: int_bound list,
   154      expr_assigns: expr_assign list,
   155      formula: formula}
   156 
   157   type raw_bound = n_ary_index * int list list
   158 
   159   datatype outcome =
   160     JavaNotFound |
   161     JavaTooOld |
   162     KodkodiNotInstalled |
   163     KodkodiTooOld |
   164     Normal of (int * raw_bound list) list * int list * string |
   165     TimedOut of int list |
   166     Error of string * int list
   167 
   168   exception SYNTAX of string * string
   169 
   170   val max_arity : int -> int
   171   val arity_of_rel_expr : rel_expr -> int
   172   val is_problem_trivially_false : problem -> bool
   173   val problems_equivalent : problem * problem -> bool
   174   val solve_any_problem :
   175     bool -> bool -> Time.time -> int -> int -> problem list -> outcome
   176 end;
   177 
   178 structure Kodkod : KODKOD =
   179 struct
   180 
   181 type n_ary_index = int * int
   182 
   183 type setting = string * string
   184 
   185 datatype tuple =
   186   Tuple of int list |
   187   TupleIndex of n_ary_index |
   188   TupleReg of n_ary_index
   189 
   190 datatype tuple_set =
   191   TupleUnion of tuple_set * tuple_set |
   192   TupleDifference of tuple_set * tuple_set |
   193   TupleIntersect of tuple_set * tuple_set |
   194   TupleProduct of tuple_set * tuple_set |
   195   TupleProject of tuple_set * int |
   196   TupleSet of tuple list |
   197   TupleRange of tuple * tuple |
   198   TupleArea of tuple * tuple |
   199   TupleAtomSeq of int * int |
   200   TupleSetReg of n_ary_index
   201 
   202 datatype tuple_assign =
   203   AssignTuple of n_ary_index * tuple |
   204   AssignTupleSet of n_ary_index * tuple_set
   205 
   206 type bound = (n_ary_index * string) list * tuple_set list
   207 type int_bound = int option * tuple_set list
   208 
   209 datatype formula =
   210   All of decl list * formula |
   211   Exist of decl list * formula |
   212   FormulaLet of expr_assign list * formula |
   213   FormulaIf of formula * formula * formula |
   214   Or of formula * formula |
   215   Iff of formula * formula |
   216   Implies of formula * formula |
   217   And of formula * formula |
   218   Not of formula |
   219   Acyclic of n_ary_index |
   220   Function of n_ary_index * rel_expr * rel_expr |
   221   Functional of n_ary_index * rel_expr * rel_expr |
   222   TotalOrdering of n_ary_index * rel_expr * rel_expr * rel_expr |
   223   Subset of rel_expr * rel_expr |
   224   RelEq of rel_expr * rel_expr |
   225   IntEq of int_expr * int_expr |
   226   LT of int_expr * int_expr |
   227   LE of int_expr * int_expr |
   228   No of rel_expr |
   229   Lone of rel_expr |
   230   One of rel_expr |
   231   Some of rel_expr |
   232   False |
   233   True |
   234   FormulaReg of int
   235 and rel_expr =
   236   RelLet of expr_assign list * rel_expr |
   237   RelIf of formula * rel_expr * rel_expr |
   238   Union of rel_expr * rel_expr |
   239   Difference of rel_expr * rel_expr |
   240   Override of rel_expr * rel_expr |
   241   Intersect of rel_expr * rel_expr |
   242   Product of rel_expr * rel_expr |
   243   IfNo of rel_expr * rel_expr |
   244   Project of rel_expr * int_expr list |
   245   Join of rel_expr * rel_expr |
   246   Closure of rel_expr |
   247   ReflexiveClosure of rel_expr |
   248   Transpose of rel_expr |
   249   Comprehension of decl list * formula |
   250   Bits of int_expr |
   251   Int of int_expr |
   252   Iden |
   253   Ints |
   254   None |
   255   Univ |
   256   Atom of int |
   257   AtomSeq of int * int |
   258   Rel of n_ary_index |
   259   Var of n_ary_index |
   260   RelReg of n_ary_index
   261 and int_expr =
   262   Sum of decl list * int_expr |
   263   IntLet of expr_assign list * int_expr |
   264   IntIf of formula * int_expr * int_expr |
   265   SHL of int_expr * int_expr |
   266   SHA of int_expr * int_expr |
   267   SHR of int_expr * int_expr |
   268   Add of int_expr * int_expr |
   269   Sub of int_expr * int_expr |
   270   Mult of int_expr * int_expr |
   271   Div of int_expr * int_expr |
   272   Mod of int_expr * int_expr |
   273   Cardinality of rel_expr |
   274   SetSum of rel_expr |
   275   BitOr of int_expr * int_expr |
   276   BitXor of int_expr * int_expr |
   277   BitAnd of int_expr * int_expr |
   278   BitNot of int_expr |
   279   Neg of int_expr |
   280   Absolute of int_expr |
   281   Signum of int_expr |
   282   Num of int |
   283   IntReg of int
   284 and decl =
   285   DeclNo of n_ary_index * rel_expr |
   286   DeclLone of n_ary_index * rel_expr |
   287   DeclOne of n_ary_index * rel_expr |
   288   DeclSome of n_ary_index * rel_expr |
   289   DeclSet of n_ary_index * rel_expr
   290 and expr_assign =
   291   AssignFormulaReg of int * formula |
   292   AssignRelReg of n_ary_index * rel_expr |
   293   AssignIntReg of int * int_expr
   294 
   295 type problem =
   296   {comment: string,
   297    settings: setting list,
   298    univ_card: int,
   299    tuple_assigns: tuple_assign list,
   300    bounds: bound list,
   301    int_bounds: int_bound list,
   302    expr_assigns: expr_assign list,
   303    formula: formula}
   304 
   305 type raw_bound = n_ary_index * int list list
   306 
   307 datatype outcome =
   308   JavaNotFound |
   309   JavaTooOld |
   310   KodkodiNotInstalled |
   311   KodkodiTooOld |
   312   Normal of (int * raw_bound list) list * int list * string |
   313   TimedOut of int list |
   314   Error of string * int list
   315 
   316 exception SYNTAX of string * string
   317 
   318 type 'a fold_expr_funcs =
   319   {formula_func: formula -> 'a -> 'a,
   320    rel_expr_func: rel_expr -> 'a -> 'a,
   321    int_expr_func: int_expr -> 'a -> 'a}
   322 
   323 fun kodkodi_version () =
   324   getenv "KODKODI_VERSION"
   325   |> space_explode "."
   326   |> map (the_default 0 o Int.fromString)
   327 
   328 fun is_kodkodi_too_old () =
   329   dict_ord int_ord (kodkodi_version (), [1, 2, 14]) = LESS
   330 
   331 (** Auxiliary functions on Kodkod problems **)
   332 
   333 fun fold_formula (F : 'a fold_expr_funcs) formula =
   334   case formula of
   335     All (ds, f) => fold (fold_decl F) ds #> fold_formula F f
   336   | Exist (ds, f) => fold (fold_decl F) ds #> fold_formula F f
   337   | FormulaLet (bs, f) => fold (fold_expr_assign F) bs #> fold_formula F f
   338   | FormulaIf (f, f1, f2) =>
   339     fold_formula F f #> fold_formula F f1 #> fold_formula F f2
   340   | Or (f1, f2) => fold_formula F f1 #> fold_formula F f2
   341   | Iff (f1, f2) => fold_formula F f1 #> fold_formula F f2
   342   | Implies (f1, f2) => fold_formula F f1 #> fold_formula F f2
   343   | And (f1, f2) => fold_formula F f1 #> fold_formula F f2
   344   | Not f => fold_formula F f
   345   | Acyclic x => fold_rel_expr F (Rel x)
   346   | Function (x, r1, r2) =>
   347     fold_rel_expr F (Rel x) #> fold_rel_expr F r1 #> fold_rel_expr F r2
   348   | Functional (x, r1, r2) =>
   349     fold_rel_expr F (Rel x) #> fold_rel_expr F r1 #> fold_rel_expr F r2
   350   | TotalOrdering (x, r1, r2, r3) =>
   351     fold_rel_expr F (Rel x) #> fold_rel_expr F r1 #> fold_rel_expr F r2
   352     #> fold_rel_expr F r3
   353   | Subset (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
   354   | RelEq (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
   355   | IntEq (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
   356   | LT (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
   357   | LE (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
   358   | No r => fold_rel_expr F r
   359   | Lone r => fold_rel_expr F r
   360   | One r => fold_rel_expr F r
   361   | Some r => fold_rel_expr F r
   362   | False => #formula_func F formula
   363   | True => #formula_func F formula
   364   | FormulaReg _ => #formula_func F formula
   365 and fold_rel_expr F rel_expr =
   366   case rel_expr of
   367     RelLet (bs, r) => fold (fold_expr_assign F) bs #> fold_rel_expr F r
   368   | RelIf (f, r1, r2) =>
   369     fold_formula F f #> fold_rel_expr F r1 #> fold_rel_expr F r2
   370   | Union (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
   371   | Difference (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
   372   | Override (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
   373   | Intersect (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
   374   | Product (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
   375   | IfNo (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
   376   | Project (r1, is) => fold_rel_expr F r1 #> fold (fold_int_expr F) is
   377   | Join (r1, r2) => fold_rel_expr F r1 #> fold_rel_expr F r2
   378   | Closure r => fold_rel_expr F r
   379   | ReflexiveClosure r => fold_rel_expr F r
   380   | Transpose r => fold_rel_expr F r
   381   | Comprehension (ds, f) => fold (fold_decl F) ds #> fold_formula F f
   382   | Bits i => fold_int_expr F i
   383   | Int i => fold_int_expr F i
   384   | Iden => #rel_expr_func F rel_expr
   385   | Ints => #rel_expr_func F rel_expr
   386   | None => #rel_expr_func F rel_expr
   387   | Univ => #rel_expr_func F rel_expr
   388   | Atom _ => #rel_expr_func F rel_expr
   389   | AtomSeq _ => #rel_expr_func F rel_expr
   390   | Rel _ => #rel_expr_func F rel_expr
   391   | Var _ => #rel_expr_func F rel_expr
   392   | RelReg _ => #rel_expr_func F rel_expr
   393 and fold_int_expr F int_expr =
   394   case int_expr of
   395     Sum (ds, i) => fold (fold_decl F) ds #> fold_int_expr F i
   396   | IntLet (bs, i) => fold (fold_expr_assign F) bs #> fold_int_expr F i
   397   | IntIf (f, i1, i2) =>
   398     fold_formula F f #> fold_int_expr F i1 #> fold_int_expr F i2
   399   | SHL (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
   400   | SHA (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
   401   | SHR (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
   402   | Add (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
   403   | Sub (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
   404   | Mult (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
   405   | Div (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
   406   | Mod (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
   407   | Cardinality r => fold_rel_expr F r
   408   | SetSum r => fold_rel_expr F r
   409   | BitOr (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
   410   | BitXor (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
   411   | BitAnd (i1, i2) => fold_int_expr F i1 #> fold_int_expr F i2
   412   | BitNot i => fold_int_expr F i
   413   | Neg i => fold_int_expr F i
   414   | Absolute i => fold_int_expr F i
   415   | Signum i => fold_int_expr F i
   416   | Num _ => #int_expr_func F int_expr
   417   | IntReg _ => #int_expr_func F int_expr
   418 and fold_decl F decl =
   419   case decl of
   420     DeclNo (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r
   421   | DeclLone (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r
   422   | DeclOne (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r
   423   | DeclSome (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r
   424   | DeclSet (x, r) => fold_rel_expr F (Var x) #> fold_rel_expr F r
   425 and fold_expr_assign F assign =
   426   case assign of
   427     AssignFormulaReg (x, f) => fold_formula F (FormulaReg x) #> fold_formula F f
   428   | AssignRelReg (x, r) => fold_rel_expr F (RelReg x) #> fold_rel_expr F r
   429   | AssignIntReg (x, i) => fold_int_expr F (IntReg x) #> fold_int_expr F i
   430 
   431 type 'a fold_tuple_funcs =
   432   {tuple_func: tuple -> 'a -> 'a,
   433    tuple_set_func: tuple_set -> 'a -> 'a}
   434 
   435 fun fold_tuple (F : 'a fold_tuple_funcs) = #tuple_func F
   436 
   437 fun fold_tuple_set F tuple_set =
   438   case tuple_set of
   439     TupleUnion (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2
   440   | TupleDifference (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2
   441   | TupleIntersect (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2
   442   | TupleProduct (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2
   443   | TupleProject (ts, _) => fold_tuple_set F ts
   444   | TupleSet ts => fold (fold_tuple F) ts
   445   | TupleRange (t1, t2) => fold_tuple F t1 #> fold_tuple F t2
   446   | TupleArea (t1, t2) => fold_tuple F t1 #> fold_tuple F t2
   447   | TupleAtomSeq _ => #tuple_set_func F tuple_set
   448   | TupleSetReg _ => #tuple_set_func F tuple_set
   449 
   450 fun fold_tuple_assign F assign =
   451   case assign of
   452     AssignTuple (x, t) => fold_tuple F (TupleReg x) #> fold_tuple F t
   453   | AssignTupleSet (x, ts) =>
   454     fold_tuple_set F (TupleSetReg x) #> fold_tuple_set F ts
   455 
   456 fun fold_bound expr_F tuple_F (zs, tss) =
   457   fold (fold_rel_expr expr_F) (map (Rel o fst) zs)
   458   #> fold (fold_tuple_set tuple_F) tss
   459 
   460 fun fold_int_bound F (_, tss) = fold (fold_tuple_set F) tss
   461 
   462 fun max_arity univ_card = floor (Math.ln 2147483647.0
   463                                  / Math.ln (Real.fromInt univ_card))
   464 
   465 fun arity_of_rel_expr (RelLet (_, r)) = arity_of_rel_expr r
   466   | arity_of_rel_expr (RelIf (_, r1, _)) = arity_of_rel_expr r1
   467   | arity_of_rel_expr (Union (r1, _)) = arity_of_rel_expr r1
   468   | arity_of_rel_expr (Difference (r1, _)) = arity_of_rel_expr r1
   469   | arity_of_rel_expr (Override (r1, _)) = arity_of_rel_expr r1
   470   | arity_of_rel_expr (Intersect (r1, _)) = arity_of_rel_expr r1
   471   | arity_of_rel_expr (Product (r1, r2)) = sum_arities_of_rel_exprs r1 r2
   472   | arity_of_rel_expr (IfNo (r1, _)) = arity_of_rel_expr r1
   473   | arity_of_rel_expr (Project (_, is)) = length is
   474   | arity_of_rel_expr (Join (r1, r2)) = sum_arities_of_rel_exprs r1 r2 - 2
   475   | arity_of_rel_expr (Closure _) = 2
   476   | arity_of_rel_expr (ReflexiveClosure _) = 2
   477   | arity_of_rel_expr (Transpose _) = 2
   478   | arity_of_rel_expr (Comprehension (ds, _)) =
   479     fold (curry op + o arity_of_decl) ds 0
   480   | arity_of_rel_expr (Bits _) = 1
   481   | arity_of_rel_expr (Int _) = 1
   482   | arity_of_rel_expr Iden = 2
   483   | arity_of_rel_expr Ints = 1
   484   | arity_of_rel_expr None = 1
   485   | arity_of_rel_expr Univ = 1
   486   | arity_of_rel_expr (Atom _) = 1
   487   | arity_of_rel_expr (AtomSeq _) = 1
   488   | arity_of_rel_expr (Rel (n, _)) = n
   489   | arity_of_rel_expr (Var (n, _)) = n
   490   | arity_of_rel_expr (RelReg (n, _)) = n
   491 and sum_arities_of_rel_exprs r1 r2 = arity_of_rel_expr r1 + arity_of_rel_expr r2
   492 and arity_of_decl (DeclNo ((n, _), _)) = n
   493   | arity_of_decl (DeclLone ((n, _), _)) = n
   494   | arity_of_decl (DeclOne ((n, _), _)) = n
   495   | arity_of_decl (DeclSome ((n, _), _)) = n
   496   | arity_of_decl (DeclSet ((n, _), _)) = n
   497 
   498 fun is_problem_trivially_false ({formula = False, ...} : problem) = true
   499   | is_problem_trivially_false _ = false
   500 
   501 val chop_solver = take 2 o space_explode ","
   502 
   503 fun settings_equivalent ([], []) = true
   504   | settings_equivalent ((key1, value1) :: settings1,
   505                          (key2, value2) :: settings2) =
   506     key1 = key2 andalso
   507     (value1 = value2 orelse key1 = "delay" orelse
   508      (key1 = "solver" andalso chop_solver value1 = chop_solver value2)) andalso
   509     settings_equivalent (settings1, settings2)
   510   | settings_equivalent _ = false
   511 
   512 fun problems_equivalent (p1 : problem, p2 : problem) =
   513   #univ_card p1 = #univ_card p2 andalso
   514   #formula p1 = #formula p2 andalso
   515   #bounds p1 = #bounds p2 andalso
   516   #expr_assigns p1 = #expr_assigns p2 andalso
   517   #tuple_assigns p1 = #tuple_assigns p2 andalso
   518   #int_bounds p1 = #int_bounds p2 andalso
   519   settings_equivalent (#settings p1, #settings p2)
   520 
   521 (** Serialization of problem **)
   522 
   523 fun base_name j =
   524   if j < 0 then string_of_int (~j - 1) ^ "'" else string_of_int j
   525 
   526 fun n_ary_name (1, j) prefix _ _ = prefix ^ base_name j
   527   | n_ary_name (2, j) _ prefix _ = prefix ^ base_name j
   528   | n_ary_name (n, j) _ _ prefix = prefix ^ string_of_int n ^ "_" ^ base_name j
   529 
   530 fun atom_name j = "A" ^ base_name j
   531 fun atom_seq_name (k, 0) = "u" ^ base_name k
   532   | atom_seq_name (k, j0) = "u" ^ base_name k ^ "@" ^ base_name j0
   533 fun formula_reg_name j = "$f" ^ base_name j
   534 fun rel_reg_name j = "$e" ^ base_name j
   535 fun int_reg_name j = "$i" ^ base_name j
   536 
   537 fun tuple_name x = n_ary_name x "A" "P" "T"
   538 fun rel_name x = n_ary_name x "s" "r" "m"
   539 fun var_name x = n_ary_name x "S" "R" "M"
   540 fun tuple_reg_name x = n_ary_name x "$A" "$P" "$T"
   541 fun tuple_set_reg_name x = n_ary_name x "$a" "$p" "$t"
   542 
   543 fun inline_comment "" = ""
   544   | inline_comment comment =
   545     " /* " ^ translate_string (fn "\n" => " " | "*" => "* " | s => s) comment ^
   546     " */"
   547 
   548 fun block_comment "" = ""
   549   | block_comment comment = prefix_lines "// " comment ^ "\n"
   550 
   551 fun commented_rel_name (x, s) = rel_name x ^ inline_comment s
   552 
   553 fun string_for_tuple (Tuple js) = "[" ^ commas (map atom_name js) ^ "]"
   554   | string_for_tuple (TupleIndex x) = tuple_name x
   555   | string_for_tuple (TupleReg x) = tuple_reg_name x
   556 
   557 val no_prec = 100
   558 val prec_TupleUnion = 1
   559 val prec_TupleIntersect = 2
   560 val prec_TupleProduct = 3
   561 val prec_TupleProject = 4
   562 
   563 fun precedence_ts (TupleUnion _) = prec_TupleUnion
   564   | precedence_ts (TupleDifference _) = prec_TupleUnion
   565   | precedence_ts (TupleIntersect _) = prec_TupleIntersect
   566   | precedence_ts (TupleProduct _) = prec_TupleProduct
   567   | precedence_ts (TupleProject _) = prec_TupleProject
   568   | precedence_ts _ = no_prec
   569 
   570 fun string_for_tuple_set tuple_set =
   571   let
   572     fun sub tuple_set outer_prec =
   573       let
   574         val prec = precedence_ts tuple_set
   575         val need_parens = (prec < outer_prec)
   576       in
   577         (if need_parens then "(" else "") ^
   578         (case tuple_set of
   579            TupleUnion (ts1, ts2) => sub ts1 prec ^ " + " ^ sub ts2 (prec + 1)
   580          | TupleDifference (ts1, ts2) =>
   581            sub ts1 prec ^ " - " ^ sub ts2 (prec + 1)
   582          | TupleIntersect (ts1, ts2) => sub ts1 prec ^ " & " ^ sub ts2 prec
   583          | TupleProduct (ts1, ts2) => sub ts1 prec ^ "->" ^ sub ts2 prec
   584          | TupleProject (ts, c) => sub ts prec ^ "[" ^ string_of_int c ^ "]"
   585          | TupleSet ts => "{" ^ commas (map string_for_tuple ts) ^ "}"
   586          | TupleRange (t1, t2) =>
   587            "{" ^ string_for_tuple t1 ^
   588            (if t1 = t2 then "" else " .. " ^ string_for_tuple t2) ^ "}"
   589          | TupleArea (t1, t2) =>
   590            "{" ^ string_for_tuple t1 ^ " # " ^ string_for_tuple t2 ^ "}"
   591          | TupleAtomSeq x => atom_seq_name x
   592          | TupleSetReg x => tuple_set_reg_name x) ^
   593         (if need_parens then ")" else "")
   594       end
   595   in sub tuple_set 0 end
   596 
   597 fun string_for_tuple_assign (AssignTuple (x, t)) =
   598     tuple_reg_name x ^ " := " ^ string_for_tuple t ^ "\n"
   599   | string_for_tuple_assign (AssignTupleSet (x, ts)) =
   600     tuple_set_reg_name x ^ " := " ^ string_for_tuple_set ts ^ "\n"
   601 
   602 fun string_for_bound (zs, tss) =
   603   "bounds " ^ commas (map commented_rel_name zs) ^ ": " ^
   604   (if length tss = 1 then "" else "[") ^ commas (map string_for_tuple_set tss) ^
   605   (if length tss = 1 then "" else "]") ^ "\n"
   606 
   607 fun int_string_for_bound (opt_n, tss) =
   608   (case opt_n of
   609      SOME n => signed_string_of_int n ^ ": "
   610    | NONE => "") ^ "[" ^ commas (map string_for_tuple_set tss) ^ "]"
   611 
   612 val prec_All = 1
   613 val prec_Or = 2
   614 val prec_Iff = 3
   615 val prec_Implies = 4
   616 val prec_And = 5
   617 val prec_Not = 6
   618 val prec_Eq = 7
   619 val prec_Some = 8
   620 val prec_SHL = 9
   621 val prec_Add = 10
   622 val prec_Mult = 11
   623 val prec_Override = 12
   624 val prec_Intersect = 13
   625 val prec_Product = 14
   626 val prec_IfNo = 15
   627 val prec_Project = 17
   628 val prec_Join = 18
   629 val prec_BitNot = 19
   630 
   631 fun precedence_f (All _) = prec_All
   632   | precedence_f (Exist _) = prec_All
   633   | precedence_f (FormulaLet _) = prec_All
   634   | precedence_f (FormulaIf _) = prec_All
   635   | precedence_f (Or _) = prec_Or
   636   | precedence_f (Iff _) = prec_Iff
   637   | precedence_f (Implies _) = prec_Implies
   638   | precedence_f (And _) = prec_And
   639   | precedence_f (Not _) = prec_Not
   640   | precedence_f (Acyclic _) = no_prec
   641   | precedence_f (Function _) = no_prec
   642   | precedence_f (Functional _) = no_prec
   643   | precedence_f (TotalOrdering _) = no_prec
   644   | precedence_f (Subset _) = prec_Eq
   645   | precedence_f (RelEq _) = prec_Eq
   646   | precedence_f (IntEq _) = prec_Eq
   647   | precedence_f (LT _) = prec_Eq
   648   | precedence_f (LE _) = prec_Eq
   649   | precedence_f (No _) = prec_Some
   650   | precedence_f (Lone _) = prec_Some
   651   | precedence_f (One _) = prec_Some
   652   | precedence_f (Some _) = prec_Some
   653   | precedence_f False = no_prec
   654   | precedence_f True = no_prec
   655   | precedence_f (FormulaReg _) = no_prec
   656 and precedence_r (RelLet _) = prec_All
   657   | precedence_r (RelIf _) = prec_All
   658   | precedence_r (Union _) = prec_Add
   659   | precedence_r (Difference _) = prec_Add
   660   | precedence_r (Override _) = prec_Override
   661   | precedence_r (Intersect _) = prec_Intersect
   662   | precedence_r (Product _) = prec_Product
   663   | precedence_r (IfNo _) = prec_IfNo
   664   | precedence_r (Project _) = prec_Project
   665   | precedence_r (Join _) = prec_Join
   666   | precedence_r (Closure _) = prec_BitNot
   667   | precedence_r (ReflexiveClosure _) = prec_BitNot
   668   | precedence_r (Transpose _) = prec_BitNot
   669   | precedence_r (Comprehension _) = no_prec
   670   | precedence_r (Bits _) = no_prec
   671   | precedence_r (Int _) = no_prec
   672   | precedence_r Iden = no_prec
   673   | precedence_r Ints = no_prec
   674   | precedence_r None = no_prec
   675   | precedence_r Univ = no_prec
   676   | precedence_r (Atom _) = no_prec
   677   | precedence_r (AtomSeq _) = no_prec
   678   | precedence_r (Rel _) = no_prec
   679   | precedence_r (Var _) = no_prec
   680   | precedence_r (RelReg _) = no_prec
   681 and precedence_i (Sum _) = prec_All
   682   | precedence_i (IntLet _) = prec_All
   683   | precedence_i (IntIf _) = prec_All
   684   | precedence_i (SHL _) = prec_SHL
   685   | precedence_i (SHA _) = prec_SHL
   686   | precedence_i (SHR _) = prec_SHL
   687   | precedence_i (Add _) = prec_Add
   688   | precedence_i (Sub _) = prec_Add
   689   | precedence_i (Mult _) = prec_Mult
   690   | precedence_i (Div _) = prec_Mult
   691   | precedence_i (Mod _) = prec_Mult
   692   | precedence_i (Cardinality _) = no_prec
   693   | precedence_i (SetSum _) = no_prec
   694   | precedence_i (BitOr _) = prec_Intersect
   695   | precedence_i (BitXor _) = prec_Intersect
   696   | precedence_i (BitAnd _) = prec_Intersect
   697   | precedence_i (BitNot _) = prec_BitNot
   698   | precedence_i (Neg _) = prec_BitNot
   699   | precedence_i (Absolute _) = prec_BitNot
   700   | precedence_i (Signum _) = prec_BitNot
   701   | precedence_i (Num _) = no_prec
   702   | precedence_i (IntReg _) = no_prec
   703 
   704 fun write_problem_file out problems =
   705   let
   706     fun out_outmost_f (And (f1, f2)) =
   707         (out_outmost_f f1; out "\n   && "; out_outmost_f f2)
   708       | out_outmost_f f = out_f f prec_And
   709     and out_f formula outer_prec =
   710       let
   711         val prec = precedence_f formula
   712         val need_parens = (prec < outer_prec)
   713       in
   714         (if need_parens then out "(" else ());
   715         (case formula of
   716            All (ds, f) => (out "all ["; out_decls ds; out "] | "; out_f f prec)
   717          | Exist (ds, f) =>
   718            (out "some ["; out_decls ds; out "] | "; out_f f prec)
   719          | FormulaLet (bs, f) =>
   720            (out "let ["; out_assigns bs; out "] | "; out_f f prec)
   721          | FormulaIf (f, f1, f2) =>
   722            (out "if "; out_f f prec; out " then "; out_f f1 prec; out " else ";
   723             out_f f2 prec)
   724          | Or (f1, f2) => (out_f f1 prec; out " || "; out_f f2 prec)
   725          | Iff (f1, f2) => (out_f f1 prec; out " <=> "; out_f f2 prec)
   726          | Implies (f1, f2) => (out_f f1 (prec + 1); out " => "; out_f f2 prec)
   727          | And (f1, f2) => (out_f f1 prec; out " && "; out_f f2 prec)
   728          | Not f => (out "! "; out_f f prec)
   729          | Acyclic x => out ("ACYCLIC(" ^ rel_name x ^ ")")
   730          | Function (x, r1, r2) =>
   731            (out ("FUNCTION(" ^ rel_name x ^ ", "); out_r r1 0; out " -> one ";
   732             out_r r2 0; out ")")
   733          | Functional (x, r1, r2) =>
   734            (out ("FUNCTION(" ^ rel_name x ^ ", "); out_r r1 0; out " -> lone ";
   735             out_r r2 0; out ")")
   736          | TotalOrdering (x, r1, r2, r3) =>
   737            (out ("TOTAL_ORDERING(" ^ rel_name x ^ ", "); out_r r1 0; out ", ";
   738             out_r r2 0; out ", "; out_r r3 0; out ")")
   739          | Subset (r1, r2) => (out_r r1 prec; out " in "; out_r r2 prec)
   740          | RelEq (r1, r2) => (out_r r1 prec; out " = "; out_r r2 prec)
   741          | IntEq (i1, i2) => (out_i i1 prec; out " = "; out_i i2 prec)
   742          | LT (i1, i2) => (out_i i1 prec; out " < "; out_i i2 prec)
   743          | LE (i1, i2) => (out_i i1 prec; out " <= "; out_i i2 prec)
   744          | No r => (out "no "; out_r r prec)
   745          | Lone r => (out "lone "; out_r r prec)
   746          | One r => (out "one "; out_r r prec)
   747          | Some r => (out "some "; out_r r prec)
   748          | False => out "false"
   749          | True => out "true"
   750          | FormulaReg j => out (formula_reg_name j));
   751         (if need_parens then out ")" else ())
   752       end
   753     and out_r rel_expr outer_prec =
   754       let
   755         val prec = precedence_r rel_expr
   756         val need_parens = (prec < outer_prec)
   757       in
   758         (if need_parens then out "(" else ());
   759         (case rel_expr of
   760            RelLet (bs, r) =>
   761            (out "let ["; out_assigns bs; out "] | "; out_r r prec)
   762          | RelIf (f, r1, r2) =>
   763            (out "if "; out_f f prec; out " then "; out_r r1 prec;
   764             out " else "; out_r r2 prec)
   765          | Union (r1, r2) => (out_r r1 prec; out " + "; out_r r2 (prec + 1))
   766          | Difference (r1, r2) =>
   767            (out_r r1 prec; out " - "; out_r r2 (prec + 1))
   768          | Override (r1, r2) => (out_r r1 prec; out " ++ "; out_r r2 prec)
   769          | Intersect (r1, r2) => (out_r r1 prec; out " & "; out_r r2 prec)
   770          | Product (r1, r2) => (out_r r1 prec; out "->"; out_r r2 prec)
   771          | IfNo (r1, r2) => (out_r r1 prec; out "\\"; out_r r2 prec)
   772          | Project (r1, is) => (out_r r1 prec; out "["; out_columns is; out "]")
   773          | Join (r1, r2) => (out_r r1 prec; out "."; out_r r2 (prec + 1))
   774          | Closure r => (out "^"; out_r r prec)
   775          | ReflexiveClosure r => (out "*"; out_r r prec)
   776          | Transpose r => (out "~"; out_r r prec)
   777          | Comprehension (ds, f) =>
   778            (out "{["; out_decls ds; out "] | "; out_f f 0; out "}")
   779          | Bits i => (out "Bits["; out_i i 0; out "]")
   780          | Int i => (out "Int["; out_i i 0; out "]")
   781          | Iden => out "iden"
   782          | Ints => out "ints"
   783          | None => out "none"
   784          | Univ => out "univ"
   785          | Atom j => out (atom_name j)
   786          | AtomSeq x => out (atom_seq_name x)
   787          | Rel x => out (rel_name x)
   788          | Var x => out (var_name x)
   789          | RelReg (_, j) => out (rel_reg_name j));
   790         (if need_parens then out ")" else ())
   791       end
   792     and out_i int_expr outer_prec =
   793       let
   794         val prec = precedence_i int_expr
   795         val need_parens = (prec < outer_prec)
   796       in
   797         (if need_parens then out "(" else ());
   798         (case int_expr of
   799            Sum (ds, i) => (out "sum ["; out_decls ds; out "] | "; out_i i prec)
   800          | IntLet (bs, i) =>
   801            (out "let ["; out_assigns bs; out "] | "; out_i i prec)
   802          | IntIf (f, i1, i2) =>
   803            (out "if "; out_f f prec; out " then "; out_i i1 prec;
   804             out " else "; out_i i2 prec)
   805          | SHL (i1, i2) => (out_i i1 prec; out " << "; out_i i2 (prec + 1))
   806          | SHA (i1, i2) => (out_i i1 prec; out " >> "; out_i i2 (prec + 1))
   807          | SHR (i1, i2) => (out_i i1 prec; out " >>> "; out_i i2 (prec + 1))
   808          | Add (i1, i2) => (out_i i1 prec; out " + "; out_i i2 (prec + 1))
   809          | Sub (i1, i2) => (out_i i1 prec; out " - "; out_i i2 (prec + 1))
   810          | Mult (i1, i2) => (out_i i1 prec; out " * "; out_i i2 (prec + 1))
   811          | Div (i1, i2) => (out_i i1 prec; out " / "; out_i i2 (prec + 1))
   812          | Mod (i1, i2) => (out_i i1 prec; out " % "; out_i i2 (prec + 1))
   813          | Cardinality r => (out "#("; out_r r 0; out ")")
   814          | SetSum r => (out "sum("; out_r r 0; out ")")
   815          | BitOr (i1, i2) => (out_i i1 prec; out " | "; out_i i2 prec)
   816          | BitXor (i1, i2) => (out_i i1 prec; out " ^ "; out_i i2 prec)
   817          | BitAnd (i1, i2) => (out_i i1 prec; out " & "; out_i i2 prec)
   818          | BitNot i => (out "~"; out_i i prec)
   819          | Neg i => (out "-"; out_i i prec)
   820          | Absolute i => (out "abs "; out_i i prec)
   821          | Signum i => (out "sgn "; out_i i prec)
   822          | Num k => out (signed_string_of_int k)
   823          | IntReg j => out (int_reg_name j));
   824         (if need_parens then out ")" else ())
   825       end
   826     and out_decls [] = ()
   827       | out_decls [d] = out_decl d
   828       | out_decls (d :: ds) = (out_decl d; out ", "; out_decls ds)
   829     and out_decl (DeclNo (x, r)) =
   830         (out (var_name x); out " : no "; out_r r 0)
   831       | out_decl (DeclLone (x, r)) =
   832         (out (var_name x); out " : lone "; out_r r 0)
   833       | out_decl (DeclOne (x, r)) =
   834         (out (var_name x); out " : one "; out_r r 0)
   835       | out_decl (DeclSome (x, r)) =
   836         (out (var_name x); out " : some "; out_r r 0)
   837       | out_decl (DeclSet (x, r)) =
   838         (out (var_name x); out " : set "; out_r r 0)
   839     and out_assigns [] = ()
   840       | out_assigns [b] = out_assign b
   841       | out_assigns (b :: bs) = (out_assign b; out ", "; out_assigns bs)
   842     and out_assign (AssignFormulaReg (j, f)) =
   843         (out (formula_reg_name j); out " := "; out_f f 0)
   844       | out_assign (AssignRelReg ((_, j), r)) =
   845         (out (rel_reg_name j); out " := "; out_r r 0)
   846       | out_assign (AssignIntReg (j, i)) =
   847         (out (int_reg_name j); out " := "; out_i i 0)
   848     and out_columns [] = ()
   849       | out_columns [i] = out_i i 0
   850       | out_columns (i :: is) = (out_i i 0; out ", "; out_columns is)
   851     and out_problem {comment, settings, univ_card, tuple_assigns, bounds,
   852                      int_bounds, expr_assigns, formula} =
   853         (out ("\n" ^ block_comment comment ^
   854               implode (map (fn (key, value) => key ^ ": " ^ value ^ "\n")
   855                             settings) ^
   856               "univ: " ^ atom_seq_name (univ_card, 0) ^ "\n" ^
   857               implode (map string_for_tuple_assign tuple_assigns) ^
   858               implode (map string_for_bound bounds) ^
   859               (if int_bounds = [] then
   860                  ""
   861                else
   862                  "int_bounds: " ^
   863                  commas (map int_string_for_bound int_bounds) ^ "\n"));
   864          map (fn b => (out_assign b; out ";")) expr_assigns;
   865          out "solve "; out_outmost_f formula; out ";\n")
   866   in
   867     out ("// This file was generated by Isabelle (most likely Nitpick)\n" ^
   868          "// " ^ ATP_Util.timestamp () ^ "\n");
   869     map out_problem problems
   870   end
   871 
   872 (** Parsing of solution **)
   873 
   874 fun is_ident_char s =
   875   Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse
   876   s = "_" orelse s = "'" orelse s = "$"
   877 
   878 fun strip_blanks [] = []
   879   | strip_blanks (" " :: ss) = strip_blanks ss
   880   | strip_blanks [s1, " "] = [s1]
   881   | strip_blanks (s1 :: " " :: s2 :: ss) =
   882     if is_ident_char s1 andalso is_ident_char s2 then
   883       s1 :: " " :: strip_blanks (s2 :: ss)
   884     else
   885       strip_blanks (s1 :: s2 :: ss)
   886   | strip_blanks (s :: ss) = s :: strip_blanks ss
   887 
   888 val scan_nat =
   889   Scan.repeat1 (Scan.one Symbol.is_ascii_digit)
   890   >> (the o Int.fromString o implode)
   891 val scan_rel_name =
   892   ($$ "s" |-- scan_nat >> pair 1
   893    || $$ "r" |-- scan_nat >> pair 2
   894    || ($$ "m" |-- scan_nat --| $$ "_") -- scan_nat) -- Scan.option ($$ "'")
   895   >> (fn ((n, j), SOME _) => (n, ~j - 1)
   896        | ((n, j), NONE) => (n, j))
   897 val scan_atom = $$ "A" |-- scan_nat
   898 fun parse_non_empty_list scan = scan ::: Scan.repeat ($$ "," |-- scan)
   899 fun parse_list scan = parse_non_empty_list scan || Scan.succeed []
   900 val parse_tuple = $$ "[" |-- parse_list scan_atom --| $$ "]"
   901 val parse_tuple_set = $$ "[" |-- parse_list parse_tuple --| $$ "]"
   902 val parse_assignment = (scan_rel_name --| $$ "=") -- parse_tuple_set
   903 val parse_instance =
   904   Scan.this_string "relations:"
   905   |-- $$ "{" |-- parse_list parse_assignment --| $$ "}"
   906 
   907 val extract_instance =
   908   fst o Scan.finite Symbol.stopper
   909             (Scan.error (!! (fn _ =>
   910                                 raise SYNTAX ("Kodkod.extract_instance",
   911                                               "ill-formed Kodkodi output"))
   912                             parse_instance))
   913   o strip_blanks o raw_explode
   914 
   915 val problem_marker = "*** PROBLEM "
   916 val outcome_marker = "---OUTCOME---\n"
   917 val instance_marker = "---INSTANCE---\n"
   918 
   919 fun read_section_body marker =
   920   Substring.string o fst o Substring.position "\n\n"
   921   o Substring.triml (size marker)
   922 
   923 fun read_next_instance s =
   924   let val s = Substring.position instance_marker s |> snd in
   925     if Substring.isEmpty s then
   926       raise SYNTAX ("Kodkod.read_next_instance", "expected \"INSTANCE\" marker")
   927     else
   928       read_section_body instance_marker s |> extract_instance
   929   end
   930 
   931 fun read_next_outcomes j (s, ps, js) =
   932   let val (s1, s2) = Substring.position outcome_marker s in
   933     if Substring.isEmpty s2 orelse
   934        not (Substring.isEmpty (Substring.position problem_marker s1
   935                                |> snd)) then
   936       (s, ps, js)
   937     else
   938       let
   939         val outcome = read_section_body outcome_marker s2
   940         val s = Substring.triml (size outcome_marker) s2
   941       in
   942         if String.isSuffix "UNSATISFIABLE" outcome then
   943           read_next_outcomes j (s, ps, j :: js)
   944         else if String.isSuffix "SATISFIABLE" outcome then
   945           read_next_outcomes j (s, (j, read_next_instance s2) :: ps, js)
   946         else
   947           raise SYNTAX ("Kodkod.read_next_outcomes",
   948                         "unknown outcome " ^ quote outcome)
   949       end
   950   end
   951 
   952 fun read_next_problems (s, ps, js) =
   953   let val s = Substring.position problem_marker s |> snd in
   954     if Substring.isEmpty s then
   955       (ps, js)
   956     else
   957       let
   958         val s = Substring.triml (size problem_marker) s
   959         val j_plus_1 = s |> Substring.takel (not_equal #" ") |> Substring.string
   960                          |> Int.fromString |> the
   961         val j = j_plus_1 - 1
   962       in read_next_problems (read_next_outcomes j (s, ps, js)) end
   963   end
   964   handle Option.Option => raise SYNTAX ("Kodkod.read_next_problems",
   965                                         "expected number after \"PROBLEM\"")
   966 
   967 fun read_output_file path =
   968   (false,
   969    read_next_problems (Substring.full (File.read path), [], [])
   970    |>> rev ||> rev)
   971   handle IO.Io _ => (true, ([], [])) | OS.SysErr _ => (true, ([], []))
   972 
   973 (** Main Kodkod entry point **)
   974 
   975 val created_temp_dir = Unsynchronized.ref false
   976 
   977 fun serial_string_and_temporary_dir_for_overlord overlord =
   978   if overlord then
   979     ("", getenv "ISABELLE_HOME_USER")
   980   else
   981     let
   982       val dir = getenv "ISABELLE_TMP"
   983       val _ = if !created_temp_dir then ()
   984               else (created_temp_dir := true; Isabelle_System.mkdirs (Path.explode dir))
   985     in (serial_string (), dir) end
   986 
   987 (* The fudge term below is to account for Kodkodi's slow start-up time, which
   988    is partly due to the JVM and partly due to the ML "bash" function. *)
   989 val fudge_ms = 250
   990 
   991 fun milliseconds_until_deadline deadline =
   992   Int.max (0, Time.toMilliseconds (deadline - Time.now ()) - fudge_ms)
   993 
   994 fun uncached_solve_any_problem overlord deadline max_threads max_solutions
   995                                problems =
   996   let
   997     val j = find_index (curry (op =) True o #formula) problems
   998     val indexed_problems = if j >= 0 then
   999                              [(j, nth problems j)]
  1000                            else
  1001                              filter_out (is_problem_trivially_false o snd)
  1002                                         (0 upto length problems - 1 ~~ problems)
  1003     val triv_js = filter_out (AList.defined (op =) indexed_problems)
  1004                              (0 upto length problems - 1)
  1005     val reindex = fst o nth indexed_problems
  1006   in
  1007     if null indexed_problems then
  1008       Normal ([], triv_js, "")
  1009     else
  1010       let
  1011         val (serial_str, temp_dir) =
  1012           serial_string_and_temporary_dir_for_overlord overlord
  1013         fun path_for suf =
  1014           Path.explode (temp_dir ^ "/kodkodi" ^ serial_str ^ "." ^ suf)
  1015         val in_path = path_for "kki"
  1016         val in_buf = Unsynchronized.ref Buffer.empty
  1017         fun out s = Unsynchronized.change in_buf (Buffer.add s)
  1018         val out_path = path_for "out"
  1019         val err_path = path_for "err"
  1020         val _ = write_problem_file out (map snd indexed_problems)
  1021         val _ = File.write_buffer in_path (!in_buf)
  1022         fun remove_temporary_files () =
  1023           if overlord then ()
  1024           else List.app (K () o try File.rm) [in_path, out_path, err_path]
  1025       in
  1026         let
  1027           val ms = milliseconds_until_deadline deadline
  1028           val outcome =
  1029             let
  1030               val code =
  1031                 Isabelle_System.bash ("cd " ^ File.bash_string temp_dir ^ ";\n\
  1032                       \\"$KODKODI/bin/kodkodi\"" ^
  1033                       (if ms >= 0 then " -max-msecs " ^ string_of_int ms
  1034                        else "") ^
  1035                       (if max_solutions > 1 then " -solve-all" else "") ^
  1036                       " -max-solutions " ^ string_of_int max_solutions ^
  1037                       (if max_threads > 0 then
  1038                          " -max-threads " ^ string_of_int max_threads
  1039                        else
  1040                          "") ^
  1041                       " < " ^ File.bash_path in_path ^
  1042                       " > " ^ File.bash_path out_path ^
  1043                       " 2> " ^ File.bash_path err_path)
  1044               val (io_error, (ps, nontriv_js)) =
  1045                 read_output_file out_path
  1046                 ||> apfst (map (apfst reindex)) ||> apsnd (map reindex)
  1047               val js = triv_js @ nontriv_js
  1048               val first_error =
  1049                 (File.fold_lines (fn line => fn "" => line | s => s) err_path ""
  1050                  handle IO.Io _ => "" | OS.SysErr _ => "")
  1051                 |> perhaps (try (unsuffix "\r"))
  1052                 |> perhaps (try (unsuffix "."))
  1053                 |> perhaps (try (unprefix "Solve error: "))
  1054                 |> perhaps (try (unprefix "Error: "))
  1055               fun has_error s =
  1056                 first_error |> Substring.full |> Substring.position s |> snd
  1057                             |> Substring.isEmpty |> not
  1058             in
  1059               if null ps then
  1060                 if code = 2 then
  1061                   TimedOut js
  1062                 else if code = 0 then
  1063                   Normal ([], js, first_error)
  1064                 else if code = 127 then
  1065                   JavaNotFound
  1066                 else if has_error "UnsupportedClassVersionError" then
  1067                   JavaTooOld
  1068                 else if has_error "NoClassDefFoundError" then
  1069                   KodkodiNotInstalled
  1070                 else if is_kodkodi_too_old () then
  1071                   KodkodiTooOld
  1072                 else if first_error <> "" then
  1073                   Error (first_error, js)
  1074                 else if io_error then
  1075                   Error ("I/O error", js)
  1076                 else
  1077                   Error ("Unknown error", js)
  1078               else
  1079                 Normal (ps, js, first_error)
  1080             end
  1081         in remove_temporary_files (); outcome end
  1082       end
  1083   end
  1084 
  1085 val cached_outcome =
  1086   Synchronized.var "Kodkod.cached_outcome"
  1087                    (NONE : ((int * problem list) * outcome) option)
  1088 
  1089 fun solve_any_problem debug overlord deadline max_threads max_solutions
  1090                       problems =
  1091   let
  1092     fun do_solve () =
  1093       uncached_solve_any_problem overlord deadline max_threads max_solutions
  1094                                  problems
  1095   in
  1096     if debug orelse overlord then
  1097       do_solve ()
  1098     else
  1099       case AList.lookup (fn ((max1, ps1), (max2, ps2)) =>
  1100                             max1 = max2 andalso length ps1 = length ps2 andalso
  1101                             forall problems_equivalent (ps1 ~~ ps2))
  1102                         (the_list (Synchronized.value cached_outcome))
  1103                         (max_solutions, problems) of
  1104         SOME outcome => outcome
  1105       | NONE =>
  1106         let val outcome = do_solve () in
  1107           (case outcome of
  1108              Normal (_, _, "") =>
  1109              Synchronized.change cached_outcome
  1110                                  (K (SOME ((max_solutions, problems), outcome)))
  1111            | _ => ());
  1112           outcome
  1113         end
  1114   end
  1115 
  1116 end;