mc2.lra
Mc2_lra
mc2.backend
mc2.core
mc2.dimacs
mc2.propositional
mc2.smtlib
mc2.uf
mc2.unin_sort
type num = Q.t
module LE : sig ... end
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