src/HOL/Tools/Function/scnp_solve.ML
author wenzelm
Tue Sep 29 16:24:36 2009 +0200 (2009-09-29)
changeset 32740 9dd0a2f83429
parent 31775 2b04504fcb69
child 33002 f3f02f36a3e2
permissions -rw-r--r--
explicit indication of Unsynchronized.ref;
haftmann@31775
     1
(*  Title:       HOL/Tools/Function/scnp_solve.ML
krauss@29125
     2
    Author:      Armin Heller, TU Muenchen
krauss@29125
     3
    Author:      Alexander Krauss, TU Muenchen
krauss@29125
     4
krauss@29125
     5
Generate certificates for SCNP using a SAT solver
krauss@29125
     6
*)
krauss@29125
     7
krauss@29125
     8
krauss@29125
     9
signature SCNP_SOLVE =
krauss@29125
    10
sig
krauss@29125
    11
krauss@29125
    12
  datatype edge = GTR | GEQ
krauss@29125
    13
  datatype graph = G of int * int * (int * edge * int) list
krauss@29125
    14
  datatype graph_problem = GP of int list * graph list
krauss@29125
    15
krauss@29125
    16
  datatype label = MIN | MAX | MS
krauss@29125
    17
krauss@29125
    18
  type certificate =
krauss@29125
    19
    label                   (* which order *)
krauss@29125
    20
    * (int * int) list list (* (multi)sets *)
krauss@29125
    21
    * int list              (* strictly ordered calls *)
krauss@29125
    22
    * (int -> bool -> int -> (int * int) option) (* covering function *)
krauss@29125
    23
krauss@29125
    24
  val generate_certificate : bool -> label list -> graph_problem -> certificate option
krauss@29125
    25
wenzelm@32740
    26
  val solver : string Unsynchronized.ref
krauss@29125
    27
end
krauss@29125
    28
krauss@29125
    29
structure ScnpSolve : SCNP_SOLVE =
krauss@29125
    30
struct
krauss@29125
    31
krauss@29125
    32
(** Graph problems **)
krauss@29125
    33
krauss@29125
    34
datatype edge = GTR | GEQ ;
krauss@29125
    35
datatype graph = G of int * int * (int * edge * int) list ;
krauss@29125
    36
datatype graph_problem = GP of int list * graph list ;
krauss@29125
    37
krauss@29125
    38
datatype label = MIN | MAX | MS ;
krauss@29125
    39
type certificate =
krauss@29125
    40
  label
krauss@29125
    41
  * (int * int) list list
krauss@29125
    42
  * int list
krauss@29125
    43
  * (int -> bool -> int -> (int * int) option)
krauss@29125
    44
krauss@29125
    45
fun graph_at (GP (_, gs), i) = nth gs i ;
krauss@29125
    46
fun num_prog_pts (GP (arities, _)) = length arities ;
krauss@29125
    47
fun num_graphs (GP (_, gs)) = length gs ;
krauss@29125
    48
fun arity (GP (arities, gl)) i = nth arities i ;
wenzelm@30190
    49
fun ndigits (GP (arities, _)) = IntInf.log2 (List.foldl (op +) 0 arities) + 1
krauss@29125
    50
krauss@29125
    51
krauss@29125
    52
(** Propositional formulas **)
krauss@29125
    53
krauss@29125
    54
val Not = PropLogic.Not and And = PropLogic.And and Or = PropLogic.Or
krauss@29125
    55
val BoolVar = PropLogic.BoolVar
krauss@29125
    56
fun Implies (p, q) = Or (Not p, q)
krauss@29125
    57
fun Equiv (p, q) = And (Implies (p, q), Implies (q, p))
krauss@29125
    58
val all = PropLogic.all
krauss@29125
    59
krauss@29125
    60
(* finite indexed quantifiers:
krauss@29125
    61
krauss@29125
    62
iforall n f   <==>      /\
krauss@29125
    63
                       /  \  f i
krauss@29125
    64
                      0<=i<n
krauss@29125
    65
 *)
krauss@29125
    66
fun iforall n f = all (map f (0 upto n - 1))
krauss@29125
    67
