/[svn]/misc/bool.ml
ViewVC logotype

Diff of /misc/bool.ml

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 275 by abate, Tue Jul 10 17:21:31 2007 UTC revision 281 by abate, Tue Jul 10 17:22:16 2007 UTC
# Line 36  Line 36 
36    
37    val print: string -> (Format.formatter -> 'a elem -> unit) -> 'a t ->    val print: string -> (Format.formatter -> 'a elem -> unit) -> 'a t ->
38      (Format.formatter -> unit) list      (Format.formatter -> unit) list
39    
40      val trivially_disjoint: 'a t -> 'a t -> bool
41  end  end
42    
43  module Make(X : ARG) =  module Make(X : ARG) =
# Line 74  Line 76 
76        | _,False -> 1        | _,False -> 1
77    
78    
 (*  
   let rec hash = function  
     | True -> 1  
     | False -> 2  
     | Split (x, p,i,n) ->  
         (X.hash x) + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n)  
 *)  
79    let rec hash = function    let rec hash = function
80      | True -> 1      | True -> 1
81      | False -> 0      | False -> 0
# Line 180  Line 175 
175     - no ``subsumption'     - no ``subsumption'
176  *)  *)
177    
178    (*
179    let rec simplify a b =    let rec simplify a b =
180      if equal a b then False      if equal a b then False
181      else match (a,b) with      else match (a,b) with
# Line 204  Line 200 
200              if (p1 != p1') || (n1 != n1') || (i1 != i1')              if (p1 != p1') || (n1 != n1') || (i1 != i1')
201              then split x1 p1' i1' n1'              then split x1 p1' i1' n1'
202              else a              else a
203  (*  *)
204    
205    
206    let rec simplify a l =    let rec simplify a l =
207      if (a = False) then False else simpl_aux1 a [] l      if (a = False) then False else simpl_aux1 a [] l
208    and simpl_aux1 a accu = function    and simpl_aux1 a accu = function
# Line 239  Line 237 
237            simpl_aux2 x p i n (b :: ap) (b :: ai) (b :: an) l            simpl_aux2 x p i n (b :: ap) (b :: ai) (b :: an) l
238          else          else
239            simpl_aux2 x p i n (p2 :: i2 :: ap) (i2 :: ai) (n2 :: i2 :: an) l            simpl_aux2 x p i n (p2 :: i2 :: ap) (i2 :: ai) (n2 :: i2 :: an) l
240  *)  
241    
242    
243    let split x p i n =    let split x p i n =
244      split x (simplify p i) i (simplify n i)      split x (simplify p [i]) i (simplify n [i])
245    
246    
247    let rec ( ++ ) a b =    let rec ( ++ ) a b =
248  (*    if equal a b then a *)  (*    if equal a b then a *)
# Line 281  Line 281 
281  (*          split x1  (*          split x1
282                (p1 ** (p2 ++ i2) ++ (p2 ** i1))                (p1 ** (p2 ++ i2) ++ (p2 ** i1))
283                (i1 ** i2)                (i1 ** i2)
284                (n1 ** (n2 ++ i2) ++ (n2 ** i1))                (n1 ** (n2 ++ i2) ++ (n2 ** i1))  *)
 *)  
285              split x1              split x1
286                ((p1 ++ i1) ** (p2 ++ i2))                ((p1 ++ i1) ** (p2 ++ i2))
287                False                False
# Line 292  Line 291 
291            else            else
292              split x2 (p2 ** a) (i2 ** a) (n2 ** a)              split x2 (p2 ** a) (i2 ** a) (n2 ** a)
293    
294      let rec trivially_disjoint a b =
295        if a == b then a = False
296        else match (a,b) with
297          | True, a | a, True -> a = False
298          | False, _ | _, False -> true
299          | Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
300              let c = X.compare x1 x2 in
301              if c = 0 then
302    (* try expanding -> p1 p2; p1 i2; i1 p2; i1 i2 ... *)
303                trivially_disjoint (p1 ++ i1) (p2 ++ i2) &&
304                trivially_disjoint (n1 ++ i1) (n2 ++ i2)
305              else if c < 0 then
306                trivially_disjoint p1 b &&
307                trivially_disjoint i1 b &&
308                trivially_disjoint n1 b
309              else
310                trivially_disjoint p2 a &&
311                trivially_disjoint i2 a &&
312                trivially_disjoint n2 a
313    
314    let rec neg = function    let rec neg = function
315      | True -> False      | True -> False
316      | False -> True      | False -> True
# Line 325  Line 344 
344    let cap = ( ** )    let cap = ( ** )
345    let diff = ( // )    let diff = ( // )
346    
347    (*
348    let diff x y =    let diff x y =
349  (*    let d = diff x y in      let d = diff x y in
350      Format.fprintf Format.std_formatter "X = %a@\nY = %a@\nX\\Z = %a@\n"      Format.fprintf Format.std_formatter "X = %a@\nY = %a@\nX\\Z = %a@\n"
351        dump x dump y dump d;  *)        dump x dump y dump d;
352      diff x y      d
353    
354      let cap x y =
355        let d = cap x y in
356        Format.fprintf Format.std_formatter "X = %a@\nY = %a@\nX**Z = %a@\n"
357          dump x dump y dump d;
358        d
359    *)
360  end  end
Legend:
Removed from v.275  
changed lines
  Added in v.281
CVS Admin">CVS Admin
 ViewVC Help
Powered by ViewVC 1.1.5