Linear constraints represent constraints on expressions.
type op
[
|
`Leq
`Geq
`Lt
`Gt
`Eq
`Neq
]
Arithmetic comparison operators.
type +'a t
=
{
expr : Expr.t;
op : 'a;
}
constraint 'a = [< op ]
Linear constraints. Expressions are implictly comapred to zero.
val compare : 'a t ‑> 'a t ‑> int
Standard comparison function.
val pp : _ t CCFormat.printer
Standard printing function.
val of_expr : Expr.t ‑> 'a ‑> 'a t
val make : Comb.t ‑> 'a ‑> C.t ‑> 'a t
Create a constraint from a linear expression/combination and a constant.
val op : 'a t ‑> 'a
val expr : _ t ‑> Expr.t
Extract the given part from a constraint.
val split : 'a t ‑> Comb.t * 'a * C.t
Split the linear combinations from the constant
val eval : subst ‑> _ t ‑> bool
Evaluate the given constraint under a substitution. TODO: document exceptions raised.