Comparison of AST for constraints

[jmhorcas]

Actually, the comparison of AST needs revision. This is important to identify redundancies (e.g., duplicate constraints with different ASTs), as well as to use 'hash' function over the AST.

A first try: to compare two AST, and therefore two constraints, first we need to pass the AST to CNF (already done), remove duplicate clauses, and sort the clauses by lenght and then by variables strings:

clauses = ast.get_clauses()
sorted_clauses = list(map(sorted, clauses))
sorted_clauses.sort(key=len)

Maybe there is another more correct way.

[jagalindo]

any examples of uses for this? Operations between two models?

[jmhorcas]

Consider the simplest example: someone defines the following constraint: A => B other stakeholder defines the following constraint: not A v B

This is a redundancy which cannot be detected without the funcionality of comparing AST. The aforementioned solution will solve this example, but maybe not others more complicated.

[jagalindo]

Yes, I understand the semantics of the functionality. But there are two main things to consider, i) as an operation clearly I see the use case, for example, you have a model and want to simplify it by removing redundant relationships (see http://ceur-ws.org/Vol-1128/paper16.pdf) ii) to have AST simplification, this is where I don't see the use case. It is true that it can simplify the analysis and, even make it faster in some cases, but a complete redundancy check would probably require a sat,bdd or the alike solver. Then, what's the usage scenario of having this functionality in the core?

[jmhorcas]

Ah ok, I see your doubt. This functionality is not the redundancies checking (that's is a possible usage), this functionality is the comparison through the __eq__ (equals) method in the AST class. That is, wether two AST are the same "semantically" or not. Not sure if the implementation of the equals should be "semantically" or "syntactically". I think this depend if you consider the AST as an AST conceptually or as a lists of clauses.

[jmhorcas]

OK, after discussing this issue with @jagalindo, I checked that in the current code and there is not any version of __eq__ method provided. Therefore, we can provide one "syntactically" in a future release or leave it without __eq__ method and close this issue.