1 (***********************************************************************)
5 (* Kim Nguyen, LRI UMR8623 *)
6 (* Université Paris-Sud & CNRS *)
8 (* Copyright 2010-2012 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 (***********************************************************************)
16 (** Implementation of hashconsed Boolean formulae *)
18 type move = [ `Left |`Right ]
19 (** Direction for automata predicates *)
24 | Or of 'hcons * 'hcons
25 | And of 'hcons * 'hcons
26 | Atom of (move * bool * State.t)
28 (** Partial internal representation of a formula,
29 used for pattern matching *)
32 (** Abstract type representing hashconsed formulae *)
35 (** Hash function for formulae *)
38 (** Returns a unique ID for formulae *)
40 val equal : t -> t -> bool
41 (** Equality over formulae *)
43 val expr : t -> t expr
44 (** Equality over formulae *)
46 val st : t -> StateSet.t * StateSet.t
47 (** states occuring left and right, positively or negatively *)
49 val compare : t -> t -> int
50 (** Comparison of formulae *)
53 (** Syntactic size of the formula *)
55 val eval_form : (StateSet.t * StateSet.t) -> t -> bool
56 (** [eval_form s_1,s_2 F] evaluates the formula [F] on [(s_1,s_2)] *)
58 val print : Format.formatter -> t -> unit
61 val is_true : t -> bool
62 (** [is_true f] tests whether the formula is the atom True *)
64 val is_false : t -> bool
65 (** [is_false f] tests whether the formula is the atom False *)
73 val atom_ : move -> bool -> StateSet.elt -> t
74 (** [atom_ dir b q] creates a down_left or down_right atom for state
75 [q]. The atom is positive if [b == true].
80 val and_ : t -> t -> t
81 (** Boolean connective *)
83 val of_bool : bool -> t
84 (** Convert an ocaml Boolean value to a formula *)
87 val ( +| ) : t -> t -> t
88 val ( *& ) : t -> t -> t
89 val ( *+ ) : move -> StateSet.elt -> t
90 val ( *- ) : move -> StateSet.elt -> t
92 (** Module to facilitate infix notations of formulae.
93 Just [open Formla.Infix] and write:
94 [let f = `Left *+ q1 +| `Right *+ q2 in ...]