From 849d4319f2a7a768b43bfb27a0783ee7b36be5ae Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 5 Jan 2022 11:59:50 -0500 Subject: [PATCH] fix theory combination for LRA --- src/arith/sidekick_arith.ml | 2 ++ src/base-solver/sidekick_base_solver.ml | 1 + src/lra/sidekick_arith_lra.ml | 12 +++++++----- 3 files changed, 10 insertions(+), 5 deletions(-) diff --git a/src/arith/sidekick_arith.ml b/src/arith/sidekick_arith.ml index 30514110..c508b636 100644 --- a/src/arith/sidekick_arith.ml +++ b/src/arith/sidekick_arith.ml @@ -50,6 +50,8 @@ module type RATIONAL = sig val minus_infinity : t + val of_bigint : bigint -> t + val is_real : t -> bool (** A proper real, not nan/infinity *) diff --git a/src/base-solver/sidekick_base_solver.ml b/src/base-solver/sidekick_base_solver.ml index 2ede3e4b..887a0003 100644 --- a/src/base-solver/sidekick_base_solver.ml +++ b/src/base-solver/sidekick_base_solver.ml @@ -98,6 +98,7 @@ module Th_lra = Sidekick_arith_lra.Make(struct let mk_bool = T.bool 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 -> let open Base_types in let module LRA = Sidekick_arith_lra in diff --git a/src/lra/sidekick_arith_lra.ml b/src/lra/sidekick_arith_lra.ml index 1f9fdcfe..c5697b94 100644 --- a/src/lra/sidekick_arith_lra.ml +++ b/src/lra/sidekick_arith_lra.ml @@ -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 *) let on_subterm (self:state) _ (t:T.t) : unit = Log.debugf 50 (fun k->k "(@[lra.cc-on-subterm@ %a@])" T.pp t); - if A.has_ty_real t && - 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 () - ) + match A.view_as_lra t with + | LRA_other _ when not (A.has_ty_real 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 = Log.debug 2 "(th-lra.setup)";