While writing this documentation, I read the paper Generalized, Efficient Array Decision Procedures of de Moura and Bjorner.
Before writing this documentation, I believed that we only implement the basic
inferences rules, which is exposed in Fig 1 of the paper. These rules are:
(idx) a == store(b, i, v) ===> a[i] = v
(down) a == store(b, i, v), w == a'[j], a ~ a' ===> i = j \/ a[j] = b[j]
(up) a == store(b, i, v), w = b'[j], b ~ b' ===> i = j \/ a[j] = b[j]
(ext) a, b know ===> a = b \/ a[k] <> b[k] (k fresh name)
(I use the double equality symbol == to denote syntactical equality and ~ for the
congruence relation.)
In fact, we implement a slightly different version of these rules. The down
, up and ext inference rules are implemented by respectively get_of_set,
get_and_set and extensionality functions in Arrays_rel module.
The idx axiom is not implemented by a dedicated function. Instead, different
instantiations of this axiom are produced by get_of_set, get_and_set and
get_from_set:
1a. (idx a) a[i] known, a ~ store(b, j, v) ==> i <> j \/ a[i] = v
1b. (idx b) store(b, i, v), store(a, j, w) known, a ~ b ==> store(a, j, w)[j] = w.
Technically, our implementation does not send directly instantiated axioms to the
SAT solver. Consider for instance the axiom down and assume that all its hypotheses
are satisfied. We produce the deduction i = j \/ a[j] = b[j] but we do not send it
to the SAT solver. Instead, we add the equality i = j in the set env.split in
order to split on its negation later. If we split on it or we see i <> j in assume,
we send a[j] = b[j] to the SAT solver.
Our implementation suffers from a number of issues:
We produce a lot of redundant axioms (see section A and section B of the paper).
For instance, we do not need to propagate a[i] = v if we already know that
a'[i'] = v' for with a ~ a', i ~ i' and v ~ v'. The same goes for other axioms.
We store all the relevant terms in huge maps which is not efficient.
We transform literal expressions into literal semantic values.
To be more efficient, our implementation only should follow equivalent classes
of read/write terms and relevant indices. When some of these classes merge, we
may have to instantiate axioms. This new version could be implemented using a union-find
in Arrays_rel itself but as I explained during the last dev meeting, this modification
will conflict with our plan for the union-find in UF (using Basile's store).
While writing this documentation, I read the paper
Generalized, Efficient Array Decision Proceduresof de Moura and Bjorner.Before writing this documentation, I believed that we only implement the basic inferences rules, which is exposed in Fig 1 of the paper. These rules are:
a == store(b, i, v) ===> a[i] = va == store(b, i, v), w == a'[j], a ~ a' ===> i = j \/ a[j] = b[j]a == store(b, i, v), w = b'[j], b ~ b' ===> i = j \/ a[j] = b[j]a, b know ===> a = b \/ a[k] <> b[k] (k fresh name)(I use the double equality symbol
==to denote syntactical equality and~for the congruence relation.)In fact, we implement a slightly different version of these rules. The
down,upandextinference rules are implemented by respectivelyget_of_set,get_and_setandextensionalityfunctions inArrays_relmodule.The
idxaxiom is not implemented by a dedicated function. Instead, different instantiations of this axiom are produced byget_of_set,get_and_setandget_from_set:1a. (idx a)
a[i] known, a ~ store(b, j, v) ==> i <> j \/ a[i] = v1b. (idx b)store(b, i, v), store(a, j, w) known, a ~ b ==> store(a, j, w)[j] = w.Technically, our implementation does not send directly instantiated axioms to the SAT solver. Consider for instance the axiom
downand assume that all its hypotheses are satisfied. We produce the deductioni = j \/ a[j] = b[j]but we do not send it to the SAT solver. Instead, we add the equalityi = jin the setenv.splitin order to split on its negation later. If we split on it or we seei <> jinassume, we senda[j] = b[j]to the SAT solver.Our implementation suffers from a number of issues:
a[i] = vif we already know thata'[i'] = v'for witha ~ a',i ~ i'andv ~ v'. The same goes for other axioms.To be more efficient, our implementation only should follow equivalent classes of read/write terms and relevant indices. When some of these classes merge, we may have to instantiate axioms. This new version could be implemented using a union-find in
Arrays_relitself but as I explained during the last dev meeting, this modification will conflict with our plan for the union-find in UF (using Basile's store).