made "query" type systes a bit more sound -- local facts, e.g. the negated conjecture, may make invalid the infinity check, e.g. if we are proving that there exists two values of an infinite type, we can use the negated conjecture that there is only one value to derive unsound proofs unless the type is properly encoded
(* Title: HOL/Tools/Function/scnp_solve.ML
Author: Armin Heller, TU Muenchen
Author: Alexander Krauss, TU Muenchen
Certificate generation 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 Unsynchronized.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 (Integer.sum arities) + 1
(** Propositional formulas **)
val Not = Prop_Logic.Not and And = Prop_Logic.And and Or = Prop_Logic.Or
val BoolVar = Prop_Logic.BoolVar
fun Implies (p, q) = Or (Not p, q)
fun Equiv (p, q) = And (Implies (p, q), Implies (q, p))
val all = Prop_Logic.all
(* finite indexed quantifiers:
iforall n f <==> /\
/ \ f i
0<=i<n
*)
fun iforall n f = all (map_range f n)
fun iexists n f = Prop_Logic.exists (map_range f n)
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) (remove (op =) x (0 upto n - 1)))
fun exactly_one n f = iexists n (the_one f n)
(* SAT solving *)
val solver = Unsynchronized.ref "auto";
fun sat_solver x =
Function_Common.PROFILE "sat_solving..." (SatSolver.invoke_solver (!solver)) x
(* "Virtual constructors" for various propositional variables *)
fun var_constrs (gp as GP (arities, _)) =
let
val n = Int.max (num_graphs gp, num_prog_pts gp)
val k = fold Integer.max arities 1
(* 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) = Prop_Logic.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 (Prop_Logic.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_range prog_pt_mapping (num_prog_pts gp) 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