QBF/qbf.ml

   1 (* ====================================================== *)
   2 (*               Squolem proof reconstruction             *)
   3 (*          (c) Copyright, Ondřej Kunčar 2010-11          *)
   4 (* ====================================================== *)
   5
   6
   7 set_jrh_lexer;;
   8
   9 let show_progress = ref false;;
  10 let show_timing = ref false;;
  11 let delete_qbf_tempfiles = ref true;;
  12
  13 type quantifier = Existential of term | Universal of term;;
  14
  15 let make_variable index =
  16   if index <= 0 then failwith "Variable of index 0 or lesser is not allowed"
  17   else mk_var ("v_"^(string_of_int index), bool_ty)
  18 ;;
  19
  20 let make_literal index =
  21   if index < 0 then mk_neg (make_variable (-index))
  22   else make_variable index
  23 ;;
  24
  25 let destroy_variable var =
  26   let var_string = string_of_term var in
  27   int_of_string (String.sub var_string 2 (String.length var_string -2))
  28 ;;
  29
  30 let destroy_literal lit =
  31   match is_neg lit with
  32   true -> - destroy_variable (dest_neg lit)
  33   | false -> destroy_variable lit
  34 ;;
  35
  36 let get_quant_var quantifier =
  37   match quantifier with
  38     Existential t -> t
  39     | Universal t -> t
  40 ;;
  41
  42 let has_quant tm =
  43         Pervasives.(||) (is_exists tm) (is_forall tm)
  44 ;;
  45
  46 let dest_quant tm =
  47         if is_exists tm then dest_exists tm
  48         else dest_forall tm
  49 ;;
  50
  51 module type Qbfcontextsig =
  52 sig
  53   type variables = (int,unit) Hashtbl.t;;
  54   type extensions = (int,term) Hashtbl.t;;
  55
  56   type quantifiers = quantifier list;;
  57   type aux_variables = int list;;
  58   type q_levels = int array;;
  59   type context = {
  60     (** all variables, i.e, variables in a formula and auxiliary variables from extensions *)
  61     variables:variables;
  62     extensions:extensions;
  63     mutable aux_variables:aux_variables;
  64     (** quantifiers prefix in bottom-up ordering *)
  65     mutable quantifiers:quantifiers;
  66     mutable q_levels:q_levels;
  67                 mutable q_ordered_levels:q_levels };;
  68
  69   val create_context : int -> context
  70   (** quantifiers must be in bottom-up ordering *)
  71   val set_quantifiers : context -> quantifiers -> unit
  72   val check_variable : context -> int -> unit
  73   val check_fresh_variable : context -> int -> unit
  74   val add_universal_variable : context -> int -> unit
  75   val add_existential_variable : context -> int -> unit
  76   val add_extension : context -> int -> term -> unit
  77   val add_conclusion_eq : context -> int -> term -> unit
  78   val get_extensions : context -> (term * term) list
  79         val get_extension : context -> int -> term
  80   val get_quantifiers : context -> quantifiers
  81   val get_aux_variables : context -> aux_variables
  82   val make_quantifiers_levels : context -> unit
  83         val make_ordered_quantifiers_levels : context -> unit
  84         val lt_levels : context  -> int -> int -> bool
  85         val lt_ordered_levels : context  -> int -> int -> bool
  86 end;;
  87
  88 module Qbfcontext : Qbfcontextsig =
  89 struct
  90   type variables = (int,unit) Hashtbl.t;;
  91   type extensions = (int,term) Hashtbl.t;;
  92
  93   type quantifiers = quantifier list;;
  94   type aux_variables = int list;;
  95   type q_levels = int array;;
  96   type context = {
  97                 variables:variables;
  98                 extensions:extensions;
  99                 mutable aux_variables:aux_variables;
 100                 mutable quantifiers:quantifiers;
 101                 mutable q_levels:q_levels;
 102                 mutable q_ordered_levels:q_levels
 103         };;
 104
 105   let create_context var_count =
 106     { variables = Hashtbl.create (2*var_count);
 107                         extensions = Hashtbl.create var_count;
 108                         aux_variables = [];
 109                         quantifiers = [];
 110                         q_levels = Array.make 0 0;
 111                         q_ordered_levels = Array.make 0 0 }
 112   ;;
 113
 114   let set_quantifiers context quants =
 115     context.quantifiers <- quants
 116   ;;
 117
 118   let check_variable context var_index =
 119     if not (Hashtbl.mem context.variables var_index) then failwith ((string_of_int var_index)^" is undefined variable")
 120   ;;
 121
 122   let check_fresh_variable context var_index =
 123     if Hashtbl.mem context.variables var_index then failwith ((string_of_int var_index)^" is not a fresh variable")
 124   ;;
 125
 126   let add_universal_variable context var_index =
 127     check_fresh_variable context var_index;
 128     Hashtbl.add context.variables var_index ()
 129   ;;
 130
 131   let add_existential_variable context var_index =
 132     check_fresh_variable context var_index;
 133     Hashtbl.add context.variables var_index ();
 134     Hashtbl.add context.extensions var_index `T`
 135   ;;
 136
 137         let add_aux_variable context var_index =
 138     check_fresh_variable context var_index;
 139     Hashtbl.add context.variables var_index ();
 140     context.aux_variables <- var_index::context.aux_variables
 141   ;;
 142
 143   let add_aux_quantifier context var_index free_variables =
 144     let quantifier = Existential (make_variable var_index) in
 145     let rec remove_from_list l ls =
 146       match ls with
 147       [] -> []
 148       | l'::ls' when l'=l -> ls'
 149       | l'::ls'-> l'::remove_from_list l ls'
 150     in
 151     let rec insert_quantifier quantifiers free_variables =
 152       match free_variables with
 153       [] -> quantifier::quantifiers
 154       | _ -> match quantifiers with
 155         q::qs -> q::(insert_quantifier qs (remove_from_list (get_quant_var q) free_variables))
 156         | [] -> failwith "add_aux_quantifier: logic error"
 157     in
 158     context.quantifiers <- List.rev ((insert_quantifier (List.rev context.quantifiers) free_variables))
 159   ;;
 160
 161   let add_extension context var_index formula =
 162     add_aux_variable context var_index;
 163     add_aux_quantifier context var_index (variables formula);
 164     Hashtbl.add context.extensions var_index formula
 165   ;;
 166
 167   let add_conclusion_eq context var_index formula =
 168     Hashtbl.replace context.extensions var_index formula
 169   ;;
 170
 171         let get_extension context var_index =
 172                 Hashtbl.find context.extensions var_index
 173         ;;
 174
 175   let get_extensions context =
 176     Hashtbl.fold (fun f s l -> (make_variable f,s)::l) context.extensions []
 177   ;;
 178
 179   let get_quantifiers context =
 180     context.quantifiers
 181   ;;
 182
 183   let get_aux_variables context =
 184     context.aux_variables
 185   ;;
 186
 187         let make_quantifiers_levels_inter context =
 188     let quantifiers = context.quantifiers in
 189                 let rec loop arr quants level =
 190       match quants with
 191       [] -> arr
 192       | q::qs ->
 193                                 arr.(((destroy_variable o get_quant_var) q) - 1) <- level;
 194                                 loop arr qs (level - 1)
 195     in
 196     let arr = Array.make (List.length quantifiers) 0 in
 197     let arr' = loop arr quantifiers (List.length quantifiers) in
 198     arr'
 199   ;;
 200
 201   let make_quantifiers_levels context =
 202     context.q_levels <- make_quantifiers_levels_inter context
 203   ;;
 204
 205         let make_ordered_quantifiers_levels context =
 206     context.q_ordered_levels <- make_quantifiers_levels_inter context
 207   ;;
 208
 209   let lt_levels context v1 v2 =
 210     context.q_levels.(v1-1) < context.q_levels.(v2-1)
 211   ;;
 212
 213         let lt_ordered_levels context v1 v2 =
 214     context.q_ordered_levels.(v1-1) < context.q_ordered_levels.(v2-1)
 215   ;;
 216
 217 end;;
 218
 219  open Qbfcontext;;
 220
 221 let rec strip_quantifiers tm =
 222   if is_forall tm then
 223     let (var,tm') = dest_forall tm in
 224     let (q',body) = (strip_quantifiers tm') in
 225     ((Universal var)::q',body)
 226   else if is_exists tm then
 227     let (var,tm') = dest_exists tm in
 228     let (q',body) = (strip_quantifiers tm') in
 229     ((Existential var)::q',body)
 230   else ([],tm)
 231 ;;
 232
 233 (** strip quantifiers in bottom-up ordering *)
 234 let strip_quantifiers_r tm =
 235   let rec loop tm acc =
 236     if is_forall tm then
 237       let (var,tm') = dest_forall tm in
 238       loop tm' ((Universal var)::acc)
 239     else if is_exists tm then
 240       let (var,tm') = dest_exists tm in
 241       loop tm' ((Existential var)::acc)
 242     else (acc,tm)
 243   in loop tm []
 244 ;;
 245
 246 (** strip quantifiers in bottom-up ordering *)
 247 let strip_quantifiers_rx tm =
 248   let rec loop tm acc =
 249     if is_forall tm then
 250       let (var,tm') = dest_forall tm in
 251       loop tm' ((true, var)::acc)
 252     else if is_exists tm then
 253       let (var,tm') = dest_exists tm in
 254       loop tm' ((false, var)::acc)
 255     else (acc,tm)
 256   in loop tm []
 257 ;;
 258
 259 let quantifiers_fold_left exist_fn universal_fn thm quantifiers =
 260   let quant_fn thm quantifier =
 261     match quantifier with
 262     Universal var -> universal_fn var thm
 263     | Existential var -> exist_fn var thm
 264   in
 265   List.fold_left quant_fn thm quantifiers
 266 ;;
 267
 268 let is_negated lit_ind = lit_ind < 0;;
 269
 270 let read_index token_stream =
 271   let index_token = Stream.next token_stream in
 272     match index_token with
 273       Genlex.Int index -> index
 274       | _ -> failwith "Bad index of variable"
 275 ;;
 276
 277 let var = abs;;
 278
 279 let read_extension_ite context new_var_index token_stream =
 280   let x_v_i = read_index token_stream in
 281   let y_v_i = read_index token_stream in
 282   let z_v_i = read_index token_stream in
 283   check_variable context (var x_v_i);
 284   check_variable context (var y_v_i);
 285   check_variable context (var z_v_i);
 286   let x_v = make_literal x_v_i in
 287   let y_v = make_literal y_v_i in
 288   let z_v = make_literal z_v_i in
 289   let formula = mk_disj (mk_conj (x_v,y_v),mk_conj(mk_neg x_v,z_v)) in
 290   add_extension context new_var_index formula;
 291 ;;
 292
 293 let read_extension_and context new_var_index token_stream =
 294   let rec read_conjucts context token_stream =
 295     let lit_ind = read_index token_stream in
 296     if lit_ind = 0 then []
 297     else
 298     begin
 299       check_variable context (var lit_ind);
 300       (make_literal lit_ind)::(read_conjucts context token_stream)
 301     end
 302   in
 303   let conjucts = read_conjucts context token_stream in
 304   let conjucts' = match conjucts with
 305     [] -> `T`
 306     | _ -> list_mk_conj conjucts
 307   in
 308   add_extension context new_var_index conjucts';
 309 ;;
 310
 311 let read_extension_line context token_stream =
 312   let new_var_index = read_index token_stream in
 313   let extension_type = Stream.next token_stream in
 314   match extension_type with
 315     Genlex.Kwd "I" -> read_extension_ite context new_var_index token_stream
 316     | Genlex.Kwd "A" -> read_extension_and context new_var_index token_stream
 317     | _ -> failwith "Unknown type of extension line"
 318 ;;
 319
 320 let read_header context token_stream =
 321   match Stream.next token_stream with
 322     Genlex.Kwd "QBCertificate" -> ()
 323     | _ -> failwith "Missing header"
 324 ;;
 325
 326 let read_resolution_line context token_stream =
 327   failwith "Resolution line: not yet implemented!";
 328 ()
 329 ;;
 330
 331 let rec read_equalities context token_stream =
 332   try
 333     let exist_var_i = read_index token_stream in
 334     check_variable context exist_var_i;
 335     let extension_var_i = read_index token_stream in
 336     check_variable context (var extension_var_i);
 337     let extension_var = make_literal extension_var_i in
 338     add_conclusion_eq context exist_var_i extension_var;
 339     read_equalities context token_stream
 340   with Stream.Failure -> ()
 341 ;;
 342
 343 let read_conlude_line context token_stream =
 344   match Stream.next token_stream with
 345   Genlex.Kwd "VALID" -> read_equalities context token_stream
 346   | Genlex.Kwd "INVALID" -> failwith "INVALID formula: not yet implemted!"
 347   | _ -> failwith "Unknown type of conclusion"
 348 ;;
 349
 350 let read_certificate context token_stream =
 351   read_header context token_stream;
 352   let rec read_line context token_stream =
 353     match Stream.next token_stream with
 354     Genlex.Kwd "E" -> read_extension_line context token_stream; read_line context token_stream
 355     | Genlex.Kwd "R" -> read_resolution_line context token_stream; read_line context token_stream
 356     | Genlex.Kwd "CONCLUDE" -> read_conlude_line context token_stream
 357     | _ -> failwith "Unknown type of line"
 358   in
 359   read_line context token_stream
 360 ;;
 361
 362 let PROPAGATE_FORALL =
 363   let MONO_FORALL_B = (UNDISCH o prove)
 364    (`(!x:bool. A x ==> B x) ==> (!) A ==> (!) B`,
 365     STRIP_TAC THEN
 366     GEN_REWRITE_TAC (BINOP_CONV o RAND_CONV) [GSYM ETA_AX] THEN
 367     ASM_MESON_TAC[]) in
 368   let a_tm = rand(lhand(concl MONO_FORALL_B))
 369   and b_tm = rand(rand(concl MONO_FORALL_B))
 370   and h_tm = hd(hyp MONO_FORALL_B) in
 371   fun v1 ->
 372      let ath = GEN_ALPHA_CONV v1 h_tm in
 373      let atm = rand(concl ath) in
 374      let pth = PROVE_HYP (EQ_MP (SYM ath) (ASSUME atm)) MONO_FORALL_B in
 375      fun thm ->
 376        let tm = concl thm in
 377        let ip,q = dest_comb tm in
 378        let i,p = dest_comb ip in
 379        let pabs = mk_abs(v1,p)
 380        and qabs = mk_abs(v1,q) in
 381        let th1 = AP_TERM i (BETA(mk_comb(pabs,v1))) in
 382        let th2 = MK_COMB(th1,BETA(mk_comb(qabs,v1))) in
 383        let th3 = GEN v1 (EQ_MP (SYM th2) thm) in
 384        let th4 = INST [pabs,a_tm; qabs,b_tm] pth in
 385        PROVE_HYP th3 th4;;
 386
 387 let PROPAGATE_RIGHT =
 388   let MONO_EXISTS_RIGHT_B = (UNDISCH o prove)
 389    (`(A ==> B(x:bool)) ==> A ==> (?) B`,
 390     ASM_CASES_TAC `A:bool` THEN ASM_REWRITE_TAC[] THEN
 391     GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [GSYM ETA_AX] THEN
 392     MESON_TAC[]) in
 393   let a_tm = lhand(concl MONO_EXISTS_RIGHT_B)
 394   and b_tm = rand(rand(concl MONO_EXISTS_RIGHT_B))
 395   and h_tm = hd(hyp MONO_EXISTS_RIGHT_B) in
 396   let x_tm = rand(rand h_tm) in
 397   fun v thm ->
 398     let tm = concl thm in
 399     let ip,q = dest_comb tm in
 400     let qabs = mk_abs(v,q) in
 401     let th1 = AP_TERM ip (BETA(mk_comb(qabs,v))) in
 402     let th2 = EQ_MP (SYM th1) thm in
 403     let th3 = INST [rand ip,a_tm; qabs,b_tm; v,x_tm] MONO_EXISTS_RIGHT_B in
 404     PROVE_HYP th2 th3;;
 405
 406 let PROPAGATE_LEFT =
 407   let MONO_EXISTS_LEFT_B = (UNDISCH o prove)
 408    (`(!x:bool. A x ==> B) ==> (?) A ==> B`,
 409     ASM_CASES_TAC `B:bool` THEN ASM_REWRITE_TAC[] THEN
 410     GEN_REWRITE_TAC (funpow 3 RAND_CONV) [GSYM ETA_AX] THEN
 411     MESON_TAC[]) in
 412   let a_tm = rand(lhand(concl MONO_EXISTS_LEFT_B))
 413   and b_tm = rand(concl MONO_EXISTS_LEFT_B)
 414   and h_tm = hd(hyp MONO_EXISTS_LEFT_B) in
 415   fun v ->
 416      let ath = GEN_ALPHA_CONV v h_tm in
 417      let atm = rand(concl ath) in
 418      let pth = PROVE_HYP (EQ_MP (SYM ath) (ASSUME atm)) MONO_EXISTS_LEFT_B in
 419      fun thm ->
 420        let tm = concl thm in
 421        let ip,q = dest_comb tm in
 422        let i,p = dest_comb ip in
 423        let pabs = mk_abs(v,p) in
 424        let th1 = AP_THM (AP_TERM i (BETA(mk_comb(pabs,v)))) q in
 425        let th2 = GEN v (EQ_MP (SYM th1) thm) in
 426        let th3 = INST [pabs,a_tm; q,b_tm] pth in
 427        PROVE_HYP th2 th3;;
 428
 429 let PROPAGATE_QUANTIFIERS_R thm ext_quants quants =
 430         let rec propagate_both thm ext_quants quants =
 431                 match (ext_quants,quants) with
 432                         | ((Universal v1)::ext_quantss,(Universal v2)::quantss) ->
 433                                 propagate_both (PROPAGATE_FORALL v1 thm) ext_quantss quantss
 434                         | (_,_) -> (thm,ext_quants,quants)
 435         in
 436         let rec propagate_right thm quants =
 437                 match quants with
 438                         | (Existential v)::quantss ->
 439                                 propagate_right (PROPAGATE_RIGHT v thm) quantss
 440                         | _ -> (thm,quants)
 441         in
 442         let rec propagate_left thm ext_quants =
 443                 match ext_quants with
 444                         | (Existential v)::ext_quantss ->
 445                                 propagate_left (PROPAGATE_LEFT v thm) ext_quantss
 446                         | _ -> (thm,ext_quants)
 447         in
 448         let rec propagate thm ext_quants quants =
 449                 match (ext_quants,quants) with
 450                         | ([],[]) -> thm
 451                         | (_,((Existential _)::_)) ->
 452                                 let (thm',quants') = propagate_right thm quants in
 453                                 let (thm'',ext_quants') = propagate_left thm' ext_quants in
 454                                 propagate thm'' ext_quants' quants'
 455                         | (((Existential _)::_),_) ->
 456                                 let (thm',ext_quants') = propagate_left thm ext_quants in
 457                                 propagate thm' ext_quants' quants
 458                         | ((Universal _)::_,(Universal _)::_) ->
 459                                 let (thm',ext_quants',quants') = propagate_both thm ext_quants quants in
 460                                 propagate thm' ext_quants' quants'
 461                         | _ -> failwith "PROPAGATE_QUANTIFIERS_R: logic error"
 462         in
 463         propagate thm ext_quants quants
 464 ;;
 465
 466 let order_quantifiers context =
 467         let add_var vertices graph var_index =
 468                 Gr.add_vertex graph (make_vertex var_index);
 469                 let extension_vars = variables (get_extension context var_index) in
 470                 let add_ext_var ext_var =
 471                         let ext_var_index = destroy_variable ext_var in
 472                         if Hashtbl.mem vertices ext_var_index then
 473                                 Gr.add_edge graph (make_vertex ext_var_index) (make_vertex var_index)
 474                 in
 475                 List.iter add_ext_var extension_vars
 476         in
 477         let rec is_sorted var_index_list =
 478                 let is_sorted_var var_index =
 479                         let extension_vars = variables (get_extension context var_index) in
 480                         List.fold_left (fun ret var -> ret && lt_levels context (destroy_variable var) var_index) true extension_vars
 481                 in
 482                 match var_index_list with
 483                 [] -> true
 484                 | var::vars -> if is_sorted_var var then is_sorted vars
 485                                                                          else false
 486         in
 487         (** exists is in up-bottom ordering *)
 488         let rec order_exists quantifiers exists =
 489                 let order_exists' tail =
 490                         if is_sorted exists then
 491                                 List.fold_left (fun tail var_index -> (Existential (make_variable var_index))::tail) tail exists
 492                         else
 493                                 let graph = Gr.create () in
 494                                 let vertices = Hashtbl.create (List.length exists) in
 495                                 List.iter (fun var -> Hashtbl.add vertices var ()) exists;
 496                                 List.iter (fun var -> add_var vertices graph var) exists;
 497                                 Topo.fold (fun vertex tail -> (Existential (make_variable (dest_vertex vertex)))::tail) graph tail
 498                 in
 499                 match quantifiers with
 500                 [] -> order_exists' []
 501                 | (Universal v)::qs -> order_exists' ((Universal v)::order qs)
 502                 | (Existential v)::qs ->
 503                         order_exists qs ((destroy_variable v)::exists)
 504         and
 505         order quantifiers =
 506                 match quantifiers with
 507                 [] -> []
 508                 | (Universal v)::qs -> (Universal v)::order qs
 509                 | (Existential v)::qs ->
 510                         order_exists ((Existential v)::qs) []
 511         in
 512         set_quantifiers context (order (get_quantifiers context));
 513         make_ordered_quantifiers_levels context
 514 ;;
 515
 516 let match_time = ref 0.0;;
 517 let lift_time = ref 0.0;;
 518 let gen_time = ref 0.0;;
 519 let test_time = ref 0.0;;
 520
 521
 522 let timex label f x =
 523   if not (!show_timing) then f x else
 524   let start_time = Sys.time() in
 525   try let result = f x in
 526       let finish_time = Sys.time() in
 527       report("CPU time (user): "^(string_of_float(finish_time -. start_time))^" ("^label^")");
 528       result
 529   with e ->
 530       let finish_time = Sys.time() in
 531       Format.print_string("Failed after (user) CPU time of "^
 532                           (string_of_float(finish_time -. start_time))^" ("^label^")"^": ");
 533       raise e;;
 534
 535 let my_time f x time_var =
 536   if not (!show_timing) then f x else
 537   let start_time = Sys.time() in
 538   try let result = f x in
 539       let finish_time = Sys.time() in
 540       time_var := !time_var +. (finish_time -. start_time);
 541       result
 542   with e ->
 543       let finish_time = Sys.time() in
 544       time_var := !time_var +. (finish_time -. start_time);
 545       raise e;;
 546
 547 let report_time label time_var =
 548         if !show_timing then
 549                 report("CPU time (user): "^(string_of_float(!time_var))^" ("^label^")");
 550 ;;
 551
 552 let FORALL_SIMP2 = prove
 553  (`t = (!x:bool. t)`,
 554   ITAUT_TAC);;
 555
 556 let ADD_MISSING_UNIVERSALS th quants =
 557         let rec add_u quants tm =
 558                 match quants with
 559                         | [] -> REFL tm
 560                         | q::qs ->
 561                                 match q with
 562                                         | Existential _ -> BINDER_CONV (add_u qs) tm
 563                                         | Universal v ->
 564                                                 if Pervasives.(||) (not (has_quant tm)) (Pervasives.compare ((fst o dest_quant) tm) v != 0) then
 565                                                         let renamed_rewr = EQ_MP (ONCE_DEPTH_CONV (ALPHA_CONV v) (concl FORALL_SIMP2)) FORALL_SIMP2 in
 566                                                         (PURE_ONCE_REWRITE_CONV [renamed_rewr] THENC BINDER_CONV (add_u qs)) tm
 567                                                 else
 568                                                         BINDER_CONV (add_u qs) tm
 569         in
 570         EQ_MP (add_u (rev quants) (concl th)) th
 571 ;;
 572
 573 let AX_UXU = (UNDISCH o prove)
 574  (`(!x:bool. p x /\ q ==> r x) ==> (!) p /\ q ==> (!) r`,
 575   let AX_UXU = MESON [] `(!x:bool. ((A x /\ B)==>C x))==>(((!x:bool. A x) /\ B)==> !x:bool. C x)` in
 576   DISCH_THEN(MP_TAC o MATCH_MP AX_UXU) THEN REWRITE_TAC[ETA_AX])
 577 and AX_EXE = (UNDISCH o prove)
 578  (`(!x:bool. p x /\ q ==> r x) ==> (?) p /\ q ==> (?) r`,
 579   let AX_EXE = MESON [] `(!x:bool. ((A x /\ B)==>C x))==>(((?x:bool. A x) /\ B)==> ?x:bool. C x)` in
 580   DISCH_THEN(MP_TAC o MATCH_MP AX_EXE) THEN REWRITE_TAC[ETA_AX]);;
 581
 582 let LIFT_LEFT ax =
 583   let p_tm = rand(lhand(lhand(concl ax)))
 584   and q_tm = rand(lhand(concl ax))
 585   and r_tm = rand(rand(concl ax))
 586   and h_tm = hd(hyp ax) in
 587   fun var ->
 588     let ath = GEN_ALPHA_CONV var h_tm in
 589     let atm = rand(concl ath) in
 590     let ax' = PROVE_HYP (EQ_MP (SYM ath) (ASSUME atm)) ax in
 591     fun th ->
 592       let tm = concl th in
 593       let ipq,r = dest_comb tm in
 594       let i,pq = dest_comb ipq in
 595       let ap,q = dest_comb pq in
 596       let a,p = dest_comb ap in
 597       let pabs = mk_abs(var,p)
 598       and rabs = mk_abs(var,r) in
 599       let th1 = AP_THM (AP_TERM a (BETA(mk_comb(pabs,var)))) q in
 600       let th2 = MK_COMB(AP_TERM i th1,BETA(mk_comb(rabs,var))) in
 601       let th3 = GEN var (EQ_MP (SYM th2) th) in
 602       let th4 = INST [pabs,p_tm; q,q_tm; rabs,r_tm] ax' in
 603       PROVE_HYP th3 th4;;
 604
 605 let AX_XUU = (UNDISCH o prove)
 606  (`(!x:bool. p /\ q x ==> r x) ==> p /\ (!) q ==> (!) r`,
 607   let AX_XUU = MESON [] `(!x:bool. ((A /\ B x)==>C x))==>((A /\ !x:bool. B x)==> !x:bool. C x)` in
 608   DISCH_THEN(MP_TAC o MATCH_MP AX_XUU) THEN REWRITE_TAC[ETA_AX])
 609 and AX_XEE = (UNDISCH o prove)
 610  (`(!x:bool. p /\ q x ==> r x) ==> p /\ (?) q ==> (?) r`,
 611   let AX_XEE = MESON [] `(!x:bool. ((A /\ B x)==>C x))==>((A /\ ?x:bool. B x)==> ?x:bool. C x)` in
 612   DISCH_THEN(MP_TAC o MATCH_MP AX_XEE) THEN REWRITE_TAC[ETA_AX]);;
 613
 614 let LIFT_RIGHT ax =
 615   let p_tm = lhand(lhand(concl ax))
 616   and q_tm = rand(rand(lhand(concl ax)))
 617   and r_tm = rand(rand(concl ax))
 618   and h_tm = hd(hyp ax) in
 619   fun var ->
 620     let ath = GEN_ALPHA_CONV var h_tm in
 621     let atm = rand(concl ath) in
 622     let ax' = PROVE_HYP (EQ_MP (SYM ath) (ASSUME atm)) ax in
 623     fun th ->
 624       let tm = concl th in
 625       let ipq,r = dest_comb tm in
 626       let i,pq = dest_comb ipq in
 627       let ap,q = dest_comb pq in
 628       let a,p = dest_comb ap in
 629       let qabs = mk_abs(var,q)
 630       and rabs = mk_abs(var,r) in
 631       let th1 = AP_TERM ap (BETA(mk_comb(qabs,var))) in
 632       let th2 = MK_COMB(AP_TERM i th1,BETA(mk_comb(rabs,var))) in
 633       let th3 = GEN var (EQ_MP (SYM th2) th) in
 634       let th4 = INST [p,p_tm; qabs,q_tm; rabs,r_tm] ax' in
 635       PROVE_HYP th3 th4;;
 636
 637 let AX_UUU = (UNDISCH o prove)
 638  (`(!x:bool. p x /\ q x ==> r x) ==> (!) p /\ (!) q ==> (!) r`,
 639   let AX_UUU = MESON [] `(!x:bool. ((A x /\ B x)==>C x))==>(((!x:bool. A x) /\ !x:bool. B x)==> !x:bool. C x)` in
 640   DISCH_THEN(MP_TAC o MATCH_MP AX_UUU) THEN REWRITE_TAC[ETA_AX])
 641 and AX_EUE = (UNDISCH o prove)
 642  (`(!x:bool. p x /\ q x ==> r x) ==> (?) p /\ (!) q ==> (?) r`,
 643   let AX_EUE = MESON [] `(!x:bool. ((A x /\ B x)==>C x))==>(((?x:bool. A x) /\ !x:bool. B x)==> ?x:bool. C x)` in
 644   DISCH_THEN(MP_TAC o MATCH_MP AX_EUE) THEN REWRITE_TAC[ETA_AX])
 645 and AX_UEE = (UNDISCH o prove)
 646  (`(!x:bool. p x /\ q x ==> r x) ==> (!) p /\ (?) q ==> (?) r`,
 647   let AX_UEE = MESON [] `(!x:bool. ((A x /\ B x)==>C x))==>(((!x:bool. A x) /\ ?x:bool. B x)==> ?x:bool. C x)` in
 648   DISCH_THEN(MP_TAC o MATCH_MP AX_UEE) THEN REWRITE_TAC[ETA_AX]);;
 649
 650 let LIFT_BOTH ax =
 651   let p_tm = rand(lhand(lhand(concl ax)))
 652   and q_tm = rand(rand(lhand(concl ax)))
 653   and r_tm = rand(rand(concl ax))
 654   and h_tm = hd(hyp ax) in
 655   fun var ->
 656     let ath = GEN_ALPHA_CONV var h_tm in
 657     let atm = rand(concl ath) in
 658     let ax' = PROVE_HYP (EQ_MP (SYM ath) (ASSUME atm)) ax in
 659     fun th ->
 660       let tm = concl th in
 661       let ipq,r = dest_comb tm in
 662       let i,pq = dest_comb ipq in
 663       let ap,q = dest_comb pq in
 664       let a,p = dest_comb ap in
 665       let pabs = mk_abs(var,p)
 666       and qabs = mk_abs(var,q)
 667       and rabs = mk_abs(var,r) in
 668       let th0 = AP_TERM a (BETA(mk_comb(pabs,var))) in
 669       let th1 = MK_COMB(th0,BETA(mk_comb(qabs,var))) in
 670       let th2 = MK_COMB(AP_TERM i th1,BETA(mk_comb(rabs,var))) in
 671       let th3 = GEN var (EQ_MP (SYM th2) th) in
 672       let th4 = INST [pabs,p_tm; qabs,q_tm; rabs,r_tm] ax' in
 673       PROVE_HYP th3 th4;;
 674
 675 let solve_quantifiers context conjuction =
 676         let solve_right_quantifier thm quant2 =
 677                 match quant2 with
 678                         | Universal v2 -> LIFT_RIGHT AX_XUU v2 thm
 679                         | Existential v2 -> LIFT_RIGHT AX_XEE v2 thm
 680         in
 681         let solve_left_quantifier thm quant1 =
 682                 match quant1 with
 683                         | Universal v1 -> LIFT_LEFT AX_UXU v1 thm
 684                         | Existential v1 -> LIFT_LEFT AX_EXE v1 thm
 685         in
 686         let solve_both_quantifiers thm quant1 quant2 =
 687     match (quant1,quant2) with
 688             (Universal v1, Universal v2) -> LIFT_BOTH AX_UUU v1 thm
 689             | (Existential v1, Universal v2) -> LIFT_BOTH AX_EUE v1 thm
 690             | (Universal v1, Existential v2) -> LIFT_BOTH AX_UEE v1 thm
 691             | _ -> failwith "Logic error in solve_quantifier"
 692   in
 693         let rec loop thm quants1 quants2 =
 694                 match (quants1,quants2) with
 695                         | ([],[]) -> thm
 696                         | (qs1,[]) -> List.fold_left solve_left_quantifier thm qs1
 697                         | ([],qs2) -> List.fold_left solve_right_quantifier thm qs2
 698                         | (quant1::qs1,quant2::qs2) ->
 699                                 let quant_var1 = get_quant_var quant1 in
 700                                 let quant_var2 = get_quant_var quant2 in
 701                                 if quant_var1 = quant_var2 then
 702                                         let thm' = solve_both_quantifiers thm quant1 quant2 in
 703                                         loop thm' qs1 qs2
 704                                 else
 705                                         if lt_ordered_levels context (destroy_variable quant_var1) (destroy_variable quant_var2) then
 706                                                 let thm' = solve_right_quantifier thm quant2 in
 707                                                 loop thm' (quant1::qs1) qs2
 708                                         else
 709                                                 let thm' = solve_left_quantifier thm quant1 in
 710                                                 loop thm' qs1 (quant2::qs2)
 711         in
 712         let conclusion = concl conjuction in
 713   let (conj1,conj2) = dest_conj conclusion in
 714   let (quants1,body1) = strip_quantifiers_r conj1 in
 715   let (quants2,body2) = strip_quantifiers_r conj2 in
 716
 717   let rew_thm = loop (DISCH_ALL (ASSUME (mk_conj (body1,body2)))) quants1 quants2 in
 718         (*print_thm rew_thm;
 719         print_newline ();
 720         print_thm conjuction;
 721         print_newline ();*)
 722   my_time (MP rew_thm) conjuction match_time
 723 ;;
 724
 725 let make_quantified_model_equality =
 726   let pth = MESON[] `?x:bool. x = t` in
 727   let t_tm = rand(body(rand(concl pth))) in
 728   fun quantifier_data (exist_var,right_side) ->
 729     let free_vars = frees right_side in
 730     let n = quantifier_data exist_var in
 731     let quants =  sort (decreasing quantifier_data)
 732                        (filter (fun v -> quantifier_data v > n) free_vars) in
 733     let exist_eq_thm = INST[right_side,t_tm] (CONV_RULE(GEN_ALPHA_CONV exist_var) pth) in
 734     let ret = GENL quants exist_eq_thm in
 735           (* print_thm ret;
 736           print_endline ""; *)
 737           ret
 738 ;;
 739
 740 let construct_model context equalities =
 741   match equalities with
 742   [] -> `T`
 743   | (eq::eqs) -> List.fold_left (C (curry mk_conj)) eq eqs
 744 ;;
 745
 746 let construct_model_thm context equalities =
 747   let eq_length = List.length equalities in
 748   let progress = ref 1 in
 749   let print_progress () =
 750           print_endline ((string_of_int o int_of_float) (((float_of_int !progress)/.(float_of_int eq_length))*.100.0))
 751   in
 752   let construct model eq =
 753
 754           let ret = solve_quantifiers context (CONJ eq model) in
 755
 756           if !show_progress then
 757           begin
 758                   progress := !progress + 1;
 759                   print_progress ();
 760           end;
 761           ret
 762   in
 763   let rec construct_recursively eqs =
 764     match eqs with
 765       [] -> failwith "Sanity check failure"
 766     | [e] -> e
 767     | [e1;e2] -> construct e1 e2
 768     | _ -> let n = length eqs in
 769            let eqs1,eqs2 = chop_list (length eqs / 2) eqs in
 770            construct (construct_recursively eqs1) (construct_recursively eqs2)
 771   in
 772   if equalities = [] then quantifiers_fold_left SIMPLE_EXISTS GEN TRUTH (get_quantifiers context)
 773   else PURE_REWRITE_RULE[GSYM CONJ_ASSOC] (construct_recursively equalities);;
 774
 775 let make_model context =
 776   let model_equalities = get_extensions context in
 777         let model = construct_model context (List.map mk_eq model_equalities) in
 778         let quantifier_list = map (function Universal v -> v | Existential v -> v)
 779                                   (get_quantifiers context) in
 780         let quantifier_table = itlist2 (|->) quantifier_list (1--length quantifier_list) undefined in
 781         let quantifier_data = apply quantifier_table in
 782         let quantified_equalities = timex "make_quantified_equalities" (List.map (make_quantified_model_equality quantifier_data)) model_equalities in
 783   let model_thm =
 784                 match_time := 0.0;
 785                 lift_time := 0.0;
 786                 gen_time := 0.0;
 787                 test_time := 0.0;
 788                 print_endline ("Number of extensions: "^ (string_of_int (List.length model_equalities)));
 789                 let ret = timex "construct_model_thm" (construct_model_thm context) quantified_equalities in
 790                 report_time "lift" lift_time;
 791                 report_time "match" match_time;
 792                 report_time "gen" gen_time;
 793                 report_time "test" test_time;
 794                 ret
 795         in
 796   (*let model_thm = construct_model_thm context (List.map (make_quantified_model_equality context) model_equalities) in*)
 797         (model, model_thm)
 798 ;;
 799
 800 let check_and_preprocess context formula =
 801   match frees formula with
 802   [ _ ] -> failwith "Formula has free variables"
 803   | _ ->
 804     let nnf_thm = NNF_CONV formula in
 805     let prenex_thm = TRANS nnf_thm (PRENEX_CONV (rhs (concl nnf_thm))) in
 806     let cnf_thm = TRANS prenex_thm (CNF_CONV (rhs (concl prenex_thm))) in
 807
 808     let rec check_and_made_rename formula index rename =
 809       let rename_quantifier constr destr add_fresh_variable =
 810         let (var,destr_formula) = destr formula in
 811         if type_of var <> bool_ty then failwith ((string_of_term var)^" is not of bool type");
 812         add_fresh_variable context index;
 813         let formula2 = check_and_made_rename destr_formula (index+1) ((make_variable index,var)::rename) in
 814         constr (make_variable index,formula2)
 815       in
 816       if is_forall formula then rename_quantifier mk_forall dest_forall add_universal_variable
 817       else if is_exists formula then rename_quantifier mk_exists dest_exists add_existential_variable
 818       else
 819         vsubst rename formula
 820     in
 821     let prenex_formula = rhs (concl cnf_thm) in
 822     let ret = TRANS cnf_thm (ALPHA prenex_formula (check_and_made_rename prenex_formula 1 [])) in
 823     let (quantifiers',_) = strip_quantifiers_r (rhs (concl ret)) in
 824     set_quantifiers context quantifiers';
 825     ret
 826 ;;
 827
 828 let get_temp_file () =
 829   Filename.open_temp_file "qbf" ""
 830 ;;
 831
 832 let split_disjuncts body =
 833  List.fold_right
 834   (fun c d ->  (disjuncts c) :: d)
 835   (conjuncts body) []
 836 ;;
 837
 838 let string_of_literal lit =
 839   string_of_int (destroy_literal lit);
 840 ;;
 841
 842 type prefix = Exists of term list | Forall of term list;;
 843
 844 let rec strip_quantifiers_as_prefix formula =
 845   if is_forall formula then
 846     let (quants,formula') = strip_forall formula in
 847     let (quants',body) = strip_quantifiers_as_prefix formula' in
 848     ((Forall quants)::quants',body)
 849   else if is_exists formula then
 850     let (quants,formula') = strip_exists formula in
 851     let (quants',body) = strip_quantifiers_as_prefix formula' in
 852     ((Exists quants)::quants',body)
 853   else
 854     ([],formula)
 855 ;;
 856
 857 let make_input context formula var_count =
 858   let (file_name,file_stream) = get_temp_file () in
 859   try
 860     let (quantifiers_list, body) = strip_quantifiers_as_prefix formula in
 861     let clause_count = length(conjuncts body) in
 862
 863
 864     let disjuncts_list = split_disjuncts body in
 865
 866     let out s = output_string file_stream s in
 867     let formula_string = Str.global_replace (Str.regexp_string "\n") "\nc " (string_of_term formula) in
 868     out "c "; out formula_string;out "\n";
 869     out "c\n";
 870     out "p cnf ";
 871     out (string_of_int var_count); out " ";
 872     out (string_of_int clause_count); out "\n";
 873
 874     let print_quantifiers q =
 875       let print_vars q =
 876         List.iter (fun var -> (out(string_of_literal var); out " ")) q;
 877         out "0\n"
 878       in
 879       match q with
 880       Exists vars -> out "e "; print_vars vars
 881       | Forall vars -> out "a "; print_vars vars
 882     in
 883
 884     List.iter
 885       (fun q ->  print_quantifiers q)
 886       quantifiers_list;
 887
 888     List.iter
 889       (fun l -> (List.iter (fun lit ->
 890         (out(string_of_literal lit); out " ")) l;
 891                   out "0\n"))
 892       disjuncts_list;
 893     close_out file_stream;
 894     file_name
 895   with x ->
 896     close_out file_stream;
 897     raise x
 898 ;;
 899
 900 let execute_squolem input_file_name =
 901   let exec_name = "squolem2 -c " ^ input_file_name in
 902   let _ = Sys.command exec_name in
 903   input_file_name ^ ".qbc"
 904 ;;
 905
 906 let parse_certificate context certificate_file_name =
 907   let file_channel = Pervasives.open_in certificate_file_name in
 908   let token_stream = (Genlex.make_lexer ["I";"A";"QBCertificate";"VALID";"INVALID";"E";"R";"CONCLUDE"] (Stream.of_channel file_channel)) in
 909   read_certificate context token_stream
 910
 911 let print_model context =
 912   let (model, model_thm) = make_model context in
 913   print_endline (string_of_term model);
 914   print_endline (string_of_thm model_thm)
 915 ;;
 916
 917 let print_quantifiers context =
 918         let print_quantifier quant =
 919                 match quant with
 920                         Existential v -> print_string "E "; print_term v; print_string " "
 921                         | Universal v -> print_string "F "; print_term v; print_string " "
 922         in
 923         List.iter print_quantifier (get_quantifiers context);
 924         print_newline ()
 925 ;;
 926
 927 let ZSAT_PROVE' =
 928   let ASSOC_EQ_CONV th =
 929     let assoc_canon = ASSOC_CONV th in
 930     fun tm -> let l,r = dest_eq tm in
 931               TRANS (assoc_canon l) (SYM(assoc_canon r)) in
 932   let opacs = [`\/`,ASSOC_EQ_CONV DISJ_ASSOC;
 933                `/\`,ASSOC_EQ_CONV CONJ_ASSOC;
 934                `<=>`,ASSOC_EQ_CONV(TAUT `(t1 <=> t2 <=> t3) <=> ((t1 <=> t2) <=> t3)`)] in
 935   let rec ASSOC_BALANCE_CONV tm =
 936     match tm with
 937       Comb(Comb(op,l),r) when can (assoc op) opacs ->
 938         let tms = striplist (dest_binop op) tm in
 939         let n = length tms in
 940         if n <= 1 then failwith "sanity check failure" else
 941         if n = 2 then BINOP_CONV ASSOC_BALANCE_CONV tm else
 942         let tms1,tms2 = chop_list (n / 2) tms in
 943         let tm1 = list_mk_binop op tms1
 944         and tm2 = list_mk_binop op tms2 in
 945         let th = assoc op opacs (mk_eq(tm,mk_binop op tm1 tm2)) in
 946         CONV_RULE (RAND_CONV (BINOP_CONV ASSOC_BALANCE_CONV)) th
 947     | _ -> REFL tm in
 948   let conv = DEPTH_BINOP_CONV `(/\)` (NNFC_CONV THENC CNF_CONV) in
 949   fun tm -> let th = COMB2_CONV (RAND_CONV conv) ASSOC_BALANCE_CONV tm in
 950             let tm' = rand(concl th) in
 951             EQ_MP (SYM th) (ZSAT_PROVE tm');;
 952
 953 let build_proof context prenex_thm =
 954   let formula = rhs (concl prenex_thm) in
 955   let (quants,formula_body) = strip_quantifiers_r formula in
 956   timex "make_q_levels" make_quantifiers_levels context;
 957         (*print_quantifiers context;*)
 958         timex "order_qs" order_quantifiers context;
 959         (*print_quantifiers context;*)
 960   let (model, model_thm) = timex "make_model" make_model context in
 961   let sat_formula = mk_imp (model,formula_body) in
 962   let proved_sat_formula = timex "sat" ZSAT_PROVE' sat_formula in
 963   let q_propagated_formula = timex "propagate" (PROPAGATE_QUANTIFIERS_R proved_sat_formula (get_quantifiers context)) quants in
 964   let (model_quantifiers,_) = strip_quantifiers_r (concl model_thm) in
 965         let proved_formula =
 966                 if List.length model_quantifiers != List.length (get_quantifiers context) then
 967                         MP q_propagated_formula (timex "add_missing" (ADD_MISSING_UNIVERSALS model_thm) (get_quantifiers context))
 968                 else
 969                         (*MP q_propagated_formula model_thm*)
 970                         MP q_propagated_formula (timex "add_missing" (ADD_MISSING_UNIVERSALS model_thm) (get_quantifiers context))
 971         in
 972   EQ_MP (GSYM prenex_thm) proved_formula
 973 ;;
 974
 975 let prove_qbf formula =
 976   let var_count = length (variables formula) in
 977   let context = create_context var_count in
 978   let prenex_thm = timex "prep" (check_and_preprocess context) formula in
 979   let input_file_name = timex "make_input" (make_input context (rand (concl prenex_thm))) var_count in
 980   let output_file_name = timex "ex_squolem" execute_squolem input_file_name in
 981   let _ = timex "parse_cert" (parse_certificate context) output_file_name in
 982   let thm = timex "build_proof" (build_proof context) prenex_thm in
 983   (if !delete_qbf_tempfiles
 984    then (Sys.remove input_file_name; Sys.remove output_file_name)
 985    else ());
 986  thm
 987 ;;
 988
 989 let prove_all_qbf dir =
 990         let filter_array f a =
 991                 let l = Array.to_list a in
 992                 let ll = List.filter f l in
 993                 Array.of_list ll
 994         in
 995   let raw_files = Sys.readdir dir in
 996         let files = filter_array (fun name -> Filename.check_suffix name ".qdimacs") raw_files in
 997   let run_prover file_name =
 998     let name = Filename.chop_suffix file_name ".qdimacs" in
 999     print_endline name;
1000     let formula = readQDimacs (dir^"/"^file_name) in
1001     let formula_thm = prove_qbf formula in
1002     (name,formula_thm)
1003   in
1004   Array.map run_prover files
1005 ;;