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:

alt-ergo/src/lib/structures/expr.ml

Lines 2799 to 2817 in 0d6300e

	| Sy.Op Get ->
	begin match e.xs with
	| [fa; i] ->
	let fa', lets =
	if is_pure fa then fa, Var.Map.empty
	else
	purify_term fa Var.Map.empty
	in
	let i', lets =
	if is_pure i then i, lets
	else
	match i.ty with
	| Ty.Tbool -> purify_form i, lets
	| _ -> purify_term i lets
	in
	if i == i' && fa == fa' then e
	else mk_lifted (mk_term e.f [fa'; i'] e.ty) lets
	| _ -> failwith "unexpected expression in purify_form"
	end

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)