package lutin

  1. Overview
  2. Docs

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

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

    expr > 0

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

    expr >= 0

    *)

Normalised linear constraints.

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

    booleans

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

    expr = 0

    *)
  3. | Ineq of ineq
    (*

    > or >=

    *)
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