Generic state restoration of stores

[ptal]

This is issue is linked to #17 and #18.

Current architecture

A store is labelled and restored by implementing the trait State. During all the exploration, a single store is active and is used as a "token" traversing the search tree. The labels obtain through State.label() are used for restoring this token to previous state.

Only the copy restoration strategy is currently implemented. It is a bit more sublte than a plain copy; the copied store will be shared among all branches and copy-on-write. This is implemented by using type Label = Rc<Store>;. However, there was one problem, calling store.label() multiple time does not enable the copy-on-write mechanism unless the store keep tracks of previous call to label() and return the same label unless something has changed. It adds an additional responsibility on the store: "state restoration", but the store has already the responsibility of providing a monotonic access to the memory. Moreover, detecting changes would have been an error-prone requirement for the update operation and a time-inefficient design (since the store is more often updated than cloned). Therefore, it was decided to let the responsibility of the restoration strategy to the Label type and to clone this value each time we need it for a new branch.

Problems

A first problem is that the API offers two ways to clone a store:

1. Using label.clone() if we already have a label.
2. Using store.mark().

It is clearly a poor choice since nothing ensures that a user won't mix up both methods, and show some flaws in the design of the system.

A second problem arise when trying to implement a trailing restoration strategy, it basically needs to have a mutable access to the trail (and thus the store) to put a mark on it.

Finally, the store should be parametrized by a memory since it already has the responsibility of acting as a "monotonic memory".

Proposal

The idea is to see a store as active (e.g. mutable) only when processing one node of the search tree. We want to "freeze" accesses to the store between node. After all, it is reasonnable to think of the branching step as the creation of new stores and the death of the current one since the union of all the new stores should be equivalent to the current store (completness property).

We propose a trait that is freezing a store and returns an object implementing the State trait.