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 OCamlPro#474

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

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))

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

tests/issues/474.expected

@@ -0,0 +1,2 @@
+
+unknown