TPA: Merge DAG nested loops #80
Conversation
BritikovKI
force-pushed
the
CPG-merge-nested-loops
branch
2 times, most recently
from
c04111e
to
51299f2
Compare
BritikovKI
force-pushed
the
CPG-merge-nested-loops
branch
from
3d9ffb2
to
f33d78a
Compare
src/engine/TPA.cc
Outdated
| @@ -46,6 +47,16 @@ VerificationResult TPAEngine::solve(ChcDirectedHyperGraph const & graph) { | |||
| auto translator = std::move(transformationResult.second); | |||
| if (transformedGraph->isNormalGraph()) { | |||
| auto normalGraph = transformedGraph->toNormalGraph(); | |||
| if (options.hasOption(Options::SIMPLIFY_NESTED)) { | |||
There was a problem hiding this comment.
Can you move this into the solve method that takes DirectedChcGraph?
| if (graph.getVertices().size() <= 3) { return loop; } | ||
| auto graphRepresentation = AdjacencyListsGraphRepresentation::from(graph); | ||
| auto vertices = reversePostOrder(graph, graphRepresentation); | ||
| std::unordered_set<int> visitedVertices; |
There was a problem hiding this comment.
These should be SymRefs, no? Not ints.
There was a problem hiding this comment.
It was supposed to be SymRef, but using it creates problems:
There was a problem hiding this comment.
I can go and try create default constructor for SymRef, but I'm not sure if it is an appropriate solution here
There was a problem hiding this comment.
You just need to provide SymRefHash as additional template parameter.
std::unordered_set<SymRef, SymRefHash>.
You have to tell the set how it is supposed to hash your custom type.
| std::move(originalGraph), graph, std::move(locationVars), std::move(argVars), simplifiedNodes); | ||
| } | ||
|
|
||
| void strongConnection(std::unordered_set<int> & visitedVertices, std::unordered_set<int> & verticesOnStack, |
There was a problem hiding this comment.
Can you add a pseudocode or a reference, or an explanation?
It is not easy to follow what the algorithm is doing.
…ved code duplications
BritikovKI
force-pushed
the
CPG-merge-nested-loops
branch
from
8955553
to
ba6b53f
Compare
This is an implementation of the merging of the nested loops into a single Transition System. It is done via the same approach as the transformation of the whole instance into the single System, but is adapted to only merge loops in the Graph structure into a single node.