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