Caching data structure, PredicateUnifier and beyond

[alexandernutz]

I think I would like to have a data structure, that manages a number of content items. It should.

• be like the predicate unifier, i.e., unify equivalent items, cache known parts of a partial order relation
• additionally keep a ternary relation with a meaning like "item A with operation B results in item C" the operations are specific to the content items In my case: "If I have a CongruenceClosure object A, and call reportEquality(x, y) on it, I get CongruenceClosure object C"

Further thoughts:

• there may be a lot of symmetry, e.g., "reportEquality(x,y)" is equivalent to "reportEquality(y, x)", and "reportEquality(x,y), reportEquality(i,j)" is equivalent to "reportEquality(i, j), reportEquality(x, y)"

Questions:

• do you think this is feasible? under which circumstances? for example I could limit items to a fixed size..
• are there overlaps with existing functionality in Ultimate I should keep in mind to avoid duplicate code? Does anyone have an interest in functionality like that? How generic should my implementation be?

[Heizmann]

I cannot understand the connection between the binary relation(s) and the ternary relation. What are the types of your relations? Are the first and the last element of the ternary relation a binary relation? What is your application? You could move all functionality of the PredicateUnifier that you need into a separate class but you should discuss that with @danieldietsch first.