From 6630b314c8efd87a35400f450117cc3e41173949 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Fri, 15 Sep 2023 12:51:48 +0200 Subject: [PATCH] Preserve mapping between old and new representatives with AC symbols In CC(X), the leaves are always terms that were present in the original problem: we do not introduce new uninterpreted terms. In AC(X), this is no longer true: we might introduce new AC leaves dynamically that are not themselves term representatives (i.e. they don't have an entry in the `repr` map) through "deep" rewriting into the AC leaf. When we have a class representative `rr` for a semantic value `r`, and a new class representative `nrr` is found, the relations see an equality (with `Subst` origin) `r = nrr`. Normally, since `rr` is a term representative, we have `rr --> rr` as a mapping, and so the relation will see `rr = nrr` and can use this to update its internal state. With these "dynamic" representative, when they later get override by a new representative, the relations will *not* see an `rr = nrr` equality, which makes its internal state get out of sync and can cause bugs. This patch makes it so that, when we encounter one of these "dynamic" representatives, we artificially add the `rr = nrr` equality (by adding `rr --> nrr` as a pivot, which will in turn cause the equality to show up). Since this case should only be possible with AC rewriting, the `rr = nrr` equality is only added in `up_uf_rs`, i.e. if there are AC rewrite rules. Fixes #474 --- src/lib/reasoners/uf.ml | 27 +++- tests/dune.inc | 264 ++++++++++++++++++++++++++++++++++++++ tests/issues/474.ae | 12 ++ tests/issues/474.expected | 2 + 4 files changed, 301 insertions(+), 4 deletions(-) create mode 100644 tests/issues/474.ae create mode 100644 tests/issues/474.expected diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml index b16f6a854..de33e7817 100644 --- a/src/lib/reasoners/uf.ml +++ b/src/lib/reasoners/uf.ml @@ -683,8 +683,8 @@ module Env = struct let up_uf_rs dep env tch = if RS.is_empty env.ac_rs then env, tch else - let env, tch, neqs_to_up = MapX.fold - (fun r (rr,ex) ((env, tch, neqs_to_up) as acc) -> + let env, tch, neqs_to_up, to_up = MapX.fold + (fun r (rr,ex) ((env, tch, neqs_to_up, to_up) as acc) -> Options.exec_thread_yield (); let nrr, ex_nrr = normal_form env rr in if X.equal nrr rr then acc @@ -699,8 +699,27 @@ module Env = struct if X.is_a_leaf r then (r,[r, nrr, ex],nrr) :: tch else tch in - env, tch, SetXX.add (rr, nrr) neqs_to_up - ) env.repr (env, tch, SetXX.empty) + (* With AC symbols, we can have r --> rr with rr not appearing in + repr (e.g. [rr = f(0, 0)] when the initial term was + [f(zero, zero)] with [zero --> 0]). + + This means that the mapping [rr --> nrr] will not appear in + [tch], which will confuse the relations. + + Hence, when a new mapping r --> nrr is introduced, we manually + add rr --> nrr as a PIVOT in this case. *) + let to_up = + match X.ac_extract rr with + | Some _ when not (MapX.mem rr env.repr) -> + MapX.add rr (nrr, ex_nrr) to_up + | _ -> to_up + in + env, tch, SetXX.add (rr, nrr) neqs_to_up, to_up + ) env.repr (env, tch, SetXX.empty, MapX.empty) + in + let tch = + MapX.fold (fun rr (nrr, ex) tch -> + (rr, [rr, nrr, ex], nrr) :: tch) to_up tch in (* Correction : Do not update neqs twice for the same r *) update_aux dep neqs_to_up env, tch diff --git a/tests/dune.inc b/tests/dune.inc index b94a3f7f2..0799b087b 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -179829,6 +179829,270 @@ (package alt-ergo) (action (diff 479.expected 479_fpa.output))) + (rule + (target 474_ci_cdcl_no_minimal_bj.output) + (deps (:input 474.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL + --no-minimal-bj + %{input}))))))) + (rule + (alias runtest-ci) + (package alt-ergo) + (action + (diff 474.expected 474_ci_cdcl_no_minimal_bj.output))) + (rule + (target 474_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input 474.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 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 + (alias runtest-ci) + (package alt-ergo) + (action + (diff + 474.expected + 474_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) + (rule + (target 474_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input 474.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 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 + (alias runtest-ci) + (package alt-ergo) + (action + (diff + 474.expected + 474_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) + (rule + (target 474_ci_no_tableaux_cdcl_in_instantiation.output) + (deps (:input 474.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-instantiation + %{input}))))))) + (rule + (alias runtest-ci) + (package alt-ergo) + (action + (diff 474.expected 474_ci_no_tableaux_cdcl_in_instantiation.output))) + (rule + (target 474_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (deps (:input 474.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-theories + %{input}))))))) + (rule + (alias runtest-ci) + (package alt-ergo) + (action + (diff + 474.expected + 474_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) + (rule + (target 474_ci_tableaux_cdcl_no_minimal_bj.output) + (deps (:input 474.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-minimal-bj + %{input}))))))) + (rule + (alias runtest-ci) + (package alt-ergo) + (action + (diff 474.expected 474_ci_tableaux_cdcl_no_minimal_bj.output))) + (rule + (target 474_cdcl.output) + (deps (:input 474.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL + %{input}))))))) + (rule + (alias runtest-quick) + (package alt-ergo) + (action + (diff 474.expected 474_cdcl.output))) + (rule + (target 474_tableaux_cdcl.output) + (deps (:input 474.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux-CDCL + %{input}))))))) + (rule + (alias runtest-quick) + (package alt-ergo) + (action + (diff 474.expected 474_tableaux_cdcl.output))) + (rule + (target 474_tableaux.output) + (deps (:input 474.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux + %{input}))))))) + (rule + (alias runtest-quick) + (package alt-ergo) + (action + (diff 474.expected 474_tableaux.output))) + (rule + (target 474_legacy.output) + (deps (:input 474.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend legacy + %{input}))))))) + (rule + (alias runtest-quick) + (package alt-ergo) + (action + (diff 474.expected 474_legacy.output))) + (rule + (target 474_dolmen.output) + (deps (:input 474.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) + (rule + (alias runtest-quick) + (package alt-ergo) + (action + (diff 474.expected 474_dolmen.output))) + (rule + (target 474_fpa.output) + (deps (:input 474.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --enable-theories fpa + %{input}))))))) + (rule + (alias runtest-quick) + (package alt-ergo) + (action + (diff 474.expected 474_fpa.output))) (rule (target 460_ci_cdcl_no_minimal_bj.output) (deps (:input 460.ae)) diff --git a/tests/issues/474.ae b/tests/issues/474.ae new file mode 100644 index 000000000..4796f479e --- /dev/null +++ b/tests/issues/474.ae @@ -0,0 +1,12 @@ +logic ac f : real, real -> real + +function id_2() : real = 2. + +axiom ax_1: + f(f(id_2, 1.), 0.) <= 0.0 + +function f_2_1() : real = f(2., 1.) + +axiom ax_2: f_2_1 <= 0.0 + +goal goal_1: false diff --git a/tests/issues/474.expected b/tests/issues/474.expected new file mode 100644 index 000000000..a6e005255 --- /dev/null +++ b/tests/issues/474.expected @@ -0,0 +1,2 @@ + +unknown