X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fata.mli;h=e4f0ffdfff574a32b4b41e17efac4fc865257708;hp=8a1119ec5d5d62d164d97813bf58f001029ef184;hb=90ce5857f6cad2ebc753fdbc8e37882a1ff47415;hpb=acd23a33d837d03c813212ec3896a86edef16e87

diff --git a/src/ata.mli b/src/ata.mli
index 8a1119e..e4f0ffd 100644
--- a/src/ata.mli
+++ b/src/ata.mli
@@ -13,32 +13,27 @@
 (*                                                                     *)
 (***********************************************************************)
 
-(*
-  Time-stamp: <Last modified on 2013-04-24 23:19:41 CEST by Kim Nguyen>
-*)
-
-type predicate =
-    First_child
-  | Next_sibling
-  | Parent
-  | Previous_sibling
-  | Stay
-  | Is_first_child
-  | Is_next_sibling
-  | Is of Tree.NodeKind.t
-  | Has_first_child
-  | Has_next_sibling
+type move = [ `First_child
+            | `Next_sibling
+            | `Parent
+            | `Previous_sibling
+            | `Stay ]
+
+type predicate = Move of move * State.t
+                 | Is_first_child
+                 | Is_next_sibling
+                 | Is of Tree.NodeKind.t
+                 | Has_first_child
+                 | Has_next_sibling
 
 val is_move : predicate -> bool
 
-type atom = predicate * bool * State.t
+module Atom : Boolean.ATOM with type data = predicate
 
-module Atom : Formula.ATOM with type data = atom
-
-module SFormula :
+module Formula :
   sig
-    include module type of Formula.Make(Atom)
-    val mk_atom : predicate -> bool -> State.t -> t
+    include module type of Boolean.Make(Atom)
+    val mk_atom : predicate -> t
     val mk_kind : Tree.NodeKind.t -> t
     val has_first_child : t
     val has_next_sibling : t
@@ -58,7 +53,7 @@ module SFormula :
 
 
 module Transition : Hcons.S with
-            type data = State.t * QNameSet.t * SFormula.t
+            type data = State.t * QNameSet.t * Formula.t
 
 module TransList : sig
   include Hlist.S with type elt = Transition.t
@@ -74,17 +69,16 @@ type config = {
   unsat : StateSet.t;
   todo : TransList.t;
   summary : node_summary;
-  mutable round : int;
 }
 
 module Config : Hcons.S with type data = config
-
+val dummy_config : Config.t
 
 type t = private {
   id : Uid.t;
   mutable states : StateSet.t;
   mutable selection_states: StateSet.t;
-  transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t;
+  transitions: (State.t, (QNameSet.t*Formula.t) list) Hashtbl.t;
   mutable cache2 : TransList.t Cache.N2.t;
   mutable cache4 : Config.t Cache.N4.t;
 }
@@ -93,12 +87,13 @@ type t = private {
 
 val create : StateSet.t -> StateSet.t -> t
 val reset : t -> unit
+val full_reset : t -> unit
 val get_trans : t -> QNameSet.elt -> StateSet.t -> TransList.t
 
 
 val eval_trans : t -> Config.t -> Config.t -> Config.t -> Config.t -> Config.t
 
-val add_trans : t -> State.t -> QNameSet.t -> SFormula.t -> unit
+val add_trans : t -> State.t -> QNameSet.t -> Formula.t -> unit
 val print : Format.formatter -> t -> unit
 val complete_transitions : t -> unit
 val cleanup_states : t -> unit