module Atom: sig end
type t =
val eq : t -> t -> bool
type atom = t
module Set: sig end
val mk_true : t
val mk_false : t
val mk_equal : Term.t * Term.t -> t
val mk_diseq : Term.t * Term.t -> t
val mk_in : Term.t * Sign.t -> t
val mk_ge : Term.t * Term.t -> t
val mk_gt : Term.t * Term.t -> t
val mk_le : Term.t * Term.t -> t
val mk_lt : Term.t * Term.t -> t
val pp : Format.formatter -> t -> unit
| Parameters: |
|
fmt |
: |
Format.formatter
|
|
?? |
: |
t
|
|
val is_negatable : t -> bool
val negate : t -> t
val vars_of : t -> Term.Set.t
val list_of_vars : t -> Term.Set.elt list
module Pairtbl: sig end
val occurs : Var.t * t -> bool
val is_connected : t -> t -> bool