setr

Abstract domain library for sets
IN THIS PACKAGE

Parameters

module Var : VAR

Signature

type var = Var.t
type t =
| False
| True
| If of t * Var.t * t * int
module HashedIf : sig ... end
module IfHashCons : sig ... end
type ctx = {
bdd_hc : t IfHashCons.t;
bdd_hc_stamp : int ref;
not_cache : ( int, t ) Hashtbl.t;
and_cache : ( int * int, t ) Hashtbl.t;
or_cache : ( int * int, t ) Hashtbl.t;
xor_cache : ( int * int, t ) Hashtbl.t;
}
val init : unit -> ctx
val clear : ctx -> unit
val false_ : 'a -> t
val true_ : 'a -> t
val is_true : 'a -> t -> bool
val is_false : 'a -> t -> bool
val ident : 'a -> t -> int
val equal : 'a -> 'b -> 'c -> bool
val mkif : ctx -> t -> Var.t -> t -> t
val var_ : ctx -> Var.t -> t
val not_ : ctx -> t -> t
val and_ : ctx -> t -> t -> t
val or_ : ctx -> t -> t -> t
val xor_ : ctx -> t -> t -> t
val exists_ : ctx -> Var.t list -> t -> t
val forall_ : ctx -> Var.t list -> t -> t
val imply_ : ctx -> t -> t -> t
val equiv_ : ctx -> t -> t -> t
val ite_ : ctx -> t -> t -> t -> t
val pp : 'a -> Format.formatter -> t -> unit
type !'a visitor = {
true_ : 'a;
false_ : 'a;
if_ : var -> 'a -> 'a -> 'a;
}
val visit : 'a -> 'b visitor -> t -> 'b
val support : 'a -> t -> Var.t list