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