simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-07 11:45:41 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix LIA->LRA cast operation

Browse source
This commit is contained in:
Simon Cruanes 2022-01-04 18:36:00 -05:00
parent 671fa6515a
commit 2378fc37ac
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
3 changed files with 24 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/base-solver/sidekick_base_solver.ml
View file

@ -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()) ->

16
src/base/Base_types.ml
View file

@ -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

25
src/smtlib/Typecheck.ml
View file

@ -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