X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=src%2Fformula.ml;h=7bd8ca6587f24c9e3f687583a2d5bbd0d4e3b61b;hb=9c0b145d050a5981010435f54848dc862782709c;hp=f7eae8516083c264f88bad92af477ede121173ba;hpb=cba2938d929fd5119b1491686ddc224d5af618c6;p=tatoo.git

diff --git a/src/formula.ml b/src/formula.ml
index f7eae85..7bd8ca6 100644
--- a/src/formula.ml
+++ b/src/formula.ml
@@ -5,28 +5,34 @@
 (*                     Kim Nguyen, LRI UMR8623                         *)
 (*                   Université Paris-Sud & CNRS                       *)
 (*                                                                     *)
-(*  Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
+(*  Copyright 2010-2013 Université Paris-Sud and Centre National de la *)
 (*  Recherche Scientifique. All rights reserved.  This file is         *)
 (*  distributed under the terms of the GNU Lesser General Public       *)
 (*  License, with the special exception on linking described in file   *)
 (*  ../LICENSE.                                                        *)
 (*                                                                     *)
 (***********************************************************************)
+
+(*
+  Time-stamp: <Last modified on 2013-02-04 16:03:28 CET by Kim Nguyễn>
+*)
+
 INCLUDE "utils.ml"
 
 open Format
-type move = [ `Left | `Right ]
-type 'hcons expr =
-  | False | True
-  | Or of 'hcons * 'hcons
-  | And of 'hcons * 'hcons
-  | Atom of (move * bool * State.t)
+
+
+type move = [ `Left | `Right | `Epsilon | `Up1 | `Up2 ]
+type 'formula expr =
+  | False
+  | True
+  | Or of 'formula * 'formula
+  | And of 'formula * 'formula
+  | Atom of move * bool * State.t
 
 type 'hcons node = {
   pos : 'hcons expr;
   mutable neg : 'hcons;
-  st : StateSet.t * StateSet.t;
-  size: int; (* Todo check if this is needed *)
 }
 
 external hash_const_variant : [> ] -> int = "%identity"
@@ -37,7 +43,7 @@ module rec Node : Hcons.S
   and Data : Hashtbl.HashedType  with type t = Node.t node =
   struct
     type t =  Node.t node
-    let equal x y = x.size == y.size &&
+    let equal x y =
       match x.pos, y.pos with
       | a,b when a == b -> true
       | Or(xf1, xf2), Or(yf1, yf2)
@@ -58,12 +64,11 @@ module rec Node : Hcons.S
   end
 
 type t = Node.t
-let hash x = x.Node.key
+let hash x = x.Node.hash
 let uid x = x.Node.id
 let equal = Node.equal
 let expr f = f.Node.node.pos
-let st f = f.Node.node.st
-let size f = f.Node.node.size
+
 let compare f1 f2 = compare f1.Node.id  f2.Node.id
 let prio f =
   match expr f with
@@ -92,6 +97,9 @@ let rec print ?(parent=false) ppf f =
           match  dir with
           | `Left ->  Pretty.down_arrow, Pretty.subscript 1
           | `Right -> Pretty.down_arrow, Pretty.subscript 2
+          | `Epsilon -> Pretty.epsilon, ""
+          | `Up1 -> Pretty.up_arrow, Pretty.subscript 1
+          | `Up2 -> Pretty.up_arrow, Pretty.subscript 2
         in
         fprintf fmt "%s%s" a_str d_str;
         State.print fmt s;
@@ -107,36 +115,20 @@ let is_true f = (expr f) == True
 let is_false f = (expr f) == False
 
 
-let cons pos neg s1 s2 size1 size2 =
-  let nnode = Node.make { pos = neg; neg = (Obj.magic 0); st = s2; size = size2 } in
-  let pnode = Node.make { pos = pos; neg = nnode ; st = s1; size = size1 } in
+let cons pos neg =
+  let nnode = Node.make { pos = neg; neg = (Obj.magic 0); } in
+  let pnode = Node.make { pos = pos; neg = nnode } in
     (Node.node nnode).neg <- pnode; (* works because the neg field isn't taken into
                                        account for hashing ! *)
     pnode,nnode
 
 
-let empty_pair = StateSet.empty, StateSet.empty
-let true_,false_ = cons True False empty_pair empty_pair 0 0
+let true_,false_ = cons True False
 let atom_ d p s =
-  let si = StateSet.singleton s in
-  let ss = match d with
-    | `Left -> si, StateSet.empty
-    | `Right -> StateSet.empty, si
-  in fst (cons (Atom(d,p,s)) (Atom(d,not p,s)) ss ss 1 1)
+  fst (cons (Atom(d,p,s)) (Atom(d,not p,s)))
 
 let not_ f = f.Node.node.neg
 
-let union_pair (l1,r1) (l2, r2) =
-  StateSet.union l1 l2,
-  StateSet.union r1 r2
-
-let merge_states f1 f2 =
-  let sp =
-    union_pair (st f1) (st f2)
-  and sn =
-    union_pair (st (not_ f1)) (st (not_ f2))
-  in
-    sp,sn
 
 let order f1 f2 = if uid f1  < uid f2 then f2,f1 else f1,f2
 
@@ -155,10 +147,7 @@ let or_ f1 f2 =
   (* commutativity of | *)
   else
     let f1, f2 = order f1 f2 in
-    let psize = (size f1) + (size f2) in
-    let nsize = (size (not_ f1)) + (size (not_ f2)) in
-    let sp, sn = merge_states f1 f2 in
-      fst (cons (Or(f1,f2)) (And(not_ f1, not_ f2)) sp sn psize nsize)
+      fst (cons (Or(f1,f2)) (And(not_ f1, not_ f2)))
 
 
 let and_ f1 f2 =
@@ -167,12 +156,3 @@ let and_ f1 f2 =
 
 let of_bool = function true -> true_ | false -> false_
 
-
-module Infix = struct
-  let ( +| ) f1 f2 = or_ f1 f2
-
-  let ( *& ) f1 f2 = and_ f1 f2
-
-  let ( *+ ) d s = atom_ d true s
-  let ( *- ) d s = atom_ d false s
-end