package lutin

  1. Overview
  2. Docs

Module Formula_to_bddSource

Encoding formula and expressions into bdds.

Sourcetype t
Sourceval init : unit -> t
Sourceval tbl_to_string : t -> string
Sourceval f : t -> Var.env_in -> Var.env -> string -> int -> Exp.formula -> t * Bdd.t

Formula_to_bdd.f input memory ctx_msg verbosity_level f returns the bdd of f where input and pre variables have been repaced by their values. ctx_msg is used for printing source information in case of errors.

ZZZ this function fills in local tables that are used later on during the random toss (e.g., via index_to_linear_constraint). Hence bdd should be build by this module.

Sourceval num_to_gne : t -> Var.env_in -> Var.env -> string -> int -> Exp.num -> t * Gne.t
Sourceval eval_int_expr : t -> Exp.num -> string -> Var.env_in -> Var.env -> int -> int option
Sourceval clear_all : t -> t

Clean-up all the internal tables that migth have been filled by (non-regression) assertions.

Sourceval clear_step : t -> t

Clean-up the cache tables that contain information that depends on input or pre. Indeed, this information is very likely to change (especially because floats) at each step, therefore we do not keep that information to avoid memory problems.

Sourceval index_to_linear_constraint : t -> int -> Constraint.t
Sourceval get_index_from_linear_constraint : t -> Constraint.t -> int
OCaml

Innovation. Community. Security.