[Draft] use algebraic number for reals

.github/workflows/install.yml

@@ -98,8 +98,21 @@ jobs:
     # Setup ocaml/opam
     - name: Setup ocaml/opam
       uses: avsm/setup-ocaml@v2
+      if: matrix.os != 'windows-latest'
       with:
         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
@@ -122,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
 

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"

src/interface/term.ml

@@ -1309,6 +1309,17 @@ 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
+  (** 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
 
 (** Signature required by terms for typing smtlib real_int arithmetic. *)

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 =

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)
 

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

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,8 +129,11 @@ 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) ->
+        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 -> 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)))
   | B.Sbv_to_fp (n, ew, prec) ->
@@ -156,7 +160,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) ->

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

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,60 @@ 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" ()
+
+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 *)
 (* ************************************************************************ *)
 
@@ -302,13 +363,28 @@ 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)
+    | 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 ->
       if reraise_for_delayed_eval
       then raise exn