From 671fa6515a3b3808d180060b8d9c57f1abf56fd8 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 4 Jan 2022 18:25:28 -0500 Subject: [PATCH] fix missing conversions --- src/base-solver/sidekick_base_solver.ml | 9 ++++++++- src/smtlib/Typecheck.ml | 12 ++++++++++-- 2 files changed, 18 insertions(+), 3 deletions(-) diff --git a/src/base-solver/sidekick_base_solver.ml b/src/base-solver/sidekick_base_solver.ml index ced4f0a8..0c493256 100644 --- a/src/base-solver/sidekick_base_solver.ml +++ b/src/base-solver/sidekick_base_solver.ml @@ -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) diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml index b9e81a39..e1568496 100644 --- a/src/smtlib/Typecheck.ml +++ b/src/smtlib/Typecheck.ml @@ -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