hypothesis_selection in progress

src/transform/hypothesis_selection.ml

@@ -38,18 +38,35 @@ end
 
 module GP = Digraph.AbstractLabeled(struct type t = Term.lsymbol end)(Int_Dft)
 module GC = Graph.AbstractLabeled(struct type t = int end)(Int_Dft)			    
-module FmlaHashtbl = Hashtbl.Make(struct type t = Term.fmla
-					 let equal x y = x.f_tag = y.f_tag
-					 let hash x = x.f_tag
-				  end)
+module FmlaHashtbl =
+  Hashtbl.Make(struct type t = Term.fmla
+		      let equal x y = x.f_tag = y.f_tag
+		      let hash x = x.f_tag
+	       end)
+module SymbHashtbl = 
+  Hashtbl.Make(struct type t = Term.lsymbol
+		      let equal x y = x.ls_name.id_tag = y.ls_name.id_tag
+		      let hash x = x.ls_name.id_tag
+	       end)
+
+let err = Format.err_formatter
 
 module Util = struct
+  let print_clauses fmt = Format.fprintf fmt "[%a]@."
+    (Pp.print_list Pp.comma (Pp.print_list Pp.comma Pretty.print_fmla))
+  let print_clause fmt = Format.fprintf fmt "[%a]@."
+    (Pp.print_list Pp.comma Pretty.print_fmla)
 end
 
 
 (** module used to reduce formulae to Normal Form *)
 module NF = struct (* add memoization, one day ? *)
 
+  (** all quantifiers in prenex form *)
+  let prenex_fmla fmla =
+    Format.fprintf err "prenex_fmla :@ @[%a@]@." Pretty.print_fmla fmla;
+    fmla
+
   (** creates a fresh formula representing a quantified formula *)
   let create_fmla (vars:Term.vsymbol list) : Term.fmla =
     let pred = create_psymbol (id_fresh "temoin")
@@ -58,37 +75,52 @@ module NF = struct (* add memoization, one day ? *)
 
 
   (** transforms a formulae into its Normal Form as a list of clauses.
-  The first argument is a hastable from formulae to formulae *)
-  let rec transform fmlaTable fmla = match fmla.f_node with
+  The first argument is a hastable from formulae to formulae.
+  A clause is a list of formulae *)
+  let rec transform fmlaTable fmla =
+    Format.fprintf err "transform : @[%a@]@." Pretty.print_fmla fmla;
+    match fmla.f_node with
     | Fquant (_,f_bound) ->
 	let var,_,f =  f_open_quant f_bound in
 	traverse fmlaTable fmla var f
-    | Fbinop (op,f1,f2) -> split_binop fmlaTable op f1 f2
+    | Fbinop (_,_,_) ->
+	let clauses = split fmla in
+	Format.fprintf err "split : %a@." Util.print_clause clauses;
+	if clauses = [fmla] then [[fmla]] else
+	  List.concat (List.map (transform fmlaTable) clauses)
     | Fnot f -> handle_not fmlaTable f
-    | Fapp (_,_) -> [fmla]
-    | Ftrue | Ffalse -> [fmla]
+    | Fapp (_,_) -> [[fmla]]
+    | Ftrue | Ffalse -> [[fmla]]
     | Fif (_,_,_) -> failwith "if formulae not handled"
     | Flet (_,_) -> failwith "let formulae not handled"
     | Fcase (_,_) -> failwith "case formulae not handled"
   and traverse fmlaTable old_fmla vars fmla = match fmla.f_node with
     | Fquant (_,f_bound) ->
-	let var,_,f =  f_open_quant f_bound in
+	let var,_,f = f_open_quant f_bound in
 	traverse fmlaTable old_fmla (var@vars) f
-    | _ ->
-	let new_f = transform fmlaTable fmla in
-	FmlaHashtbl.add fmlaTable old_fmla (create_fmla vars);
-	assert false
-  and split_binop fmlaTable op f1 f2 = match (op,f1,f2) with
-    | Fimplies,{f_node = Fbinop (For, h1, h2)},f2 ->
-	split_binop fmlaTable op h1 f2 @ split_binop fmlaTable op h2 f2
-    | Fimplies,f1,f2 ->
-	List.concat
-	  (List.map (fun f -> split_binop fmlaTable op f1 f)
-	     (transform fmlaTable f2))
-    | Fand,f1,f2 ->
-	transform fmlaTable f1 @ transform fmlaTable f2
-    | _,_,_ ->
-	[f_binary op f1 f2]
+    | _ -> (* TODO !! *)
+	if FmlaHashtbl.mem fmlaTable fmla then
+	  [[FmlaHashtbl.find fmlaTable fmla]]
+	else
+	  let new_fmla = (create_fmla vars) in
+	  FmlaHashtbl.add fmlaTable old_fmla new_fmla;
+	  [[new_fmla]]
+  and skipPrenex fmlaTable fmla = match fmla.f_node with
+    | Fquant (_,f_bound) ->
+	let var,_,f = f_open_quant f_bound in
+	skipPrenex fmlaTable f
+    | _ -> transform fmlaTable fmla
+  and split f = match f.f_node with
+    | Fbinop(Fimplies,{f_node = Fbinop (For, h1, h2)},f2) ->
+	split (f_binary Fimplies h1 f2) @ split (f_binary Fimplies h2 f2)
+    | Fbinop(Fimplies,f1,f2) ->
+	let clauses = split f2 in
+	if List.length clauses >= 2 then
+	  List.concat
+	    (List.map (fun f -> split (f_binary Fimplies f1 f)) clauses)
+	else [f]
+    | Fbinop(Fand,f1,f2) -> [f1; f2]
+    | _ -> [f]
   and handle_not fmlaTable f = match f.f_node with
     | Fnot f1 -> transform fmlaTable f1
     | Fbinop (Fand,f1,f2) ->
