diff --git a/src/engine/TPA.cc b/src/engine/TPA.cc index 6d6fc9a9..0a739623 100644 --- 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 index 53b28df7..0851727d 100644 --- 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::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 loop, LocationVarMap & locationVars, PositionVarMap & argVars) { Logic & logic = graph.getLogic(); diff --git a/src/transformers/NestedLoopTransformation.h b/src/transformers/NestedLoopTransformation.h index d9bfccd5..346f9f43 100644 --- 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 {