Merging nested loops: fixed formatting

usi-verification-and-security · Sep 17, 2024 · 8955553 · 8955553
1 parent 150be41
commit 8955553
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 7 deletions.
diff --git a/src/engine/TPA.cc b/src/engine/TPA.cc
@@ -75,8 +75,8 @@ VerificationResult TPAEngine::solve(const ChcDirectedGraph & graph) {
                 throw std::logic_error("Unreachable!");
         }
     } else if ((isTransitionSystemDAG(graph) && not options.hasOption(Options::FORCE_TS)) ||
-                options.hasOption(Options::SIMPLIFY_NESTED)) {
-        if(options.hasOption(Options::SIMPLIFY_NESTED)) {
+               options.hasOption(Options::SIMPLIFY_NESTED)) {
+        if (options.hasOption(Options::SIMPLIFY_NESTED)) {
             NestedLoopTransformation transformation;
             auto normalGraph = graph;
             auto preTranslator = transformation.transform(normalGraph);

diff --git a/src/transformers/NestedLoopTransformation.cc b/src/transformers/NestedLoopTransformation.cc
@@ -11,7 +11,6 @@
 #include "graph/ChcGraph.h"
 #include "utils/SmtSolver.h"
 
-
 std::unique_ptr<NestedLoopTransformation::WitnessBackTranslator>
 NestedLoopTransformation::transform(ChcDirectedGraph & graph) {
     auto vertices = graph.getVertices();
@@ -28,8 +27,6 @@ NestedLoopTransformation::transform(ChcDirectedGraph & graph) {
         std::move(originalGraph), graph, std::move(locationVars), std::move(argVars), simplifiedNodes);
 }
 
-
-
 SymRef NestedLoopTransformation::simplifyLoop(ChcDirectedGraph & graph, std::vector<EId> loop,
                                               LocationVarMap & locationVars, PositionVarMap & argVars) {
     Logic & logic = graph.getLogic();

diff --git a/src/transformers/NestedLoopTransformation.h b/src/transformers/NestedLoopTransformation.h
@@ -6,8 +6,8 @@
 #ifndef GOLEM_NESTED_LOOP_TRANSFORMATION_H
 #define GOLEM_NESTED_LOOP_TRANSFORMATION_H
 
-#include "TransitionSystem.h"
 #include "LoopTransformation.h"
+#include "TransitionSystem.h"
 #include "Witnesses.h"
 #include "graph/ChcGraph.h"
 
@@ -36,7 +36,7 @@
  * values for location variables. This may still leave some undesired variables in the invariant. We currently make
  * best effort to eliminate these variables by simplifying the formula.
  */
-class NestedLoopTransformation:LoopTransformation {
+class NestedLoopTransformation : LoopTransformation {
 
 public:
     class WitnessBackTranslator {