simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-08 20:25:31 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix missing conversions

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

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

@ -103,7 +103,14 @@ module Th_lra = Sidekick_arith_lra.Make(struct
let module LRA = Sidekick_arith_lra in
begin match l with
| Arith_const c -> LRA.LRA_const c
| _ -> assert false
| Arith_pred (p,a,b) -> LRA.LRA_pred(p,a,b)
| Arith_op(op,a,b) -> LRA.LRA_op(op,a,b)
| 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_var x -> LRA.LRA_other x
end
| T.Eq (a,b) when Ty.equal (T.ty a) (Ty.real()) ->
LRA.LRA_pred (Eq, a, b)

12
src/smtlib/Typecheck.ml
View file

@ -203,8 +203,16 @@ let conv_arith_op (ctx:Ctx.t) t (op:PA.arith_op) (l:T.t list) : T.t =
errorf_ctx ctx "cannot handle non-linear div %a" PA.pp_term t
end
| PA.Div, _ ->
errorf_ctx ctx "cannot handle integer div %a" PA.pp_term t
| PA.Div, [a;b] ->
(* becomes a real *)
begin match t_as_q a, t_as_q b with
| Some a, Some b -> T.lra tst (Arith_const (Q.div a b))
| _, Some b ->
let a = cast_to_real ctx a in
T.lra tst (Arith_mult (Q.inv b, a))
| _, None ->
errorf_ctx ctx "cannot handle non-linear div %a" PA.pp_term t
end
| _ ->
errorf_ctx ctx "cannot handle arith construct %a" PA.pp_term t