Module LowLevelSeplog.Make

Parameters

module _ : CONFIG

Signature

Variables

module Variable : sig ... end

Terms

module Term : sig ... end

Formulae

type t
val show : t -> string

Constructors

val emp : t

The emp atom.

val tt : t

The true atom.

val mk_eq : Term.t list -> t

Equality of n terms.

  • raises SortError

    when arguments do not have the same width.

val mk_eq2 : Term.t -> Term.t -> t

Binary equality terms.

  • raises SortError

    when arguments do not have the same width.

val mk_distinct : Term.t list -> t

Pairwise disequality of n terms.

  • raises SortError

    when arguments do not have the same width.

val mk_distinct2 : Term.t -> Term.t -> t

Disequality of two terms.

  • raises SortError

    when arguments do not have the same width.

val mk_pto : Term.t -> Term.t -> t

mk_pto x y creates a poinst-to assertion x \mapsto y.

val mk_pto_array : ?const:Bitvector.t -> size:Term.t -> Term.t -> t

mk_pto x ~const ~size creates an array poinst-to assertion x \mapsto const[size]. The default value of const is \top.

val mk_star : t list -> t

Separating conjunction.

val mk_exists : Variable.t list -> t -> t

Existential quantification.

Satisfiability

val check_sat : t -> [ `Sat | `Unsat | `Unknown ]