Model support algebraic number

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

   Error path should be improved

src/interface/term.ml

@@ -1176,7 +1176,8 @@ module type Smtlib_Real = sig
   val div : t -> t -> t
   (** Real division. See Smtlib theory for a full description. *)
 
-  val root_of_with_order : string list -> string -> t
+  val algebraic_ordered_root : string list -> string -> t
+  val algebraic_enclosed_root : string list -> (string * string) -> (string * string) -> t
 
 end
 

src/model/real.ml

@@ -163,21 +163,27 @@ module A = struct
 
   let from_order poly order =
     let poly = Flint.FMPZ_poly.create poly in
-    let roots = Calcium.QQBAR.from_roots poly in
-    !!(Calcium.CA.from_qqbar ~ctx (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 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"
+    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
 
 
@@ -247,11 +253,17 @@ let op2_zero ~eval ~env ~cst f =
 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.Root_of_with_order {coeffs; order} ->
+  | 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.Lt `Real -> cmp ~cst A.lt
+  | 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

src/standard/builtin.ml

@@ -62,11 +62,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
-  | Root_of_with_order of { coeffs: string list; order: 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

src/standard/builtin.mli

@@ -165,6 +165,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. *)
@@ -193,7 +197,7 @@ type _ t +=
       representation for the real number [2].
 
       Real literals can be parsed using ZArith's [Q.of_string]. *)
-  | Root_of_with_order of { coeffs: string list; order: string }
+  | Algebraic of algebraic
   | Lt of [ `Int | `Rat | `Real ]
   (** [Lt: {a=(Int|Rational|Real)} a -> a -> Prop]:
       strict comparison (less than) on numbers

src/standard/expr.ml

@@ -2072,13 +2072,51 @@ module Term = struct
             mk' ~builtin:(Builtin.Decimal s) s [] [] Ty.real
           )
 
-      let root_of_with_order =
+      let algebraic_ordered_root =
         let cache = Hashtbl.create 113 in
         fun coeffs order ->
             with_cache ~cache (fun (coeffs,order) ->
-                mk' ~builtin:(Builtin.Root_of_with_order {coeffs;order}) "algebraic" [] [] Ty.real
+              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)
@@ -3252,8 +3290,10 @@ module Term = struct
 
   module Real = struct
     let mk = real
-    let root_of_with_order coeffs order =
-      apply_cst (Const.Real.root_of_with_order coeffs order) [] []
+    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]

src/standard/expr.mli

@@ -1037,8 +1037,15 @@ module Term : sig
       val real : string -> t
       (** Real literals. *)
 
-      val root_of_with_order : string list -> string -> t
-      (** Algebraic number *)
+      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. *)

src/typecheck/arith.ml

@@ -836,7 +836,42 @@ module Smtlib2 = struct
         | Warn msg -> Type._warn env (Ast ast) (Restriction msg)
         | Error msg -> Type._error env (Ast ast) (Forbidden msg)
 
-      let parse_coeffs _ = ["-2";"0";"1"]
+      let parse_int env ast =
+        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
+        | _ ->
+          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 ~arith version env s =
         match s with
@@ -847,18 +882,21 @@ module Smtlib2 = struct
         | 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"; } ->
-            Type.builtin_term (Base.make_op2 (module Type) env s (fun _ast (coeffs,num) ->
-              let coeffs = match coeffs.term with
-                | App ({term = Symbol {Id.ns = Term; name = Simple "coeffs"}; _},args) ->
-                  parse_coeffs args
-                | _ -> assert false
-              in
-              let num = match num.term with
-                | Symbol  { Id.ns = Value (Integer); name = Simple name; } ->
-                    name
-                | _ -> assert false
-              in
-              T.root_of_with_order coeffs num )
+          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"; } ->
+            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; } ->

tests/model/real/algebraic.rsmt2

@@ -1,4 +1,6 @@
 sat
 (
 (define-fun sqrt2 () Real (root-of-with-order (coeffs (- 2) 0 1) 1))
+(define-fun sqrt3 () Real (root-of-with-enclosure (coeffs (- 3) 0 1) 1.0 2.0))
+(define-fun sqrt4 () Real (root-of-with-enclosure (coeffs (- 4) 0 1) (/ (- 1.0) 2.0) (/ 5.0 2.0)))
 )

tests/model/real/algebraic.smt2

@@ -1,4 +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)