dolmen.std
Term.Rat
Rational operations
dolmen
dolmen.ae
dolmen.class
dolmen.dimacs
dolmen.icnf
dolmen.intf
dolmen.line
dolmen.smtlib2
dolmen.tptp
dolmen.zf
dolmen_smtlib2_poly
dolmen_smtlib2_v6
dolmen_smtlib2_v6_response
dolmen_smtlib2_v6_script
dolmen_tptp_v6_3_0
Satisfy the common interface for TPTP's arithmetic over Rationals
include Dolmen_intf.Term.Tptp_Tff_Arith_Common with type t := t
val minus : t -> t
Arithmetic unary minus/negation.
val add : t -> t -> t
Arithmetic addition.
val sub : t -> t -> t
Arithmetic substraction
val mul : t -> t -> t
Arithmetic multiplication
val div_e : t -> t -> t
Euclidian division quotient
val div_t : t -> t -> t
Truncation of the rational/real division.
val div_f : t -> t -> t
Floor of the ration/real division.
val rem_e : t -> t -> t
Euclidian division remainder
val rem_t : t -> t -> t
Remainder for the truncation of the rational/real division.
val rem_f : t -> t -> t
Remaidner for the floor of the ration/real division.
val lt : t -> t -> t
Arithmetic "less than" comparison.
val le : t -> t -> t
Arithmetic "less or equal" comparison.
val gt : t -> t -> t
Arithmetic "greater than" comparison.
val ge : t -> t -> t
Arithmetic "greater or equal" comparison.
val floor : t -> t
Floor function.
val ceiling : t -> t
Ceiling
val truncate : t -> t
Truncation.
val round : t -> t
Rounding to the nearest integer.
val is_int : t -> t
Integer testing
val is_rat : t -> t
Rationality testing.
val to_int : t -> t
Convesion to an integer.
val to_rat : t -> t
Conversion to a rational.
val to_real : t -> t
Conversion to a real.
val mk : string -> t
Create a rational constant.
val div : t -> t -> t
Exact division on rationals.
val div_zero : term_cst
Symbol for interpretation of division by zero.
val rem_zero : term_cst
Symbol for interpretation of modulo by zero.