logtk

Core types and algorithms for logic
IN THIS PACKAGE
Module type Logtk . Polynomial . S
type t
type coeff
type indet
val const : coeff -> t
val indet : indet -> t
val add : t -> t -> t
val mult_const : int -> t -> t
val mult_indet : indet -> t -> t
val compare : t -> t -> int

Compares two polynomials by comparing the coefficients for each monomial: If all coefficients of p1 >= the corresponding coefficient in p2, and one is even >, then return 1. If all coefficients of p1 <= the corresponding coefficient in p2, and one is even <, then return -1. If the polynomials are equal, return 0. If some coefficients are < and some are >, return 0.

val equal : t -> t -> bool
val pp : Format.formatter -> t -> unit