Merging nested loops: small clean-up

src/TransformationUtils.cc

@@ -38,13 +38,13 @@ std::unique_ptr<TransitionSystem> toTransitionSystem(ChcDirectedGraph const & gr
     auto vertices = reversePostOrder(graph, adjacencyRepresentation);
     assert(vertices.size() == 3);
     auto loopNode = vertices[1];
-    auto edges = graph.getEdges();
     EId loopEdge = getSelfLoopFor(loopNode, graph, adjacencyRepresentation).value();
     auto edgeVars = getVariablesFromEdge(logic, graph, loopEdge);
     // Now we can continue building the transition system
     auto systemType = systemTypeFrom(edgeVars.stateVars, edgeVars.auxiliaryVars, logic);
     auto stateVars = systemType->getStateVars();
     auto nextStateVars = systemType->getNextStateVars();
+    auto auxiliaryVars = systemType->getAuxiliaryVars();
     assert(stateVars.size() == edgeVars.stateVars.size());
     assert(nextStateVars.size() == edgeVars.nextStateVars.size());
     PTRef init = PTRef_Undef;
@@ -122,6 +122,7 @@ bool TarjanLoopDetection(ChcDirectedGraph const & graph) {
     auto vertices = reversePostOrder(graph, graphRepresentation);
     std::unordered_set<int> visitedVertices;
     std::unordered_set<int> verticesOnStack;
+
     for (uint i = 1; i < vertices.size() - 1; i++) {
         if (visitedVertices.find(vertices[i].x) == visitedVertices.end()) {
             bool loop_detected =

src/Witnesses.cc

@@ -113,7 +113,6 @@ InvalidityWitness InvalidityWitness::fromErrorPath(ErrorPath const & errorPath,
 
     InvalidityWitness witness;
     witness.setDerivation(std::move(derivation));
-    witness.ep = errorPath;
     return witness;
 }
 
@@ -183,29 +182,19 @@ ValidityWitness::fromTransitionSystem(Logic & logic, ChcDirectedGraph const & gr
                                       TransitionSystem const & transitionSystem, PTRef inductiveInvariant) {
     if (not isTransitionSystem(graph)) { return {}; }
     auto vertices = graph.getVertices();
-    auto edges = graph.getEdges();
-    EId loop;
-    for(auto edge: edges) {
-        if(graph.getSource(edge) != graph.getEntry() && graph.getTarget(edge) != graph.getExit()){
-            loop = edge;
-        }
-    }
     assert(vertices.size() == 3);
     auto vertex = vertices[2];
     assert(vertex != graph.getEntry() and vertex != graph.getExit());
     TermUtils utils(logic);
     TimeMachine timeMachine(logic);
     TermUtils::substitutions_map subs;
-    auto graphVars = getVariablesFromEdge(logic, graph, loop).stateVars;
-    auto origVars = utils.predicateArgsInOrder(graph.getStateVersion(vertex));
+    auto graphVars = utils.predicateArgsInOrder(graph.getStateVersion(vertex));
     auto systemVars = transitionSystem.getStateVars();
     vec<PTRef> unversionedVars;
     assert(graphVars.size() == systemVars.size());
-    for (std::size_t i = 0; i < origVars.size(); ++i) {
-        unversionedVars.push(timeMachine.getUnversioned(origVars[i]));
-    }
     for (std::size_t i = 0; i < graphVars.size(); ++i) {
-        subs.insert({systemVars[i], timeMachine.getUnversioned(graphVars[i])});
+        unversionedVars.push(timeMachine.getUnversioned(graphVars[i]));
+        subs.insert({systemVars[i], unversionedVars.last()});
     }
     PTRef graphInvariant = utils.varSubstitute(inductiveInvariant, subs);
 //    std::cout << "Graph invariant: " << logic.printTerm(graphInvariant) << std::endl;

src/Witnesses.h

@@ -72,7 +72,6 @@ class InvalidityWitness {
     Derivation derivation;
 
 public:
-    ErrorPath ep;
     void setDerivation(Derivation derivation_) { derivation = std::move(derivation_); }
 
     [[nodiscard]] Derivation const & getDerivation() const { return derivation; }

src/engine/TPA.cc

@@ -1701,9 +1701,8 @@ TransitionSystemNetworkManager::QueryResult TransitionSystemNetworkManager::quer
         auto model = solver.getModel();
         ModelBasedProjection mbp(logic);
         PTRef query = logic.mkAnd({sourceCondition, label, target});
-        auto targetVars = getVariablesFromEdge(logic, graph, eid);
-        PTRef eliminated = mbp.keepOnly(query, targetVars.nextStateVars, *model);
-        getVariablesFromEdge(logic, graph, eid);
+        auto targetVars = TermUtils(logic).predicateArgsInOrder(graph.getNextStateVersion(graph.getTarget(eid)));
+        PTRef eliminated = mbp.keepOnly(query, targetVars, *model);
         eliminated = TimeMachine(logic).sendFlaThroughTime(eliminated, -1);
         TRACE(1, "Propagating along the edge " << logic.pp(eliminated))
         return {ReachabilityResult::REACHABLE, eliminated};