diff options
Diffstat (limited to 'plugins/micromega/sos.mli')
| -rw-r--r-- | plugins/micromega/sos.mli | 32 |
1 files changed, 1 insertions, 31 deletions
diff --git a/plugins/micromega/sos.mli b/plugins/micromega/sos.mli index 31c9518c8..42e22ffec 100644 --- a/plugins/micromega/sos.mli +++ b/plugins/micromega/sos.mli @@ -6,33 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) - -type vname = string;; - -type term = -| Zero -| Const of Num.num -| Var of vname -| Inv of term -| Opp of term -| Add of (term * term) -| Sub of (term * term) -| Mul of (term * term) -| Div of (term * term) -| Pow of (term * int) - -type positivstellensatz = - Axiom_eq of int - | Axiom_le of int - | Axiom_lt of int - | Rational_eq of Num.num - | Rational_le of Num.num - | Rational_lt of Num.num - | Square of term - | Monoid of int list - | Eqmul of term * positivstellensatz - | Sum of positivstellensatz * positivstellensatz - | Product of positivstellensatz * positivstellensatz +open Sos_types type poly @@ -55,10 +29,6 @@ val term_of_sos : positivstellensatz * (Num.num * poly) list -> val string_of_poly : poly -> string -exception TooDeep - -val deepen_until : int -> (int -> 'a) -> int -> 'a - val real_positivnullstellensatz_general : bool -> int -> poly list -> (poly * positivstellensatz) list -> poly -> poly list * (positivstellensatz * (Num.num * poly) list) list |