From ac4ca6776b5a941992fd63a2a91776af83543bda Mon Sep 17 00:00:00 2001 From: Pierrot Date: Fri, 5 Apr 2024 19:05:52 +0200 Subject: [PATCH] Fix soudness bug in Enum (#1091) The PR #1078 introduces a soundness bug in `assume_distinct`. We have to propagate explanations of singleton domains, otherwise we may raise Inconsistency with an empty explanation. Add a test that caught the bug. --- src/lib/reasoners/enum_rel.ml | 18 +- tests/dune.inc | 292 +++++++++++++++++++++++++++++ tests/sum/testfile-sum019.ae | 15 ++ tests/sum/testfile-sum019.expected | 2 + 4 files changed, 319 insertions(+), 8 deletions(-) create mode 100644 tests/sum/testfile-sum019.ae create mode 100644 tests/sum/testfile-sum019.expected diff --git a/src/lib/reasoners/enum_rel.ml b/src/lib/reasoners/enum_rel.ml index ba2437873..db5a75faa 100644 --- a/src/lib/reasoners/enum_rel.ml +++ b/src/lib/reasoners/enum_rel.ml @@ -51,9 +51,9 @@ module Domain = struct let[@inline always] choose { constrs; _ } = HSS.choose constrs - let[@inline always] as_singleton { constrs; _ } = + let[@inline always] as_singleton { constrs; ex } = if HSS.cardinal constrs = 1 then - Some (HSS.choose constrs) + Some (HSS.choose constrs, ex) else None @@ -128,10 +128,10 @@ module Domains = struct let get r t = match Th.embed r with - | Cons (r, _) -> + | Cons (c, _) -> (* For sake of efficiency, we don't look in the map if the semantic value is a constructor. *) - Domain.singleton ~ex:Explanation.empty r + Domain.singleton ~ex:Explanation.empty c | _ -> try MX.find r t.domains with Not_found -> @@ -297,14 +297,16 @@ let assume_distinct ~ex r1 r2 env = let d2 = Domains.get r2 env.domains in let env = match Domain.as_singleton d1 with - | Some c -> + | Some (c, ex1) -> + let ex = Ex.union ex1 ex in let nd = Domain.remove ~ex c d2 in tighten_domain r2 nd env | None -> env in match Domain.as_singleton d2 with - | Some c -> + | Some (c, ex2) -> + let ex = Ex.union ex2 ex in let nd = Domain.remove ~ex c d1 in tighten_domain r1 nd env | None -> @@ -364,9 +366,9 @@ let propagate_domains env = Domains.propagate (fun eqs rr d -> match Domain.as_singleton d with - | Some c -> + | Some (c, ex) -> let nr = Th.is_mine (Cons (c, X.type_info rr)) in - let eq = Literal.LSem (LR.mkv_eq rr nr), d.ex, Th_util.Other in + let eq = Literal.LSem (LR.mkv_eq rr nr), ex, Th_util.Other in eq :: eqs | None -> eqs diff --git a/tests/dune.inc b/tests/dune.inc index afb3e4513..abae5c9ea 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -223883,6 +223883,298 @@ (package alt-ergo) (action (diff testfile-sum_poly_arrays001.expected testfile-sum_poly_arrays001_fpa.output))) + (rule + (target testfile-sum019_optimize.output) + (deps (:input testfile-sum019.ae)) + (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 + --optimize + %{input}))))))) + (rule + (deps testfile-sum019_optimize.output) + (alias runtest) + (package alt-ergo) + (action + (diff testfile-sum019.expected testfile-sum019_optimize.output))) + (rule + (target testfile-sum019_ci_cdcl_no_minimal_bj.output) + (deps (:input testfile-sum019.ae)) + (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-sum019_ci_cdcl_no_minimal_bj.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff testfile-sum019.expected testfile-sum019_ci_cdcl_no_minimal_bj.output))) + (rule + (target testfile-sum019_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input testfile-sum019.ae)) + (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-sum019_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff testfile-sum019.expected testfile-sum019_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) + (rule + (target testfile-sum019_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input testfile-sum019.ae)) + (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-sum019_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff testfile-sum019.expected testfile-sum019_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) + (rule + (target testfile-sum019_ci_no_tableaux_cdcl_in_instantiation.output) + (deps (:input testfile-sum019.ae)) + (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-sum019_ci_no_tableaux_cdcl_in_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff testfile-sum019.expected testfile-sum019_ci_no_tableaux_cdcl_in_instantiation.output))) + (rule + (target testfile-sum019_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (deps (:input testfile-sum019.ae)) + (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-sum019_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff testfile-sum019.expected testfile-sum019_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) + (rule + (target testfile-sum019_ci_tableaux_cdcl_no_minimal_bj.output) + (deps (:input testfile-sum019.ae)) + (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-sum019_ci_tableaux_cdcl_no_minimal_bj.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff testfile-sum019.expected testfile-sum019_ci_tableaux_cdcl_no_minimal_bj.output))) + (rule + (target testfile-sum019_cdcl.output) + (deps (:input testfile-sum019.ae)) + (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-sum019_cdcl.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-sum019.expected testfile-sum019_cdcl.output))) + (rule + (target testfile-sum019_tableaux_cdcl.output) + (deps (:input testfile-sum019.ae)) + (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-sum019_tableaux_cdcl.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-sum019.expected testfile-sum019_tableaux_cdcl.output))) + (rule + (target testfile-sum019_tableaux.output) + (deps (:input testfile-sum019.ae)) + (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-sum019_tableaux.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-sum019.expected testfile-sum019_tableaux.output))) + (rule + (target testfile-sum019_legacy.output) + (deps (:input testfile-sum019.ae)) + (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 legacy + %{input}))))))) + (rule + (deps testfile-sum019_legacy.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-sum019.expected testfile-sum019_legacy.output))) + (rule + (target testfile-sum019_dolmen.output) + (deps (:input testfile-sum019.ae)) + (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-sum019_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-sum019.expected testfile-sum019_dolmen.output))) + (rule + (target testfile-sum019_fpa.output) + (deps (:input testfile-sum019.ae)) + (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-sum019_fpa.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-sum019.expected testfile-sum019_fpa.output))) (rule (target testfile-sum018_optimize.output) (deps (:input testfile-sum018.ae)) diff --git a/tests/sum/testfile-sum019.ae b/tests/sum/testfile-sum019.ae new file mode 100644 index 000000000..e360cd670 --- /dev/null +++ b/tests/sum/testfile-sum019.ae @@ -0,0 +1,15 @@ +type house = H1 | H2 | H3 | H4 + +logic h1, h2 : house + +predicate leftof(h1: house, h2: house) = + (h2 = H2 -> h1 <> H2 and h1 <> H3 and h1 <> H4) (* h1 = H1 *) + and + (h2 = H3 -> h1 <> H1 and h1 <> H3 and h1 <> H4) (* h1 = H2 *) + and + (h2 = H4 -> h1 <> H1 and h1 <> H2 and h1 <> H4) (* h1 = H3 *) + and + (h2 = H1 -> h1 <> H1 and h1 <> H2 and h1 <> H3) (* h1 = H4 *) + +axiom clue : leftof(h1, h2) +goal g : false diff --git a/tests/sum/testfile-sum019.expected b/tests/sum/testfile-sum019.expected new file mode 100644 index 000000000..a6e005255 --- /dev/null +++ b/tests/sum/testfile-sum019.expected @@ -0,0 +1,2 @@ + +unknown