package ocplib-simplex

  1. Overview
  2. Docs

Same than Make but allows to choose the implementation of polynomials, maps and sets

Parameters

module R : ExtSigs.Coefs
module V : ExtSigs.Value with type r = R.t
module R2 : Rat2.SIG with module R = R and module V = V
module P : Polys.SIG with module Var = Var and module R = R
module MX : ExtSigs.MapSig with type key = Var.t
module SX : ExtSigs.SetSig with type elt = Var.t

Signature

Modules

module Var = Var

The type of variables maipulated by the simplex algorithm.

module Ex = Ex

An interface for explanations; in practice, they are labels attached to bounds used for backtracking information on how bounds were discovered. The simplex algorithm does not create explanations: it will only attach empty explanations to bounds, build the union of explanations and print them. It is the user's job to provide the initial explanations when initializing the simplex core.

module R = R

The interface for rationals provided by users for the coefficient.

module V = V

The interface for values of variable and bounds provided by users.

module R2 : Rat2.SIG with module R = R and module V = V

Pairs of rationals R representing bounds with an offset x + kƐ.

module P = P

Linear relations of variables.

module MX = MX

Collections of variables.

module SX = SX

Types

type bound = {
  1. bvalue : R2.t;
  2. explanation : Ex.t;
}

A bound is a value of the form x + kƐ and an explanation.

type value_status =
  1. | ValueOK
    (*

    The value is inbetween bounds.

    *)
  2. | LowerKO
    (*

    The value is smaller than the lower bound.

    *)
  3. | UpperKO
    (*

    The value is greater than the upper bound.

    *)
type var_info = {
  1. mini : bound option;
  2. maxi : bound option;
  3. value : R2.t;
  4. vstatus : value_status;
  5. empty_dom : bool;
}
type solution = {
  1. main_vars : (Var.t * V.t) list;
  2. slake_vars : (Var.t * V.t) list;
  3. int_sol : bool;
  4. epsilon : V.t;
}
type maximum = {
  1. max_v : bound;
  2. is_le : bool;
}
type result =
  1. | Unknown
  2. | Unsat of Ex.t Lazy.t
  3. | Sat of solution Lazy.t
  4. | Unbounded of solution Lazy.t
  5. | Max of maximum Lazy.t * solution Lazy.t
type simplex_status =
  1. | UNK
  2. | UNSAT of Var.t
  3. | SAT
type t = {
  1. basic : (var_info * P.t) MX.t;
  2. non_basic : (var_info * SX.t) MX.t;
  3. slake : P.t MX.t;
  4. fixme : SX.t;
  5. is_int : bool;
  6. status : simplex_status;
  7. check_invs : bool;
  8. nb_pivots : int ref;
}
val empty : is_int:bool -> check_invs:bool -> t

Returns a simplex environment with three parameters:

  • is_int: will the simplex work on an integer optimization problem or a rational problem?
  • check_invs: processes checks after the calculation (deprecated).
val on_integers : t -> bool

Returns true if the simplex environment is on integers.

val equals_optimum : R2.t -> bound option -> bool

Equality check between bounds.

val consistent_bounds : var_info -> bool

Checks if the lower bound of a variable is smaller than its upper bound.

val violates_min_bound : R2.t -> bound option -> bool

violates_min_bound b mb returns true if b is smaller than mb.

val violates_max_bound : R2.t -> bound option -> bool

violates_max_bound b mb returns true if b is greater than mb.

val set_min_bound : var_info -> bound option -> var_info * bool

set_min_bound vinfo b returns a couple (vinfo', changed) where:

  • vinfo' is the new variable info where the new min bound b has been set.
  • changed is true if the new bound has changed the variable info
val set_max_bound : var_info -> bound option -> var_info * bool

Same as set_min_bound, but for max bounds.

val ajust_value_of_non_basic : var_info -> var_info * bool

ajust_value_of_non_basic vinfo updates the info's value with the upper bound (resp. the lower bound), if vinfo's status is UpperKO (resp. LowerKO). Otherwise, do nothing. The boolean returned is true if the new variable var_info has changed.

val ajust_status_of_basic : var_info -> var_info

ajust_status_of_basic vinfo checks a variable info's bound matches its status. If its value violates its lower bound, its status is set to LowerKO. In the other case, it is set to UpperKO. If the value is between the two bounds, it is set to ValueOK.

val evaluate_poly : t -> P.t -> R2.t

Evaluates a polynomial of non basic variables.

val poly_of_slake : t -> Var.t -> P.t option

poly_of_slake env slake returns the polynomial associated to the variable slake in env.

val expl_of_min_bound : var_info -> Ex.t

Returns the explanation associated to a variable lower bound.

val expl_of_max_bound : var_info -> Ex.t

Same as `expl_of_min_bound`, but for upper bounds.

Debug functions

Only use for internal debugging

val check_invariants : t -> (t -> result) -> unit

Checks several invariants in the project

val print : result -> Format.formatter -> t -> unit

Pretty prints the environment.

val debug : string -> t -> (t -> result) -> unit
  • deprecated
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