From a3bb6d0cb9aa8482f103dc9756501923c7c98637 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Thu, 11 May 2023 15:39:51 +0200
Subject: [PATCH 1/9] [model] use algebraic number for reals

Tentative introduction of root-of-with-order

Model support algebraic number

   root-of-with-order and root-of-with-enclosure

   Error path should be improved

[Model] Set version of calcium needed

Accept root-of-with-ordering

[Algebraic] accept also root-of-with-interval

[Algebraic] accept "-3" coefficient for experiment
---
 dolmen_model.opam                             |   1 +
 src/interface/term.ml                         |   3 +
 src/model/coercion.ml                         |   2 +-
 src/model/dune                                |   2 +
 src/model/fp.ml                               |   9 +-
 src/model/real.ml                             | 256 +++++++++++++++---
 src/model/real.mli                            |  71 ++++-
 src/standard/builtin.ml                       |   5 +
 src/standard/builtin.mli                      |   5 +
 src/standard/expr.ml                          |  50 ++++
 src/standard/expr.mli                         |  10 +
 src/typecheck/arith.ml                        |  68 ++++-
 tests/model/real/algebraic.expected           |   0
 tests/model/real/algebraic.rsmt2              |   7 +
 tests/model/real/algebraic.smt2               |   8 +
 tests/model/real/dune                         |  66 +++++
 .../model/real/kissing_2_6_scramble.expected  |   0
 tests/model/real/kissing_2_6_scramble.rsmt2   |  27 ++
 tests/model/real/kissing_2_6_scramble.smt2    |  39 +++
 19 files changed, 585 insertions(+), 44 deletions(-)
 create mode 100644 tests/model/real/algebraic.expected
 create mode 100644 tests/model/real/algebraic.rsmt2
 create mode 100644 tests/model/real/algebraic.smt2
 create mode 100644 tests/model/real/kissing_2_6_scramble.expected
 create mode 100644 tests/model/real/kissing_2_6_scramble.rsmt2
 create mode 100644 tests/model/real/kissing_2_6_scramble.smt2

diff --git a/dolmen_model.opam b/dolmen_model.opam
index 6667b1f14..9165cceee 100644
--- a/dolmen_model.opam
+++ b/dolmen_model.opam
@@ -16,6 +16,7 @@ depends: [
   "odoc" { with-doc }
   "zarith" { >= "1.10" }
   "farith"
+  "calcium" { >= "0.3" }
 ]
 tags: [ "logic" "type" "model" "modelchecking" "first order" ]
 homepage: "https://github.com/Gbury/dolmen"
diff --git a/src/interface/term.ml b/src/interface/term.ml
index 21f866e92..881cb4027 100644
--- a/src/interface/term.ml
+++ b/src/interface/term.ml
@@ -1309,6 +1309,9 @@ module type Smtlib_Real = sig
   val div : t -> t -> t
   (** Real division. See Smtlib theory for a full description. *)
 
+  val algebraic_ordered_root : string list -> string -> t
+  val algebraic_enclosed_root : string list -> (string * string) -> (string * string) -> t
+
 end
 
 (** Signature required by terms for typing smtlib real_int arithmetic. *)
diff --git a/src/model/coercion.ml b/src/model/coercion.ml
index 05192b137..3c23f84e9 100644
--- a/src/model/coercion.ml
+++ b/src/model/coercion.ml
@@ -21,7 +21,7 @@ let int_to_real =
   let v =
     Fun.fun_1 ~cst (fun v ->
         let z = Value.extract_exn ~ops:Int.ops v in
-        Real.mk (Q.of_bigint z))
+        Real.mk (Real.A.of_bigint z))
   in
   [E.Ty.int; E.Ty.real], (fun _ -> v)
 
diff --git a/src/model/dune b/src/model/dune
index 466fabc98..e1201c16c 100644
--- a/src/model/dune
+++ b/src/model/dune
@@ -17,6 +17,8 @@
     ; compilation errors due to a missing .cmi file (and type aliases not being
     ; fully resolved).
     farith ppx_deriving.runtime
+    ; Algebraic numbers
+    calcium
   )
   (modules
     ; Model checking
diff --git a/src/model/fp.ml b/src/model/fp.ml
index d0ebcf2cd..107e9eda6 100644
--- a/src/model/fp.ml
+++ b/src/model/fp.ml
@@ -128,8 +128,10 @@ let builtins ~eval env (cst : Dolmen.Std.Expr.Term.Const.t) =
   | B.Real_to_fp (ew, prec) ->
     Some (Fun.mk_clos @@ Fun.fun_2 ~cst (fun m r ->
         check ~ew ~mw:(prec - 1);
-        mk (f_of_q ~ew ~mw:(prec - 1) (mode m) (Real.get r))))
-  | B.Fp_to_fp (_ew1, _prec1, ew2, prec2) ->
+        match Real.A.to_q  @@ Real.get r with
+        | Some q -> mk (f_of_q ~ew ~mw:(prec - 1) (mode m) q)
+        | None -> invalid_arg "not implemented: algebraic number to floating point"))
+ | B.Fp_to_fp (_ew1, _prec1, ew2, prec2) ->
     Some (Fun.mk_clos @@ Fun.fun_2 ~cst
             (fun m f1 -> mk @@ f_round ~ew:ew2 ~mw:(prec2 - 1) (mode m) (fp f1)))
   | B.Sbv_to_fp (n, ew, prec) ->
@@ -156,7 +158,8 @@ let builtins ~eval env (cst : Dolmen.Std.Expr.Term.Const.t) =
         mk @@
         f_of_bits ~ew ~mw:(prec - 1) (Bitv.ubitv (ew + prec) bv)))
   | B.To_real (_ew, _prec) ->
-    Some (Fun.mk_clos @@ Fun.fun_1 ~cst (fun f -> Real.mk @@ (F.to_q (fp f))))
+    Some (Fun.mk_clos @@ Fun.fun_1 ~cst
+     (fun f -> Real.mk @@ Real.A.of_q @@ (F.to_q (fp f))))
   | B.Plus_infinity (ew, prec) ->
     Some (mk @@ f_inf ~ew ~mw:(prec - 1) false)
   | B.Minus_infinity (ew, prec) ->
diff --git a/src/model/real.ml b/src/model/real.ml
index 0f201645c..e9017e0ea 100644
--- a/src/model/real.ml
+++ b/src/model/real.ml
@@ -4,23 +4,201 @@
 (* Value definition *)
 (* ************************************************************************* *)
 
-(* Real are currently represented as rationals.
-   This is correct for quantifier free logic, since without non-rational
-   contants, we do not have a way to create non-rational values.
-   However, we may need to upgrade this representation to a more complete
-   one when we add quantifiers and/or new constants/operators on real
-   values. *)
-type t = Q.t
-
-let compare = Q.compare
+(* Real are currently represented as algebraic numbers *)
+
+(* Extending Q module from Zarith *)
+module Q = struct
+    let pp fmt q =
+        match Q.classify q with
+        | Q.ZERO -> Format.pp_print_char fmt '0'
+        | Q.INF -> Format.pp_print_string fmt "+∞"
+        | Q.MINF -> Format.pp_print_string fmt "-∞"
+        | Q.UNDEF -> Format.pp_print_string fmt "!undef!"
+        | Q.NZERO -> Q.pp_print fmt q
+
+
+  let two = Q.of_int 2
+  let is_integer q = Z.equal Z.one q.Q.den
+
+  let is_unsigned_integer size q =
+    is_integer q && (Z.sign q.Q.num >= 0) && (Z.numbits q.Q.num <= size)
+
+  let floor x = Q.of_bigint (Z.fdiv x.Q.num x.Q.den)
+  let ceil x = Q.of_bigint (Z.cdiv x.Q.num x.Q.den)
+  let truncate d = if (Q.sign d > 0) then floor d else ceil d
+
+  let div_e a b =
+    let s = Q.sign b in
+    let d = Q.div a b in
+    if (s > 0) then floor d else ceil d
+
+  let div_t a b = truncate (Q.div a b)
+  let div_f a b = floor (Q.div a b)
+  let mod_e a b = Q.sub a (Q.mul (div_e a b) b)
+  let mod_t a b = Q.sub a (Q.mul (div_t a b) b)
+  let mod_f a b = Q.sub a (Q.mul (div_f a b) b)
+  let is_zero c = (Q.sign c) = 0
+  let pow q n =
+    if n < 0 then (
+      assert ((Q.sign q <> 0));
+      Q.make (Z.pow q.den (-n)) (Z.pow q.num (-n)))
+    else Q.make (Z.pow q.num n) (Z.pow q.den n)
+
+    include Q (* Module from Zarith *)
+end
+
+module A = struct
+  let ctx = Calcium.CTX.mk ()
+
+    module A = Calcium.CA
+
+    type t = Q of Q.t | A of A.t [@@deriving hash]
+
+    let to_a = function Q q -> A.of_q ~ctx q | A a -> a
+
+    let compare a b =
+      match (a, b) with
+      | Q a, Q b -> Q.compare a b
+      | A a, Q b -> A.compare_q ~ctx a b
+      | Q a, A b -> -A.compare_q ~ctx b a
+      | A a, A b -> A.compare ~ctx a b
+
+    let equal a b =
+      match (a, b) with
+      | Q a, Q b -> Q.equal a b
+      | A a, Q b -> (not (Z.equal b.den Z.one)) && A.compare_q ~ctx a b = 0
+      | Q a, A b -> (not (Z.equal a.den Z.one)) && A.compare_q ~ctx b a = 0
+      | A a, A b -> A.compare ~ctx a b = 0
+
+    let pp fmt = function Q q -> Q.pp fmt q | A a -> Calcium.CA.pp ~ctx fmt a
+
+  let zero = Q Q.zero
+  let one = Q Q.one
+  let half = Q (Q.make Z.one (Z.of_int 2))
+  let minus_one = Q Q.minus_one
+  let two = Q Q.two
+  let sign = function Q q -> Q.sign q | A a -> A.sign ~ctx a
+  let ge a b = compare a b >= 0
+  let gt a b = compare a b > 0
+  let le a b = compare a b <= 0
+  let lt a b = compare a b < 0
+  let min a b = if lt a b then a else b
+  let max a b = if gt a b then a else b
+  let of_string s = Q (Q.of_string s)
+  let to_string = function Q q -> Q.to_string q | A a -> A.to_string ~ctx a
+  let is_integer = function Q q -> Q.is_integer q | A _ -> false
+  (* by normalization *)
+
+  let is_real = function Q q -> Q.is_real q | A _ -> true
+  let to_z = function Q q -> q.Q.num | A _ -> assert false
+  let to_int = function Q q -> Q.to_int q | A _ -> assert false
+
+  let to_q = function Q q -> Some q | A _ -> None
+  let inf = Q Q.inf
+  let minus_inf = Q Q.minus_inf
+
+  let normalize (a : A.t) =
+    match A.to_q ~ctx a with None -> A a | Some q -> Q q
+
+  let ( !! ) = normalize
+
+  let is_unsigned_integer size = function
+    | Q q -> Q.is_unsigned_integer size q
+    | A _ -> false
+
+  let of_q q = Q q
+  let of_z z = Q (Q.of_bigint z)
+  let of_int z = Q (Q.of_int z)
+  let of_bigint = of_z
+  let floor = function Q q -> Q (Q.floor q) | A a -> of_z (A.floor ~ctx a)
+  let ceil = function Q q -> Q (Q.ceil q) | A a -> of_z (A.ceil ~ctx a) 
+
+  let truncate = function
+    | Q q -> Q (Q.truncate q)
+    | A a -> of_z (A.truncate ~ctx a)
+
+  let neg = function Q q -> Q (Q.neg q) | A a -> normalize (A.neg ~ctx a)
+  let inv = function Q q -> Q (Q.inv q) | A a -> normalize (A.inv ~ctx a)
+  let abs = function Q q -> Q (Q.abs q) | A a -> normalize (A.abs ~ctx a)
+
+  let combine2 fq fa cv a b =
+    match (a, b) with
+    | Q a, Q b -> Q (fq a b)
+    | _ ->
+        cv (fa ~ctx (to_a a) (to_a b))
+
+  (* todo special case for one, zero, ... *)
+  let div = combine2 Q.div A.div normalize
+  let add = combine2 Q.add A.add normalize
+  let sub = combine2 Q.sub A.sub normalize
+  let mul = combine2 Q.mul A.mul normalize
+  let ( + ) = add
+  let ( - ) = sub
+  let ( ~- ) = neg
+  let ( ~+ ) x = x
+  let ( * ) = mul
+  let ( / ) = div
+  let div_e = combine2 Q.div_e A.div_e of_z
+  let div_t = combine2 Q.div_t A.div_t of_z
+  let div_f = combine2 Q.div_f A.div_f of_z
+  let mod_e = combine2 Q.mod_e A.mod_e normalize
+  let mod_t = combine2 Q.mod_t A.mod_t normalize
+  let mod_f = combine2 Q.mod_f A.mod_f normalize
+  let is_zero c = match c with Q q -> Q.is_zero q | A _ -> false
+  (* by normalization *)
+  let round x =
+    if lt zero x then ceil (sub x half) else floor (add x half)
+
+  let none_zero c = if is_zero c then None else Some c
+  let is_not_zero c = not ((sign c) = 0)
+
+  let pow q n =
+    match q with Q q -> Q (Q.pow q n) | A a -> !!(A.pow_int ~ctx a n)
+
+  let positive_root q n =
+    if n = 0 then one else !!(A.pow ~ctx (to_a q) (Q.make Z.one (Z.of_int n)))
+
+  let positive_pow q n =
+    !!(A.pow ~ctx (to_a q) n)
+
+  let from_order poly order =
+    let poly = Flint.FMPZ_poly.create poly in
+    let roots = Calcium.QQBAR.from_roots ~unsorted:true poly in
+    if Stdlib.Array.length roots <= order then invalid_arg "Not enough roots";
+    if Stdlib.Array.exists (fun x -> not (Calcium.QQBAR.is_real x)) roots
+    then invalid_arg "Roots must all be reals";
+    let roots = Stdlib.Array.map (Calcium.CA.from_qqbar ~ctx) roots in
+    let cmp r1 r2 = Calcium.CA.compare ~ctx r1 r2 in
+    Stdlib.Array.sort cmp roots;
+    !!( (Stdlib.Array.get roots order))
+
+  let from_enclosure poly min max =
+    let poly = Flint.FMPZ_poly.create poly in
+    let roots = Calcium.QQBAR.from_roots ~unsorted:true poly in
+    let roots = Stdlib.Array.map (Calcium.CA.from_qqbar ~ctx) roots in
+    let inside r = Calcium.CA.compare_q ~ctx r min >= 0 &&
+        Calcium.CA.compare_q ~ctx r max <= 0
+    in
+    let roots = List.filter inside (Stdlib.Array.to_list roots) in
+    match roots with
+    | [] -> invalid_arg "No roots found in the enclosure"
+    | [r] -> !!r
+    | _ -> invalid_arg "The roots are not uniq in the enclosure"
+  end
+
+
+
+type t = A.t
+
+let compare = A.compare
 let print fmt r =
-  Format.fprintf fmt "%a" Q.pp_print r
+  Format.fprintf fmt "%a" A.pp r
 
 let ops = Value.ops ~compare ~print ()
 
 (* Value helpers *)
 (* ************************************************************************* *)
-
+(*
 let ceil x = Q.of_bigint @@ Int.ceil x
 let floor x = Q.of_bigint @@ Int.floor x
 let truncate x = Q.of_bigint @@ Int.truncate x
@@ -40,7 +218,7 @@ let div_f a b = floor (Q.div a b)
 let mod_e a b = Q.sub a (Q.mul (div_e a b) b)
 let mod_t a b = Q.sub a (Q.mul (div_t a b) b)
 let mod_f a b = Q.sub a (Q.mul (div_f a b) b)
-
+*)
 
 (* Builtins *)
 (* ************************************************************************* *)
