package lutin

  1. Overview
  2. Docs

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.