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 sf,sn F] evaluates the formula [F] on [(sf,sn)] *)
58 val infer_form : (StateSet.t * StateSet.t) -> (StateSet.t * StateSet.t) -> t -> bool
59 (** [eval_form S1 S2 F] infers S1; S2 |- F *)
61 val print : Format.formatter -> t -> unit
64 val is_true : t -> bool
65 (** [is_true f] tests whether the formula is the atom True *)
67 val is_false : t -> bool
68 (** [is_false f] tests whether the formula is the atom False *)
76 val atom_ : move -> bool -> StateSet.elt -> t
77 (** [atom_ dir b q] creates a down_left or down_right atom for state
78 [q]. The atom is positive if [b == true].
83 val and_ : t -> t -> t
84 (** Boolean connective *)
86 val of_bool : bool -> t
87 (** Convert an ocaml Boolean value to a formula *)
90 val ( +| ) : t -> t -> t
91 val ( *& ) : t -> t -> t
92 val ( *+ ) : move -> StateSet.elt -> t
93 val ( *- ) : move -> StateSet.elt -> t
95 (** Module to facilitate infix notations of formulae.
96 Just [open Formla.Infix] and write:
97 [let f = `Left *+ q1 +| `Right *+ q2 in ...]