package libzipperposition

You can search for identifiers within the package.

in-package search v0.2.0

Library for Zipperposition

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (4)

Authors

Maintainers

S

simon.cruanes.2007@m4x.org

Sources

1.6.tar.gz

md5=97cdb2f90468e9e27c7bbe3b4fb160bb

sha512=fee73369f673a91dfa9e265fc69be08b32235e10a495f3af6477d404fcd01e3452a0d012b150f3d7f97c00af2f6045019ad039164bf698f70d771231cc4efe5d

doc/libzipperposition.calculi/Libzipperposition_calculi/Simplex/MakeHelp/index.html

Module `Simplex.MakeHelp`Source

Parameters

module Var : OrderedType

Signature

Sourcetype external_var = Var.t

User provided variable type

Sourcetype var = private

| Intern of int
| Extern of external_var

Sourceval fresh_var : unit -> var

Fresh internal variable

Sourceval mk_var : external_var -> var

Lift an external variable in the var type

the usual system, but the extended variable type

include S with type var := var

Sourcetype t

The type of a (possibly not solved) linear system

Sourcetype 'cert res =

| Solution of (var * Q.t) list
| Unsatisfiable of 'cert

Generic type returned when solving the simplex. A solution is a list of bindings that satisfies all the constraints inside the system. If the system is unsatisfiable, an explanation of type 'cert is returned.

Sourcetype k_cert = var * (Q.t * var) list

An unsatisfiability explanation is a couple (x, expr). If expr is the empty list, then there is a contradiction between two given bounds of x. Else, the explanation is an equality x = expr that is valid (it can be derived from the original equations of the system) from which a bound can be deduced which contradicts an already given bound of the system.

Sourcetype n_cert = cert_tree option ref

Sourceand cert_tree =

| Branch of var * Z.t * n_cert * n_cert
| Explanation of k_cert
(*
The type of explanation for integer systems. In one case, the system is unsatisfiable when seen as a rational system. In the other case, two cases are considered : for a given variable x and a bound b, either x is lower than b, or it is greater then b + 1.
*)

Sourcetype k_res = k_cert res

Sourcetype n_res = n_cert res

Types returned when solving a system.

Sourcetype optim =

| Tight of var
| Multiply of var * Q.t

The type of traces of the optimizations performed on a simplex.

Sourcetype debug_printer = Format.formatter -> t -> unit

TODO

Simplex construction

Sourceval empty : t

The empty system

Sourceval add_eq : t -> (var * (Q.t * var) list) -> t

add_eq s (x, eq) returns a system containing the same constraints as s, plus the equation (x = eq).

Sourceval add_bounds : t -> (var * Q.t * Q.t) -> t

add_bounds (x, lower, upper) returns a system containing the same constraints as s, plus the bounds lower and upper for the given variable x. If the bound is loose on one side (no upper bounds for instance), the values Zarith.Q.inf and Zarith.Q.minus_inf can be used. By default, in a system, all variables have no bounds, i.e have lower bound Zarith.Q.minus_inf and upper bound Zarith.Q.inf.

Simplex solving

Sourceval ksolve : ?debug:debug_printer -> t -> k_res

ksolve s solves the system s and returns a solution, if one exists. This function may change the internal representation of the system to that of an equivalent one (permutation of basic and non basic variables and pivot operation on the tableaux).

parameter debug
An optional debug option can be given, and will be applied to all systems encountered while solving the system, including the initial and final states of the system. Can be used for printing intermediate states of the system.

Sourceval nsolve : t -> var list -> n_res

nsolve s int_vars solve the system s considering the variables in int_vars as integers instead of rationals. There is no guarantee that this function will terminate (for instance, on the system (1 <= 3 * x + 3 * y <= 2, nsolve will NOT terminate), it hence recommended to apply a global bounds to the variables of a system before trying to solve it with this function.

parameter debug
An optional debug option can be given, and will be applied to all systems encountered at the end of a branch while solving the system. Can be used for printing intermediate states of the system.

Sourceval safe_nsolve : t -> var list -> Q.t * n_res

safe_nsolve s int_vars solves the system s considering the variables in int_vars as integers. This function always terminate, thanks to a global bound that is applied to all variables of int_vars. The global bound is also returned to allow for verification. Due to the bounds being very high, safe_nsolve may take a lot of time and memory. It is recommended to apply some optimizations before trying to solve system using this function.

Simplex optimizations

Sourceval tighten : var list -> t -> optim list

tighten int_vars s tightens all the bounds of the variables in int_vars and returns the list of optimizations performed on the system.

Sourceval normalize : var list -> t -> optim list

normalize int_vars s, normalizes the system s (in place), and returns the list of optimizations performed on it. int_vars is the list of variable that should be assigned an integer. A normalized system has only integer coefficients in his tableaux. Furthermore, in any line (i.e in the expression of a basic variable x), the gcd of all coefficients is 1. This includes the bounds of x, except in the following case. If all pertinent variables (have a non-zero coefficient) in the expression of x are in int_vars, then the bounds are divided by the gcd of the coefficients in the expression, and then rounded (since we can deduce that x must be an integer as well).

Sourceval preprocess : t -> var list -> optim list

Apply all optimizations to a simplex.

Sourceval apply_optims : (t -> optim list) list -> t -> optim list

Apply the given optimizations to the simplex.

Access functions

Sourceval get_tab : t -> var list * var list * Q.t list list

get_tab s returns the current tableaux of s as a triple (l, l', tab) where l is the list of the non-basic variables, l' the list of basic variables and tab the list of the rows of the tableaux in the same order as l and l'.

Sourceval get_assign : t -> (var * Q.t) list

get_assign s returns the current (partial) assignment of the variables in s as a list of bindings. Only non-basic variables (as given by get_tab) should appear in this assignent. As such, and according to simplex invariants, all variables in the assignment returned should satisfy their bounds.

Sourceval get_full_assign : t -> (var * Q.t) list

Sourceval get_bounds : t -> var -> Q.t * Q.t

get_bounds s x returns the pair (low, upp) of the current bounds for the variable x. Notice that it is possible that low is strictly greater than upp.

Sourceval get_all_bounds : t -> (var * (Q.t * Q.t)) list

get_all_bounds s returns the list of all the explicit bounds of s. Any variable not present in the return value is assumed to have no bounds (i.e lower bound Zarith.Q.minus_inf and upper bound Zarith.Q.inf).

Printing functions

Source

val print_debug : 
  (Format.formatter -> var -> unit) ->
  Format.formatter ->
  t ->
  unit

print_debug print_var returns a suitable function for printing debug info on the current state of a system. It can for instance be used as the debug function of solve to see the evolution of the simplex.

Sourcetype monome = (Q.t * external_var) list

Sourcetype op =

| LessEq
| Eq
| GreaterEq

Sourcetype constraint_ = op * monome * Q.t

Sourceval add_constraints : t -> constraint_ list -> t

On This Page

Parameters
Signature