wip: representing real types and values

src/base-term/Base_types.ml

@@ -60,6 +60,7 @@ and ty = {
 
 and ty_view =
   | Ty_bool
+  | Ty_real
   | Ty_atomic of {
       def: ty_def;
       args: ty list;
@@ -116,6 +117,7 @@ and value =
       eq: value_custom_view -> value_custom_view -> bool;
       hash: value_custom_view -> int;
     } (** Custom value *)
+  | V_real of Q.t
 
 and value_custom_view = ..
 
@@ -157,7 +159,8 @@ let rec eq_value a b = match a, b with
   | V_cstor x1, V_cstor x2 ->
     eq_cstor x1.c x2.c &&
     CCList.equal eq_value x1.args x2.args
-  | (V_bool _ | V_element _ | V_custom _ | V_cstor _), _
+  | V_real a, V_real b -> Q.equal a b
+  | (V_bool _ | V_element _ | V_custom _ | V_cstor _ | V_real _), _
     -> false
 
 let rec hash_value a = match a with
@@ -166,6 +169,7 @@ let rec hash_value a = match a with
   | V_custom x -> x.hash x.view
   | V_cstor x ->
     Hash.combine3 42 (ID.hash x.c.cstor_id) (Hash.list hash_value x.args)
+  | V_real x -> Hash.combine3 50 (Z.hash @@ Q.num x) (Z.hash @@ Q.den x)
 
 let rec pp_value out = function
   | V_bool b -> Fmt.bool out b
@@ -174,11 +178,13 @@ let rec pp_value out = function
   | V_cstor {c;args=[]} -> ID.pp out c.cstor_id
   | V_cstor {c;args} ->
     Fmt.fprintf out "(@[%a@ %a@])" ID.pp c.cstor_id (Util.pp_list pp_value) args
+  | V_real x -> Q.pp_print out x
 
 let pp_db out (i,_) = Format.fprintf out "%%%d" i
 
 let rec pp_ty out t = match t.ty_view with
   | Ty_bool -> Fmt.string out "Bool"
+  | Ty_real -> Fmt.string out "Real"
   | Ty_atomic {def=Ty_uninterpreted id; args=[]; _} -> ID.pp out id
   | Ty_atomic {def=Ty_uninterpreted id; args; _} ->
     Fmt.fprintf out "(@[%a@ %a@])" ID.pp id (Util.pp_list pp_ty) args
@@ -214,6 +220,7 @@ module Ty : sig
   type t = ty
   type view = ty_view =
     | Ty_bool
+    | Ty_real
     | Ty_atomic of {
       def: ty_def;
       args: ty list;
@@ -235,6 +242,7 @@ module Ty : sig
   val view : t -> view
 
   val bool : t
+  val real : t
   val atomic : def -> t list -> t
 
   val atomic_uninterpreted : ID.t -> t
@@ -268,6 +276,7 @@ end = struct
   type t = ty
   type view = ty_view =
     | Ty_bool
+    | Ty_real
     | Ty_atomic of {
       def: ty_def;
       args: ty list;
@@ -302,13 +311,15 @@ end = struct
       type t = ty
       let equal a b = match a.ty_view, b.ty_view with
         | Ty_bool, Ty_bool -> true
+        | Ty_real, Ty_real -> true
         | Ty_atomic a1, Ty_atomic a2 ->
           equal_def a1.def a2.def && CCList.equal equal a1.args a2.args
-        | Ty_bool, _ | Ty_atomic _, _
+        | (Ty_bool | Ty_atomic _ | Ty_real), _
           -> false
 
       let hash t = match t.ty_view with
         | Ty_bool -> 1
+        | Ty_real -> 2
         | Ty_atomic {def=Ty_uninterpreted id; args; _} ->
           Hash.combine3 10 (ID.hash id) (Hash.list hash args)
         | Ty_atomic {def=Ty_def d; args; _} ->
@@ -330,13 +341,15 @@ end = struct
 
   let finite t = match view t with
     | Ty_bool -> true
+    | Ty_real -> false
     | Ty_atomic {finite=f; _} -> f
 
   let set_finite t b = match view t with
-    | Ty_bool -> assert false
+    | Ty_bool | Ty_real -> assert false
     | Ty_atomic r -> r.finite <- b
 
   let bool = make_ Ty_bool
+  let real = make_ Ty_real
 
   let atomic def args : t =
     make_ (Ty_atomic {def; args; finite=true;})
@@ -598,7 +611,7 @@ end = struct
     | Ite (_, b, _) -> b.term_ty
     | App_fun (f, args) ->
       begin match Fun.view f with
-        | Fun_undef fty -> 
+        | Fun_undef fty ->
           let ty_args, ty_ret = Ty.Fun.unfold fty in
           (* check arity *)
           if List.length ty_args <> IArray.length args then (
@@ -880,10 +893,13 @@ module Value : sig
         eq: value_custom_view -> value_custom_view -> bool;
         hash: value_custom_view -> int;
       }
+    | V_real of Q.t
 
   val true_ : t
   val false_ : t
   val bool : bool -> t
+  val real : Q.t -> t
+  val real_of_string : string -> t
 
   val mk_elt : ID.t -> Ty.t -> t
 
@@ -911,10 +927,13 @@ end = struct
         eq: value_custom_view -> value_custom_view -> bool;
         hash: value_custom_view -> int;
       }
+    | V_real of Q.t
 
   let true_ = V_bool true
   let false_ = V_bool false
   let[@inline] bool v = if v then true_ else false_
+  let real x = V_real x
+  let real_of_string x = V_real (Q.of_string x)
 
   let mk_elt id ty : t = V_element {id; ty}
 

src/base-term/dune

@@ -2,5 +2,5 @@
  (name sidekick_base_term)
  (public_name sidekick.base-term)
  (synopsis "Basic term definitions for the standalone SMT solver")
- (libraries containers sidekick.core sidekick.util)
+ (libraries containers sidekick.core sidekick.util zarith)
  (flags :standard -w -32 -open Sidekick_util))

src/smtlib/Process.ml

@@ -1,5 +1,6 @@
 (** {2 Conversion into {!Term.t}} *)
 
+module BT = Sidekick_base_term
 open Sidekick_base_term
 
 [@@@ocaml.warning "-32"]
@@ -270,7 +271,7 @@ module Th_data = Sidekick_th_data.Make(struct
         Ty_data {cstors=Lazy.force data.data.data_cstors |> ID.Map.values}
       | Ty_atomic {def=_;args;finite=_} ->
         Ty_app{args=Iter.of_list args}
-      | Ty_bool -> Ty_app {args=Iter.empty}
+      | Ty_bool | Ty_real -> Ty_app {args=Iter.empty}
 
     let view_as_data t = match Term.view t with
       | Term.App_fun ({fun_view=Fun.Fun_cstor c;_}, args) -> T_cstor (c, args)
@@ -303,6 +304,7 @@ end)
 
 module Th_lra = Sidekick_lra.Make(struct
   module S = Solver
+  module T = S.T.Term
   type term = S.T.Term.t
 
   let view_as_lra _ = assert false (* TODO *)
@@ -321,7 +323,7 @@ module Th_lra = Sidekick_lra.Make(struct
       let name = Printf.sprintf "_sk_lra_%s%d" pre self.fresh in
       self.fresh <- 1 + self.fresh;
       let id = ID.make name in
-      T.const self.tst @@ Fun.mk_undef_const id ty
+      BT.Term.const self.tst @@ Fun.mk_undef_const id ty
   end
 end)
 

src/smtlib/Typecheck.ml

@@ -88,14 +88,7 @@ let find_id_ ctx (s:string): ID.t * Ctx.kind =
 (* parse a type *)
 let rec conv_ty ctx (t:PA.ty) : Ty.t = match t with
   | PA.Ty_bool -> Ty.bool
-  | PA.Ty_real ->
-    ill_typed ctx "cannot handle reals for now"
-      (* FIXME
-    Ty.rat, Ctx.K_ty Ctx.K_other
-         *) 
-  | PA.Ty_app ("Rat",[]) ->
-    ill_typed ctx "cannot handle reals for now"
-    (* TODO A.Ty.rat, Ctx.K_ty Ctx.K_other *)
+  | PA.Ty_real -> Ty.real
   | PA.Ty_app ("Int",[]) ->
     ill_typed ctx "cannot handle ints for now"
     (* TODO: A.Ty.int , Ctx.K_ty Ctx.K_other *)
@@ -158,7 +151,7 @@ let rec conv_term (ctx:Ctx.t) (t:PA.term) : T.t =
     Ctx.with_lets ctx bs (fun () -> conv_term ctx body)
   | PA.Distinct l ->
     let l = List.map (conv_term ctx) l in
-    Form.distinct_l tst l 
+    Form.distinct_l tst l
   | PA.And l ->
     let l = List.map (conv_term ctx) l in
     Form.and_l tst l