Module Micromega_plugin.Sos_types

type vname = string
type term =
| Zero
| Const of NumCompat.Q.t
| Var of vname
| Opp of term
| Add of term * term
| Sub of term * term
| Mul of term * term
| Pow of term * int
val output_term : Stdlib.out_channel -> term -> unit
type positivstellensatz =
| Axiom_eq of int
| Axiom_le of int
| Axiom_lt of int
| Rational_eq of NumCompat.Q.t
| Rational_le of NumCompat.Q.t
| Rational_lt of NumCompat.Q.t
| Square of term
| Monoid of int list
| Eqmul of term * positivstellensatz
| Sum of positivstellensatz * positivstellensatz
| Product of positivstellensatz * positivstellensatz
val output_psatz : Stdlib.out_channel -> positivstellensatz -> unit