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