fun iexists n f = PropLogic.exists (map f (0 upto n - 1))
krauss@29125
    68
fun iforall2 n m f = all (map_product f (0 upto n - 1) (0 upto m - 1))
krauss@29125
    69
krauss@29125
    70
fun the_one var n x = all (var x :: map (Not o var) ((0 upto n - 1) \\ [x]))
krauss@29125
    71
fun exactly_one n f = iexists n (the_one f n)
krauss@29125
    72
krauss@29125
    73
(* SAT solving *)
wenzelm@32740
    74
val solver = Unsynchronized.ref "auto";
krauss@29125
    75
fun sat_solver x =
krauss@29125
    76
  FundefCommon.PROFILE "sat_solving..." (SatSolver.invoke_solver (!solver)) x
krauss@29125
    77
krauss@29125
    78
(* "Virtual constructors" for various propositional variables *)
krauss@29125
    79
fun var_constrs (gp as GP (arities, gl)) =
krauss@29125
    80
  let
krauss@29125
    81
    val n = Int.max (num_graphs gp, num_prog_pts gp)
wenzelm@30190
    82
    val k = List.foldl Int.max 1 arities
krauss@29125
    83
krauss@29125
    84
    (* Injective, provided  a < 8, x < n, and i < k. *)
krauss@29125
    85
    fun prod a x i j = ((j * k + i) * n + x) * 8 + a + 1
krauss@29125
    86
krauss@29125
    87
    fun ES (g, i, j) = BoolVar (prod 0 g i j)
krauss@29125
    88
    fun EW (g, i, j) = BoolVar (prod 1 g i j)
krauss@29125
    89
    fun WEAK g       = BoolVar (prod 2 g 0 0)
krauss@29125
    90
    fun STRICT g     = BoolVar (prod 3 g 0 0)
krauss@29125
    91
    fun P (p, i)     = BoolVar (prod 4 p i 0)
krauss@29125
    92
    fun GAM (g, i, j)= BoolVar (prod 5 g i j)
krauss@29125
    93
    fun EPS (g, i)   = BoolVar (prod 6 g i 0)
krauss@29125
    94
    fun TAG (p, i) b = BoolVar (prod 7 p i b)
krauss@29125
    95
  in
krauss@29125
    96
    (ES,EW,WEAK,STRICT,P,GAM,EPS,TAG)
krauss@29125
    97
  end
krauss@29125
    98
krauss@29125
    99
krauss@29125
   100
fun graph_info gp g =
krauss@29125
   101
  let
krauss@29125
   102
    val G (p, q, edgs) = graph_at (gp, g)
krauss@29125
   103
  in
krauss@29125
   104
    (g, p, q, arity gp p, arity gp q, edgs)
krauss@29125
   105
  end
krauss@29125
   106
krauss@29125
   107
krauss@29125
   108
(* Order-independent part of encoding *)
krauss@29125
   109
krauss@29125
   110
fun encode_graphs bits gp =
krauss@29125
   111
  let
krauss@29125
   112
    val ng = num_graphs gp
krauss@29125
   113
    val (ES,EW,_,_,_,_,_,TAG) = var_constrs gp
krauss@29125
   114
krauss@29125
   115
    fun encode_constraint_strict 0 (x, y) = PropLogic.False
krauss@29125
   116
      | encode_constraint_strict k (x, y) =
krauss@29125
   117
        Or (And (TAG x (k - 1), Not (TAG y (k - 1))),
krauss@29125
   118
            And (Equiv (TAG x (k - 1), TAG y (k - 1)),
krauss@29125
   119
                 encode_constraint_strict (k - 1) (x, y)))
krauss@29125
   120
krauss@29125
   121
    fun encode_constraint_weak k (x, y) =
krauss@29125
   122
        Or (encode_constraint_strict k (x, y),
krauss@29125
   123
            iforall k (fn i => Equiv (TAG x i, TAG y i)))
krauss@29125
   124
krauss@29125
   125
    fun encode_graph (g, p, q, n, m, edges) =
krauss@29125
   126
      let
krauss@29125
   127
        fun encode_edge i j =
krauss@29125
   128
          if exists (fn x => x = (i, GTR, j)) edges then
