Module Mc2_lra

Linear Rational Arithmetic

type num = Q.t
module LE = Mc2_lra__.Linexp
type op =
| Eq0
| Leq0
| Lt0

Boolean operator

val k_rat : Mc2_core.ty Mc2_core.Service.Key.t

Type of rationals

val k_make_const : (num -> Mc2_core.term) Mc2_core.Service.Key.t

Constant as a term

val k_make_pred : (op -> Mc2_lra__.Linexp.t -> Mc2_core.term) Mc2_core.Service.Key.t

Build constraint

val plugin : Mc2_core.Plugin.Factory.t
val set_lra_alt : int -> unit