package lutin

  1. Overview
  2. Docs
package lutin
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

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.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct