Sanitize the representation of formula

[tatoo.git] / src / ata.mli

diff --git a/src/ata.mli b/src/ata.mli
index bb94a7c..e4f0ffd 100644 (file)
--- a/src/ata.mli
+++ b/src/ata.mli
@@ -13,32 +13,27 @@
 (*                                                                     *)
 (***********************************************************************)
 
-(*
-  Time-stamp: <Last modified on 2013-04-04 18:42:38 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
@@ -66,27 +61,39 @@ module TransList : sig
 end
 
 
+type node_summary = private int
+val node_summary : bool -> bool -> bool -> bool -> Tree.NodeKind.t -> node_summary
+val dummy_summary : node_summary
+type config = {
+  sat : StateSet.t;
+  unsat : StateSet.t;
+  todo : TransList.t;
+  summary : node_summary;
+}
+
+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 cache6 : (TransList.t*StateSet.t) Cache.N6.t;
+  mutable cache4 : Config.t Cache.N4.t;
 }
 
 
 
 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 -> TransList.t
-  -> StateSet.t -> StateSet.t -> StateSet.t -> StateSet.t
-  -> bool -> bool -> bool -> bool -> Tree.NodeKind.t
-  -> TransList.t*StateSet.t
 
-val add_trans : t -> State.t -> QNameSet.t -> SFormula.t -> unit
+val eval_trans : t -> Config.t -> Config.t -> Config.t -> Config.t -> Config.t
+
+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