simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-28 04:14:50 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix theory combination for LRA

Browse source
This commit is contained in:
Simon Cruanes 2022-01-05 11:59:50 -05:00
parent eb97161992
commit 849d4319f2
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
3 changed files with 10 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/arith/sidekick_arith.ml
View file

@ -50,6 +50,8 @@ module type RATIONAL = sig
val minus_infinity : t val minus_infinity : t
val of_bigint : bigint -> t
val is_real : t -> bool val is_real : t -> bool
(** A proper real, not nan/infinity *) (** A proper real, not nan/infinity *)

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

@ -98,6 +98,7 @@ module Th_lra = Sidekick_arith_lra.Make(struct
let mk_bool = T.bool let mk_bool = T.bool
let rec view_as_lra t = match T.view t with let rec view_as_lra t = match T.view t with
| T.LIA (Arith_const i) -> LRA.LRA_const (Q.of_bigint i)
| T.LRA l -> | T.LRA l ->
let open Base_types in let open Base_types in
let module LRA = Sidekick_arith_lra in let module LRA = Sidekick_arith_lra in

12
src/lra/sidekick_arith_lra.ml
View file

@ -630,11 +630,13 @@ module Make(A : ARG) : S with module A = A = struct
(* look for subterms of type Real, for they will need theory combination *) (* look for subterms of type Real, for they will need theory combination *)
let on_subterm (self:state) _ (t:T.t) : unit = let on_subterm (self:state) _ (t:T.t) : unit =
Log.debugf 50 (fun k->k "(@[lra.cc-on-subterm@ %a@])" T.pp t); Log.debugf 50 (fun k->k "(@[lra.cc-on-subterm@ %a@])" T.pp t);
if A.has_ty_real t && match A.view_as_lra t with
not (T.Tbl.mem self.needs_th_combination t) then ( | LRA_other _ when not (A.has_ty_real t) -> ()
Log.debugf 5 (fun k->k "(@[lra.needs-th-combination@ %a@])" T.pp t); | _ ->
T.Tbl.add self.needs_th_combination t () if not (T.Tbl.mem self.needs_th_combination t) then (
) Log.debugf 5 (fun k->k "(@[lra.needs-th-combination@ %a@])" T.pp t);
T.Tbl.add self.needs_th_combination t ()
)
let create_and_setup si = let create_and_setup si =
Log.debug 2 "(th-lra.setup)"; Log.debug 2 "(th-lra.setup)";