krauss@29125
   129
            And (ES (g, i, j), EW (g, i, j))
krauss@29125
   130
          else if not (exists (fn x => x = (i, GEQ, j)) edges) then
krauss@29125
   131
            And (Not (ES (g, i, j)), Not (EW (g, i, j)))
krauss@29125
   132
          else
krauss@29125
   133
            And (
krauss@29125
   134
              Equiv (ES (g, i, j),
krauss@29125
   135
                     encode_constraint_strict bits ((p, i), (q, j))),
krauss@29125
   136
              Equiv (EW (g, i, j),
krauss@29125
   137
                     encode_constraint_weak bits ((p, i), (q, j))))
krauss@29125
   138
       in
krauss@29125
   139
        iforall2 n m encode_edge
krauss@29125
   140
      end
krauss@29125
   141
  in
krauss@29125
   142
    iforall ng (encode_graph o graph_info gp)
krauss@29125
   143
  end
krauss@29125
   144
krauss@29125
   145
krauss@29125
   146
(* Order-specific part of encoding *)
krauss@29125
   147
krauss@29125
   148
fun encode bits gp mu =
krauss@29125
   149
  let
krauss@29125
   150
    val ng = num_graphs gp
krauss@29125
   151
    val (ES,EW,WEAK,STRICT,P,GAM,EPS,_) = var_constrs gp
krauss@29125
   152
krauss@29125
   153
    fun encode_graph MAX (g, p, q, n, m, _) =
krauss@29712
   154
        And (
krauss@29125
   155
          Equiv (WEAK g,
krauss@29125
   156
            iforall m (fn j =>
krauss@29125
   157
              Implies (P (q, j),
krauss@29125
   158
                iexists n (fn i =>
krauss@29125
   159
                  And (P (p, i), EW (g, i, j)))))),
krauss@29125
   160
          Equiv (STRICT g,
krauss@29712
   161
            And (
krauss@29712
   162
              iforall m (fn j =>
krauss@29712
   163
                Implies (P (q, j),
krauss@29712
   164
                  iexists n (fn i =>
krauss@29712
   165
                    And (P (p, i), ES (g, i, j))))),
krauss@29712
   166
              iexists n (fn i => P (p, i)))))
krauss@29125
   167
      | encode_graph MIN (g, p, q, n, m, _) =
krauss@29712
   168
        And (
krauss@29125
   169
          Equiv (WEAK g,
krauss@29125
   170
            iforall n (fn i =>
krauss@29125
   171
              Implies (P (p, i),
krauss@29125
   172
                iexists m (fn j =>
krauss@29125
   173
                  And (P (q, j), EW (g, i, j)))))),
krauss@29125
   174
          Equiv (STRICT g,
krauss@29712
   175
            And (
krauss@29712
   176
              iforall n (fn i =>
krauss@29712
   177
                Implies (P (p, i),
krauss@29712
   178
                  iexists m (fn j =>
krauss@29712
   179
                    And (P (q, j), ES (g, i, j))))),
krauss@29712
   180
              iexists m (fn j => P (q, j)))))
krauss@29125
   181
      | encode_graph MS (g, p, q, n, m, _) =
krauss@29125
   182
        all [
krauss@29125
   183
          Equiv (WEAK g,
krauss@29125
   184
            iforall m (fn j =>
krauss@29125
   185
              Implies (P (q, j),
krauss@29125
   186
                iexists n (fn i => GAM (g, i, j))))),
krauss@29125
   187
          Equiv (STRICT g,
krauss@29125
   188
            iexists n (fn i =>
krauss@29125
   189
              And (P (p, i), Not (EPS (g, i))))),
krauss@29125
   190
          iforall2 n m (fn i => fn j =>
krauss@29125
   191
            Implies (GAM (g, i, j),
krauss@29125
   192
              all [
krauss@29125
   193
                P (p, i),
krauss@29125
   194
                P (q, j),
krauss@29125
   195
                EW (g, i, j),
krauss@29125
   196
                Equiv (Not (EPS (g, i)), ES (g, i, j))])),
krauss@29125
   197
          iforall n (fn i =>
krauss@29125
   198
            Implies (And (P (p, i), EPS (g, i)),
krauss@29125
   199
              exactly_one m (fn j => GAM (g, i, j))))
krauss@29125
   200
        ]