@@ -99,7 +131,7 @@ module NF = struct (* add memoization, one day ? *)
 	transform fmlaTable (f_and f1 (f_not f2))
     | Fbinop (Fiff,f1,f2) ->
 	transform fmlaTable (f_or (f_and f1 (f_not f2)) (f_and (f_not f1) f2))
-    | _ -> [f_not f] (* default case *)
+    | _ -> [[f_not f]] (* default case *)
 
 end
 
@@ -114,26 +146,64 @@ end
 (** module used to compute the directed graph of predicates *)
 module GraphPredicate = struct
 
-  (** analyse a single clause *)
-  let analyse_clause gp clause = assert false
-
-  let analyse_prop fmlaTable gp prop =
-    let clauses = NF.transform fmlaTable prop in
-    List.fold_left analyse_clause gp clauses
+  exception Exit of lsymbol
+
+  let is_negative = function
+    | { f_node = Fnot _ } -> true
+    | _ -> false
+
+  let extract_symbol fmla = 
+    let rec search = function
+      | { f_node = Fapp(p,_) } -> raise (Exit p)
+      | f -> f_map (fun t->t) search f in
+    try search fmla;
+      Format.eprintf "invalid formula : ";
+      Pretty.print_fmla Format.err_formatter fmla; assert false
+    with Exit p -> p
+ 
+  let find symbTbl x = try
+    SymbHashtbl.find symbTbl x
+  with Not_found ->
+    let new_v = GP.V.create x in
+    SymbHashtbl.add symbTbl x new_v;
+    new_v
 
-  let add_symbol gp lsymbol =
-    GP.add_vertex gp (GP.V.create lsymbol)
+  (** analyse a single clause *)
+  let analyse_clause symbTbl gp clause =
+    let negative,positive = List.partition is_negative clause in
+    let get_symbol x = find symbTbl (extract_symbol x) in
+    let negative = List.map get_symbol negative in
+    let positive = List.map get_symbol positive in
+    let n = List.length clause in
+    let add left gp right =
+      let e = GP.E.create left n right in
+      GP.add_edge_e gp e in 
+    List.fold_left (* add an edge from every negative to any positive *)
+      (fun gp left ->
+	 List.fold_left (add left) gp positive) gp negative
+
+  (** takes a prop, puts it in Normal Form and then builds a clause
+      from it *)
+  let analyse_prop fmlaTable symbTbl gp prop =
+    let prenex_fmla = NF.prenex_fmla prop in
+    let clauses = NF.skipPrenex fmlaTable prenex_fmla in
+    Format.eprintf "==>@ @[%a@]@.@." Util.print_clauses clauses;
+    List.fold_left (analyse_clause symbTbl) gp clauses
+
+  let add_symbol symbTbl gp lsymbol =
+    GP.add_vertex gp (find symbTbl lsymbol)
 
   (** takes a constant graph and a task_head, and add any interesting
-  element to the graph it returns. *)
-  let update fmlaTable gp task_head =
+      element to the graph it returns. *)
+  let update fmlaTable symbTbl gp task_head =
     match task_head.task_decl with
       | Decl {d_node = Dprop (_,_,prop_decl) } ->
 	  (* a proposition to analyse *)
-	  analyse_prop fmlaTable gp prop_decl
+	  analyse_prop fmlaTable symbTbl gp prop_decl
       | Decl {d_node = Dlogic logic_decls } ->
 	  (* a symbol to add *)
-	  List.fold_left (fun gp logic_decl -> add_symbol gp (fst logic_decl))
+	  List.fold_left
+	    (fun gp logic_decl -> add_symbol symbTbl gp (fst logic_decl))
 	    gp logic_decls
       | _ -> gp
 end
@@ -146,28 +216,30 @@ module Select = struct
 end
 
 (** collects data on predicates and constants in task *)
-let collect_info fmlaTable =
+let collect_info fmlaTable symbTbl =
   Trans.fold (fun t (gc, gp) ->
-    GraphConstant.update gc t, GraphPredicate.update fmlaTable gp t)
+		GraphConstant.update gc t,
+		GraphPredicate.update fmlaTable symbTbl gp t)
     (GC.empty, GP.empty)
 
 (** the transformation, made from applying collect_info and
 then mapping Select.filter *)
-let transformation fmlaTable task =
-  let (gc,gp) = Trans.apply (collect_info fmlaTable) task in
+let transformation fmlaTable symbTbl task =
+  let (gc,gp) = Trans.apply (collect_info fmlaTable symbTbl) task in
   Trans.apply (Trans.decl (Select.filter (gc,gp)) None) task
 
 (** the transformation to be registered *)
 let hypothesis_selection =
   Register.store
-    (fun () -> Trans.store (transformation (FmlaHashtbl.create 17)))
+    (fun () -> Trans.store
+       (transformation (FmlaHashtbl.create 17) (SymbHashtbl.create 17)))
 
 let _ = Register.register_transform
   "hypothesis_selection" hypothesis_selection
 
 (*
 Local Variables: 
-compile-command: "unset LANG; make -k -C ../.."
+compile-command: "unset LANG; cd ../..; make"
 End: 
 *)