From 2378fc37aca0690505096b2f67aa1120c60cc0d8 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Tue, 4 Jan 2022 18:36:00 -0500
Subject: [PATCH] fix LIA->LRA cast operation

---
 src/base-solver/sidekick_base_solver.ml |  5 ++---
 src/base/Base_types.ml                  | 16 ++++++++--------
 src/smtlib/Typecheck.ml                 | 25 ++++++++++++++-----------
 3 files changed, 24 insertions(+), 22 deletions(-)

diff --git a/src/base-solver/sidekick_base_solver.ml b/src/base-solver/sidekick_base_solver.ml
index 0c493256..2ede3e4b 100644
--- a/src/base-solver/sidekick_base_solver.ml
+++ b/src/base-solver/sidekick_base_solver.ml
@@ -97,7 +97,7 @@ module Th_lra = Sidekick_arith_lra.Make(struct
     | LRA.LRA_simplex_pred (x,p,c) -> T.lra store (Arith_simplex_pred (x,p,c))
   let mk_bool = T.bool
 
-  let view_as_lra t = match T.view t with
+  let rec view_as_lra t = match T.view t with
     | T.LRA l ->
       let open Base_types in
       let module LRA = Sidekick_arith_lra in
@@ -108,8 +108,7 @@ module Th_lra = Sidekick_arith_lra.Make(struct
         | Arith_mult (c,x) -> LRA.LRA_mult (c,x)
         | Arith_simplex_var x -> LRA.LRA_simplex_var x
         | Arith_simplex_pred (x,p,c) -> LRA.LRA_simplex_pred(x,p,c)
-
-        | Arith_to_real x
+        | Arith_to_real x -> view_as_lra x
         | Arith_var x -> LRA.LRA_other x
       end
     | T.Eq (a,b) when Ty.equal (T.ty a) (Ty.real()) ->
diff --git a/src/base/Base_types.ml b/src/base/Base_types.ml
index 420eb1be..d7df7c1a 100644
--- a/src/base/Base_types.ml
+++ b/src/base/Base_types.ml
@@ -23,16 +23,16 @@ type ('num, 'a) arith_view =
   | Arith_simplex_pred of 'a * Sidekick_arith_lra.S_op.t * 'num
   | Arith_simplex_var of 'a
 
-let map_arith_view f (l:_ arith_view) : _ arith_view =
+let map_arith_view ~f_c f (l:_ arith_view) : _ arith_view =
   begin match l with
     | Arith_pred (p, a, b) -> Arith_pred (p, f a, f b)
     | Arith_op (p, a, b) -> Arith_op (p, f a, f b)
-    | Arith_mult (n,a) -> Arith_mult (n, f a)
-    | Arith_const q -> Arith_const q
+    | Arith_mult (n,a) -> Arith_mult (f_c n, f a)
+    | Arith_const c -> Arith_const (f_c c)
     | Arith_var x -> Arith_var (f x)
     | Arith_to_real x -> Arith_to_real (f x)
     | Arith_simplex_var v -> Arith_simplex_var (f v)
-    | Arith_simplex_pred (v, op, q) -> Arith_simplex_pred (f v, op, q)
+    | Arith_simplex_pred (v, op, c) -> Arith_simplex_pred (f v, op, f_c c)
   end
 
 let iter_arith_view f l : unit =
@@ -820,8 +820,8 @@ end = struct
     | Not u -> Not (f u)
     | Eq (a,b) -> Eq (f a, f b)
     | Ite (a,b,c) -> Ite (f a, f b, f c)
-    | LRA l -> LRA (map_arith_view f l)
-    | LIA l -> LIA (map_arith_view f l)
+    | LRA l -> LRA (map_arith_view ~f_c:CCFun.id f l)
+    | LIA l -> LIA (map_arith_view ~f_c:CCFun.id f l)
 end
 
 (** Term creation and manipulation *)
@@ -1158,8 +1158,8 @@ end = struct
     | Not u -> not_ tst (f u)
     | Eq (a,b) -> eq tst (f a) (f b)
     | Ite (a,b,c) -> ite tst (f a) (f b) (f c)
-    | LRA l -> lra tst (map_arith_view f l)
-    | LIA l -> lia tst (map_arith_view f l)
+    | LRA l -> lra tst (map_arith_view ~f_c:CCFun.id f l)
+    | LIA l -> lia tst (map_arith_view ~f_c:CCFun.id f l)
 
   let store_size tst = H.size tst.tbl
   let store_iter tst = H.to_iter tst.tbl
diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml
index e1568496..a138cd63 100644
--- a/src/smtlib/Typecheck.ml
+++ b/src/smtlib/Typecheck.ml
@@ -127,17 +127,20 @@ let is_real t =
 
 (* convert [t] to a real term *)
 let cast_to_real (ctx:Ctx.t) (t:T.t) : T.t =
-  match T.view t with
-  | T.LRA _ -> t
-  | _ when Ty.equal (T.ty t) (Ty.real()) -> t
-  | T.LIA (Arith_const n) ->
-    (* TODO: do that but for more general constant expressions *)
-    T.lra ctx.tst (Arith_const (Q.of_bigint n))
-  | T.LIA _ ->
-    (* insert implicit cast *)
-    T.lra ctx.tst (Arith_to_real t)
-  | _ ->
-    errorf_ctx ctx "cannot cast term to real@ :term %a" T.pp t
+  let rec conv t =
+    match T.view t with
+    | T.LRA _ -> t
+    | _ when Ty.equal (T.ty t) (Ty.real()) -> t
+    | T.LIA (Arith_const n) ->
+      T.lra ctx.tst (Arith_const (Q.of_bigint n))
+    | T.LIA l ->
+      (* try to convert the whole structure to reals *)
+      let l = Base_types.map_arith_view ~f_c:Q.of_bigint conv l in
+      T.lra ctx.tst l
+    | _ ->
+      errorf_ctx ctx "cannot cast term to real@ :term %a" T.pp t
+  in
+  conv t
 
 let conv_arith_op (ctx:Ctx.t) t (op:PA.arith_op) (l:T.t list) : T.t =
   let open Base_types in