krauss@29125
   201
  in
krauss@29125
   202
    all [
krauss@29125
   203
      encode_graphs bits gp,
krauss@29125
   204
      iforall ng (encode_graph mu o graph_info gp),
krauss@29125
   205
      iforall ng (fn x => WEAK x),
krauss@29125
   206
      iexists ng (fn x => STRICT x)
krauss@29125
   207
    ]
krauss@29125
   208
  end
krauss@29125
   209
krauss@29125
   210
krauss@29125
   211
(*Generieren des level-mapping und diverser output*)
krauss@29125
   212
fun mk_certificate bits label gp f =
krauss@29125
   213
  let
krauss@29125
   214
    val (ES,EW,WEAK,STRICT,P,GAM,EPS,TAG) = var_constrs gp
krauss@29125
   215
    fun assign (PropLogic.BoolVar v) = the_default false (f v)
krauss@29125
   216
    fun assignTag i j =
krauss@29125
   217
      (fold (fn x => fn y => 2 * y + (if assign (TAG (i, j) x) then 1 else 0))
krauss@29125
   218
        (bits - 1 downto 0) 0)
krauss@29125
   219
krauss@29125
   220
    val level_mapping =
krauss@29125
   221
      let fun prog_pt_mapping p =
krauss@29125
   222
            map_filter (fn x => if assign (P(p, x)) then SOME (x, assignTag p x) else NONE)
krauss@29125
   223
              (0 upto (arity gp p) - 1)
krauss@29125
   224
      in map prog_pt_mapping (0 upto num_prog_pts gp - 1) end
krauss@29125
   225
krauss@29125
   226
    val strict_list = filter (assign o STRICT) (0 upto num_graphs gp - 1)
krauss@29125
   227
krauss@29125
   228
    fun covering_pair g bStrict j =
krauss@29125
   229
      let
krauss@29125
   230
        val (_, p, q, n, m, _) = graph_info gp g
krauss@29125
   231
krauss@29125
   232
        fun cover        MAX j = find_index (fn i => assign (P (p, i))      andalso      assign (EW  (g, i, j))) (0 upto n - 1)
krauss@29125
   233
          | cover        MS  k = find_index (fn i =>                                     assign (GAM (g, i, k))) (0 upto n - 1)
krauss@29125
   234
          | cover        MIN i = find_index (fn j => assign (P (q, j))      andalso      assign (EW  (g, i, j))) (0 upto m - 1)
krauss@29125
   235
        fun cover_strict MAX j = find_index (fn i => assign (P (p, i))      andalso      assign (ES  (g, i, j))) (0 upto n - 1)
krauss@29125
   236
          | cover_strict MS  k = find_index (fn i => assign (GAM (g, i, k)) andalso not (assign (EPS (g, i)  ))) (0 upto n - 1)
krauss@29125
   237
          | cover_strict MIN i = find_index (fn j => assign (P (q, j))      andalso      assign (ES  (g, i, j))) (0 upto m - 1)
krauss@29125
   238
        val i = if bStrict then cover_strict label j else cover label j
krauss@29125
   239
      in
krauss@29125
   240
        find_first (fn x => fst x = i) (nth level_mapping (if label = MIN then q else p))
krauss@29125
   241
      end
krauss@29125
   242
  in
krauss@29125
   243
    (label, level_mapping, strict_list, covering_pair)
krauss@29125
   244
  end
krauss@29125
   245
krauss@29125
   246
(*interface for the proof reconstruction*)
krauss@29125
   247
fun generate_certificate use_tags labels gp =
krauss@29125
   248
  let
krauss@29125
   249
    val bits = if use_tags then ndigits gp else 0
krauss@29125
   250
  in
krauss@29125
   251
    get_first
krauss@29125
   252
      (fn l => case sat_solver (encode bits gp l) of
krauss@29125
   253
                 SatSolver.SATISFIABLE f => SOME (mk_certificate bits l gp f)
krauss@29125
   254
               | _ => NONE)
krauss@29125
   255
      labels
krauss@29125
   256
  end
krauss@29125
   257
end