Minisat/sat_common_tools.ml

   1
   2 (* miscellaneous useful stuff that doesn't fit in anywhere else *)
   3
   4 let pair_map f (x,y) = (f x,f y)
   5
   6 (* module for maps keyed on terms *)
   7 module Termmap = Map.Make (struct type t = term let compare = Pervasives.compare end)
   8
   9 module Litset = Set.Make (struct type t = bool * int let compare = Pervasives.compare end)
  10
  11 let tm_listItems m = List.rev (Termmap.fold (fun k v l -> (k,v)::l) m [])
  12
  13 let print_term t = print_string (string_of_term t)
  14
  15 let print_type ty = print_string (string_of_type ty)
  16
  17 (*FIXME: inefficient to read chars one by one; 1024 can be improved upon*)
  18 let input_all in_ch =
  19   let rec loop b =
  20     match
  21       (try Some (input_char in_ch)
  22       with End_of_file -> None)
  23     with
  24       Some c -> (Buffer.add_char b c; loop b)
  25     | None -> () in
  26   let b = Buffer.create 1024 in
  27   let _ = loop b in
  28   Buffer.contents b
  29
  30 let QUANT_CONV conv  = RAND_CONV(ABS_CONV conv)
  31
  32 let BINDER_CONV conv = ABS_CONV conv ORELSEC QUANT_CONV conv
  33
  34 let rec LAST_FORALL_CONV c tm =
  35   if is_forall (snd (dest_forall tm))
  36   then
  37     BINDER_CONV (LAST_FORALL_CONV c) tm
  38   else c tm
  39
  40 let FORALL_IMP_CONV tm =
  41   let (bvar,bbody) = dest_forall tm in
  42   let (ant,conseq) = dest_imp bbody in
  43   let fant = free_in bvar ant in
  44   let fconseq =  free_in bvar conseq in
  45   let ant_thm = ASSUME ant in
  46   let tm_thm = ASSUME tm in
  47   if (fant && fconseq)
  48   then failwith("FORALL_IMP_CONV"^
  49                 ("`"^(fst(dest_var bvar))^"` free on both sides of `==>`"))
  50   else
  51     if fant
  52     then
  53       let asm = mk_exists(bvar,ant) in
  54       let th1 = CHOOSE(bvar,ASSUME asm) (UNDISCH(SPEC bvar tm_thm)) in
  55       let imp1 = DISCH tm (DISCH asm th1) in
  56       let cncl = rand(concl imp1) in
  57       let th2 = MP (ASSUME cncl) (EXISTS (asm,bvar) ant_thm) in
  58       let imp2 = DISCH cncl (GEN bvar (DISCH ant th2)) in
  59       IMP_ANTISYM_RULE imp1 imp2
  60     else
  61       if fconseq
  62       then
  63         let imp1 = DISCH ant(GEN bvar(UNDISCH(SPEC bvar tm_thm))) in
  64         let cncl = concl imp1 in
  65         let imp2 = GEN bvar(DISCH ant(SPEC bvar(UNDISCH(ASSUME cncl)))) in
  66         IMP_ANTISYM_RULE (DISCH tm imp1) (DISCH cncl imp2)
  67       else
  68         let asm = mk_exists(bvar,ant) in
  69         let tmp = UNDISCH (SPEC bvar tm_thm) in
  70         let th1 = GEN bvar (CHOOSE(bvar,ASSUME asm) tmp) in
  71         let imp1 = DISCH tm (DISCH asm th1) in
  72         let cncl = rand(concl imp1) in
  73         let th2 = SPEC bvar (MP(ASSUME cncl) (EXISTS (asm,bvar) ant_thm)) in
  74         let imp2 = DISCH cncl (GEN bvar (DISCH ant th2)) in
  75         IMP_ANTISYM_RULE imp1 imp2
  76
  77 let LEFT_IMP_EXISTS_CONV tm =
  78    let ant, _ = dest_imp tm in
  79    let bvar,bdy = dest_exists ant in
  80    let x' = variant (frees tm) bvar in
  81    let t' = subst [x',bvar] bdy in
  82    let th1 = GEN x' (DISCH t'(MP(ASSUME tm)(EXISTS(ant,x')(ASSUME t')))) in
  83    let rtm = concl th1 in
  84    let th2 = CHOOSE (x',ASSUME ant) (UNDISCH(SPEC x'(ASSUME rtm))) in
  85      IMP_ANTISYM_RULE (DISCH tm th1) (DISCH rtm (DISCH ant th2))
  86
  87
  88
  89 (*********** terms **************)
  90
  91 let lrand x = rand (rator x)
  92
  93 let t_tm = `T`;;
  94 let f_tm = `F`;;
  95
  96 let is_T tm = (tm = t_tm)
  97
  98 let is_F tm = (tm = f_tm)
  99
 100 (************ HOL **************)
 101
 102 let rec ERC lt tm =
 103   if is_comb lt
 104   then
 105     let ((ltl,ltr),(tml,tmr)) =
 106       pair_map dest_comb (lt,tm) in
 107     (ERC ltl tml)@(ERC ltr tmr)
 108   else
 109     if is_var lt
 110     then [(tm,lt)]
 111     else []
 112
 113 (* easier REWR_CONV which assumes that the supplied theorem is ground and quantifier free,
 114    so type instantiation and var capture checks are not needed *)
 115 (* no restrictions on the term argument *)
 116 let EREWR_CONV th tm =
 117   let lt = lhs(concl th) in
 118   let il = ERC lt tm in
 119   INST il th