Stream: Elpi users & devs

Topic: Design pattern: collecting info in the constraint store


view this post on Zulip Enzo Crance (May 16 2023 at 14:01):

During traversal of a term, I want to store information in the constraint store, in the form of dependencies between integers (e.g., variable n°1 depends on variable n°2, dep 1 2). After the traversal, I want to turn all this information into a precedence graph where there is an edge I -> J if dep I J is in the constraint store.

To do this, I create a constraint graph G M that will take an empty map as M and a fresh variable as G:

std.int.map.empty M,
declare_constraint (graph G M) [_]

Then, with a rule involving graph and dep, I can run through all of the entries in the constraint store and make my graph grow, until there is no dep in the store, and I can assign the final map to G and delete the graph constraint:

rule \ (graph G M) (dep I J) <=> (
  % ...
)
rule \ (graph G M) <=> (G = M).

Now, my variable G is filled with the precedence graph and I can continue execution after the line that declared the graph constraint initially.

The problem of this approach is that it must delete the dep entries in the constraint store in order to build the graph. Indeed, not deleting them would cause the first rule to indefinitely loop on the same dep entry, never finishing the construction of the graph. If I want to keep the dep constraint after building a graph, I need a way to distinguish entries that have already been taken into account by the rule from ones it has not seen yet.

My usual pattern is to add an integer as an additional field in the dep constraint (i.e., dep I J becomes dep I J N). The rule now deletes dep I J 0 and declares dep I J 1, so that I do not lose the information and I do not process twice the same entry. If I need more than one traversal, then it is easy to add a mechanism to track the current value of N shared by all the constraints, only match this one in the rules and declare the entries with counter N+1.

My question is the following: do you know any design pattern that would be better for this kind of problem? Thanks. (The current way of solving it is perfectly fine, I am just wondering if there is anything better)

view this post on Zulip Enrico Tassi (May 16 2023 at 14:28):

Hum, you could try rule (dep I J) \ (graph G M) | (not(map.mem I J M)) <=> ... but I've never written anything like this before (I guess it won't be super fast...)


Last updated: Oct 13 2024 at 01:02 UTC