fix(AC): Also abstract non-AC arguments of AC symbols

Alt-Ergo uses an abstraction mechanism for the arguments of AC symbols
to ensure termination of the induced rewrite ordering without resorting
to a recursive path ordering.

This is described in section 6 of [this paper][1], except that the
implementation doesn't do exactly what is described there -- in
particular, it only abstracts nested AC symbols, which is an issue when
an argument is not an AC symbol but a semantic value that contains
another AC symbol.

This patch changes the `abstract2` function in `ac.ml`, where this
abstraction mechanism is implemented, to also introduce abstracted
constants for non-constant terms.

Fixes #964

[1]: https://arxiv.org/abs/1207.3262

src/lib/reasoners/ac.ml

@@ -166,7 +166,16 @@ module Make (X : Sig.X) = struct
   let abstract2 sy t r acc =
     match X.ac_extract r with
     | Some ac when Sy.equal sy ac.h -> r, acc
-    | None -> r, acc
+    | None -> (
+        if X.is_constant r then r, acc
+        else
+          match Expr.term_view t with
+          | { Expr.xs = []; bind = B_none; _ } -> r, acc
+          | { ty; _ } ->
+            let k = Expr.fresh_name ty in
+            let eq = Expr.mk_eq ~iff:false k t in
+            X.term_embed k, eq::acc
+      )
     | Some _ -> match Expr.term_view t with
       | { Expr.f = Sy.Name (hs, Sy.Ac, _); xs; ty; _ } ->
         let aro_sy = Sy.name ("@" ^ (HS.view hs)) in

tests/issues/964.ae

@@ -0,0 +1,4 @@
+logic ac u : int, int -> int
+logic ac v : int, int -> int
+
+goal g : v(0, 1) = u(-v(0, 1), 2)

tests/issues/964.expected

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