package mc2

  1. Overview
  2. Docs

Linear Rational Arithmetic

type num = Q.t
module LE : sig ... end
type op =
  1. | Eq0
  2. | Leq0
  3. | Lt0

Boolean operator

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 set_lra_alt : int -> unit