@@ -67,35 +245,45 @@ let op2_zero ~eval ~env ~cst f =
   Some (Fun.mk_clos @@ Fun.fun_2 ~cst (fun x y ->
       let v_x = Value.extract_exn ~ops x in
       let v_y = Value.extract_exn ~ops y in
-      if Q.equal Q.zero v_y then
+      if A.equal A.zero v_y then
         Fun.corner_case ~eval env cst [] [x; y]
       else mk @@ f v_x v_y
     ))
 
 let builtins ~eval env (cst : Dolmen.Std.Expr.Term.Const.t) =
   match cst.builtin with
-  | B.Decimal i -> Some (mk (Q.of_string i))
-  | B.Lt `Real -> cmp ~cst Q.lt
-  | B.Gt `Real -> cmp ~cst Q.gt
-  | B.Geq `Real -> cmp ~cst Q.geq
-  | B.Leq `Real -> cmp ~cst Q.leq
-  | B.Minus `Real -> op1 ~cst (fun x -> Q.neg x)
-  | B.Add `Real -> op2 ~cst Q.add
-  | B.Sub `Real -> op2 ~cst Q.sub
-  | B.Mul `Real -> op2 ~cst Q.mul
-  | B.Div `Real -> op2_zero Q.div ~cst ~env ~eval
-  | B.Div_e `Real -> op2 ~cst div_e
-  | B.Div_t `Real -> op2 ~cst div_t
-  | B.Div_f `Real -> op2 ~cst div_f
-  | B.Modulo_e `Real -> op2 ~cst mod_e
-  | B.Modulo_t `Real -> op2 ~cst mod_t
-  | B.Modulo_f `Real -> op2 ~cst mod_f
+  | B.Decimal i -> Some (mk (A.of_string i))
+  | B.Algebraic (Ordered_root {coeffs; order}) ->
+    let coeffs = Stdlib.Array.of_list (List.map Z.of_string coeffs) in
+    let order = int_of_string order in
+    Some (mk (A.from_order coeffs order))
+  | B.Algebraic (Enclosed_root {coeffs; min; max}) ->
+      let coeffs = Stdlib.Array.of_list (List.map Z.of_string coeffs) in
+      let q_of_pair (num,den) = Q.div (Q.of_string num) (Q.of_string den) in
+      let min = q_of_pair min in
+      let max = q_of_pair max in
+      Some (mk (A.from_enclosure coeffs min max))
+    | B.Lt `Real -> cmp ~cst A.lt
+  | B.Gt `Real -> cmp ~cst A.gt
+  | B.Geq `Real -> cmp ~cst A.ge
+  | B.Leq `Real -> cmp ~cst A.le
+  | B.Minus `Real -> op1 ~cst (fun x -> A.neg x)
+  | B.Add `Real -> op2 ~cst A.add
+  | B.Sub `Real -> op2 ~cst A.sub
+  | B.Mul `Real -> op2 ~cst A.mul
+  | B.Div `Real -> op2_zero A.div ~cst ~env ~eval
+  | B.Div_e `Real -> op2 ~cst A.div_e
+  | B.Div_t `Real -> op2 ~cst A.div_t
+  | B.Div_f `Real -> op2 ~cst A.div_f
+  | B.Modulo_e `Real -> op2 ~cst A.mod_e
+  | B.Modulo_t `Real -> op2 ~cst A.mod_t
+  | B.Modulo_f `Real -> op2 ~cst A.mod_f
   | B.Is_rat `Real -> Some (Bool.mk true)
-  | B.Floor `Real -> op1 ~cst floor
-  | B.Ceiling `Real -> op1 ~cst ceil
-  | B.Truncate `Real -> op1 ~cst truncate
-  | B.Round `Real -> op1 ~cst round
+  | B.Floor `Real -> op1 ~cst A.floor
+  | B.Ceiling `Real -> op1 ~cst A.ceil
+  | B.Truncate `Real -> op1 ~cst A.truncate
+  | B.Round `Real -> op1 ~cst A.round
   | B.Is_int `Real ->
-    Some (fun1 ~cst (fun x -> Bool.mk (Z.equal Z.one x.Q.den)))
+    Some (fun1 ~cst (fun x -> Bool.mk (A.is_integer x)))
   | _ -> None
 
diff --git a/src/model/real.mli b/src/model/real.mli
index 01b8e2200..b8df44153 100644
--- a/src/model/real.mli
+++ b/src/model/real.mli
@@ -1,13 +1,74 @@
 
 (* This file is free software, part of dolmen. See file "LICENSE" for more information *)
 
+module A : sig
+   (** Algebraic numbers *)
+  type t
+
+  val compare : t -> t -> int
+  val equal : t -> t -> bool
+  val pp : Format.formatter -> t -> unit
+  val zero : t
+  val one : t
+  val half : t
+  val minus_one : t
+  val two : t
+  val sign : t -> int
+  val ge : t -> t -> bool
+  val gt : t -> t -> bool
+  val le : t -> t -> bool
+  val lt : t -> t -> bool
+  val min : t -> t -> t
+  val max : t -> t -> t
+  val of_string : string -> t
+  val to_string : t -> string
+  val is_integer : t -> bool
+  val is_real : t -> bool
+  val to_z : t -> Z.t
+  val to_int : t -> int
+  val to_q : t -> Q.t option
+  val inf : t
+  val minus_inf : t
+  val is_unsigned_integer : int -> t -> bool
+  val of_q : Q.t -> t
+  val of_z : Z.t -> t
+  val of_int : int -> t
+  val of_bigint : Z.t -> t
+  val floor : t -> t
+  val ceil : t -> t
+  val truncate : t -> t
+  val neg : t -> t
+  val inv : t -> t
+  val abs : t -> t
+  val div : t -> t -> t
+  val add : t -> t -> t
+  val sub : t -> t -> t
+  val mul : t -> t -> t
+  val ( + ) : t -> t -> t
+  val ( - ) : t -> t -> t
+  val ( ~- ) : t -> t
+  val ( ~+ ) : 'a -> 'a
+  val ( * ) : t -> t -> t
+  val ( / ) : t -> t -> t
+  val div_e : t -> t -> t
+  val div_t : t -> t -> t
+  val div_f : t -> t -> t
+  val mod_e : t -> t -> t
+  val mod_t : t -> t -> t
+  val mod_f : t -> t -> t
+  val is_zero : t -> bool
+  val round : t -> t
+  val none_zero : t -> t option
+  val is_not_zero : t -> bool
+  val pow : t -> int -> t
+  val positive_root : t -> int -> t
+  val positive_pow : t -> Q.t -> t
+end
+
 (** {2 Value definition} *)
 (** ************************************************************************ *)
 
-type t = Q.t
-(* Reals as rationals. Currently works because we have limited operations
-   on reals, but we might need to upgrade to a more complete represetnation
-   at one point. *)
+type t = A.t
 
 val ops : t Value.ops
 (** ops for real values. *)
@@ -15,7 +76,7 @@ val ops : t Value.ops
 val mk : t -> Value.t
 (** real value creation. *)
 
-val get : Value.t -> Q.t
+val get : Value.t -> t
 (** Get a rational value. *)
 
 
diff --git a/src/standard/builtin.ml b/src/standard/builtin.ml
index a509a8221..ad3b4045b 100644
--- a/src/standard/builtin.ml
+++ b/src/standard/builtin.ml
@@ -63,10 +63,15 @@ type _ t +=
 type rat_real = [ `Rat | `Real ]
 type int_rat_real = [ `Int | `Rat | `Real ]
 
+type algebraic =
+| Ordered_root of { coeffs : string list; order : string; }
+| Enclosed_root of { coeffs : string list; min : string * string; max: string * string; }
+
 type _ t +=
   | Int | Integer of string
   | Rat | Rational of string
   | Real | Decimal of string
+  | Algebraic of algebraic (* instead of algebraic_ordered_root *)
   | Lt of int_rat_real | Leq of int_rat_real
   | Gt of int_rat_real | Geq of int_rat_real
   | Minus of int_rat_real
diff --git a/src/standard/builtin.mli b/src/standard/builtin.mli
index 1c8c6fae7..6108749c4 100644
--- a/src/standard/builtin.mli
+++ b/src/standard/builtin.mli
@@ -166,6 +166,10 @@ type _ t +=
 (** {2 Arithmetic Builtins} *)
 (*  ************************************************************************* *)
 
+type algebraic =
+| Ordered_root of { coeffs : string list; order : string; }
+| Enclosed_root of { coeffs : string list; min : string * string; max: string * string; }
+
 type _ t +=
   | Int
   (** [Int: ttype] the type for signed integers of arbitrary precision. *)
@@ -194,6 +198,7 @@ type _ t +=
       representation for the real number [2].
 
       Real literals can be parsed using ZArith's [Q.of_string]. *)
+  | Algebraic of algebraic
   | Lt of [ `Int | `Rat | `Real ]
   (** [Lt: {a=(Int|Rational|Real)} a -> a -> Prop]:
       strict comparison (less than) on numbers
diff --git a/src/standard/expr.ml b/src/standard/expr.ml
index fe1a6ec7f..69ecdca8b 100644
--- a/src/standard/expr.ml
+++ b/src/standard/expr.ml
@@ -2111,6 +2111,52 @@ module Term = struct
             mk' ~builtin:(Builtin.Decimal s) s [] [] Ty.real
           )
 
