Purification of embedded formulas in Arrays

[Halbaroth]

While trying to solve #1156, I took a look at our purification module in Expr and I suspect that this piece of code: https://github.com/OCamlPro/alt-ergo/blob/0d6300ec27446ea57626a19dc0a7b00a80daf3a7/src/lib/structures/expr.ml#L2799-L2817 is dead.

Indeed, consider the input:

(set-logic ALL)
(set-option :produce-models true)
(declare-const a (Array Bool Bool))
(declare-const x Int)
(declare-const y Int)
(assert (select a (= x y)))
(check-sat)
(get-model)

We got

unknown
[Error]Expect a uninterpreted term declared by the user, got (= y  x)
Fatal error: exception File "src/lib/reasoners/uf.ml", line 1245, characters 10-16: Assertion failed

If we purify ourselves the formula:

(set-logic ALL)
(set-option :produce-models true)
(declare-const a (Array Bool Bool))
(declare-const x Int)
(declare-const y Int)
(assert (let ((b (= x y))) (select a b)))
(check-sat)
(get-model)

We obtain the expected result:

unknown
(
  (define-fun x () Int 0)
  (define-fun y () Int 1)
  (define-fun a () (Array Bool Bool)
   (store (as @a3 (Array Bool Bool)) false true))
)

The above code is dead because a term is pure if and only if all its arguments are pure and it is not an ite term. So (select a (= x y)) is pure for this definition.

[bclement-ocp]

I don't think this code is dead; (select a (= x y)) is not pure because (= x y) is not pure (we could argue about it, but changing this is probably going to break the purification algo in many subtle and not-so-subtle ways). We can probably skip literals in compute_concrete_model_of_val (their value should be defined by the propositional model; although maybe not always with CDCL-Tableaux?).

[bclement-ocp]

Following dev meeting, here is an example of a file where this code is not dead:

(set-logic ALL)
(declare-const a (Array Bool Bool))
(declare-const x Int)
(declare-const y Int)
(assert (ite (select a (= x y)) true false))
(check-sat)
(get-model)