From 7363cd05a0b3af10a6a6b98738ee0810899052b2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= <129742207+bclement-ocp@users.noreply.github.com> Date: Fri, 24 Nov 2023 15:56:19 +0000 Subject: [PATCH] fix(BV): Do not call [X.make] on non-subterm, reloaded (#969) This is a follow-up to https://github.com/OCamlPro/alt-ergo/pull/954 Somehow convinced myself that the cases where we perform simplifications were fine because we would only be simplifying into a subterm, but that is obviously not the case due to negation. Let's just do the safe thing and always return the original term with the appropriate equalities. All of this code should be removed in favor of doing these computations in the relations instead anyways, which would make sure we always treat [bv2nat] in the same way for literals and after substitution (see also https://github.com/OCamlPro/alt-ergo/issues/824 ) --- src/lib/reasoners/bitv.ml | 38 ++-- tests/bitv/testfile-bitv025.expected | 2 + tests/bitv/testfile-bitv025.smt2 | 5 + tests/dune.inc | 249 +++++++++++++++++++++++++++ 4 files changed, 276 insertions(+), 18 deletions(-) create mode 100644 tests/bitv/testfile-bitv025.expected create mode 100644 tests/bitv/testfile-bitv025.smt2 diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml index 54821c23f..07d254876 100644 --- a/src/lib/reasoners/bitv.ml +++ b/src/lib/reasoners/bitv.ml @@ -1324,24 +1324,26 @@ module Shostak(X : ALIEN) = struct let maybe_negate t = if negated then E.Ints.(~$$Z.(~$1 lsl sz - ~$1) - t) else t in - begin match E.term_view t with - | { f = Op Int2BV _; _ } -> - (* bv2nat will simplify: we must call [X.make] again *) - E.BV.bv2nat t |> maybe_negate |> X.make - | { ty = Tbitv n; _ } -> - assert (n = sz); - if negated then - (* if we are negated, we will simplify *) - E.BV.bv2nat t |> maybe_negate |> X.make - else - (* bv2nat will *not* simplify: become uninterpreted with interval - information *) - let t = E.BV.bv2nat t |> maybe_negate in - X.term_embed t, - [ E.Ints.(~$0 <= t) ; E.Ints.(t < ~$$Z.(~$1 lsl n)) ] - | { ty; _ } -> - Util.internal_error "expected bitv, got %a" Ty.print ty - end + let t', ctx = + begin match E.term_view t with + | { f = Op Int2BV _; _ } -> + (* bv2nat will simplify: we must call [X.make] again *) + E.BV.bv2nat t |> maybe_negate, [] + | { ty = Tbitv n; _ } -> + assert (n = sz); + if negated then + (* if we are negated, we will simplify *) + E.BV.bv2nat t |> maybe_negate, [] + else + (* bv2nat will *not* simplify: become uninterpreted with interval + information *) + let t = E.BV.bv2nat t |> maybe_negate in + t, [ E.Ints.(~$0 <= t) ; E.Ints.(t < ~$$Z.(~$1 lsl n)) ] + | { ty; _ } -> + Util.internal_error "expected bitv, got %a" Ty.print ty + end + in + X.term_embed ot, E.Core.eq ot t' :: ctx | _ -> (* Note: we can't just call [X.make] on the result of [abstract_to_nat] because [X.make] should only be called on subterms. If we do it, it diff --git a/tests/bitv/testfile-bitv025.expected b/tests/bitv/testfile-bitv025.expected new file mode 100644 index 000000000..a6e005255 --- /dev/null +++ b/tests/bitv/testfile-bitv025.expected @@ -0,0 +1,2 @@ + +unknown diff --git a/tests/bitv/testfile-bitv025.smt2 b/tests/bitv/testfile-bitv025.smt2 new file mode 100644 index 000000000..0463dfef1 --- /dev/null +++ b/tests/bitv/testfile-bitv025.smt2 @@ -0,0 +1,5 @@ +(set-logic QF_BV) +(declare-fun s () (_ BitVec 32)) +(declare-fun t () (_ BitVec 32)) +(assert (= (bvshl s (bvnot (bvmul s t))) (_ bv0 32))) +(check-sat) diff --git a/tests/dune.inc b/tests/dune.inc index fbfb00957..dad2dd8b3 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -120886,6 +120886,255 @@ (package alt-ergo) (action (diff testfile-bv2nat-delayed.dolmen.expected testfile-bv2nat-delayed.dolmen_dolmen.output))) + (rule + (target testfile-bitv025_ci_cdcl_no_minimal_bj.output) + (deps (:input testfile-bitv025.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL + --no-minimal-bj + %{input}))))))) + (rule + (deps testfile-bitv025_ci_cdcl_no_minimal_bj.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff testfile-bitv025.expected testfile-bitv025_ci_cdcl_no_minimal_bj.output))) + (rule + (target testfile-bitv025_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input testfile-bitv025.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-minimal-bj + --no-tableaux-cdcl-in-theories + --no-tableaux-cdcl-in-instantiation + %{input}))))))) + (rule + (deps testfile-bitv025_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff testfile-bitv025.expected testfile-bitv025_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) + (rule + (target testfile-bitv025_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input testfile-bitv025.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-theories + --no-tableaux-cdcl-in-instantiation + %{input}))))))) + (rule + (deps testfile-bitv025_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff testfile-bitv025.expected testfile-bitv025_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) + (rule + (target testfile-bitv025_ci_no_tableaux_cdcl_in_instantiation.output) + (deps (:input testfile-bitv025.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-instantiation + %{input}))))))) + (rule + (deps testfile-bitv025_ci_no_tableaux_cdcl_in_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff testfile-bitv025.expected testfile-bitv025_ci_no_tableaux_cdcl_in_instantiation.output))) + (rule + (target testfile-bitv025_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (deps (:input testfile-bitv025.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-theories + %{input}))))))) + (rule + (deps testfile-bitv025_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff testfile-bitv025.expected testfile-bitv025_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) + (rule + (target testfile-bitv025_ci_tableaux_cdcl_no_minimal_bj.output) + (deps (:input testfile-bitv025.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-minimal-bj + %{input}))))))) + (rule + (deps testfile-bitv025_ci_tableaux_cdcl_no_minimal_bj.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff testfile-bitv025.expected testfile-bitv025_ci_tableaux_cdcl_no_minimal_bj.output))) + (rule + (target testfile-bitv025_cdcl.output) + (deps (:input testfile-bitv025.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL + %{input}))))))) + (rule + (deps testfile-bitv025_cdcl.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-bitv025.expected testfile-bitv025_cdcl.output))) + (rule + (target testfile-bitv025_tableaux_cdcl.output) + (deps (:input testfile-bitv025.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux-CDCL + %{input}))))))) + (rule + (deps testfile-bitv025_tableaux_cdcl.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-bitv025.expected testfile-bitv025_tableaux_cdcl.output))) + (rule + (target testfile-bitv025_tableaux.output) + (deps (:input testfile-bitv025.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux + %{input}))))))) + (rule + (deps testfile-bitv025_tableaux.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-bitv025.expected testfile-bitv025_tableaux.output))) + (rule + (target testfile-bitv025_dolmen.output) + (deps (:input testfile-bitv025.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) + (rule + (deps testfile-bitv025_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-bitv025.expected testfile-bitv025_dolmen.output))) + (rule + (target testfile-bitv025_fpa.output) + (deps (:input testfile-bitv025.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 0) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --enable-theories fpa + %{input}))))))) + (rule + (deps testfile-bitv025_fpa.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-bitv025.expected testfile-bitv025_fpa.output))) (rule (target testfile-bitv024_ci_cdcl_no_minimal_bj.output) (deps (:input testfile-bitv024.smt2))