--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Function/scnp_solve.ML Tue Jun 23 12:09:30 2009 +0200
@@ -0,0 +1,257 @@
+(* Title: HOL/Tools/Function/scnp_solve.ML
+ Author: Armin Heller, TU Muenchen
+ Author: Alexander Krauss, TU Muenchen
+
+Generate certificates for SCNP using a SAT solver
+*)
+
+
+signature SCNP_SOLVE =
+sig
+
+ datatype edge = GTR | GEQ
+ datatype graph = G of int * int * (int * edge * int) list
+ datatype graph_problem = GP of int list * graph list
+
+ datatype label = MIN | MAX | MS
+
+ type certificate =
+ label (* which order *)
+ * (int * int) list list (* (multi)sets *)
+ * int list (* strictly ordered calls *)
+ * (int -> bool -> int -> (int * int) option) (* covering function *)
+
+ val generate_certificate : bool -> label list -> graph_problem -> certificate option
+
+ val solver : string ref
+end
+
+structure ScnpSolve : SCNP_SOLVE =
+struct
+
+(** Graph problems **)
+
+datatype edge = GTR | GEQ ;
+datatype graph = G of int * int * (int * edge * int) list ;
+datatype graph_problem = GP of int list * graph list ;
+
+datatype label = MIN | MAX | MS ;
+type certificate =
+ label
+ * (int * int) list list
+ * int list
+ * (int -> bool -> int -> (int * int) option)
+
+fun graph_at (GP (_, gs), i) = nth gs i ;
+fun num_prog_pts (GP (arities, _)) = length arities ;
+fun num_graphs (GP (_, gs)) = length gs ;
+fun arity (GP (arities, gl)) i = nth arities i ;
+fun ndigits (GP (arities, _)) = IntInf.log2 (List.foldl (op +) 0 arities) + 1
+
+
+(** Propositional formulas **)
+
+val Not = PropLogic.Not and And = PropLogic.And and Or = PropLogic.Or
+val BoolVar = PropLogic.BoolVar
+fun Implies (p, q) = Or (Not p, q)
+fun Equiv (p, q) = And (Implies (p, q), Implies (q, p))
+val all = PropLogic.all
+
+(* finite indexed quantifiers:
+
+iforall n f <==> /\
+ / \ f i
+ 0<=i<n
+ *)
+fun iforall n f = all (map f (0 upto n - 1))
+fun iexists n f = PropLogic.exists (map f (0 upto n - 1))
+fun iforall2 n m f = all (map_product f (0 upto n - 1) (0 upto m - 1))
+
+fun the_one var n x = all (var x :: map (Not o var) ((0 upto n - 1) \\ [x]))
+fun exactly_one n f = iexists n (the_one f n)
+
+(* SAT solving *)
+val solver = ref "auto";
+fun sat_solver x =
+ FundefCommon.PROFILE "sat_solving..." (SatSolver.invoke_solver (!solver)) x
+
+(* "Virtual constructors" for various propositional variables *)
+fun var_constrs (gp as GP (arities, gl)) =
+ let
+ val n = Int.max (num_graphs gp, num_prog_pts gp)
+ val k = List.foldl Int.max 1 arities
+
+ (* Injective, provided a < 8, x < n, and i < k. *)
+ fun prod a x i j = ((j * k + i) * n + x) * 8 + a + 1
+
+ fun ES (g, i, j) = BoolVar (prod 0 g i j)
+ fun EW (g, i, j) = BoolVar (prod 1 g i j)
+ fun WEAK g = BoolVar (prod 2 g 0 0)
+ fun STRICT g = BoolVar (prod 3 g 0 0)
+ fun P (p, i) = BoolVar (prod 4 p i 0)
+ fun GAM (g, i, j)= BoolVar (prod 5 g i j)
+ fun EPS (g, i) = BoolVar (prod 6 g i 0)
+ fun TAG (p, i) b = BoolVar (prod 7 p i b)
+ in
+ (ES,EW,WEAK,STRICT,P,GAM,EPS,TAG)
+ end
+
+
+fun graph_info gp g =
+ let
+ val G (p, q, edgs) = graph_at (gp, g)
+ in
+ (g, p, q, arity gp p, arity gp q, edgs)
+ end
+
+
+(* Order-independent part of encoding *)
+
+fun encode_graphs bits gp =
+ let
+ val ng = num_graphs gp
+ val (ES,EW,_,_,_,_,_,TAG) = var_constrs gp
+
+ fun encode_constraint_strict 0 (x, y) = PropLogic.False
+ | encode_constraint_strict k (x, y) =
+ Or (And (TAG x (k - 1), Not (TAG y (k - 1))),
+ And (Equiv (TAG x (k - 1), TAG y (k - 1)),
+ encode_constraint_strict (k - 1) (x, y)))
+
+ fun encode_constraint_weak k (x, y) =
+ Or (encode_constraint_strict k (x, y),
+ iforall k (fn i => Equiv (TAG x i, TAG y i)))
+
+ fun encode_graph (g, p, q, n, m, edges) =
+ let
+ fun encode_edge i j =
+ if exists (fn x => x = (i, GTR, j)) edges then
+ And (ES (g, i, j), EW (g, i, j))
+ else if not (exists (fn x => x = (i, GEQ, j)) edges) then
+ And (Not (ES (g, i, j)), Not (EW (g, i, j)))
+ else
+ And (
+ Equiv (ES (g, i, j),
+ encode_constraint_strict bits ((p, i), (q, j))),
+ Equiv (EW (g, i, j),
+ encode_constraint_weak bits ((p, i), (q, j))))
+ in
+ iforall2 n m encode_edge
+ end
+ in
+ iforall ng (encode_graph o graph_info gp)
+ end
+
+
+(* Order-specific part of encoding *)
+
+fun encode bits gp mu =
+ let
+ val ng = num_graphs gp
+ val (ES,EW,WEAK,STRICT,P,GAM,EPS,_) = var_constrs gp
+
+ fun encode_graph MAX (g, p, q, n, m, _) =
+ And (
+ Equiv (WEAK g,
+ iforall m (fn j =>
+ Implies (P (q, j),
+ iexists n (fn i =>
+ And (P (p, i), EW (g, i, j)))))),
+ Equiv (STRICT g,
+ And (
+ iforall m (fn j =>
+ Implies (P (q, j),
+ iexists n (fn i =>
+ And (P (p, i), ES (g, i, j))))),
+ iexists n (fn i => P (p, i)))))
+ | encode_graph MIN (g, p, q, n, m, _) =
+ And (
+ Equiv (WEAK g,
+ iforall n (fn i =>
+ Implies (P (p, i),
+ iexists m (fn j =>
+ And (P (q, j), EW (g, i, j)))))),
+ Equiv (STRICT g,
+ And (
+ iforall n (fn i =>
+ Implies (P (p, i),
+ iexists m (fn j =>
+ And (P (q, j), ES (g, i, j))))),
+ iexists m (fn j => P (q, j)))))
+ | encode_graph MS (g, p, q, n, m, _) =
+ all [
+ Equiv (WEAK g,
+ iforall m (fn j =>
+ Implies (P (q, j),
+ iexists n (fn i => GAM (g, i, j))))),
+ Equiv (STRICT g,
+ iexists n (fn i =>
+ And (P (p, i), Not (EPS (g, i))))),
+ iforall2 n m (fn i => fn j =>
+ Implies (GAM (g, i, j),
+ all [
+ P (p, i),
+ P (q, j),
+ EW (g, i, j),
+ Equiv (Not (EPS (g, i)), ES (g, i, j))])),
+ iforall n (fn i =>
+ Implies (And (P (p, i), EPS (g, i)),
+ exactly_one m (fn j => GAM (g, i, j))))
+ ]
+ in
+ all [
+ encode_graphs bits gp,
+ iforall ng (encode_graph mu o graph_info gp),
+ iforall ng (fn x => WEAK x),
+ iexists ng (fn x => STRICT x)
+ ]
+ end
+
+
+(*Generieren des level-mapping und diverser output*)
+fun mk_certificate bits label gp f =
+ let
+ val (ES,EW,WEAK,STRICT,P,GAM,EPS,TAG) = var_constrs gp
+ fun assign (PropLogic.BoolVar v) = the_default false (f v)
+ fun assignTag i j =
+ (fold (fn x => fn y => 2 * y + (if assign (TAG (i, j) x) then 1 else 0))
+ (bits - 1 downto 0) 0)
+
+ val level_mapping =
+ let fun prog_pt_mapping p =
+ map_filter (fn x => if assign (P(p, x)) then SOME (x, assignTag p x) else NONE)
+ (0 upto (arity gp p) - 1)
+ in map prog_pt_mapping (0 upto num_prog_pts gp - 1) end
+
+ val strict_list = filter (assign o STRICT) (0 upto num_graphs gp - 1)
+
+ fun covering_pair g bStrict j =
+ let
+ val (_, p, q, n, m, _) = graph_info gp g
+
+ fun cover MAX j = find_index (fn i => assign (P (p, i)) andalso assign (EW (g, i, j))) (0 upto n - 1)
+ | cover MS k = find_index (fn i => assign (GAM (g, i, k))) (0 upto n - 1)
+ | cover MIN i = find_index (fn j => assign (P (q, j)) andalso assign (EW (g, i, j))) (0 upto m - 1)
+ fun cover_strict MAX j = find_index (fn i => assign (P (p, i)) andalso assign (ES (g, i, j))) (0 upto n - 1)
+ | cover_strict MS k = find_index (fn i => assign (GAM (g, i, k)) andalso not (assign (EPS (g, i) ))) (0 upto n - 1)
+ | cover_strict MIN i = find_index (fn j => assign (P (q, j)) andalso assign (ES (g, i, j))) (0 upto m - 1)
+ val i = if bStrict then cover_strict label j else cover label j
+ in
+ find_first (fn x => fst x = i) (nth level_mapping (if label = MIN then q else p))
+ end
+ in
+ (label, level_mapping, strict_list, covering_pair)
+ end
+
+(*interface for the proof reconstruction*)
+fun generate_certificate use_tags labels gp =
+ let
+ val bits = if use_tags then ndigits gp else 0
+ in
+ get_first
+ (fn l => case sat_solver (encode bits gp l) of
+ SatSolver.SATISFIABLE f => SOME (mk_certificate bits l gp f)
+ | _ => NONE)
+ labels
+ end
+end