+      let algebraic_ordered_root =
+        let cache = Hashtbl.create 113 in
+        fun coeffs order ->
+            with_cache ~cache (fun (coeffs,order) ->
+              let algebraic = "algebraic" in
+              let len = List.fold_left (fun acc x -> 1 + acc + String.length x) 0 coeffs
+              + String.length order
+              + String.length algebraic
+              + 3
+            in
+              let b = Buffer.create len in
+              Buffer.add_string b algebraic;
+              Buffer.add_char b '(';
+              List.iter (fun x -> Buffer.add_string b x; Buffer.add_char b ';') coeffs;
+              Buffer.add_char b '|';
+              Buffer.add_string b order;
+              Buffer.add_char b ')';
+              let s = Buffer.contents b in
+                mk' ~builtin:(Builtin.Algebraic (Ordered_root {coeffs;order})) s [] [] Ty.real
+              ) (coeffs,order)
+
+              let algebraic_enclosed_root =
+                let cache = Hashtbl.create 113 in
+                fun coeffs min max ->
+                    with_cache ~cache (fun (coeffs,((min_num,min_den)as min),((max_num,max_den) as max)) ->
+                      let algebraic = "algebraic" in
+                      let len = List.fold_left (fun acc x -> 1 + acc + String.length x) 0 coeffs
+                      + String.length min_num + String.length min_den
+                      + String.length max_num + String.length max_den
+                      + String.length algebraic
+                      + 6
+                    in
+                      let b = Buffer.create len in
+                      Buffer.add_string b algebraic;
+                      Buffer.add_char b '(';
+                      List.iter (fun x -> Buffer.add_string b x; Buffer.add_char b ';') coeffs;
+                      Buffer.add_char b '|';
+                      Buffer.add_string b min_num; Buffer.add_char b '/'; Buffer.add_string b min_den;
+                      Buffer.add_char b ',';
+                      Buffer.add_string b max_num; Buffer.add_char b '/'; Buffer.add_string b max_den;
+                      Buffer.add_char b ')';
+                      let s = Buffer.contents b in
+                        mk' ~builtin:(Builtin.Algebraic (Enclosed_root {coeffs;min;max})) s [] [] Ty.real
+                        ) (coeffs,min,max)
+        
+
       let minus = mk'
           ~pos:Pretty.Prefix ~name:"-" ~builtin:(Builtin.Minus `Real)
            "Minus" [] [Ty.real] Ty.real
@@ -3291,6 +3337,10 @@ module Term = struct
 
   module Real = struct
     let mk = real
+    let algebraic_ordered_root coeffs order =
+      apply_cst (Const.Real.algebraic_ordered_root coeffs order) [] []
+    let algebraic_enclosed_root coeffs min max =
+      apply_cst (Const.Real.algebraic_enclosed_root coeffs min max) [] []
     let div' = Const.Real.div
     let minus t = apply_cst Const.Real.minus [] [t]
     let add a b = apply_cst Const.Real.add [] [a; b]
diff --git a/src/standard/expr.mli b/src/standard/expr.mli
index d7b5e1c47..f8ad85cb1 100644
--- a/src/standard/expr.mli
+++ b/src/standard/expr.mli
@@ -1069,6 +1069,16 @@ module Term : sig
       val real : string -> t
       (** Real literals. *)
 
+      val algebraic_ordered_root : string list -> string -> t
+      (** Algebraic number defined with a polynomial (coefficient of smallest
+              degree first), and the ordered of the root when ordered from
+              smallest to biggest *)
+
+      val algebraic_enclosed_root : string list ->
+         string * string -> string * string -> t
+      (** Algebraic number defined with a polynomial (coefficient of smallest
+            degree first), and an interval where the polynomial as uniq root *)
+
       val minus : t
       (** Real unary minus/negation. *)
 
diff --git a/src/typecheck/arith.ml b/src/typecheck/arith.ml
index b3c50ce51..453e908db 100644
--- a/src/typecheck/arith.ml
+++ b/src/typecheck/arith.ml
@@ -894,7 +894,56 @@ module Smtlib2 = struct
         | Warn msg -> Type._warn env (Ast ast) (Restriction (config, msg))
         | Error msg -> Type._error env (Ast ast) (Forbidden (config, msg))
 
-      let rec parse ~config version env s =
+      let parse_int env ast =
+        let rec is_int i s =
+          String.length s <= i ||
+          begin
+            match s.[i] with
+            | '-' -> i = 0
+            | '0' | '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9' -> true
+            | _ -> false
+          end
+          || is_int (i+1) s
+        in
+      match ast.Term.term with
+        | Symbol  { Id.ns = Value (Integer); name = Simple name; } ->
+          name
+        | App({term = Symbol { Id.ns = Term; name = Simple "-"; };_},
+              [{term=Symbol  { Id.ns = Value (Integer); name = Simple name; };_}]) ->
+            "-"^name
+        | Symbol  { Id.ns = Term; name = Simple name; } when is_int 0 name ->
+          name
+        | _ ->
+          Type._error env (Ast ast) (Forbidden "An integer constant is expected")
+
+      let parse_rat env ast =
+        match ast.Term.term with
+        | Symbol  { Id.ns = Value (Integer | Rational | Real); name = Simple name; } ->
+            (name,"1.0")
+        | App({term = Symbol { Id.ns = Term; name = Simple "-"; };_},
+              [{term=Symbol  { Id.ns = Value (Integer | Rational | Real ); name = Simple name; };_}]) ->
+              "-"^name,"1.0"
+        | App({term = Symbol { Id.ns = Term; name = Simple "/"; };_},
+              [{term=Symbol  { Id.ns = Value (Integer | Rational | Real ); name = Simple name1; };_};
+                {term=Symbol  { Id.ns = Value (Integer | Rational | Real ); name = Simple name2; };_}]) ->
+                (name1,name2)
+        | App({term = Symbol { Id.ns = Term; name = Simple "/"; };_},
+                [{term=App({term = Symbol { Id.ns = Term; name = Simple "-"; };_},
+                  [{term=Symbol  { Id.ns = Value (Integer | Rational | Real ); name = Simple name1};_}]);_};
+                {term=Symbol  { Id.ns = Value (Integer | Rational | Real ); name = Simple name2; };_}]) ->
+                ("-"^name1,name2)
+          | _ ->
+            Type._error env (Ast ast) (Forbidden "A rational model is expected")
+    
+      let parse_coeffs env ast =
+        match ast.Term.term with
+        | App ({term = Symbol { Id.ns = Term; name = Simple "coeffs"; };_},args) ->
+          List.map (parse_int env) args
+        | _ ->
+          Type._error env (Ast ast)
+           (Forbidden "A list of coefficient starting with \"coeffs\" is expected")
+
+           let rec parse ~config version env s =
         match s with
         (* type *)
         | Type.Id { Id.ns = Sort; name = Simple "Real"; } ->
@@ -902,6 +951,23 @@ module Smtlib2 = struct
         (* values *)
         | Type.Id { Id.ns = Value (Integer | Real); name = Simple name; } ->
           Type.builtin_term (Base.app0 (module Type) env s (T.mk name))
+        | Type.Id { Id.ns = Term; name = Simple ("root-of-with-order"|"root-of-with-ordering"); } ->
+          Type.builtin_term (Base.make_op2 (module Type) env s (fun _ast (coeffs,num) ->
+            let coeffs = parse_coeffs env coeffs in
+            let num = match num.term with
+              | Symbol  { Id.ns = Value (Integer); name = Simple name; } ->
+                  name
+              | _ -> Type._error env (Ast num) (Forbidden "A positive integer is expected")
+            in
+            T.algebraic_ordered_root coeffs num )
+          )
+          | Type.Id { Id.ns = Term; name = Simple ("root-of-with-enclosure"|"root-of-with-interval"); } ->
+            Type.builtin_term (Base.make_op3 (module Type) env s (fun _ast (coeffs,min,max) ->
+              let coeffs = parse_coeffs env coeffs in
+              let min = parse_rat env min in
+              let max = parse_rat env max in
+              T.algebraic_enclosed_root coeffs min max )
+            )
         (* terms *)
         | Type.Id { Id.ns = Term; name = Simple name; } ->
           begin match name with
diff --git a/tests/model/real/algebraic.expected b/tests/model/real/algebraic.expected
new file mode 100644
index 000000000..e69de29bb
diff --git a/tests/model/real/algebraic.rsmt2 b/tests/model/real/algebraic.rsmt2
new file mode 100644
index 000000000..ed90f753b
--- /dev/null
+++ b/tests/model/real/algebraic.rsmt2
@@ -0,0 +1,7 @@
+sat
+(
+(define-fun sqrt2 () Real (root-of-with-order (coeffs (- 2) 0 1) 1))
+; accept extensions for simplicity for SMTCOMP 2023
+(define-fun sqrt3 () Real (root-of-with-enclosure (coeffs -3 0 1) 1.0 2.0))
+(define-fun sqrt4 () Real (root-of-with-interval (coeffs (- 4) 0 1) (/ (- 1.0) 2.0) (/ 5.0 2.0)))
+)
\ No newline at end of file
diff --git a/tests/model/real/algebraic.smt2 b/tests/model/real/algebraic.smt2
new file mode 100644
index 000000000..b55adb4be
--- /dev/null
+++ b/tests/model/real/algebraic.smt2
@@ -0,0 +1,8 @@
+(set-logic NRA)
+(declare-fun sqrt2 () Real)
+(declare-fun sqrt3 () Real)
+(declare-fun sqrt4 () Real)
+(assert (= (* sqrt2 sqrt2) 2.0))
+(assert (= (* sqrt3 sqrt3) 3.0))
+(assert (= sqrt4 2.0))
+(check-sat)
\ No newline at end of file
diff --git a/tests/model/real/dune b/tests/model/real/dune
index 5d228e79e..de58a10eb 100644
--- a/tests/model/real/dune
+++ b/tests/model/real/dune
@@ -33,6 +33,38 @@
   (action (diff add.expected add.full)))
 
 
+; Test for algebraic.smt2
+; Incremental test
+
+(rule
+   (target  algebraic.incremental)
+   (deps    (:response algebraic.rsmt2) (:input algebraic.smt2))
+   (package dolmen_bin)
+   (action (chdir %{workspace_root}
+            (with-outputs-to %{target}
+             (with-accepted-exit-codes (or 0 (not 0))
+              (run dolmen --check-model=true -r %{response} --mode=incremental --color=never %{input} %{read-lines:flags.dune}))))))
+(rule
+  (alias runtest)
+  (package dolmen_bin)
+  (action (diff algebraic.expected algebraic.incremental)))
+
+; Full mode test
+
+(rule
+   (target  algebraic.full)
+   (deps    (:response algebraic.rsmt2) (:input algebraic.smt2))
+   (package dolmen_bin)
+   (action (chdir %{workspace_root}
+            (with-outputs-to %{target}
+             (with-accepted-exit-codes (or 0 (not 0))
+              (run dolmen --check-model=true -r %{response} --mode=full --color=never %{input} %{read-lines:flags.dune}))))))
+(rule
+  (alias runtest)
+  (package dolmen_bin)
+  (action (diff algebraic.expected algebraic.full)))
+
+
 ; Test for div.smt2
 ; Incremental test
 
@@ -97,4 +129,38 @@
   (action (diff div_zero_1.expected div_zero_1.full)))
 
 
+; Test for kissing_2_6_scramble.smt2
+; Incremental test
+
+(rule
+   (target  kissing_2_6_scramble.incremental)
+   (deps    (:response kissing_2_6_scramble.rsmt2)
+            (:input kissing_2_6_scramble.smt2))
+   (package dolmen_bin)
+   (action (chdir %{workspace_root}
+            (with-outputs-to %{target}
+             (with-accepted-exit-codes (or 0 (not 0))
+              (run dolmen --check-model=true -r %{response} --mode=incremental --color=never %{input} %{read-lines:flags.dune}))))))
+(rule
+  (alias runtest)
+  (package dolmen_bin)
+  (action (diff kissing_2_6_scramble.expected kissing_2_6_scramble.incremental)))
+
+; Full mode test
+
+(rule
+   (target  kissing_2_6_scramble.full)
+   (deps    (:response kissing_2_6_scramble.rsmt2)
+            (:input kissing_2_6_scramble.smt2))
+   (package dolmen_bin)
+   (action (chdir %{workspace_root}
+            (with-outputs-to %{target}
+             (with-accepted-exit-codes (or 0 (not 0))
+              (run dolmen --check-model=true -r %{response} --mode=full --color=never %{input} %{read-lines:flags.dune}))))))
+(rule
+  (alias runtest)
+  (package dolmen_bin)
+  (action (diff kissing_2_6_scramble.expected kissing_2_6_scramble.full)))
+
+
 ; Auto-generated part end
diff --git a/tests/model/real/kissing_2_6_scramble.expected b/tests/model/real/kissing_2_6_scramble.expected
new file mode 100644
index 000000000..e69de29bb
diff --git a/tests/model/real/kissing_2_6_scramble.rsmt2 b/tests/model/real/kissing_2_6_scramble.rsmt2
new file mode 100644
index 000000000..198267acd
--- /dev/null
+++ b/tests/model/real/kissing_2_6_scramble.rsmt2
@@ -0,0 +1,27 @@
+sat
+(
+  (define-fun x3 () Real
+    (root-of-with-ordering (coeffs (- 3) 0 4) 0))
+  (define-fun x9 () Real
+    (/ 1.0 2.0))
+  (define-fun x4 () Real
+    (root-of-with-ordering (coeffs (- 3) 0 4) 0))
+  (define-fun x6 () Real
+    (root-of-with-ordering (coeffs (- 3) 0 4) 1))
+  (define-fun x5 () Real
+    1.0)
+  (define-fun x8 () Real
+    (- (/ 1.0 2.0)))
+  (define-fun x2 () Real
+    (/ 1.0 2.0))
+  (define-fun x1 () Real
+    (- (/ 1.0 2.0)))
+  (define-fun x10 () Real
+    (- 1.0))
+  (define-fun x11 () Real
+    (root-of-with-ordering (coeffs (- 3) 0 4) 1))
+  (define-fun x12 () Real
+    0.0)
+  (define-fun x7 () Real
+    0.0)
+)
\ No newline at end of file
diff --git a/tests/model/real/kissing_2_6_scramble.smt2 b/tests/model/real/kissing_2_6_scramble.smt2
new file mode 100644
index 000000000..7e3db8bd2
--- /dev/null
+++ b/tests/model/real/kissing_2_6_scramble.smt2
@@ -0,0 +1,39 @@
+(set-option :print-success false)
+(set-option :produce-models true)
+(set-logic QF_NRA)
+(declare-fun x6 () Real)
+(declare-fun x5 () Real)
+(declare-fun x10 () Real)
+(declare-fun x11 () Real)
+(declare-fun x7 () Real)
+(declare-fun x1 () Real)
+(declare-fun x12 () Real)
+(declare-fun x2 () Real)
+(declare-fun x4 () Real)
+(declare-fun x8 () Real)
+(declare-fun x3 () Real)
+(declare-fun x9 () Real)
+(assert (= (+ (* x1 x1) (* x11 x11)) 1))
+(assert (>= (+ (* (- x10 x8) (- x10 x8)) (* (- x12 x4) (- x12 x4))) 1))
+(assert (= (+ (* x2 x2) (* x6 x6)) 1))
+(assert (>= (+ (* (- x1 x5) (- x1 x5)) (* (- x11 x7) (- x11 x7))) 1))
+(assert (<= 1 (+ (* (- x2 x5) (- x2 x5)) (* (- x6 x7) (- x6 x7)))))
+(assert (>= (+ (* (- x12 x11) (- x12 x11)) (* (- x10 x1) (- x10 x1))) 1))
+(assert (>= (+ (* (- x8 x5) (- x8 x5)) (* (- x4 x7) (- x4 x7))) 1))
+(assert (= (+ (* x4 x4) (* x8 x8)) 1))
+(assert (<= 1 (+ (* (- x2 x1) (- x2 x1)) (* (- x6 x11) (- x6 x11)))))
+(assert (>= (+ (* (- x10 x2) (- x10 x2)) (* (- x12 x6) (- x12 x6))) 1))
+(assert (= 1 (+ (* x12 x12) (* x10 x10))))
+(assert (<= 1 (+ (* (- x9 x8) (- x9 x8)) (* (- x3 x4) (- x3 x4)))))
+(assert (<= 1 (+ (* (- x10 x5) (- x10 x5)) (* (- x12 x7) (- x12 x7)))))
+(assert (>= (+ (* (- x9 x1) (- x9 x1)) (* (- x3 x11) (- x3 x11))) 1))
+(assert (= (+ (* x9 x9) (* x3 x3)) 1))
+(assert (>= (+ (* (- x9 x5) (- x9 x5)) (* (- x3 x7) (- x3 x7))) 1))
+(assert (<= 1 (+ (* (- x9 x2) (- x9 x2)) (* (- x3 x6) (- x3 x6)))))
+(assert (= (+ (* x7 x7) (* x5 x5)) 1))
+(assert (>= (+ (* (- x8 x1) (- x8 x1)) (* (- x4 x11) (- x4 x11))) 1))
+(assert (>= (+ (* (- x3 x12) (- x3 x12)) (* (- x9 x10) (- x9 x10))) 1))
+(assert (>= (+ (* (- x2 x8) (- x2 x8)) (* (- x6 x4) (- x6 x4))) 1))
+(check-sat)
+(get-model)
+(exit)

From fc0d820f89a248859dfa2dd7ce9c3fa0099dc38a Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Fri, 23 Jun 2023 15:00:16 +0200
Subject: [PATCH 2/9] Try and fix windows CI (again)

---
 .github/workflows/install.yml | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/.github/workflows/install.yml b/.github/workflows/install.yml
index 11d719d24..075c53106 100644
--- a/.github/workflows/install.yml
+++ b/.github/workflows/install.yml
@@ -104,6 +104,15 @@ jobs:
     - name: Debugging
       run: opam switch list-available
       if: always ()
+    # If on windows: add the official repo as a second repo.
+    # THis is ebcause the current setup-ocaml will set the
+    # opam-repository-mingw as the repo, and it has not been
+    # updated since august 2021. Still, since it contains fixes
+    # specific to windows for some packages, it's useful to have,
+    # but we also need the official repo for recent packages
+    - name: Add official repo (windows only)
+      run: opam repo add upstream https://opam.ocaml.org --rank 2 --all-switches --set-default
+      if: matrix.os == 'windows-latest'
     # Run opam udpate to get an up-to-date repo
     - name: Update opam repo
       run: opam update

From 5d29df691b71a8bcff7db0368d26b01d6631be83 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Fri, 23 Jun 2023 17:10:48 +0200
Subject: [PATCH 3/9] Try and fix ci again...

---
 .github/workflows/install.yml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/install.yml b/.github/workflows/install.yml
index 075c53106..0bc1debab 100644
--- a/.github/workflows/install.yml
+++ b/.github/workflows/install.yml
@@ -99,13 +99,18 @@ jobs:
     - name: Setup ocaml/opam
       uses: avsm/setup-ocaml@v2
       with:
+        # disabling the automatic opam pin because this forces the
+        # installation of dependencies, and in some cases (e.g. windows,
+        # see later actions) we need to do some other things (such as
+        # adding repos) before installing dependencies.
+        opam-pin: false
         ocaml-compiler: ${{ matrix.ocaml-version }}
     # Debug
     - name: Debugging
       run: opam switch list-available
       if: always ()
     # If on windows: add the official repo as a second repo.
-    # THis is ebcause the current setup-ocaml will set the
+    # This is ebcause the current setup-ocaml will set the
     # opam-repository-mingw as the repo, and it has not been
     # updated since august 2021. Still, since it contains fixes
     # specific to windows for some packages, it's useful to have,

From 430126f3eea1473e9472c3274153d9b0753d9827 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Mon, 26 Jun 2023 11:50:29 +0200
Subject: [PATCH 4/9] Try and fix CI again

---
 .github/workflows/install.yml | 29 ++++++++++++++---------------
 1 file changed, 14 insertions(+), 15 deletions(-)

diff --git a/.github/workflows/install.yml b/.github/workflows/install.yml
index 0bc1debab..b1554c265 100644
--- a/.github/workflows/install.yml
+++ b/.github/workflows/install.yml
@@ -98,26 +98,25 @@ jobs:
     # Setup ocaml/opam
     - name: Setup ocaml/opam
       uses: avsm/setup-ocaml@v2
+      if: matrix.os != 'windows-latest'
       with:
-        # disabling the automatic opam pin because this forces the
-        # installation of dependencies, and in some cases (e.g. windows,
-        # see later actions) we need to do some other things (such as
-        # adding repos) before installing dependencies.
-        opam-pin: false
         ocaml-compiler: ${{ matrix.ocaml-version }}
+    # Setup ocaml/opam
+    - name: Setup ocaml/opam
+      uses: avsm/setup-ocaml@v2
+      if: matrix.os == 'windows-latest'
+      with:
+        ocaml-compiler: ${{ matrix.ocaml-version }}
+        # If on windows: use both the mingw repo **and** the official repo.
+        # This is because the mingw repo contians fixes windows-specific, but
+        # it has not been updated since august 2021.
+        opam-repositories: |
+          mingw: https://github.com/ocaml-opam/opam-repository-mingw.git
+          default: https://github.com/ocaml/opam-repository.git
     # Debug
     - name: Debugging
       run: opam switch list-available
       if: always ()
-    # If on windows: add the official repo as a second repo.
-    # This is ebcause the current setup-ocaml will set the
-    # opam-repository-mingw as the repo, and it has not been
-    # updated since august 2021. Still, since it contains fixes
-    # specific to windows for some packages, it's useful to have,
-    # but we also need the official repo for recent packages
-    - name: Add official repo (windows only)
-      run: opam repo add upstream https://opam.ocaml.org --rank 2 --all-switches --set-default
-      if: matrix.os == 'windows-latest'
     # Run opam udpate to get an up-to-date repo
     - name: Update opam repo
       run: opam update
@@ -136,7 +135,7 @@ jobs:
     # Install each package
     - name: Install dolmen
       run: opam install . --with-test --with-doc
-      timeout-minutes: 20
       # Ensure that installation does not take too long
       # (particularly with regards to flambda)
+      timeout-minutes: 20
 

From d3c7e48f5961f7a5219543dbc90d29fd0aea97b5 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Tue, 27 Jun 2023 17:31:41 +0200
Subject: [PATCH 5/9] Cleanup + some more tests

---
 src/interface/term.ml                      |  10 +-
 src/model/fp.ml                            |   6 +-
 src/model/fp.mli                           |   9 +-
 src/model/loop.ml                          |  72 +++++-
 src/model/real.ml                          | 282 ++++++++++++++-------
 src/model/real.mli                         |  82 ++++--
 src/standard/builtin.ml                    |   2 +-
 src/standard/builtin.mli                   |  23 +-
 src/standard/expr.ml                       |  81 +++---
 src/standard/expr.mli                      |  15 +-
 src/typecheck/arith.ml                     | 115 +++++++--
 tests/model/real/bad_ordered_root.expected |   6 +
 tests/model/real/bad_ordered_root.rsmt2    |   4 +
 tests/model/real/bad_ordered_root.smt2     |   5 +
 tests/model/real/complex_roots.expected    |   5 +
 tests/model/real/complex_roots.rsmt2       |   4 +
 tests/model/real/complex_roots.smt2        |   5 +
 tests/model/real/dune                      |  64 +++++
 18 files changed, 587 insertions(+), 203 deletions(-)
 create mode 100644 tests/model/real/bad_ordered_root.expected
 create mode 100644 tests/model/real/bad_ordered_root.rsmt2
 create mode 100644 tests/model/real/bad_ordered_root.smt2
 create mode 100644 tests/model/real/complex_roots.expected
 create mode 100644 tests/model/real/complex_roots.rsmt2
 create mode 100644 tests/model/real/complex_roots.smt2

diff --git a/src/interface/term.ml b/src/interface/term.ml
index 881cb4027..a5cca3d06 100644
--- a/src/interface/term.ml
+++ b/src/interface/term.ml
@@ -1310,7 +1310,15 @@ module type Smtlib_Real = sig
   (** Real division. See Smtlib theory for a full description. *)
 
   val algebraic_ordered_root : string list -> string -> t
-  val algebraic_enclosed_root : string list -> (string * string) -> (string * string) -> t
+  (** Algebraic number defined with a polynomial (coefficient of smallest
+      degree first), and the ordered of the root when ordered from
+      smallest to biggest *)
+
+  val algebraic_enclosed_root :
+    string list -> (string * string) -> (string * string) -> t
+  (** Algebraic number defined with a polynomial (coefficient of smallest
+      degree first), and an interval where the polynomial has a unique root.
+      Each bound of the interval is a rational expressed as two integers. *)
 
 end
 
diff --git a/src/model/fp.ml b/src/model/fp.ml
index 107e9eda6..7c8b6f17e 100644
--- a/src/model/fp.ml
+++ b/src/model/fp.ml
@@ -23,6 +23,7 @@ let ops =
 module E = Dolmen.Std.Expr
 module B = Dolmen.Std.Builtin
 
+exception Real_to_fp of { a : Real.A.t; }
 exception Unhandled_exponand_and_mantissa of { ew : int; mw : int; }
 
 let mk f = Value.mk ~ops f
@@ -128,9 +129,10 @@ let builtins ~eval env (cst : Dolmen.Std.Expr.Term.Const.t) =
   | B.Real_to_fp (ew, prec) ->
     Some (Fun.mk_clos @@ Fun.fun_2 ~cst (fun m r ->
         check ~ew ~mw:(prec - 1);
-        match Real.A.to_q  @@ Real.get r with
+        let a = Real.get r in
+        match Real.A.to_q a with
         | Some q -> mk (f_of_q ~ew ~mw:(prec - 1) (mode m) q)
-        | None -> invalid_arg "not implemented: algebraic number to floating point"))
+        | None -> raise (Real_to_fp { a })))
  | B.Fp_to_fp (_ew1, _prec1, ew2, prec2) ->
     Some (Fun.mk_clos @@ Fun.fun_2 ~cst
             (fun m f1 -> mk @@ f_round ~ew:ew2 ~mw:(prec2 - 1) (mode m) (fp f1)))
diff --git a/src/model/fp.mli b/src/model/fp.mli
index b65c61328..27c513e9a 100644
--- a/src/model/fp.mli
+++ b/src/model/fp.mli
@@ -14,8 +14,15 @@ val mk : F.t -> Value.t
 (** {2 Corner cases & builtins} *)
 (** ************************************************************************ *)
 
+exception Real_to_fp of { a : Real.A.t; }
+(** Raised when a converison from real to floating point cannot be completed.
+    Currently this may happen when the real is a non-rational algebraic
+    number.
+    Note: this is an implementation limitation of Dolmen, and should
+    eventually be solved/lifted. *)
+
 exception Unhandled_exponand_and_mantissa of { ew : int; mw : int; }
-(** Raised when the exponand and mantissa siez do not respect the constraints
+(** Raised when the exponand and mantissa size do not respect the constraints
     imposed by `Farith`. *)
 
 val builtins : Env.builtins
diff --git a/src/model/loop.ml b/src/model/loop.ml
index 31ad3e932..4afdc3e2a 100644
--- a/src/model/loop.ml
+++ b/src/model/loop.ml
@@ -67,6 +67,12 @@ module E = Dolmen.Std.Expr
 let pp_wrap pp fmt x =
   Format.fprintf fmt "`%a`" pp x
 
+let pp_order fmt = function
+  | 0 -> Format.fprintf fmt "1st"
+  | 1 -> Format.fprintf fmt "2nd"
+  | 2 -> Format.fprintf fmt "3rd"
+  | n -> Format.fprintf fmt "%dth" (n + 1)
+
 let pp_app fmt (cst, args) =
   match (E.Term.Const.get_tag cst E.Tags.pos) with
   | None | Some Dolmen.Std.Pretty.Prefix ->
@@ -87,6 +93,13 @@ let pp_located fmt { contents = _; file = _; loc; } =
   let loc = Dolmen.Std.Loc.full_loc loc in
   Format.fprintf fmt "%a" Dolmen.Std.Loc.fmt loc
 
+let limitation_hint=
+  (fun _ -> Some (
+       Format.dprintf "%a"
+         Format.pp_print_text
+         "This is a current implementation limitation of dolmen. \
+          Please report upstream if encounter this error, ^^"))
+
 let code =
   Dolmen_loop.Code.create
     ~category:"Model"
@@ -230,12 +243,44 @@ let unhandled_float_exponand_and_mantissa =
           "%a:@ (%d, %d)." Format.pp_print_text
           "The following size for exponand and mantissa are not currently \
            handled by dolmen" ew mw)
-    ~hints:[(fun _ -> Some (Format.dprintf "%a"
-        Format.pp_print_text
-          "This is a current implementation limitation of dolmen. \
-           Please report upstream if encounter this error, ^^")); ]
+    ~hints:[ limitation_hint; ]
     ~name:"Unhandled Floating point sizes" ()
 
+let real_to_fp =
+  Dolmen_loop.Report.Error.mk ~code ~mnemonic:"real-to-fp"
+    ~message:(fun fmt a ->
+        Format.fprintf fmt
+          "%a:@ %a"
+          Format.pp_print_text
+          "Dolmen cannot currently convert the following non-rational \
+           real number to a floating point number"
+          Real.A.pp a)
+    ~hints:[ limitation_hint; ]
+    ~name:"Real to FP" ()
+
+let no_ordered_root =
+  Dolmen_loop.Report.Error.mk ~code ~mnemonic:"no-ordered-root"
+    ~message:(fun fmt (poly, num_roots, order) ->
+        Format.fprintf fmt "%a %d %a %a root:@ %a"
+          Format.pp_print_text "The following polynomial has" num_roots
+          Format.pp_print_text "roots, but the model tried to use its"
+          pp_order order Real.Poly.pp poly)
+    ~hints:[ (fun _ -> Some (
+        Format.dprintf "%a" Format.pp_print_text
+          "Root orders start at 0 for the first (smallest) root"));
+      ]
+    ~name:"No Ordered root" ()
+
+let complex_roots =
+  Dolmen_loop.Report.Error.mk ~code ~mnemonic:"complex-roots"
+    ~message:(fun fmt poly ->
+        Format.fprintf fmt "%a:@ %a"
+          Format.pp_print_text
+          "The following polynomial has complex roots, \
+           which prevents from ordering roots"
+          Real.Poly.pp poly)
+    ~name:"Complex Roots" ()
+
 (* Pipe *)
 (* ************************************************************************ *)
 
@@ -302,13 +347,26 @@ module Make
     try
       Eval.eval env term
     with
-    | Eval.Quantifier -> _err fo_model ()
-    | Eval.Unhandled_builtin b -> _err unhandled_builtin b
-    | Eval.Undefined_variable v -> _err undefined_variable v
+
+    (* Evaluation errors *)
+    | Eval.Quantifier ->
+      _err fo_model ()
+    | Eval.Unhandled_builtin b ->
+      _err unhandled_builtin b
+    | Eval.Undefined_variable v ->
+      _err undefined_variable v
     | Model.Incorrect_extension (cst, args, ret) ->
       _err bad_extension (cst, args, ret)
+    | Fp.Real_to_fp { a } ->
+      _err real_to_fp a
     | Fp.Unhandled_exponand_and_mantissa { ew; mw } ->
       _err unhandled_float_exponand_and_mantissa (ew, mw)
+    | Real.A.Complex_roots { poly; } ->
+      _err complex_roots poly
+    | Real.A.No_ordered_root { poly; num_roots; order; } ->
+      _err no_ordered_root (poly, num_roots, order)
+
+    (* Special cases for delayed evaluation *)
     | Eval.Undefined_constant c as exn ->
       if reraise_for_delayed_eval
       then raise exn
diff --git a/src/model/real.ml b/src/model/real.ml
index e9017e0ea..8fd8f7018 100644
--- a/src/model/real.ml
+++ b/src/model/real.ml
@@ -1,21 +1,18 @@
 
 (* This file is free software, part of dolmen. See file "LICENSE" for more information *)
 
-(* Value definition *)
+(* Rational numbers *)
 (* ************************************************************************* *)
 
-(* Real are currently represented as algebraic numbers *)
-
 (* Extending Q module from Zarith *)
 module Q = struct
-    let pp fmt q =
-        match Q.classify q with
-        | Q.ZERO -> Format.pp_print_char fmt '0'
-        | Q.INF -> Format.pp_print_string fmt "+∞"
-        | Q.MINF -> Format.pp_print_string fmt "-∞"
-        | Q.UNDEF -> Format.pp_print_string fmt "!undef!"
-        | Q.NZERO -> Q.pp_print fmt q
-
+  let pp fmt q =
+    match Q.classify q with
+    | Q.ZERO -> Format.pp_print_char fmt '0'
+    | Q.INF -> Format.pp_print_string fmt "+∞"
+    | Q.MINF -> Format.pp_print_string fmt "-∞"
+    | Q.UNDEF -> Format.pp_print_string fmt "!undef!"
+    | Q.NZERO -> Q.pp_print fmt q
 
   let two = Q.of_int 2
   let is_integer q = Z.equal Z.one q.Q.den
@@ -44,63 +41,126 @@ module Q = struct
       Q.make (Z.pow q.den (-n)) (Z.pow q.num (-n)))
     else Q.make (Z.pow q.num n) (Z.pow q.den n)
 
-    include Q (* Module from Zarith *)
+  include Q (* Module from Zarith *)
 end
 
+(* Polynomials *)
+(* ************************************************************************* *)
+
+module Poly = Flint.FMPZ_poly
+
+
+(* Algebraic numbers *)
+(* ************************************************************************* *)
+
 module A = struct
   let ctx = Calcium.CTX.mk ()
 
-    module A = Calcium.CA
+  module A = Calcium.CA
+
+  (* Types & exceptions *)
+
+  type t =
+    | Q of Q.t
+    | A of A.t
 
-    type t = Q of Q.t | A of A.t [@@deriving hash]
+  exception Complex_roots of {
+      poly : Poly.t;
+    }
 
-    let to_a = function Q q -> A.of_q ~ctx q | A a -> a
+  exception No_ordered_root of {
+      order : int;
+      poly : Poly.t;
+      num_roots : int;
+    }
+
+  exception Bad_root_enclosure of {
+      poly : Poly.t;
+      min : Q.t;
+      max : Q.t;
+      roots : t list;
+    }
+
+  (* Usual functions *)
+  let compare a b =
+    match (a, b) with
+    | Q a, Q b -> Q.compare a b
+    | A a, Q b -> A.compare_q ~ctx a b
+    | Q a, A b -> -A.compare_q ~ctx b a
+    | A a, A b -> A.compare ~ctx a b
 
-    let compare a b =
-      match (a, b) with
-      | Q a, Q b -> Q.compare a b
-      | A a, Q b -> A.compare_q ~ctx a b
-      | Q a, A b -> -A.compare_q ~ctx b a
-      | A a, A b -> A.compare ~ctx a b
+  let equal a b =
+    match (a, b) with
+    | Q a, Q b -> Q.equal a b
+    | A a, Q b -> (not (Z.equal b.den Z.one)) && A.compare_q ~ctx a b = 0
+    | Q a, A b -> (not (Z.equal a.den Z.one)) && A.compare_q ~ctx b a = 0
+    | A a, A b -> A.compare ~ctx a b = 0
 
-    let equal a b =
-      match (a, b) with
-      | Q a, Q b -> Q.equal a b
-      | A a, Q b -> (not (Z.equal b.den Z.one)) && A.compare_q ~ctx a b = 0
-      | Q a, A b -> (not (Z.equal a.den Z.one)) && A.compare_q ~ctx b a = 0
-      | A a, A b -> A.compare ~ctx a b = 0
+  let pp fmt = function
+    | Q q -> Q.pp fmt q
+    | A a -> Calcium.CA.pp ~ctx fmt a
 
-    let pp fmt = function Q q -> Q.pp fmt q | A a -> Calcium.CA.pp ~ctx fmt a
+  (* Constants *)
 
   let zero = Q Q.zero
   let one = Q Q.one
   let half = Q (Q.make Z.one (Z.of_int 2))
   let minus_one = Q Q.minus_one
   let two = Q Q.two
-  let sign = function Q q -> Q.sign q | A a -> A.sign ~ctx a
+  let inf = Q Q.inf
+  let minus_inf = Q Q.minus_inf
+
+  (* Normalization *)
+
+  let normalize (a : A.t) =
+    match A.to_q ~ctx a with
+    | None -> A a
+    | Some q -> Q q
+
+  let ( !! ) = normalize
+
+  (* Inspection *)
+
   let ge a b = compare a b >= 0
   let gt a b = compare a b > 0
   let le a b = compare a b <= 0
   let lt a b = compare a b < 0
+
   let min a b = if lt a b then a else b
   let max a b = if gt a b then a else b
+
+  let sign = function
+    | Q q -> Q.sign q
+    | A a -> A.sign ~ctx a
+
+  (* Conversions
+     Note: values of type [t] are normalised, so that a [A a] is guaranteed
+     to be a non-rational algebraic. *)
+
   let of_string s = Q (Q.of_string s)
-  let to_string = function Q q -> Q.to_string q | A a -> A.to_string ~ctx a
-  let is_integer = function Q q -> Q.is_integer q | A _ -> false
-  (* by normalization *)
+  let to_string = function
+    | Q q -> Q.to_string q
+    | A a -> A.to_string ~ctx a
 
-  let is_real = function Q q -> Q.is_real q | A _ -> true
-  let to_z = function Q q -> q.Q.num | A _ -> assert false
-  let to_int = function Q q -> Q.to_int q | A _ -> assert false
+  let is_integer = function
+    | Q q -> Q.is_integer q
+    | A _ -> false (* because of normalization *)
 
-  let to_q = function Q q -> Some q | A _ -> None
-  let inf = Q Q.inf
-  let minus_inf = Q Q.minus_inf
+  let is_real = function
+    | Q q -> Q.is_real q
+    | A _ -> true (* because of normalization *)
 
-  let normalize (a : A.t) =
-    match A.to_q ~ctx a with None -> A a | Some q -> Q q
+  let to_z = function
+    | Q q -> q.Q.num
+    | A _ -> assert false
 
-  let ( !! ) = normalize
+  let to_int = function
+    | Q q -> Q.to_int q
+    | A _ -> assert false
+
+  let to_q = function
+    | Q q -> Some q
+    | A _ -> None
 
   let is_unsigned_integer size = function
     | Q q -> Q.is_unsigned_integer size q
@@ -110,24 +170,48 @@ module A = struct
   let of_z z = Q (Q.of_bigint z)
   let of_int z = Q (Q.of_int z)
   let of_bigint = of_z
-  let floor = function Q q -> Q (Q.floor q) | A a -> of_z (A.floor ~ctx a)
-  let ceil = function Q q -> Q (Q.ceil q) | A a -> of_z (A.ceil ~ctx a) 
+
+  (* Floor/ceil &co *)
+
+  let floor = function
+    | Q q -> Q (Q.floor q)
+    | A a -> of_z (A.floor ~ctx a)
+
+  let ceil = function
+    | Q q -> Q (Q.ceil q)
+    | A a -> of_z (A.ceil ~ctx a) 
 
   let truncate = function
     | Q q -> Q (Q.truncate q)
     | A a -> of_z (A.truncate ~ctx a)
 
-  let neg = function Q q -> Q (Q.neg q) | A a -> normalize (A.neg ~ctx a)
-  let inv = function Q q -> Q (Q.inv q) | A a -> normalize (A.inv ~ctx a)
-  let abs = function Q q -> Q (Q.abs q) | A a -> normalize (A.abs ~ctx a)
+  (* Arithmetic functions *)
+
+  let neg = function
+    | Q q -> Q (Q.neg q)
+    | A a -> normalize (A.neg ~ctx a)
+
+  let inv = function
+    | Q q -> Q (Q.inv q)
+    | A a -> normalize (A.inv ~ctx a)
+
+  let abs = function
+    | Q q -> Q (Q.abs q)
+    | A a -> normalize (A.abs ~ctx a)
+
+  (* Helpers *)
+
+  let to_a = function
+    | Q q -> A.of_q ~ctx q
+    | A a -> a
 
   let combine2 fq fa cv a b =
     match (a, b) with
     | Q a, Q b -> Q (fq a b)
-    | _ ->
-        cv (fa ~ctx (to_a a) (to_a b))
+    | _ -> cv (fa ~ctx (to_a a) (to_a b))
 
-  (* todo special case for one, zero, ... *)
+  (* TODO: consider special casing some of these for performance
+          (e.g. division by one, zero, ...) *)
   let div = combine2 Q.div A.div normalize
   let add = combine2 Q.add A.add normalize
   let sub = combine2 Q.sub A.sub normalize
@@ -144,16 +228,22 @@ module A = struct
   let mod_e = combine2 Q.mod_e A.mod_e normalize
   let mod_t = combine2 Q.mod_t A.mod_t normalize
   let mod_f = combine2 Q.mod_f A.mod_f normalize
-  let is_zero c = match c with Q q -> Q.is_zero q | A _ -> false
-  (* by normalization *)
+
+  let is_zero = function
+    | Q q -> Q.is_zero q
+    | A _ -> false (* because of normalization *)
+
   let round x =
     if lt zero x then ceil (sub x half) else floor (add x half)
 
   let none_zero c = if is_zero c then None else Some c
+
   let is_not_zero c = not ((sign c) = 0)
 
   let pow q n =
-    match q with Q q -> Q (Q.pow q n) | A a -> !!(A.pow_int ~ctx a n)
+    match q with
+    | Q q -> Q (Q.pow q n)
+    | A a -> !!(A.pow_int ~ctx a n)
 
   let positive_root q n =
     if n = 0 then one else !!(A.pow ~ctx (to_a q) (Q.make Z.one (Z.of_int n)))
@@ -164,9 +254,17 @@ module A = struct
   let from_order poly order =
     let poly = Flint.FMPZ_poly.create poly in
     let roots = Calcium.QQBAR.from_roots ~unsorted:true poly in
-    if Stdlib.Array.length roots <= order then invalid_arg "Not enough roots";
-    if Stdlib.Array.exists (fun x -> not (Calcium.QQBAR.is_real x)) roots
-    then invalid_arg "Roots must all be reals";
+    (* Check that there are enough roots *)
+    if Stdlib.Array.length roots <= order then
+      raise (No_ordered_root {
+          poly; order;
+          num_roots = Stdlib.Array.length roots;
+        });
+    (* Check that the polynomial only has real (not imaginary) roots *)
+    if Stdlib.Array.exists (fun x -> not (Calcium.QQBAR.is_real x)) roots then
+      raise (Complex_roots { poly; });
+    (* Convert roots, sort them in increasing order, and fetch the
+       root that was asked *)
     let roots = Stdlib.Array.map (Calcium.CA.from_qqbar ~ctx) roots in
     let cmp r1 r2 = Calcium.CA.compare ~ctx r1 r2 in
     Stdlib.Array.sort cmp roots;
@@ -175,50 +273,35 @@ module A = struct
   let from_enclosure poly min max =
     let poly = Flint.FMPZ_poly.create poly in
     let roots = Calcium.QQBAR.from_roots ~unsorted:true poly in
+    (* TODO: do we need to check that all roots are real ? *)
     let roots = Stdlib.Array.map (Calcium.CA.from_qqbar ~ctx) roots in
-    let inside r = Calcium.CA.compare_q ~ctx r min >= 0 &&
-        Calcium.CA.compare_q ~ctx r max <= 0
+    let inside r =
+      Calcium.CA.compare_q ~ctx r min >= 0 &&
+      Calcium.CA.compare_q ~ctx r max <= 0
+    in
+    let roots =
+      Stdlib.Array.to_list roots
+      |> List.filter inside
+      |> List.map (!!)
     in
-    let roots = List.filter inside (Stdlib.Array.to_list roots) in
     match roots with
-    | [] -> invalid_arg "No roots found in the enclosure"
-    | [r] -> !!r
-    | _ -> invalid_arg "The roots are not uniq in the enclosure"
-  end
+    | [r] -> r
+    | [] | _ :: _ :: _ ->
+      raise (Bad_root_enclosure { poly; min; max; roots; })
 
+end
 
+(* Real values *)
+(* ************************************************************************* *)
 
+(* Real are currently represented as algebraic numbers *)
 type t = A.t
 
 let compare = A.compare
-let print fmt r =
-  Format.fprintf fmt "%a" A.pp r
+let print fmt r = Format.fprintf fmt "%a" A.pp r
 
 let ops = Value.ops ~compare ~print ()
 
-(* Value helpers *)
-(* ************************************************************************* *)
-(*
-let ceil x = Q.of_bigint @@ Int.ceil x
-let floor x = Q.of_bigint @@ Int.floor x
-let truncate x = Q.of_bigint @@ Int.truncate x
-
-let half = { Q.num = Z.one; Q.den = Z.of_int 2 }
-
-let round x =
-  if Q.lt Q.zero x then ceil (Q.sub x half) else floor (Q.add x half)
-
-let div_e a b =
-  let s = Q.sign b in
-  let d = Q.div a b in
-  if s > 0 then floor d else ceil d
-
-let div_t a b = truncate (Q.div a b)
-let div_f a b = floor (Q.div a b)
-let mod_e a b = Q.sub a (Q.mul (div_e a b) b)
-let mod_t a b = Q.sub a (Q.mul (div_t a b) b)
-let mod_f a b = Q.sub a (Q.mul (div_f a b) b)
-*)
 
 (* Builtins *)
 (* ************************************************************************* *)
@@ -247,23 +330,29 @@ let op2_zero ~eval ~env ~cst f =
       let v_y = Value.extract_exn ~ops y in
       if A.equal A.zero v_y then
         Fun.corner_case ~eval env cst [] [x; y]
-      else mk @@ f v_x v_y
+      else
+        mk @@ f v_x v_y
     ))
 
+let q_of_pair (num,den) =
+  Q.div (Q.of_string num) (Q.of_string den)
+
+let mk_coeffs l =
+  Stdlib.Array.of_list (List.map Z.of_string l)
+
 let builtins ~eval env (cst : Dolmen.Std.Expr.Term.Const.t) =
   match cst.builtin with
   | B.Decimal i -> Some (mk (A.of_string i))
   | B.Algebraic (Ordered_root {coeffs; order}) ->
-    let coeffs = Stdlib.Array.of_list (List.map Z.of_string coeffs) in
+    let coeffs = mk_coeffs coeffs in
     let order = int_of_string order in
     Some (mk (A.from_order coeffs order))
   | B.Algebraic (Enclosed_root {coeffs; min; max}) ->
-      let coeffs = Stdlib.Array.of_list (List.map Z.of_string coeffs) in
-      let q_of_pair (num,den) = Q.div (Q.of_string num) (Q.of_string den) in
-      let min = q_of_pair min in
-      let max = q_of_pair max in
-      Some (mk (A.from_enclosure coeffs min max))
-    | B.Lt `Real -> cmp ~cst A.lt
+    let coeffs = mk_coeffs coeffs in
+    let min = q_of_pair min in
+    let max = q_of_pair max in
+    Some (mk (A.from_enclosure coeffs min max))
+  | B.Lt `Real -> cmp ~cst A.lt
   | B.Gt `Real -> cmp ~cst A.gt
   | B.Geq `Real -> cmp ~cst A.ge
   | B.Leq `Real -> cmp ~cst A.le
@@ -283,7 +372,6 @@ let builtins ~eval env (cst : Dolmen.Std.Expr.Term.Const.t) =
   | B.Ceiling `Real -> op1 ~cst A.ceil
   | B.Truncate `Real -> op1 ~cst A.truncate
   | B.Round `Real -> op1 ~cst A.round
-  | B.Is_int `Real ->
-    Some (fun1 ~cst (fun x -> Bool.mk (A.is_integer x)))
+  | B.Is_int `Real -> Some (fun1 ~cst (fun x -> Bool.mk (A.is_integer x)))
   | _ -> None
 
diff --git a/src/model/real.mli b/src/model/real.mli
index b8df44153..3253eaf5a 100644
--- a/src/model/real.mli
+++ b/src/model/real.mli
@@ -1,18 +1,75 @@
 
 (* This file is free software, part of dolmen. See file "LICENSE" for more information *)
 
+(** {2 Value definition} *)
+(** ************************************************************************ *)
+
+type t
+
+val ops : t Value.ops
+(** ops for real values. *)
+
+val mk : t -> Value.t
+(** real value creation. *)
+
+val get : Value.t -> t
+(** Get a rational value. *)
+
+
+(** {2 Corner cases & builtins} *)
+(** ************************************************************************ *)
+
+val builtins : Env.builtins
+(** builtins for reals *)
+
+
+(** {2 Algebraic number manipulation} *)
+(** ************************************************************************ *)
+
+(** Polynomials *)
+module Poly = Flint.FMPZ_poly
+
+(** Algebraic numbers *)
 module A : sig
-   (** Algebraic numbers *)
-  type t
+
+  type nonrec t = t
+  (** The type of algebraic numbers *)
+
+  exception Complex_roots of {
+      poly : Poly.t;
+    }
+  (** Exception raised when trying to create an algebraic number
+      from a polynomial that has complex roots. *)
+
+  exception No_ordered_root of {
+      order : int;
+      poly : Poly.t;
+      num_roots : int;
+    }
+  (** Exception raised when trying to create an algebraic number
+      from the [order]-th root (first root = 0) of [poly], but [poly]
+      only has [num_roots] (with [num_roots <= order]). *)
+
+  exception Bad_root_enclosure of {
+      poly : Poly.t;
+      min : Q.t;
+      max : Q.t;
+      roots : t list;
+    }
+  (** Exception raised when trying to create an algebraic number
+      from the root of [poly] that is within [min] and [max],
+      but there was not exactly 1 root in that interval. *)
 
   val compare : t -> t -> int
   val equal : t -> t -> bool
   val pp : Format.formatter -> t -> unit
+
   val zero : t
   val one : t
   val half : t
   val minus_one : t
   val two : t
+
   val sign : t -> int
   val ge : t -> t -> bool
   val gt : t -> t -> bool
@@ -65,25 +122,4 @@ module A : sig
   val positive_pow : t -> Q.t -> t
 end
 
-(** {2 Value definition} *)
-(** ************************************************************************ *)
-
-type t = A.t
-
-val ops : t Value.ops
-(** ops for real values. *)
-
-val mk : t -> Value.t
-(** real value creation. *)
-
-val get : Value.t -> t
-(** Get a rational value. *)
-
-
-(** {2 Corner cases & builtins} *)
-(** ************************************************************************ *)
-
-val builtins : Env.builtins
-(** builtins for reals *)
-
 
diff --git a/src/standard/builtin.ml b/src/standard/builtin.ml
index ad3b4045b..8566b3f51 100644
--- a/src/standard/builtin.ml
+++ b/src/standard/builtin.ml
@@ -71,7 +71,7 @@ type _ t +=
   | Int | Integer of string
   | Rat | Rational of string
   | Real | Decimal of string
-  | Algebraic of algebraic (* instead of algebraic_ordered_root *)
+  | Algebraic of algebraic
   | Lt of int_rat_real | Leq of int_rat_real
   | Gt of int_rat_real | Geq of int_rat_real
   | Minus of int_rat_real
diff --git a/src/standard/builtin.mli b/src/standard/builtin.mli
index 6108749c4..cae1dbee3 100644
--- a/src/standard/builtin.mli
+++ b/src/standard/builtin.mli
@@ -167,8 +167,25 @@ type _ t +=
 (*  ************************************************************************* *)
 
 type algebraic =
-| Ordered_root of { coeffs : string list; order : string; }
-| Enclosed_root of { coeffs : string list; min : string * string; max: string * string; }
+  | Ordered_root of { coeffs : string list; order : string; }
+  (** [Ordered_root{ coeffs; order = n; }: Real]
+      This real represent the n-th root (including multiplicity) of the
+      polynomial represented by [coeffs]. The numbers in [coeffs] are the
+      coefficients of the monomials, in increasing order of exponent. Each
+      string represents an integer number, potentially preceded by a "-" sign.
+      For instance the list [["1"; "0"; "-2"; "1"]] representes the polynomial
+      [x^3 - 2*x^2 + 1].*)
+  | Enclosed_root of {
+      coeffs : string list;
+      min : string * string;
+      max : string * string; }
+  (** [Enclosed_root{coeefs; min; max; }: Real]
+      This represents a real that is a root of the polynomial represented by
+      [coeffs] (see doc of {Ordered_root} for explanations about how [coeffs]
+      represent polynomial), which is in the interval [min; max]. There should
+      be exactly one root in that interval, but this property is not checked
+      during typechecking. *)
+(** Type used to represent algebraic numbers. *)
 
 type _ t +=
   | Int
@@ -199,6 +216,8 @@ type _ t +=
 
       Real literals can be parsed using ZArith's [Q.of_string]. *)
   | Algebraic of algebraic
+  (** [Algebraic: Real] real literals, using algebraic numbers. See
+      documentation of the {algebraic} type for more information. *)
   | Lt of [ `Int | `Rat | `Real ]
   (** [Lt: {a=(Int|Rational|Real)} a -> a -> Prop]:
       strict comparison (less than) on numbers
diff --git a/src/standard/expr.ml b/src/standard/expr.ml
index 69ecdca8b..7f65d4fa0 100644
--- a/src/standard/expr.ml
+++ b/src/standard/expr.ml
@@ -2111,51 +2111,42 @@ module Term = struct
             mk' ~builtin:(Builtin.Decimal s) s [] [] Ty.real
           )
 
