1 files changed, 431 insertions, 0 deletions
diff --git a/src/extraction/sat_checker.ml b/src/extraction/sat_checker.ml
new file mode 100644
index 0000000..59635e0
--- /dev/null
+++ b/src/extraction/sat_checker.ml
@@ -0,0 +1,431 @@
+(** val negb : bool -> bool **)
+
+let negb = function
+| true -> false
+| false -> true
+
+type 'a list =
+| Nil
+| Cons of 'a * 'a list
+
+(** val existsb : ('a1 -> bool) -> 'a1 list -> bool **)
+
+let rec existsb f = function
+| Nil -> false
+| Cons (a, l0) -> if f a then true else existsb f l0
+
+type int = ExtrNative.uint
+
+(** val lsl0 : int -> int -> int **)
+
+let lsl0 = ExtrNative.l_sl
+
+(** val lsr0 : int -> int -> int **)
+
+let lsr0 = ExtrNative.l_sr
+
+(** val land0 : int -> int -> int **)
+
+let land0 = ExtrNative.l_and
+
+(** val lxor0 : int -> int -> int **)
+
+let lxor0 = ExtrNative.l_xor
+
+(** val sub : int -> int -> int **)
+
+let sub = ExtrNative.sub
+
+(** val eqb : int -> int -> bool **)
+
+let eqb = fun i j -> ExtrNative.compare i j = ExtrNative.Eq
+
+(** val foldi_cont :
+    (int -> ('a1 -> 'a2) -> 'a1 -> 'a2) -> int -> int -> ('a1 -> 'a2) -> 'a1
+    -> 'a2 **)
+
+let foldi_cont = ExtrNative.foldi_cont
+
+(** val foldi_down_cont :
+    (int -> ('a1 -> 'a2) -> 'a1 -> 'a2) -> int -> int -> ('a1 -> 'a2) -> 'a1
+    -> 'a2 **)
+
+let foldi_down_cont = ExtrNative.foldi_down_cont
+
+(** val is_zero : int -> bool **)
+
+let is_zero i =
+  eqb i (ExtrNative.of_uint(0))
+
+(** val is_even : int -> bool **)
+
+let is_even i =
+  is_zero (land0 i (ExtrNative.of_uint(1)))
+
+(** val compare : int -> int -> ExtrNative.comparison **)
+
+let compare = ExtrNative.compare
+
+(** val foldi : (int -> 'a1 -> 'a1) -> int -> int -> 'a1 -> 'a1 **)
+
+let foldi f from to0 =
+  foldi_cont (fun i cont a -> cont (f i a)) from to0 (fun a -> a)
+
+(** val foldi_down : (int -> 'a1 -> 'a1) -> int -> int -> 'a1 -> 'a1 **)
+
+let foldi_down f from downto0 =
+  foldi_down_cont (fun i cont a -> cont (f i a)) from downto0 (fun a -> a)
+
+type 'a array = 'a ExtrNative.parray
+
+(** val make : int -> 'a1 -> 'a1 array **)
+
+let make = ExtrNative.parray_make
+
+module Coq__1 = struct 
+ (** val get : 'a1 array -> int -> 'a1 **)
+ 
+ let get = ExtrNative.parray_get
+end
+let get = Coq__1.get
+
+(** val set : 'a1 array -> int -> 'a1 -> 'a1 array **)
+
+let set = ExtrNative.parray_set
+
+(** val length : 'a1 array -> int **)
+
+let length = ExtrNative.parray_length
+
+(** val to_list : 'a1 array -> 'a1 list **)
+
+let to_list t0 =
+  let len = length t0 in
+  if eqb (ExtrNative.of_uint(0)) len
+  then Nil
+  else foldi_down (fun i l -> Cons ((get t0 i), l))
+         (sub len (ExtrNative.of_uint(1))) (ExtrNative.of_uint(0)) Nil
+
+(** val fold_left : ('a1 -> 'a2 -> 'a1) -> 'a1 -> 'a2 array -> 'a1 **)
+
+let fold_left f a t0 =
+  let len = length t0 in
+  if eqb (ExtrNative.of_uint(0)) len
+  then a
+  else foldi (fun i a0 -> f a0 (get t0 i)) (ExtrNative.of_uint(0))
+         (sub (length t0) (ExtrNative.of_uint(1))) a
+
+(** val foldi_right :
+    (int -> 'a1 -> 'a2 -> 'a2) -> 'a1 array -> 'a2 -> 'a2 **)
+
+let foldi_right f t0 b =
+  let len = length t0 in
+  if eqb (ExtrNative.of_uint(0)) len
+  then b
+  else foldi_down (fun i b0 -> f i (get t0 i) b0)
+         (sub len (ExtrNative.of_uint(1))) (ExtrNative.of_uint(0)) b
+
+module Valuation = 
+ struct 
+  type t = int -> bool
+ end
+
+module Var = 
+ struct 
+  (** val _true : int **)
+  
+  let _true =
+    (ExtrNative.of_uint(0))
+  
+  (** val _false : int **)
+  
+  let _false =
+    (ExtrNative.of_uint(1))
+  
+  (** val interp : Valuation.t -> int -> bool **)
+  
+  let interp rho x =
+    rho x
+ end
+
+module Lit = 
+ struct 
+  (** val is_pos : int -> bool **)
+  
+  let is_pos l =
+    is_even l
+  
+  (** val blit : int -> int **)
+  
+  let blit l =
+    lsr0 l (ExtrNative.of_uint(1))
+  
+  (** val lit : int -> int **)
+  
+  let lit x =
+    lsl0 x (ExtrNative.of_uint(1))
+  
+  (** val neg : int -> int **)
+  
+  let neg l =
+    lxor0 l (ExtrNative.of_uint(1))
+  
+  (** val nlit : int -> int **)
+  
+  let nlit x =
+    neg (lit x)
+  
+  (** val _true : int **)
+  
+  let _true =
+    (ExtrNative.of_uint(0))
+  
+  (** val _false : int **)
+  
+  let _false =
+    (ExtrNative.of_uint(2))
+  
+  (** val eqb : int -> int -> bool **)
+  
+  let eqb l l' =
+    eqb l l'
+  
+  (** val interp : Valuation.t -> int -> bool **)
+  
+  let interp rho l =
+    if is_pos l
+    then Var.interp rho (blit l)
+    else negb (Var.interp rho (blit l))
+ end
+
+module C = 
+ struct 
+  type t = int list
+  
+  (** val interp : Valuation.t -> t -> bool **)
+  
+  let interp rho l =
+    existsb (Lit.interp rho) l
+  
+  (** val _true : t **)
+  
+  let _true =
+    Cons (Lit._true, Nil)
+  
+  (** val is_false : t -> bool **)
+  
+  let is_false = function
+  | Nil -> true
+  | Cons (i, l) -> false
+  
+  (** val or_aux : (t -> t -> t) -> int -> t -> t -> int list **)
+  
+  let rec or_aux or0 l1 c1 c2 = match c2 with
+  | Nil -> Cons (l1, c1)
+  | Cons (l2, c2') ->
+    (match compare l1 l2 with
+     | ExtrNative.Eq -> Cons (l1, (or0 c1 c2'))
+     | ExtrNative.Lt -> Cons (l1, (or0 c1 c2))
+     | ExtrNative.Gt -> Cons (l2, (or_aux or0 l1 c1 c2')))
+  
+  (** val coq_or : t -> t -> t **)
+  
+  let rec coq_or c1 c2 =
+    match c1 with
+    | Nil -> c2
+    | Cons (l1, c3) ->
+      (match c2 with
+       | Nil -> c1
+       | Cons (l2, c2') ->
+         (match compare l1 l2 with
+          | ExtrNative.Eq -> Cons (l1, (coq_or c3 c2'))
+          | ExtrNative.Lt -> Cons (l1, (coq_or c3 c2))
+          | ExtrNative.Gt -> Cons (l2, (or_aux coq_or l1 c3 c2'))))
+  
+  (** val resolve_aux : (t -> t -> t) -> int -> t -> t -> t **)
+  
+  let rec resolve_aux resolve0 l1 c1 c2 = match c2 with
+  | Nil -> _true
+  | Cons (l2, c2') ->
+    (match compare l1 l2 with
+     | ExtrNative.Eq -> Cons (l1, (resolve0 c1 c2'))
+     | ExtrNative.Lt ->
+       if eqb (lxor0 l1 l2) (ExtrNative.of_uint(1))
+       then coq_or c1 c2'
+       else Cons (l1, (resolve0 c1 c2))
+     | ExtrNative.Gt ->
+       if eqb (lxor0 l1 l2) (ExtrNative.of_uint(1))
+       then coq_or c1 c2'
+       else Cons (l2, (resolve_aux resolve0 l1 c1 c2')))
+  
+  (** val resolve : t -> t -> t **)
+  
+  let rec resolve c1 c2 =
+    match c1 with
+    | Nil -> _true
+    | Cons (l1, c3) ->
+      (match c2 with
+       | Nil -> _true
+       | Cons (l2, c2') ->
+         (match compare l1 l2 with
+          | ExtrNative.Eq -> Cons (l1, (resolve c3 c2'))
+          | ExtrNative.Lt ->
+            if eqb (lxor0 l1 l2) (ExtrNative.of_uint(1))
+            then coq_or c3 c2'
+            else Cons (l1, (resolve c3 c2))
+          | ExtrNative.Gt ->
+            if eqb (lxor0 l1 l2) (ExtrNative.of_uint(1))
+            then coq_or c3 c2'
+            else Cons (l2, (resolve_aux resolve l1 c3 c2'))))
+ end
+
+module S = 
+ struct 
+  type t = C.t array
+  
+  (** val get : t -> int -> C.t **)
+  
+  let get s cid =
+    get s cid
+  
+  (** val internal_set : t -> int -> C.t -> t **)
+  
+  let internal_set s cid c =
+    set s cid c
+  
+  (** val make : int -> t **)
+  
+  let make nclauses =
+    make nclauses C._true
+  
+  (** val insert : int -> int list -> int list **)
+  
+  let rec insert l1 c = match c with
+  | Nil -> Cons (l1, Nil)
+  | Cons (l2, c') ->
+    (match compare l1 l2 with
+     | ExtrNative.Eq -> c
+     | ExtrNative.Lt ->
+       if eqb (lxor0 l1 l2) (ExtrNative.of_uint(1))
+       then C._true
+       else Cons (l1, c)
+     | ExtrNative.Gt ->
+       if eqb (lxor0 l1 l2) (ExtrNative.of_uint(1))
+       then C._true
+       else Cons (l2, (insert l1 c')))
+  
+  (** val sort_uniq : int list -> int list **)
+  
+  let rec sort_uniq = function
+  | Nil -> Nil
+  | Cons (l1, c0) -> insert l1 (sort_uniq c0)
+  
+  (** val set_clause : t -> int -> C.t -> t **)
+  
+  let set_clause s pos c =
+    set s pos (sort_uniq c)
+  
+  (** val set_resolve : t -> int -> int array -> t **)
+  
+  let set_resolve s pos r =
+    let len = length r in
+    if eqb len (ExtrNative.of_uint(0))
+    then s
+    else let c =
+           foldi (fun i c -> C.resolve (get s (Coq__1.get r i)) c)
+             (ExtrNative.of_uint(1)) (sub len (ExtrNative.of_uint(1)))
+             (get s (Coq__1.get r (ExtrNative.of_uint(0))))
+         in
+         internal_set s pos c
+ end
+
+(** val afold_left :
+    'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a2 -> 'a1) -> 'a2 array -> 'a1 **)
+
+let afold_left default oP f v =
+  let n = length v in
+  if eqb n (ExtrNative.of_uint(0))
+  then default
+  else foldi (fun i a -> oP a (f (get v i))) (ExtrNative.of_uint(1))
+         (sub n (ExtrNative.of_uint(1))) (f (get v (ExtrNative.of_uint(0))))
+
+type 'step _trace_ = 'step array array
+
+(** val _checker_ :
+    (S.t -> 'a1 -> S.t) -> (C.t -> bool) -> S.t -> 'a1 _trace_ -> int -> bool **)
+
+let _checker_ check_step is_false0 s t0 confl =
+  let s' = fold_left (fun s0 a -> fold_left check_step s0 a) s t0 in
+  is_false0 (S.get s' confl)
+
+module Sat_Checker = 
+ struct 
+  type step =
+  | Res of int * int array
+  
+  (** val step_rect : (int -> int array -> 'a1) -> step -> 'a1 **)
+  
+  let step_rect f = function
+  | Res (x, x0) -> f x x0
+  
+  (** val step_rec : (int -> int array -> 'a1) -> step -> 'a1 **)
+  
+  let step_rec f = function
+  | Res (x, x0) -> f x x0
+  
+  (** val resolution_checker :
+      (C.t -> bool) -> S.t -> step _trace_ -> int -> bool **)
+  
+  let resolution_checker s t0 =
+    _checker_ (fun s0 st -> let Res (pos, r) = st in S.set_resolve s0 pos r)
+      s t0
+  
+  type dimacs = int array array
+  
+  (** val coq_C_interp_or : Valuation.t -> int array -> bool **)
+  
+  let coq_C_interp_or rho c =
+    afold_left false (fun b1 b2 -> if b1 then true else b2) (Lit.interp rho)
+      c
+  
+  (** val valid : Valuation.t -> dimacs -> bool **)
+  
+  let valid rho d =
+    afold_left true (fun b1 b2 -> if b1 then b2 else false)
+      (coq_C_interp_or rho) d
+  
+  type certif =
+  | Certif of int * step _trace_ * int
+  
+  (** val certif_rect :
+      (int -> step _trace_ -> int -> 'a1) -> certif -> 'a1 **)
+  
+  let certif_rect f = function
+  | Certif (x, x0, x1) -> f x x0 x1
+  
+  (** val certif_rec :
+      (int -> step _trace_ -> int -> 'a1) -> certif -> 'a1 **)
+  
+  let certif_rec f = function
+  | Certif (x, x0, x1) -> f x x0 x1
+  
+  (** val add_roots : S.t -> dimacs -> S.t **)
+  
+  let add_roots s d =
+    foldi_right (fun i c s0 -> S.set_clause s0 i (to_list c)) d s
+  
+  (** val checker : dimacs -> certif -> bool **)
+  
+  let checker d = function
+  | Certif (nclauses, t0, confl_id) ->
+    resolution_checker C.is_false (add_roots (S.make nclauses) d) t0 confl_id
+  
+  (** val interp_var : (int -> bool) -> int -> bool **)
+  
+  let interp_var rho x =
+    match compare x (ExtrNative.of_uint(1)) with
+    | ExtrNative.Eq -> false
+    | ExtrNative.Lt -> true
+    | ExtrNative.Gt -> rho (sub x (ExtrNative.of_uint(1)))
+ end
+