Open Halbaroth opened 4 weeks ago
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?).
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)
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:
We got
If we purify ourselves the formula:
We obtain the expected result:
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.