Do not unfold the AST on deep-copying

[merkste]

After certain replacements, e.g., formula substitution, the AST becomes a directed acyclic graph. On copying we want to preserve this structure. The identification of duplicates is non-local since duplicates may appear everywhere in the AST/DAG.

Significance

Certain more complex models that feature nested formulas cannot be handled with reasonable time and memory bounds with the current traversal and copying implementation. In one case-study this makes the difference between building and model-checking in a few seconds and running out of time and 16g memory right after parsing the input file. Even syntax-highlighting does not work at all.

Structure

This PR consists of three logical parts.

1. Small refactoring of ExpressionQuant hierarchy to avoid code duplicates
2. Introduction of a visitor that keeps track of the nodes already visited
3. Implementation of deep-copying that does not unfold the AST's DAG structure

Changes to ASTTraverse / ASTTraverseModify

Part 2 introduces a new root class for AST traversal, DAGVisitor that keeps track of visited nodes. The method visit now visits only nodes never seen before. If a new node is seen, the newly introduced method visitNow is called. Subclasses have to override this method instead of visit to implement their behavior. If they decide to visit node, they should call visit. There are no changes to visitPre and visitPost For the complete ASTTraverse and ASTTraverseModify hierarchy this is already done. Hence adaption of visitors in existing branches is done by simply renaming their implementation of visit to visitNow. Furthermore, if needed, the duplicate identification can be turned off which leads to the old behavior of visiting nodes multiple times.

For details, please see commits

• 98228f0 [DAG-visit] Implement DAG-aware visitor and
• 48a14d1 [DAG-visit] Adapt existing visitors to be DAG-aware

Changes to deep copying

Part 3 splits deep-copying into two steps. First, creating a shallow copy of an AST node by calling clone. Second, copying sub-nodes of the clone using deepCopy with the DeepCopy visitor.
This is already implemented for all ASTElement classes. Newly created ASTElements are only required to provide an implementation of clone and deepCopy(DeepCopy copier) instead of the old monolithic deepCopy(). Nothing else changes.

For details, please see commit

• 802a5a6 [DAG-copy] Implement deep-copying the AST without unfolding the DAG

[merkste]

If required, we could easily implement a new method unfold for the case that we actually want to unfold the AST. This would also make the memory/time implications clear. However, it seems not to be needed at the moment.

[merkste]

I've rearranged and split some commits to make the PR more approachable.