VIATRA-Generator
VIATRA-Generator copied to clipboard
Improve Viatra Solver's abstract interpretation of queries by reification
Currently, if a query has constraints C and D, where for a specific variable substitution both C and D evaluate to unknown (1/2), then C && D will evaluate to unknown as well. However, there are cases where it may be inferred that C and D cannot hold at the same time.
Suggested approach: reify the existence/non-existence of partial model elements into constraint variables, and reify the existence of query matches as well, with a constraint network spanning inbetween.