package lutin

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

Module ConstraintSource

Internal representation of constraints used in formula, namely, linear constraints over Booleans, integers, and floats.

Sourcetype ineq =
  1. | GZ of Ne.t
    (*

    expr > 0

    *)
  2. | GeqZ of Ne.t
    (*

    expr >= 0

    *)

Normalised linear constraints.

Sourcetype t =
  1. | Bv of Exp.var
    (*

    booleans

    *)
  2. | EqZ of Ne.t
    (*

    expr = 0

    *)
  3. | Ineq of ineq
    (*

    > or >=

    *)
Sourceval dimension : t -> int

Returns the number of variables involved in the constraint

Sourceval dimension_ineq : ineq -> int
Sourceval get_vars : t -> string list

returns the vars appearing in a constraint

Sourceval get_vars_ineq : ineq -> string list
Sourceval apply_subst : Ne.subst -> t -> t

apply_subst cstr s applies s to cstr. Note that the result could have been multiplied by a constant.

Sourceval apply_subst_ineq : Ne.subst -> ineq -> ineq
Sourceval apply_substl : Ne.subst list -> t -> t
Sourceval apply_substl_ineq : Ne.subst list -> ineq -> ineq
Sourceval neg_ineq : ineq -> ineq

neg_ineq cstr returns the negation of an inequality constraint.

Sourceval opp_ineq : ineq -> ineq

neg_ineq cstr returns cstr where its Ne.t is replaces by its opposite.

Sourceval to_string : t -> string

Pretty printing.

Sourceval to_string_verbose : t -> string
Sourceval print : t -> unit
Sourceval ineq_to_string : ineq -> string
Sourceval print_ineq : ineq -> unit
Sourceval eval_ineq : Var.num_subst list -> ineq -> bool
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