Review AC(X) implementation

[bclement-ocp]

Need to understand:

• How the implementation actually relates to what is described in the paper,
• What are the assumptions made about the orderings used in different places of the implementation?

The AC(X) paper: https://arxiv.org/pdf/1207.3262.pdf

[bclement-ocp]

Noting here something I noticed that might be useful when coming back to this issue: the implementation of color in arith.ml looks shady.

  let color ac =
    match ac.Sig.l with
    | [(_, 1)] -> assert false
    | _ ->
      let p = unsafe_ac_to_arith ac in
      if not ac.distribute then
        if has_ac p (fun ac -> is_mult ac.h) then X.ac_embed ac
        else is_mine p
      else
        let xp = is_mine p in
        if contains_a_fresh_alien xp then
          let l, _ = P.to_list p in
          let mx = max_list_ l in
          if mx = 0 || mx = 1 || number_of_vars ac.l > mx then is_mine p
          else X.ac_embed ac
        else xp

We are doing something different whether we "contain a fresh alien" (i.e. a term with namespace "Fresh" i.e. a term created with E.fresh_name) or not. I believe this is intended to be part of the implementation of the abstraction mechanism (replacing AC(X) terms with fresh constants as described in the paper). However such fresh names are created not only for AC(X) purposes (see abstract2 in ac.ml and subst_bigger in arith.ml) but also in other situations (for instance, in abstract_selectors, or to enforce congruences in omega).

When we hit this code with fresh names that are not introduced for AC(X) purposes, weird things (and incompleteness) seem to happen. I don't have a simple example at the moment; this occurred while debugging seemingly unrelated code with bv2nat where I was able to produce AC rewrite rules of the form "x '' 1024.k3 ~~> y" which seem wrong¹. The left-hand side should have been simplified into 1024 * x'*'.k3 by color, but it was not because .k3 is a "fresh alien".

(set-logic ALL)
(declare-const mult Int)
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Int)
(declare-const e Int)

(assert (= a (* 1024 b)))
(assert (= (* a c) d))
(assert (= (* d e) mult))
(assert (distinct mult (* 1024 b c e)))
(check-sat)

We are able to prove unsat from a critical pair here, but we still introduce an AC rewrite rule of the form e'*'(1024*.k2) ~~> mult that looks suspicious (to me, at least).

Footnotes

1. AC(X) rewrite rules for multiplications usually rewrite monomials into monomials. In this situation, what should happen (and what does happen if we explicitly assert x * (1024 * y) = z) is that a new variable .k4 should be created with y = 1024 * .k4 and the rewrite rule x '*' .k3 ~~> .k4 added instead. Note that we can also hit this behavior with: ↩

[bclement-ocp]

Another note to self regarding #1172: this is maybe the wrong approach, because we still do different behavior depending on whether we have an AC-introduced constant for a top symbol that is not a multiplication. But maybe we must not do distributivity in that case either, I am not sure. Needs more thinking/review.