setr

Abstract domain library for sets
IN THIS PACKAGE
Module SETr_DS_CNF
type lit = bool * int
type clause = lit list
type clauses = clause list
val mk_true : 'a list
val mk_false : 'a list list
val mk_and : 'a list -> 'a list -> 'a list
val mk_var : 'a -> (bool * 'a) list list
val iter_distrib : ( 'a list -> unit ) -> 'a list list -> unit
module LSet : sig ... end
val mk_not : (bool * int) list list -> LSet.elt list list
val mk_or : 'a list list -> 'a list list -> 'a list list
val mk_imply : (bool * int) list list -> LSet.elt list list -> LSet.elt list list
val mk_eq : LSet.elt list list -> LSet.elt list list -> LSet.elt list list
exception Clause_true
val cofactor : 'a -> 'b -> ('a * 'b) list list -> ('a * 'b) list list
val mk_forall : 'a -> (bool * 'a) list list -> (bool * 'a) list list
val mk_exists : 'a -> (bool * 'a) list list -> (bool * 'a) list list
module Int : sig ... end
module ISet : sig ... end
val symbols : clauses -> int list
val pp : ( Format.formatter -> 'a -> unit ) -> Format.formatter -> (bool * 'a) list list -> unit
val pp_int : Format.formatter -> (bool * int) list list -> unit