[r2005-05-07 21:46:36 by afrisch] Empty log message

Original author: afrisch
Date: 2005-05-07 21:46:36+00:00

misc/bool.ml

@@ -599,7 +599,7 @@ module Simplify(M : MAKE)(X : Custom.T) = struct
 
   type f = { vars: (X.t * bool) list; (* toplevel vars and their polarity *)
 	     subs: f list; (* subformulas *)
-	     allvars: (X.t * int * int) list; (* # of pos,neg occurences *)
+	     mutable allvars: (X.t * int * int) list; (* # of pos,neg occurences *)
 	     mutable form: B.t option;
 	     mutable id: int  (* unique id for hash consing *)
 	   }
@@ -716,28 +716,26 @@ module Simplify(M : MAKE)(X : Custom.T) = struct
   let mk =
     let tbl = W.create 16387 in
     let id = ref 0 in
-    fun f ->
-      if (f.id != 0) then f 
-      else
-	let f = W.merge tbl f in
-	if (f.id = 0) then f.id <- (incr id; !id);
-	f
+    fun vars subs ->
+      let f = W.merge tbl { tmpl with vars = vars; subs = subs } in
+      if (f.id = 0) then (
+	f.id <- (incr id; !id);
+	f.allvars <- compute_allvars subs vars;
+      );
+      f
       
-  let empty = mk { tmpl with subs = [] }
-  let full = mk { tmpl with subs = [ empty ] }
+  let empty = mk [] []
+  let full = mk [] [empty]
 
   let check f = ()
 
-  let posvar x = mk { tmpl with vars = [x,true]; allvars = [x,1,0] }
-  let negvar x = mk { tmpl with vars = [x,false]; allvars = [x,0,1] }
+  let posvar x = mk [x,true] []
+  let negvar x = mk [x,false] []
 
   let neg = function
-    | { vars = [x,true]; subs = [] } -> negvar x
-    | { vars = [x,false]; subs = [] } -> posvar x
-    | { vars = []; subs = [ f ] } -> f
-    | f -> mk { tmpl with
-		allvars = List.map (fun (x,p,n) -> (x,n,p)) f.allvars; 
-		subs = [ f ] }
+    | { vars = [x,v]; subs = [] } -> mk [x, not v] []
+    | { vars = []; subs = [f] } -> f
+    | f -> mk [] [f]
 
   let has_complement f1 f2 = List.memq f2 f1.subs
 
@@ -787,11 +785,6 @@ module Simplify(M : MAKE)(X : Custom.T) = struct
 	else z2::(cvars vars1 vars2')
     | vars,[] | [],vars -> vars
 
-  let mk_vs vars subs =
-    mk { tmpl with 
-	   vars = vars; allvars = compute_allvars subs vars;
-	   subs = subs }
-
   let rec split_vars vars1 vars2 = match vars1,vars2 with
     | ((x1,xv1) as z1)::vars1', ((x2,xv2) as z2)::vars2' ->
 	let c = X.compare x1 x2 in
@@ -842,9 +835,9 @@ module Simplify(M : MAKE)(X : Custom.T) = struct
 	    else if has_complement f1 f2 then f2::(aux (remove_complement f1 f2) s)
 	    else f2::(aux f1 s)
 	  else (
-	    let f1' = mk_vs vars1 subs1 in
-	    let f2' = mk_vs vars2 subs2 in
-	    let f   = mk_vs vars subs in
+	    let f1' = mk vars1 subs1 in
+	    let f2' = mk vars2 subs2 in
+	    let f   = mk vars subs in
 	    let f' = cup f (cap f1' f2') in
 (*	    Format.fprintf Format.std_formatter
 	      "MERGE %a+%a==>%a@." dump f1 dump f2 dump f'; *)
@@ -882,7 +875,7 @@ module Simplify(M : MAKE)(X : Custom.T) = struct
       | f :: s -> f :: (aux s) in
     let subs = aux subs in
 
-    let f = mk_vs vars subs in
+    let f = mk vars subs in
     List.fold_left cup f !hoist
 
   and elim_real elv f =
@@ -965,9 +958,9 @@ module Simplify(M : MAKE)(X : Custom.T) = struct
     if vars = [] && subs = [] then
       neg (cup (neg f1) (neg f2))
     else
-      let f1 = mk_vs vars1 subs1 in
-      let f2 = mk_vs vars2 subs2 in
-      let f  = mk_vs vars subs in
+      let f1 = mk vars1 subs1 in
+      let f2 = mk vars2 subs2 in
+      let f  = mk vars subs in
 (*      print_int (List.length vars); print_char ':';
       print_int (List.length subs); print_char ' '; *)
       cup f (cap f1 f2)
@@ -992,7 +985,7 @@ module Simplify(M : MAKE)(X : Custom.T) = struct
     if vars = [] && subs = [] then
       neg (cup (neg f1) f2)
     else
-      let f1 = mk_vs vars1 subs1 in
+      let f1 = mk vars1 subs1 in
 (*      print_int (List.length vars); print_char '!';
       print_int (List.length subs); print_char ' '; *)
       diff f1 f2
@@ -1020,8 +1013,8 @@ module Simplify(M : MAKE)(X : Custom.T) = struct
 	    cup (cap (negvar x) (elim [x,false] f)) 
 	      (cap (posvar x) (elim [x,true] f))
 	in
-	Format.fprintf Format.std_formatter
-	  "Simplify %a ==> %a@." dump f dump g;
+(*	Format.fprintf Format.std_formatter
+	  "Simplify %a ==> %a@." dump f dump g; *)
 	g
       )
       else
@@ -1086,7 +1079,7 @@ module Simplify(M : MAKE)(X : Custom.T) = struct
     B.compute ~empty ~full ~cup ~cap ~diff ~atom (form f)
 
   let get f = 
-    B.get (form (simplify f))
+    B.get (form ((*simplify*) f))
 
 
   module V = Custom.List(Custom.Pair(X)(Custom.Bool))
@@ -1099,6 +1092,6 @@ module Simplify(M : MAKE)(X : Custom.T) = struct
     let vars = List.sort (fun (x1,v1) (x2,v2) -> X.compare x1 x2) vars in
     let subs = Serialize.Get.list deserialize s in
     let subs = List.sort (fun f1 f2 -> f1.id - f2.id) subs in
-    mk_vs vars subs
+    mk vars subs
    
 end