Module Polynomial.WithProof

module WithProof constructs polynomials packed with the proof that their sign is correct.

type t = (LinPoly.t * op) * ProofFormat.prf_rule
exception InvalidProof

InvalidProof is raised if the operation is invalid.

val compare : t -> t -> int
val annot : string -> t -> t
val of_cstr : (cstr * ProofFormat.prf_rule) -> t
val output : Stdlib.out_channel -> t -> unit

out_channel chan c pretty-prints the constraint c over the channel chan

val output_sys : Stdlib.out_channel -> t list -> unit
val zero : t

zero represents the tautology (0=0)

val const : NumCompat.Q.t -> t

const n represents the tautology (n>=0)

val product : t -> t -> t

product p q

returns

the polynomial p*q with its sign and proof

val addition : t -> t -> t

addition p q

returns

the polynomial p+q with its sign and proof

val mult : LinPoly.t -> t -> t

mult p q

returns

the polynomial p*q with its sign and proof.

raises InvalidProof

if p is not a constant and p is not an equality

val cutting_plane : t -> t option

cutting_plane p does integer reasoning and adjust the constant to be integral

val linear_pivot : t list -> t -> Vect.var -> t -> t option

linear_pivot sys p x q

returns

the polynomial q where x is eliminated using the polynomial p The pivoting operation is only defined if

  • p is linear in x i.e p = a.x+b and x neither occurs in a and b
  • The pivoting also requires some sign conditions for a
val subst : t list -> t list
val subst1 : t list -> t list

subst1 sys performs a single substitution

val saturate_subst : bool -> t list -> t list
val is_substitution : bool -> t -> var option
val mul_bound : t -> t -> t option