1 (***********************************************************************)
5 (* Kim Nguyen, LRI UMR8623 *)
6 (* Université Paris-Sud & CNRS *)
8 (* Copyright 2010-2013 Université Paris-Sud and Centre National de la *)
9 (* Recherche Scientifique. All rights reserved. This file is *)
10 (* distributed under the terms of the GNU Lesser General Public *)
11 (* License, with the special exception on linking described in file *)
14 (***********************************************************************)
24 | Is of Tree.NodeKind.t
28 val is_move : predicate -> bool
30 type atom = predicate * bool * State.t
32 module Atom : Formula.ATOM with type data = atom
36 include module type of Formula.Make(Atom)
37 val mk_atom : predicate -> bool -> State.t -> t
38 val mk_kind : Tree.NodeKind.t -> t
39 val has_first_child : t
40 val has_next_sibling : t
41 val is_first_child : t
42 val is_next_sibling : t
45 val is_processing_instruction : t
47 val first_child : State.t -> t
48 val next_sibling : State.t -> t
49 val parent : State.t -> t
50 val previous_sibling : State.t -> t
51 val stay : State.t -> t
52 val get_states : t -> StateSet.t
56 module Transition : Hcons.S with
57 type data = State.t * QNameSet.t * SFormula.t
59 module TransList : sig
60 include Hlist.S with type elt = Transition.t
61 val print : Format.formatter -> ?sep:string -> t -> unit
65 type node_summary = private int
66 val node_summary : bool -> bool -> bool -> bool -> Tree.NodeKind.t -> node_summary
67 val dummy_summary : node_summary
72 summary : node_summary;
75 module Config : Hcons.S with type data = config
76 val dummy_config : Config.t
80 mutable states : StateSet.t;
81 mutable selection_states: StateSet.t;
82 transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t;
83 mutable cache2 : TransList.t Cache.N2.t;
84 mutable cache4 : Config.t Cache.N4.t;
89 val create : StateSet.t -> StateSet.t -> t
91 val full_reset : t -> unit
92 val get_trans : t -> QNameSet.elt -> StateSet.t -> TransList.t
95 val eval_trans : t -> Config.t -> Config.t -> Config.t -> Config.t -> Config.t
97 val add_trans : t -> State.t -> QNameSet.t -> SFormula.t -> unit
98 val print : Format.formatter -> t -> unit
99 val complete_transitions : t -> unit
100 val cleanup_states : t -> unit
101 val normalize_negations : t -> unit