Module `While_analysis.NonRelationalDomain`

module Terms : sig ... end

val name : string

type t

type binary = Operator.Function_symbol.binary Terms.t

type integer = Operator.Function_symbol.integer Terms.t

type boolean = Operator.Function_symbol.boolean Terms.t

type enum = Operator.Function_symbol.enum Terms.t

val equal : t -> t -> bool

val top : t

module Integer_Query : sig ... end

module Query : sig ... end

val nondet : 
  doma:t ->
  tupa:Terms.any Immutable_array.t ->
  domb:t ->
  tupb:Terms.any Immutable_array.t ->
  tupres:Terms.any Immutable_array.t ->
  t

val widened_fixpoint_step : 
  previous:t ->
  previous_tup:Terms.any Immutable_array.t ->
  next:t ->
  next_tup:Terms.any Immutable_array.t ->
  bool ->
  res_tup:Terms.any Immutable_array.t ->
  t * bool

val integer_empty : t -> integer -> t

val boolean_empty : t -> boolean -> t

val binary_empty : size:Units.In_bits.t -> t -> binary -> t

val enum_empty : t -> enum -> t

val integer_unknown : t -> integer -> t

val boolean_unknown : t -> boolean -> t

val binary_unknown : size:Units.In_bits.t -> t -> binary -> t

val enum_unknown : enumsize:int -> t -> enum -> t

val assume : t -> boolean -> t option

module Domain_Arity : sig ... end

module Boolean_Forward : sig ... end

module Integer_Forward : sig ... end

module Binary_Forward : sig ... end

module Enum_Forward : sig ... end

val boolean_pretty : t -> Stdlib.Format.formatter -> boolean -> unit

val integer_pretty : t -> Stdlib.Format.formatter -> integer -> unit

val binary_pretty : 
  size:Units.In_bits.t ->
  t ->
  Stdlib.Format.formatter ->
  binary ->
  unit

val enum_pretty : t -> Stdlib.Format.formatter -> enum -> unit

val pretty : Stdlib.Format.formatter -> t -> unit

val fixpoint_open : unit -> unit

val fixpoint_step : 
  lvl:int ->
  iteration:int ->
  t ->
  actuals:Terms.any Immutable_array.t ->
  t ->
  args:Terms.any Immutable_array.t ->
  t ->
  finals:Terms.any Immutable_array.t ->
  bool * (close:bool -> Terms.any Immutable_array.t -> t)

Module While_analysis.NonRelationalDomain

Module `While_analysis.NonRelationalDomain`