package lutin

You can search for identifiers within the package.

in-package search v0.2.0

Legend:
Library
Module
Module type
Parameter
Class
Class type

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

type ineq =

Normalised linear constraints.

type t =

val dimension : t -> int

Returns the number of variables involved in the constraint

val dimension_ineq : ineq -> int

val get_vars : t -> string list

returns the vars appearing in a constraint

val get_vars_ineq : ineq -> string list

val 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.

val apply_subst_ineq : Ne.subst -> ineq -> ineq

val apply_substl : Ne.subst list -> t -> t

val apply_substl_ineq : Ne.subst list -> ineq -> ineq

val neg_ineq : ineq -> ineq

neg_ineq cstr returns the negation of an inequality constraint.

val opp_ineq : ineq -> ineq

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

val to_string : t -> string

Pretty printing.

val to_string_verbose : t -> string

val print : t -> unit

val ineq_to_string : ineq -> string

val print_ineq : ineq -> unit

val eval_ineq : Var.num_subst list -> ineq -> bool