Documentation of Arrays_rel #1268
Conversation
src/lib/reasoners/arrays_rel.ml
Outdated
| type stype = {s:E.t; st:E.t; si:E.t; sv:E.t} | ||
| module S :Set.S with type elt = stype = Set.Make | ||
| module S = Set.Make | ||
| (struct type t = stype let compare t1 t2 = E.compare t1.s t2.s end) | ||
|
|
||
| (* map t |-> {set(t,-,-)} qui associe a chaque tableau l'ensemble |
There was a problem hiding this comment.
I didn't translate it because this comment is useless as the meaning of the TBS module is explained in the documentation of the field tbset. I suggest to remove it.
There was a problem hiding this comment.
Alright, there is another in line 49 that should also be removed
src/lib/reasoners/arrays_rel.ml
Outdated
| gets : G.t; | ||
| (* Set of all the known reads. *) |
There was a problem hiding this comment.
The documentations talks about reads and writes (referring to select and store) but the code refers to them as sets and gets. I think it should be harmonized and only one notation should be used.
Maybe at some point we should simply switch to the standard and use select and store internally, but I think select is used in the ADT theory as well.
There was a problem hiding this comment.
I agree, it's a mess... There are three notations:
set/getfrom the codeselect/storefrom the SMT-LIB standard,read/writefrom many papers on Array theories.
In my opinion, we should use the SMT-LIB standard but, as you pointed out, select is already in use in the ADT theory. I suggest that we keep set/get in Array and harmonize notations later.
There was a problem hiding this comment.
I've pushed a new commit to address your comments. Is it better?
src/lib/reasoners/arrays_rel.ml
Outdated
|
|
||
| split : LRset.t; | ||
| (* Set of equalities or disequalities on relevant indices. | ||
| There are the hypotheses of consequences in the field [conseq]. |
There was a problem hiding this comment.
| There are the hypotheses of consequences in the field [conseq]. | |
| These are the hypotheses of consequences in the field [conseq]. |
src/lib/reasoners/arrays_rel.ml
Outdated
| (* size_splits : Numbers.Q.t; *) | ||
| (* Limit the number of case splits performed on indices. This field | ||
| is currently unused. *) | ||
|
|
There was a problem hiding this comment.
I suppose it can be removed
src/lib/reasoners/arrays_rel.ml
Outdated
| `gi <> si` at the same time. *) | ||
| assert false | ||
|
|
||
| (* Produce a formula to propagate a read over a store. |
There was a problem hiding this comment.
Same as the comment above about notation, we should settle one notation and not mix multiple ones (in comments use read and write, in the code we use get and set, and here we use store as well)
src/lib/reasoners/arrays_rel.ml
Outdated
|
|
||
| (* Assume that [stype] represents the write `(store b j v)`. | ||
| For all known writes of the form `(store a i w)` such that `a` and | ||
| `b` are equal, we form the formula: |
There was a problem hiding this comment.
nitpick: this is more of a preference really
| `b` are equal, we form the formula: | |
| `b` are equal, we create the formula: |
src/lib/reasoners/arrays_rel.ml
Outdated
| let two = Numbers.Q.from_int 2 | ||
|
|
||
| (* Choose a equality/disequality between relevant indices to split on it. *) |
There was a problem hiding this comment.
| (* Choose a equality/disequality between relevant indices to split on it. *) | |
| (* Choose an equality/disequality between relevant indices to split on it. *) |
src/lib/reasoners/arrays_rel.ml
Outdated
| (* unused | ||
| let count_splits env la = | ||
| let nb = | ||
| List.fold_left | ||
| (fun nb (_,_,_,i) -> | ||
| match i with | ||
| | Th_util.CS (Th_util.Th_arrays, n) -> Numbers.Q.mult nb n | ||
| | _ -> nb | ||
| )env.size_splits la | ||
| in | ||
| {env with size_splits = nb} | ||
| ) env.size_splits la | ||
| in | ||
| {env with size_splits = nb} *) |
Halbaroth
force-pushed
the
documentation-arrays
branch
from
e4397fa to
3807cee
Compare
| and an index `i`. | ||
| - A relevant index is any term that appears as an index in get or set terms. | ||
| - A get or set term is known if it has been encountered in [assume]. *) | ||
|
|
||
| let src = Logs.Src.create ~doc:"Arrays_rel" __MODULE__ | ||
| module Log = (val Logs.src_log src : Logs.LOG) | ||
|
|
There was a problem hiding this comment.
Unfortunately, GitHub doesn't allow comments on unchanged lines, but the comment in line 49 should be removed
There was a problem hiding this comment.
I know this issue, it's really annoying!
| (* In this module, we follow the below conventions in the comments: | ||
| - A get term refers to a term of the form `(select a i)` for an array `a` and | ||
| an index `i`. | ||
| - A set term refers to a term of the form `(store a i v)` for an array `a` | ||
| and an index `i`. | ||
| - A relevant index is any term that appears as an index in get or set terms. | ||
| - A get or set term is known if it has been encountered in [assume]. *) |
There was a problem hiding this comment.
I'd argue that it would make more sense to call these "select terms" and "store terms" in documentation, with a comment mentioning that the variable names are legacy (or also rename the variables).
There was a problem hiding this comment.
I missed the other discussion — ignore this comment.
There was a problem hiding this comment.
As you've reviewed the PR, I need your approbation to merge it now :D
|
Strangely the CI failed on Ubuntu targets. I remember there is a test that fails sometimes on MacOS because the MacOS runner is too slow but it didn't happen on Ubuntu too? I restarted these tasks. |
It is (somewhat) the opposite -- that test is supposed to timeout, but sometimes the runner is fast and it doesn't (and fails with a reported reason of "incomplete" or "proof-search" instead of "timeout"), because our "reproducible-resource-limit" is related to time and not actually reproducible. See #1277 for an attempt at a fix. |
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 thecongruence 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, differentinstantiations of this axiom are produced by
get_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 hypothesesare satisfied. We produce the deduction
i = j \/ a[j] = b[j]but we do not send itto the SAT solver. Instead, we add the equality
i = jin the setenv.splitinorder to split on its negation later. If we split on it or we see
i <> jinassume,we send
a[j] = b[j]to the SAT solver.Our implementation suffers from a number of issues:
For instance, we do not need to propagate
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 modificationwill conflict with our plan for the union-find in UF (using Basile's store).