module Arith: sig end
Operation on
linear arithmetic function symbols.
mk_num q, mk_multq q, and mk_add construct hashconsed function
symbols for representing Num(q), Multq(q), and Add, respectively.get f returns the arithmetic function symbol represented by f,
or raises Not_found. - The tests
is_num f, is_multq f, is_add f succeed iff f represents
a Num _, Multq _, or Add, respectively.
d_num f (d_multq f) returns q if f represents Num(q) (Multq(q)) and
raises Not_found otherwise.pp p fmt (op, al) pretty-prints the appliation of op to the list of
arguments al depending on the value of Pretty.flag. In particular,
if Pretty.flag is set to Pretty.Mixfix, then the application of
addition is printed infix. See also Pretty.apply. It assumes a
constant application to Num _, a unary application to Multq _,
and an nary application to Add.
val mk_num : Mpa.Q.t -> Sym.t
val mk_multq : Mpa.Q.t -> Sym.t
val mk_add : Sym.t
val get : Sym.t -> Sym.arith
val is_num : Sym.t -> bool
val is_multq : Sym.t -> bool
val is_add : Sym.t -> bool
val d_num : Sym.t -> Mpa.Q.t
val d_multq : Sym.t -> Mpa.Q.t
val pp : 'a Pretty.printer -> (Sym.arith * 'a list) Pretty.printer