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 (***********************************************************************)
17 Time-stamp: <Last modified on 2013-02-07 10:03:26 CET by Kim Nguyen>
20 module type PREDICATE =
24 val eval : ctx -> t -> bool
26 include Utils.Hcons.Abstract with type t := t
27 include Utils.Sigs.AUX.Printable with type t := t
30 type ('formula,'pred) expr =
33 | Or of 'formula * 'formula
34 | And of 'formula * 'formula
37 (** View of the internal representation of a formula,
38 used for pattern matching *)
40 module Make(P : PREDICATE) :
44 (** Abstract type representing hashconsed formulae *)
47 (** Hash function for formulae *)
49 val uid : t -> Utils.Uid.t
50 (** Returns a unique ID for formulae *)
52 val equal : t -> t -> bool
53 (** Equality over formulae *)
55 val expr : t -> (t,P.t) expr
56 (** Equality over formulae *)
58 val compare : t -> t -> int
59 (** Comparison of formulae *)
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 *)
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 *)
89 val eval : P.ctx -> t -> bool
90 (** Evaluate a formula given a context for atomic predicates *)