From c71be56df371ee7cc125c69996c2cb39a1d3f078 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Fri, 22 Mar 2024 22:37:38 +0100 Subject: [PATCH] fix(BV): Properly set fully interpreted operators Alt-Ergo calls "fully interpreted" symbols that are fully internalized in semantic values and do not need to be taken into consideration by the CC(X) algorithm (see function `congruents` in `ccx.ml`). (Note that `fully_interpreted` is only called for the Shostak theory associated with the symbol according to `is_min_symb`.) The BV theory incorrectly states that all its symbols are fully interpreted, including `bv2nat`, `int2bv`, etc.; however, only `concat`, `extract` and `bv2nat` are fully interpreted. This means that Alt-Ergo never performs congruence closure for these functions, leading to missed reasoning opportunities. --- src/lib/reasoners/bitv.ml | 5 ++++- src/lib/reasoners/sig.mli | 3 +++ 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml index e7f190e93..2ab1f9a1e 100644 --- a/src/lib/reasoners/bitv.ml +++ b/src/lib/reasoners/bitv.ml @@ -1464,7 +1464,10 @@ module Shostak(X : ALIEN) = struct let compare = compare_mine end) *) - let fully_interpreted _ = true + let fully_interpreted sb = + match sb with + | Sy.Op (Concat | Extract _ | BVnot) -> true + | _ -> false let term_extract _ = None, false diff --git a/src/lib/reasoners/sig.mli b/src/lib/reasoners/sig.mli index ef3d8170f..09be490e7 100644 --- a/src/lib/reasoners/sig.mli +++ b/src/lib/reasoners/sig.mli @@ -92,6 +92,9 @@ module type SHOSTAK = sig val print : Format.formatter -> t -> unit + (** return true if the symbol is fully interpreted by the theory, i.e. it + is fully embedded into semantic values and does not need term-level + congruence *) val fully_interpreted : Symbols.t -> bool val abstract_selectors : t -> (r * r) list -> r * (r * r) list