+      let print_rat fmt (num,denom) =
+        Format.fprintf fmt "%s / %s" num denom
+
+      let print_coef fmt c =
+        let n = String.length c in
+        assert (n > 0);
+        if c.[0] = '-'
+        then Format.fprintf fmt "- %s" (String.sub c 1 (n - 1))
+        else Format.fprintf fmt "+ %s" c
+
+      let print_monomial fmt (c, n) =
+        if c = "0" then ()
+        else if n <= 0 then print_coef fmt c
+        else Format.fprintf fmt "%a x^%d" print_coef c n
+
+      let print_polynomial fmt l =
+        let rec aux fmt n = function
+          | [] -> ()
+          | c :: r -> print_monomial fmt (c, n); aux fmt (n + 1) r
+        in
+        aux fmt 0 l
+
       let algebraic_ordered_root =
-        let cache = Hashtbl.create 113 in
-        fun coeffs order ->
-            with_cache ~cache (fun (coeffs,order) ->
-              let algebraic = "algebraic" in
-              let len = List.fold_left (fun acc x -> 1 + acc + String.length x) 0 coeffs
-              + String.length order
-              + String.length algebraic
-              + 3
+        with_cache ~cache:(Hashtbl.create 13) (fun (coeffs,order) ->
+            let s = Format.asprintf "root<%s, %a>" order print_polynomial coeffs in
+            mk' ~builtin:(Builtin.Algebraic (Ordered_root {coeffs;order})) s [] [] Ty.real
+          )
+
+      let algebraic_enclosed_root =
+        with_cache ~cache:(Hashtbl.create 13) (fun (coeffs,min,max) ->
+            let s =
+              Format.asprintf "root<%a,%a,%a>"
+                print_rat min print_rat max print_polynomial coeffs
             in
-              let b = Buffer.create len in
-              Buffer.add_string b algebraic;
-              Buffer.add_char b '(';
-              List.iter (fun x -> Buffer.add_string b x; Buffer.add_char b ';') coeffs;
-              Buffer.add_char b '|';
-              Buffer.add_string b order;
-              Buffer.add_char b ')';
-              let s = Buffer.contents b in
-                mk' ~builtin:(Builtin.Algebraic (Ordered_root {coeffs;order})) s [] [] Ty.real
-              ) (coeffs,order)
-
-              let algebraic_enclosed_root =
-                let cache = Hashtbl.create 113 in
-                fun coeffs min max ->
-                    with_cache ~cache (fun (coeffs,((min_num,min_den)as min),((max_num,max_den) as max)) ->
-                      let algebraic = "algebraic" in
-                      let len = List.fold_left (fun acc x -> 1 + acc + String.length x) 0 coeffs
-                      + String.length min_num + String.length min_den
-                      + String.length max_num + String.length max_den
-                      + String.length algebraic
-                      + 6
-                    in
-                      let b = Buffer.create len in
-                      Buffer.add_string b algebraic;
-                      Buffer.add_char b '(';
-                      List.iter (fun x -> Buffer.add_string b x; Buffer.add_char b ';') coeffs;
-                      Buffer.add_char b '|';
-                      Buffer.add_string b min_num; Buffer.add_char b '/'; Buffer.add_string b min_den;
-                      Buffer.add_char b ',';
-                      Buffer.add_string b max_num; Buffer.add_char b '/'; Buffer.add_string b max_den;
-                      Buffer.add_char b ')';
-                      let s = Buffer.contents b in
-                        mk' ~builtin:(Builtin.Algebraic (Enclosed_root {coeffs;min;max})) s [] [] Ty.real
-                        ) (coeffs,min,max)
-        
+            mk' ~builtin:(Builtin.Algebraic (Enclosed_root {coeffs;min;max})) s [] [] Ty.real
+          )
 
       let minus = mk'
           ~pos:Pretty.Prefix ~name:"-" ~builtin:(Builtin.Minus `Real)
@@ -3338,9 +3329,9 @@ module Term = struct
   module Real = struct
     let mk = real
     let algebraic_ordered_root coeffs order =
-      apply_cst (Const.Real.algebraic_ordered_root coeffs order) [] []
+      apply_cst (Const.Real.algebraic_ordered_root (coeffs, order)) [] []
     let algebraic_enclosed_root coeffs min max =
-      apply_cst (Const.Real.algebraic_enclosed_root coeffs min max) [] []
+      apply_cst (Const.Real.algebraic_enclosed_root (coeffs, min, max)) [] []
     let div' = Const.Real.div
     let minus t = apply_cst Const.Real.minus [] [t]
     let add a b = apply_cst Const.Real.add [] [a; b]
diff --git a/src/standard/expr.mli b/src/standard/expr.mli
index f8ad85cb1..9b46c293e 100644
--- a/src/standard/expr.mli
+++ b/src/standard/expr.mli
@@ -1066,18 +1066,21 @@ module Term : sig
 
     (** A module for real constant symbols that occur in terms. *)
     module Real : sig
+
       val real : string -> t
       (** Real literals. *)
 
-      val algebraic_ordered_root : string list -> string -> t
+      val algebraic_ordered_root :
+        string list * string -> t
       (** Algebraic number defined with a polynomial (coefficient of smallest
-              degree first), and the ordered of the root when ordered from
-              smallest to biggest *)
+          degree first), and the ordered of the root when ordered from
+          smallest to biggest *)
 
-      val algebraic_enclosed_root : string list ->
-         string * string -> string * string -> t
+      val algebraic_enclosed_root :
+        string list * (string * string) * (string * string) -> t
       (** Algebraic number defined with a polynomial (coefficient of smallest
-            degree first), and an interval where the polynomial as uniq root *)
+          degree first), and an interval where the polynomial has a unique root.
+          Each bound of the interval is a rational expressed as two integers. *)
 
       val minus : t
       (** Real unary minus/negation. *)
diff --git a/src/typecheck/arith.ml b/src/typecheck/arith.ml
index 453e908db..12cb1f120 100644
--- a/src/typecheck/arith.ml
+++ b/src/typecheck/arith.ml
@@ -770,6 +770,61 @@ module Smtlib2 = struct
 
   end
 
+  (* Polynomial coefficients for algebraic numbers *)
+  module Poly(Type : Tff_intf.S) = struct
+
+    let parse_int_as_string env ast =
+      let rec is_int i s =
+        String.length s <= i ||
+        begin
+          match s.[i] with
+          | '-' -> i = 0
+          | '0' | '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9' -> true
+          | _ -> false
+        end
+        || is_int (i+1) s
+      in
+      match ast.Term.term with
+      | Symbol  { Id.ns = Value (Integer); name = Simple name; } ->
+        name
+      | App({ term = Symbol { Id.ns = Term; name = Simple "-"; };_},
+            [{ term = Symbol  { Id.ns = Value (Integer); name = Simple name; }; _}]) ->
+        "-" ^ name
+      | Symbol  { Id.ns = Term; name = Simple name; } when is_int 0 name ->
+        (* TODO: is this one necessary ? *)
+        name
+      | _ ->
+        Type._error env (Ast ast) (Type.Expected ("An integer constant", None))
+
+    let parse_rat_as_string env ast =
+      match ast.Term.term with
+      | Symbol  { Id.ns = Value (Integer | Rational | Real); name = Simple name; } ->
+        (name, "1.0")
+      | App({term = Symbol { Id.ns = Term; name = Simple "-"; };_},
+            [{term=Symbol  { Id.ns = Value (Integer | Rational | Real ); name = Simple name; };_}]) ->
+        ("-" ^ name, "1.0")
+      | App({term = Symbol { Id.ns = Term; name = Simple "/"; };_},
+            [{term = Symbol { Id.ns = Value (Integer | Rational | Real ); name = Simple name1; };_};
+             {term = Symbol { Id.ns = Value (Integer | Rational | Real ); name = Simple name2; };_}]) ->
+        (name1, name2)
+      | App({term = Symbol { Id.ns = Term; name = Simple "/"; };_},
+            [{term=App({term = Symbol { Id.ns = Term; name = Simple "-"; };_},
+                       [{term=Symbol  { Id.ns = Value (Integer | Rational | Real ); name = Simple name1};_}]);_};
+             {term=Symbol  { Id.ns = Value (Integer | Rational | Real ); name = Simple name2; };_}]) ->
+        ("-" ^ name1, name2)
+      | _ ->
+        Type._error env (Ast ast) (Type.Expected ("A rational constant", None))
+
+    let parse_poly_coeffs_as_strings env ast =
+      match ast.Term.term with
+      | App ({term = Symbol { Id.ns = Term; name = Simple "coeffs"; };_},args) ->
+        List.map (parse_int_as_string env) args
+      | _ ->
+        Type._error env (Ast ast)
+          (Type.Expected ("A list of coefficient starting with \"coeffs\"", None))
+
+  end
+
   (* Integer arithmetics *)
 
   module Int = struct
@@ -880,6 +935,7 @@ module Smtlib2 = struct
         (T : Dolmen.Intf.Term.Smtlib_Real with type t := Type.T.t
                                            and type cst := Type.T.Const.t) = struct
 
+      module P = Poly(Type)
       module F = Filter(Type)
 
       type _ Type.warn +=
@@ -934,7 +990,7 @@ module Smtlib2 = struct
                 ("-"^name1,name2)
           | _ ->
             Type._error env (Ast ast) (Forbidden "A rational model is expected")
-    
+
       let parse_coeffs env ast =
         match ast.Term.term with
         | App ({term = Symbol { Id.ns = Term; name = Simple "coeffs"; };_},args) ->
@@ -943,31 +999,35 @@ module Smtlib2 = struct
           Type._error env (Ast ast)
            (Forbidden "A list of coefficient starting with \"coeffs\" is expected")
 
-           let rec parse ~config version env s =
+      let rec parse ~config version env s =
         match s with
+
         (* type *)
         | Type.Id { Id.ns = Sort; name = Simple "Real"; } ->
           Type.builtin_ty (Base.app0 (module Type) env s Ty.real)
+
         (* values *)
         | Type.Id { Id.ns = Value (Integer | Real); name = Simple name; } ->
           Type.builtin_term (Base.app0 (module Type) env s (T.mk name))
-        | Type.Id { Id.ns = Term; name = Simple ("root-of-with-order"|"root-of-with-ordering"); } ->
+        | Type.Id { Id.ns = Term;
+                    name = Simple ("root-of-with-order"|"root-of-with-ordering"); } ->
           Type.builtin_term (Base.make_op2 (module Type) env s (fun _ast (coeffs,num) ->
-            let coeffs = parse_coeffs env coeffs in
-            let num = match num.term with
-              | Symbol  { Id.ns = Value (Integer); name = Simple name; } ->
-                  name
-              | _ -> Type._error env (Ast num) (Forbidden "A positive integer is expected")
-            in
-            T.algebraic_ordered_root coeffs num )
-          )
-          | Type.Id { Id.ns = Term; name = Simple ("root-of-with-enclosure"|"root-of-with-interval"); } ->
-            Type.builtin_term (Base.make_op3 (module Type) env s (fun _ast (coeffs,min,max) ->
-              let coeffs = parse_coeffs env coeffs in
-              let min = parse_rat env min in
-              let max = parse_rat env max in
-              T.algebraic_enclosed_root coeffs min max )
-            )
+              let coeffs = P.parse_poly_coeffs_as_strings env coeffs in
+              let num = match num.term with
+                | Symbol { Id.ns = Value (Integer); name = Simple name; } -> name
+                | _ -> Type._error env (Ast num) (Forbidden "A positive integer is expected")
+              in
+              T.algebraic_ordered_root coeffs num
+            ))
+        | Type.Id { Id.ns = Term;
+                    name = Simple ("root-of-with-enclosure"|"root-of-with-interval"); } ->
+          Type.builtin_term (Base.make_op3 (module Type) env s (fun _ast (coeffs,min,max) ->
+              let coeffs = P.parse_poly_coeffs_as_strings env coeffs in
+              let min = P.parse_rat_as_string env min in
+              let max = P.parse_rat_as_string env max in
+              T.algebraic_enclosed_root coeffs min max
+            ))
+
         (* terms *)
         | Type.Id { Id.ns = Term; name = Simple name; } ->
           begin match name with
@@ -1024,6 +1084,7 @@ module Smtlib2 = struct
                                                and type Int.cst := Type.T.Const.t
                                                and type Real.cst := Type.T.Const.t) = struct
 
+      module P = Poly(Type)
       module F = Filter(Type)
 
       type _ Type.warn +=
@@ -1077,6 +1138,24 @@ module Smtlib2 = struct
           Type.builtin_term (Base.app0 (module Type) env s (T.Int.mk name))
         | Type.Id { Id.ns = Value Real; name = Simple name; } ->
           Type.builtin_term (Base.app0 (module Type) env s (T.Real.mk name))
+        | Type.Id { Id.ns = Term;
+                    name = Simple ("root-of-with-order"|"root-of-with-ordering"); } ->
+          Type.builtin_term (Base.make_op2 (module Type) env s (fun _ast (coeffs,num) ->
+              let coeffs = P.parse_poly_coeffs_as_strings env coeffs in
+              let num = match num.term with
+                | Symbol { Id.ns = Value (Integer); name = Simple name; } -> name
+                | _ -> Type._error env (Ast num) (Forbidden "A positive integer is expected")
+              in
+              T.Real.algebraic_ordered_root coeffs num
+            ))
+        | Type.Id { Id.ns = Term;
+                    name = Simple ("root-of-with-enclosure"|"root-of-with-interval"); } ->
+          Type.builtin_term (Base.make_op3 (module Type) env s (fun _ast (coeffs,min,max) ->
+              let coeffs = P.parse_poly_coeffs_as_strings env coeffs in
+              let min = P.parse_rat_as_string env min in
+              let max = P.parse_rat_as_string env max in
+              T.Real.algebraic_enclosed_root coeffs min max
+            ))
 
         (* terms *)
         | Type.Id { Id.ns = Term; name = Simple name; } ->
diff --git a/tests/model/real/bad_ordered_root.expected b/tests/model/real/bad_ordered_root.expected
new file mode 100644
index 000000000..ad8aee70a
--- /dev/null
+++ b/tests/model/real/bad_ordered_root.expected
@@ -0,0 +1,6 @@
+File "tests/model/real/bad_ordered_root.rsmt2", line 3, character 2-66:
+3 |   (define-fun a () Real (root-of-with-order (coeffs 1 0 (- 1)) 2))
+      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error The following polynomial has 2 roots, but the model tried to use
+      its 3rd root: -x^2+1
+Hint: Root orders start at 0 for the first (smallest) root
diff --git a/tests/model/real/bad_ordered_root.rsmt2 b/tests/model/real/bad_ordered_root.rsmt2
new file mode 100644
index 000000000..af2a405d5
--- /dev/null
+++ b/tests/model/real/bad_ordered_root.rsmt2
@@ -0,0 +1,4 @@
+sat
+(
+  (define-fun a () Real (root-of-with-order (coeffs 1 0 (- 1)) 2))
+)
diff --git a/tests/model/real/bad_ordered_root.smt2 b/tests/model/real/bad_ordered_root.smt2
new file mode 100644
index 000000000..07830b0f1
--- /dev/null
+++ b/tests/model/real/bad_ordered_root.smt2
@@ -0,0 +1,5 @@
+(set-logic NRA)
+(declare-fun a () Real)
+; the assert does not matter
+(assert (= a 1))
+(check-sat)
diff --git a/tests/model/real/complex_roots.expected b/tests/model/real/complex_roots.expected
new file mode 100644
index 000000000..92383fc6e
--- /dev/null
+++ b/tests/model/real/complex_roots.expected
@@ -0,0 +1,5 @@
+File "tests/model/real/complex_roots.rsmt2", line 3, character 2-68:
+3 |   (define-fun a () Real (root-of-with-order (coeffs 1 0 0 (- 1)) 2))
+      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error The following polynomial has complex roots, which prevents from
+      ordering roots: -x^3+1
diff --git a/tests/model/real/complex_roots.rsmt2 b/tests/model/real/complex_roots.rsmt2
new file mode 100644
index 000000000..4c3024c78
--- /dev/null
+++ b/tests/model/real/complex_roots.rsmt2
@@ -0,0 +1,4 @@
+sat
+(
+  (define-fun a () Real (root-of-with-order (coeffs 1 0 0 (- 1)) 2))
+)
diff --git a/tests/model/real/complex_roots.smt2 b/tests/model/real/complex_roots.smt2
new file mode 100644
index 000000000..07830b0f1
--- /dev/null
+++ b/tests/model/real/complex_roots.smt2
@@ -0,0 +1,5 @@
+(set-logic NRA)
+(declare-fun a () Real)
+; the assert does not matter
+(assert (= a 1))
+(check-sat)
diff --git a/tests/model/real/dune b/tests/model/real/dune
index de58a10eb..053ad963d 100644
--- a/tests/model/real/dune
+++ b/tests/model/real/dune
@@ -65,6 +65,70 @@
   (action (diff algebraic.expected algebraic.full)))
 
 
+; Test for bad_ordered_root.smt2
+; Incremental test
+
+(rule
+   (target  bad_ordered_root.incremental)
+   (deps    (:response bad_ordered_root.rsmt2) (:input bad_ordered_root.smt2))
+   (package dolmen_bin)
+   (action (chdir %{workspace_root}
+            (with-outputs-to %{target}
+             (with-accepted-exit-codes (or 0 (not 0))
+              (run dolmen --check-model=true -r %{response} --mode=incremental --color=never %{input} %{read-lines:flags.dune}))))))
+(rule
+  (alias runtest)
+  (package dolmen_bin)
+  (action (diff bad_ordered_root.expected bad_ordered_root.incremental)))
+
+; Full mode test
+
+(rule
+   (target  bad_ordered_root.full)
+   (deps    (:response bad_ordered_root.rsmt2) (:input bad_ordered_root.smt2))
+   (package dolmen_bin)
+   (action (chdir %{workspace_root}
+            (with-outputs-to %{target}
+             (with-accepted-exit-codes (or 0 (not 0))
+              (run dolmen --check-model=true -r %{response} --mode=full --color=never %{input} %{read-lines:flags.dune}))))))
+(rule
+  (alias runtest)
+  (package dolmen_bin)
+  (action (diff bad_ordered_root.expected bad_ordered_root.full)))
+
+
+; Test for complex_roots.smt2
+; Incremental test
+
+(rule
+   (target  complex_roots.incremental)
+   (deps    (:response complex_roots.rsmt2) (:input complex_roots.smt2))
+   (package dolmen_bin)
+   (action (chdir %{workspace_root}
+            (with-outputs-to %{target}
+             (with-accepted-exit-codes (or 0 (not 0))
+              (run dolmen --check-model=true -r %{response} --mode=incremental --color=never %{input} %{read-lines:flags.dune}))))))
+(rule
+  (alias runtest)
+  (package dolmen_bin)
+  (action (diff complex_roots.expected complex_roots.incremental)))
+
+; Full mode test
+
+(rule
+   (target  complex_roots.full)
+   (deps    (:response complex_roots.rsmt2) (:input complex_roots.smt2))
+   (package dolmen_bin)
+   (action (chdir %{workspace_root}
+            (with-outputs-to %{target}
+             (with-accepted-exit-codes (or 0 (not 0))
+              (run dolmen --check-model=true -r %{response} --mode=full --color=never %{input} %{read-lines:flags.dune}))))))
+(rule
+  (alias runtest)
+  (package dolmen_bin)
+  (action (diff complex_roots.expected complex_roots.full)))
+
+
 ; Test for div.smt2
 ; Incremental test
 

From d6fc2939e4241d29d09aac6eedb1c8f3831fc1cd Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Wed, 28 Jun 2023 14:20:08 +0200
Subject: [PATCH 6/9] More tests and proper errors

---
 src/model/loop.ml                             | 18 +++++
 src/model/real.ml                             |  3 +-
 src/model/real.mli                            | 70 +++++++++++++------
 src/standard/expr.ml                          | 36 ++++++----
 tests/model/real/bad_root_enclosure.expected  |  4 ++
 tests/model/real/bad_root_enclosure.rsmt2     |  4 ++
 tests/model/real/bad_root_enclosure.smt2      |  5 ++
 .../real/complex_root_enclosure.expected      |  0
 tests/model/real/complex_root_enclosure.rsmt2 |  4 ++
 tests/model/real/complex_root_enclosure.smt2  |  4 ++
 tests/model/real/dune                         | 68 ++++++++++++++++++
 11 files changed, 182 insertions(+), 34 deletions(-)
 create mode 100644 tests/model/real/bad_root_enclosure.expected
 create mode 100644 tests/model/real/bad_root_enclosure.rsmt2
 create mode 100644 tests/model/real/bad_root_enclosure.smt2
 create mode 100644 tests/model/real/complex_root_enclosure.expected
 create mode 100644 tests/model/real/complex_root_enclosure.rsmt2
 create mode 100644 tests/model/real/complex_root_enclosure.smt2

diff --git a/src/model/loop.ml b/src/model/loop.ml
index 4afdc3e2a..c41a04f39 100644
--- a/src/model/loop.ml
+++ b/src/model/loop.ml
@@ -281,6 +281,22 @@ let complex_roots =
           Real.Poly.pp poly)
     ~name:"Complex Roots" ()
 
+let bad_root_enclosure =
+  Dolmen_loop.Report.Error.mk ~code ~mnemonic:"bad-root-enclsoure"
+    ~message:(fun fmt (poly, min, max, roots) ->
+        match roots with
+        | [] ->
+          Format.fprintf fmt "%a@ %a@ and@ %a:@ %a"
+            Format.pp_print_text "There are no roots between"
+            Q.pp_print min Q.pp_print max Real.Poly.pp poly
+        | _ ->
+          Format.fprintf fmt
+            "The@ polynomial@ '%a'@ has@ more@ than@ one@ root@ beetween@ \
+             %a@ and@ %a: %a"
+          Real.Poly.pp poly Q.pp_print min Q.pp_print max
+          Fmt.(list ~sep:Fmt.(any ",@ ") Real.A.pp) roots)
+    ~name:"Bad Root enclosure" ()
+
 (* Pipe *)
 (* ************************************************************************ *)
 
@@ -365,6 +381,8 @@ module Make
       _err complex_roots poly
     | Real.A.No_ordered_root { poly; num_roots; order; } ->
       _err no_ordered_root (poly, num_roots, order)
+    | Real.A.Bad_root_enclosure { poly; min; max; roots; } ->
+      _err bad_root_enclosure (poly, min, max, roots)
 
     (* Special cases for delayed evaluation *)
     | Eval.Undefined_constant c as exn ->
diff --git a/src/model/real.ml b/src/model/real.ml
index 8fd8f7018..772ec34a0 100644
--- a/src/model/real.ml
+++ b/src/model/real.ml
@@ -273,7 +273,8 @@ module A = struct
   let from_enclosure poly min max =
     let poly = Flint.FMPZ_poly.create poly in
     let roots = Calcium.QQBAR.from_roots ~unsorted:true poly in
-    (* TODO: do we need to check that all roots are real ? *)
+    (* Note: the comparisons in [inside] will only succeed if [r] is a real
+       (i.e. no complex part), so we do not need to filter out non-real roots. *)
     let roots = Stdlib.Array.map (Calcium.CA.from_qqbar ~ctx) roots in
     let inside r =
       Calcium.CA.compare_q ~ctx r min >= 0 &&
diff --git a/src/model/real.mli b/src/model/real.mli
index 3253eaf5a..bd208ba1a 100644
--- a/src/model/real.mli
+++ b/src/model/real.mli
@@ -32,6 +32,8 @@ module Poly = Flint.FMPZ_poly
 (** Algebraic numbers *)
 module A : sig
 
+  (** {2 Types and exceptions} *)
+
   type nonrec t = t
   (** The type of algebraic numbers *)
 
@@ -60,40 +62,57 @@ module A : sig
       from the root of [poly] that is within [min] and [max],
       but there was not exactly 1 root in that interval. *)
 
+
+  (** {2 Usual functions} *)
+
   val compare : t -> t -> int
   val equal : t -> t -> bool
   val pp : Format.formatter -> t -> unit
 
+
+  (** {2 Constants} *)
+
   val zero : t
   val one : t
   val half : t
   val minus_one : t
   val two : t
+  val inf : t
+  val minus_inf : t
+
+
+  (** {2 Conversions} *)
 
-  val sign : t -> int
-  val ge : t -> t -> bool
-  val gt : t -> t -> bool
-  val le : t -> t -> bool
-  val lt : t -> t -> bool
-  val min : t -> t -> t
-  val max : t -> t -> t
   val of_string : string -> t
   val to_string : t -> string
-  val is_integer : t -> bool
-  val is_real : t -> bool
+  (** String conversions *)
+
   val to_z : t -> Z.t
-  val to_int : t -> int
+  val of_z : Z.t -> t
+  val of_bigint : Z.t -> t
+  (** Natural nnumbers conversions. *)
+
   val to_q : t -> Q.t option
-  val inf : t
-  val minus_inf : t
-  val is_unsigned_integer : int -> t -> bool
   val of_q : Q.t -> t
-  val of_z : Z.t -> t
+  (* Rational numbers conversions. *)
+
+  val to_int : t -> int
   val of_int : int -> t
-  val of_bigint : Z.t -> t
-  val floor : t -> t
-  val ceil : t -> t
-  val truncate : t -> t
+  (* Standard int conversions. *)
+
+
+  (** {2 Testing/Inspection} *)
+
+  val sign : t -> int
+  val is_zero : t -> bool
+  val is_not_zero : t -> bool
+  val is_real : t -> bool
+  val is_integer : t -> bool
+  val is_unsigned_integer : int -> t -> bool
+
+
+  (** {2 Arithmetic operations} *)
+
   val neg : t -> t
   val inv : t -> t
   val abs : t -> t
@@ -113,13 +132,24 @@ module A : sig
   val mod_e : t -> t -> t
   val mod_t : t -> t -> t
   val mod_f : t -> t -> t
-  val is_zero : t -> bool
+
+  val ge : t -> t -> bool
+  val gt : t -> t -> bool
+  val le : t -> t -> bool
+  val lt : t -> t -> bool
+  val min : t -> t -> t
+  val max : t -> t -> t
+
+  val floor : t -> t
+  val ceil : t -> t
+  val truncate : t -> t
   val round : t -> t
   val none_zero : t -> t option
-  val is_not_zero : t -> bool
+
   val pow : t -> int -> t
   val positive_root : t -> int -> t
   val positive_pow : t -> Q.t -> t
+
 end
 
 
diff --git a/src/standard/expr.ml b/src/standard/expr.ml
index 7f65d4fa0..109ea0e0d 100644
--- a/src/standard/expr.ml
+++ b/src/standard/expr.ml
@@ -2114,35 +2114,45 @@ module Term = struct
       let print_rat fmt (num,denom) =
         Format.fprintf fmt "%s / %s" num denom
 
-      let print_coef fmt c =
+      let print_coef ~sign fmt c =
         let n = String.length c in
         assert (n > 0);
-        if c.[0] = '-'
-        then Format.fprintf fmt "- %s" (String.sub c 1 (n - 1))
-        else Format.fprintf fmt "+ %s" c
-
-      let print_monomial fmt (c, n) =
+        if c.[0] = '-' then
+          if c = "-1" then
+            Format.fprintf fmt "-"
+          else
+            Format.fprintf fmt "-%s" (String.sub c 1 (n - 1))
+        else if sign then
+          Format.fprintf fmt "+%s" c
+        else
+          Format.fprintf fmt "%s" c
+
+      let print_monomial ~sign fmt (c, n) =
         if c = "0" then ()
-        else if n <= 0 then print_coef fmt c
-        else Format.fprintf fmt "%a x^%d" print_coef c n
+        else if n <= 0
+        then Format.fprintf fmt "%a@," (print_coef ~sign) c
+        else Format.fprintf fmt "%ax^%d@," (print_coef ~sign) c n
 
       let print_polynomial fmt l =
-        let rec aux fmt n = function
+        let rec aux fmt sign n = function
           | [] -> ()
-          | c :: r -> print_monomial fmt (c, n); aux fmt (n + 1) r
+          | c :: r ->
+            let () = print_monomial ~sign fmt (c, n) in
+            let sign = sign || c <> "0" in
+            aux fmt sign (n + 1) r
         in
-        aux fmt 0 l
+        aux fmt false 0 l
 
       let algebraic_ordered_root =
         with_cache ~cache:(Hashtbl.create 13) (fun (coeffs,order) ->
-            let s = Format.asprintf "root<%s, %a>" order print_polynomial coeffs in
+            let s = Format.asprintf "root<%s, @[<hov>%a@]>" order print_polynomial coeffs in
             mk' ~builtin:(Builtin.Algebraic (Ordered_root {coeffs;order})) s [] [] Ty.real
           )
 
       let algebraic_enclosed_root =
         with_cache ~cache:(Hashtbl.create 13) (fun (coeffs,min,max) ->
             let s =
-              Format.asprintf "root<%a,%a,%a>"
+              Format.asprintf "root<%a,%a,@[<hov>%a@]>"
                 print_rat min print_rat max print_polynomial coeffs
             in
             mk' ~builtin:(Builtin.Algebraic (Enclosed_root {coeffs;min;max})) s [] [] Ty.real
diff --git a/tests/model/real/bad_root_enclosure.expected b/tests/model/real/bad_root_enclosure.expected
new file mode 100644
index 000000000..c7e6e3972
--- /dev/null
+++ b/tests/model/real/bad_root_enclosure.expected
@@ -0,0 +1,4 @@
+File "tests/model/real/bad_root_enclosure.rsmt2", line 3, character 2-80:
+3 |   (define-fun a () Real (root-of-with-enclosure (coeffs 1 0 (- 1)) (- 1.0) 1.0))
+      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+Error The polynomial '-x^2+1' has more than one root beetween -1 and 1: 1, -1
diff --git a/tests/model/real/bad_root_enclosure.rsmt2 b/tests/model/real/bad_root_enclosure.rsmt2
new file mode 100644
index 000000000..bb4f6ed4c
--- /dev/null
+++ b/tests/model/real/bad_root_enclosure.rsmt2
@@ -0,0 +1,4 @@
+sat
+(
+  (define-fun a () Real (root-of-with-enclosure (coeffs 1 0 (- 1)) (- 1.0) 1.0))
+)
diff --git a/tests/model/real/bad_root_enclosure.smt2 b/tests/model/real/bad_root_enclosure.smt2
new file mode 100644
index 000000000..07830b0f1
--- /dev/null
+++ b/tests/model/real/bad_root_enclosure.smt2
@@ -0,0 +1,5 @@
+(set-logic NRA)
+(declare-fun a () Real)
+; the assert does not matter
+(assert (= a 1))
+(check-sat)
diff --git a/tests/model/real/complex_root_enclosure.expected b/tests/model/real/complex_root_enclosure.expected
new file mode 100644
index 000000000..e69de29bb
diff --git a/tests/model/real/complex_root_enclosure.rsmt2 b/tests/model/real/complex_root_enclosure.rsmt2
new file mode 100644
index 000000000..baf9704d6
--- /dev/null
+++ b/tests/model/real/complex_root_enclosure.rsmt2
@@ -0,0 +1,4 @@
+sat
+(
+  (define-fun a () Real (root-of-with-enclosure (coeffs 1 0 0 (- 1)) 1.0 1.0))
+)
diff --git a/tests/model/real/complex_root_enclosure.smt2 b/tests/model/real/complex_root_enclosure.smt2
new file mode 100644
index 000000000..b236095ea
--- /dev/null
+++ b/tests/model/real/complex_root_enclosure.smt2
@@ -0,0 +1,4 @@
+(set-logic NRA)
+(declare-fun a () Real)
+(assert (= a 1))
+(check-sat)
diff --git a/tests/model/real/dune b/tests/model/real/dune
index 053ad963d..299a1a304 100644
--- a/tests/model/real/dune
+++ b/tests/model/real/dune
@@ -97,6 +97,74 @@
   (action (diff bad_ordered_root.expected bad_ordered_root.full)))
 
 
+; Test for bad_root_enclosure.smt2
+; Incremental test
+
+(rule
+   (target  bad_root_enclosure.incremental)
+   (deps    (:response bad_root_enclosure.rsmt2)
+            (:input bad_root_enclosure.smt2))
+   (package dolmen_bin)
+   (action (chdir %{workspace_root}
+            (with-outputs-to %{target}
+             (with-accepted-exit-codes (or 0 (not 0))
+              (run dolmen --check-model=true -r %{response} --mode=incremental --color=never %{input} %{read-lines:flags.dune}))))))
+(rule
+  (alias runtest)
+  (package dolmen_bin)
+  (action (diff bad_root_enclosure.expected bad_root_enclosure.incremental)))
+
+; Full mode test
+
+(rule
+   (target  bad_root_enclosure.full)
+   (deps    (:response bad_root_enclosure.rsmt2)
+            (:input bad_root_enclosure.smt2))
+   (package dolmen_bin)
+   (action (chdir %{workspace_root}
+            (with-outputs-to %{target}
+             (with-accepted-exit-codes (or 0 (not 0))
+              (run dolmen --check-model=true -r %{response} --mode=full --color=never %{input} %{read-lines:flags.dune}))))))
+(rule
+  (alias runtest)
+  (package dolmen_bin)
+  (action (diff bad_root_enclosure.expected bad_root_enclosure.full)))
+
+
+; Test for complex_root_enclosure.smt2
+; Incremental test
+
+(rule
+   (target  complex_root_enclosure.incremental)
+   (deps    (:response complex_root_enclosure.rsmt2)
+            (:input complex_root_enclosure.smt2))
+   (package dolmen_bin)
+   (action (chdir %{workspace_root}
+            (with-outputs-to %{target}
+             (with-accepted-exit-codes (or 0 (not 0))
+              (run dolmen --check-model=true -r %{response} --mode=incremental --color=never %{input} %{read-lines:flags.dune}))))))
+(rule
+  (alias runtest)
+  (package dolmen_bin)
+  (action (diff complex_root_enclosure.expected complex_root_enclosure.incremental)))
+
+; Full mode test
+
+(rule
+   (target  complex_root_enclosure.full)
+   (deps    (:response complex_root_enclosure.rsmt2)
+            (:input complex_root_enclosure.smt2))
+   (package dolmen_bin)
+   (action (chdir %{workspace_root}
+            (with-outputs-to %{target}
+             (with-accepted-exit-codes (or 0 (not 0))
+              (run dolmen --check-model=true -r %{response} --mode=full --color=never %{input} %{read-lines:flags.dune}))))))
+(rule
+  (alias runtest)
+  (package dolmen_bin)
+  (action (diff complex_root_enclosure.expected complex_root_enclosure.full)))
+
+
 ; Test for complex_roots.smt2
 ; Incremental test
 

From 24080ffcc492e3d59c82b716067b73dc1e442b55 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Wed, 28 Jun 2023 14:31:02 +0200
Subject: [PATCH 7/9] Better formatting for some error messages

---
 src/loop/typer.ml      | 12 ++++++------
 src/typecheck/arith.ml | 21 ++++++++++-----------
 2 files changed, 16 insertions(+), 17 deletions(-)

diff --git a/src/loop/typer.ml b/src/loop/typer.ml
index 72702d956..33594802c 100644
--- a/src/loop/typer.ml
+++ b/src/loop/typer.ml
@@ -90,10 +90,6 @@ let print_res fmt res =
     Format.fprintf fmt "the term@ %a" (pp_wrap Dolmen.Std.Expr.Term.print) t
   | T.Tags _ -> Format.fprintf fmt "some tags"
 
-let print_opt pp fmt = function
-  | None -> Format.fprintf fmt "<none>"
-  | Some x -> pp fmt x
-
 let rec print_expected fmt = function
   | [] -> assert false
   | x :: [] -> Format.fprintf fmt "%d" x
@@ -445,8 +441,12 @@ let not_well_founded_datatype =
 let expect_error =
   Report.Error.mk ~code ~mnemonic:"typing-bad-kind"
     ~message:(fun fmt (expected, got) ->
-        Format.fprintf fmt "Expected %s but got %a"
-          expected (print_opt print_res) got)
+        let pp_got fmt got =
+          match got with
+          | None -> ()
+          | Some res -> Format.fprintf fmt ",@ but got %a" print_res res
+        in
+        Format.fprintf fmt "Expected %s%a" expected pp_got got)
     ~name:"Bad kind" ()
 
 let bad_index_arity =
diff --git a/src/typecheck/arith.ml b/src/typecheck/arith.ml
index 12cb1f120..7d4f4c8de 100644
--- a/src/typecheck/arith.ml
+++ b/src/typecheck/arith.ml
@@ -773,6 +773,11 @@ module Smtlib2 = struct
   (* Polynomial coefficients for algebraic numbers *)
   module Poly(Type : Tff_intf.S) = struct
 
+    let parse_order env ast =
+      match ast.Term.term with
+      | Symbol { Id.ns = Value (Integer); name = Simple name; } -> name
+      | _ -> Type._error env (Ast ast) (Type.Expected ("a positive integer", None))
+
     let parse_int_as_string env ast =
       let rec is_int i s =
         String.length s <= i ||
@@ -794,7 +799,7 @@ module Smtlib2 = struct
         (* TODO: is this one necessary ? *)
         name
       | _ ->
-        Type._error env (Ast ast) (Type.Expected ("An integer constant", None))
+        Type._error env (Ast ast) (Type.Expected ("an integer constant", None))
 
     let parse_rat_as_string env ast =
       match ast.Term.term with
@@ -813,7 +818,7 @@ module Smtlib2 = struct
              {term=Symbol  { Id.ns = Value (Integer | Rational | Real ); name = Simple name2; };_}]) ->
         ("-" ^ name1, name2)
       | _ ->
-        Type._error env (Ast ast) (Type.Expected ("A rational constant", None))
+        Type._error env (Ast ast) (Type.Expected ("a rational constant", None))
 
     let parse_poly_coeffs_as_strings env ast =
       match ast.Term.term with
@@ -821,7 +826,7 @@ module Smtlib2 = struct
         List.map (parse_int_as_string env) args
       | _ ->
         Type._error env (Ast ast)
-          (Type.Expected ("A list of coefficient starting with \"coeffs\"", None))
+          (Type.Expected ("a list of coefficient starting with \"coeffs\"", None))
 
   end
 
@@ -1013,10 +1018,7 @@ module Smtlib2 = struct
                     name = Simple ("root-of-with-order"|"root-of-with-ordering"); } ->
           Type.builtin_term (Base.make_op2 (module Type) env s (fun _ast (coeffs,num) ->
               let coeffs = P.parse_poly_coeffs_as_strings env coeffs in
-              let num = match num.term with
-                | Symbol { Id.ns = Value (Integer); name = Simple name; } -> name
-                | _ -> Type._error env (Ast num) (Forbidden "A positive integer is expected")
-              in
+              let num = P.parse_order env num in
               T.algebraic_ordered_root coeffs num
             ))
         | Type.Id { Id.ns = Term;
@@ -1142,10 +1144,7 @@ module Smtlib2 = struct
                     name = Simple ("root-of-with-order"|"root-of-with-ordering"); } ->
           Type.builtin_term (Base.make_op2 (module Type) env s (fun _ast (coeffs,num) ->
               let coeffs = P.parse_poly_coeffs_as_strings env coeffs in
-              let num = match num.term with
-                | Symbol { Id.ns = Value (Integer); name = Simple name; } -> name
-                | _ -> Type._error env (Ast num) (Forbidden "A positive integer is expected")
-              in
+              let num = P.parse_order env num in
               T.Real.algebraic_ordered_root coeffs num
             ))
         | Type.Id { Id.ns = Term;

From cd44a90d1beca933390c5c20285f12a910d6537b Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Wed, 28 Jun 2023 15:46:31 +0200
Subject: [PATCH 8/9] typo

---
 src/model/loop.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/model/loop.ml b/src/model/loop.ml
index c41a04f39..b67591075 100644
--- a/src/model/loop.ml
+++ b/src/model/loop.ml
@@ -93,7 +93,7 @@ let pp_located fmt { contents = _; file = _; loc; } =
   let loc = Dolmen.Std.Loc.full_loc loc in
   Format.fprintf fmt "%a" Dolmen.Std.Loc.fmt loc
 
-let limitation_hint=
+let limitation_hint =
   (fun _ -> Some (
        Format.dprintf "%a"
          Format.pp_print_text

From e056909c6750ae6a22fb99e8bf8e7f77bbd7b91a Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Wed, 25 Oct 2023 17:23:06 +0200
Subject: [PATCH 9/9] Build fixes

---
 src/standard/expr.ml   |  4 ++--
 src/typecheck/arith.ml | 49 ------------------------------------------
 src/typecheck/intf.ml  |  3 +++
 3 files changed, 5 insertions(+), 51 deletions(-)

diff --git a/src/standard/expr.ml b/src/standard/expr.ml
index 109ea0e0d..9e448ad28 100644
--- a/src/standard/expr.ml
+++ b/src/standard/expr.ml
@@ -2144,13 +2144,13 @@ module Term = struct
         aux fmt false 0 l
 
       let algebraic_ordered_root =
-        with_cache ~cache:(Hashtbl.create 13) (fun (coeffs,order) ->
+        with_cache (fun (coeffs,order) ->
             let s = Format.asprintf "root<%s, @[<hov>%a@]>" order print_polynomial coeffs in
             mk' ~builtin:(Builtin.Algebraic (Ordered_root {coeffs;order})) s [] [] Ty.real
           )
 
       let algebraic_enclosed_root =
-        with_cache ~cache:(Hashtbl.create 13) (fun (coeffs,min,max) ->
+        with_cache (fun (coeffs,min,max) ->
             let s =
               Format.asprintf "root<%a,%a,@[<hov>%a@]>"
                 print_rat min print_rat max print_polynomial coeffs
diff --git a/src/typecheck/arith.ml b/src/typecheck/arith.ml
index 7d4f4c8de..b44dab778 100644
--- a/src/typecheck/arith.ml
+++ b/src/typecheck/arith.ml
@@ -955,55 +955,6 @@ module Smtlib2 = struct
         | Warn msg -> Type._warn env (Ast ast) (Restriction (config, msg))
         | Error msg -> Type._error env (Ast ast) (Forbidden (config, msg))
 
-      let parse_int env ast =
-        let rec is_int i s =
-          String.length s <= i ||
-          begin
-            match s.[i] with
-            | '-' -> i = 0
-            | '0' | '1' | '2' | '3' | '4' | '5' | '6' | '7' | '8' | '9' -> true
-            | _ -> false
-          end
-          || is_int (i+1) s
-        in
-      match ast.Term.term with
-        | Symbol  { Id.ns = Value (Integer); name = Simple name; } ->
-          name
-        | App({term = Symbol { Id.ns = Term; name = Simple "-"; };_},
-              [{term=Symbol  { Id.ns = Value (Integer); name = Simple name; };_}]) ->
-            "-"^name
-        | Symbol  { Id.ns = Term; name = Simple name; } when is_int 0 name ->
-          name
-        | _ ->
-          Type._error env (Ast ast) (Forbidden "An integer constant is expected")
-
-      let parse_rat env ast =
-        match ast.Term.term with
-        | Symbol  { Id.ns = Value (Integer | Rational | Real); name = Simple name; } ->
-            (name,"1.0")
-        | App({term = Symbol { Id.ns = Term; name = Simple "-"; };_},
-              [{term=Symbol  { Id.ns = Value (Integer | Rational | Real ); name = Simple name; };_}]) ->
-              "-"^name,"1.0"
-        | App({term = Symbol { Id.ns = Term; name = Simple "/"; };_},
-              [{term=Symbol  { Id.ns = Value (Integer | Rational | Real ); name = Simple name1; };_};
-                {term=Symbol  { Id.ns = Value (Integer | Rational | Real ); name = Simple name2; };_}]) ->
-                (name1,name2)
-        | App({term = Symbol { Id.ns = Term; name = Simple "/"; };_},
-                [{term=App({term = Symbol { Id.ns = Term; name = Simple "-"; };_},
-                  [{term=Symbol  { Id.ns = Value (Integer | Rational | Real ); name = Simple name1};_}]);_};
-                {term=Symbol  { Id.ns = Value (Integer | Rational | Real ); name = Simple name2; };_}]) ->
-                ("-"^name1,name2)
-          | _ ->
-            Type._error env (Ast ast) (Forbidden "A rational model is expected")
-
-      let parse_coeffs env ast =
-        match ast.Term.term with
-        | App ({term = Symbol { Id.ns = Term; name = Simple "coeffs"; };_},args) ->
-          List.map (parse_int env) args
-        | _ ->
-          Type._error env (Ast ast)
-           (Forbidden "A list of coefficient starting with \"coeffs\" is expected")
-
       let rec parse ~config version env s =
         match s with
 
diff --git a/src/typecheck/intf.ml b/src/typecheck/intf.ml
index 7bc5c1fc5..93109cc4f 100644
--- a/src/typecheck/intf.ml
+++ b/src/typecheck/intf.ml
@@ -495,6 +495,9 @@ module type Formulas = sig
   val _error : env -> 'a fragment -> 'a err -> _
   (** Raise an error *)
 
+  val _expected : env -> string -> Dolmen.Std.Term.t -> res option -> _
+  (** Helper to raise the [Expected] error. *)
+
   val suggest : limit:int -> env -> Dolmen.Std.Id.t -> Dolmen.Std.Id.t list
   (** From a dolmen identifier, return a list of existing bound identifiers
       in the env that are up to [~limit] in terms of distance of edition. *)