Merging nested loops: UNSAT Witess draft ready

src/TransformationUtils.cc

@@ -32,37 +32,19 @@ bool isTransitionSystem(ChcDirectedGraph const & graph) {
     return true;
 }
 
-
 std::unique_ptr<TransitionSystem> toTransitionSystem(ChcDirectedGraph const & graph) {
     Logic & logic = graph.getLogic();
     auto adjacencyRepresentation = AdjacencyListsGraphRepresentation::from(graph);
     auto vertices = reversePostOrder(graph, adjacencyRepresentation);
     assert(vertices.size() == 3);
     auto loopNode = vertices[1];
     auto edges = graph.getEdges();
-    EId inputEdge;
-    EId exitEdge;
-    EId loopEdge;
-    for(auto edge: edges){
-        if (graph.getSource(edge) == graph.getEntry()){
-            inputEdge = edge;
-        } else if (graph.getTarget(edge) == graph.getExit()){
-            exitEdge = edge;
-        } else {
-            loopEdge = edge;
-        }
-    }
-//    EId loopEdge = getSelfLoopFor(loopNode, graph, adjacencyRepresentation).value();
-//    auto inputVars = getVariablesFromEdge(logic, graph, inputEdge);
+    EId loopEdge = getSelfLoopFor(loopNode, graph, adjacencyRepresentation).value();
     auto edgeVars = getVariablesFromEdge(logic, graph, loopEdge);
-//    auto exitVars = getVariablesFromEdge(logic, graph, exitEdge);
-//    assert(inputVars.nextStateVars.size() == edgeVars.stateVars.size());
-//    assert(exitVars.stateVars.size() == edgeVars.nextStateVars.size());
     // 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;
@@ -123,9 +105,7 @@ bool strongConnection(std::unordered_set<int> & visitedVertices, std::unordered_
             if (visitedVertices.find(nextVertex.x) == visitedVertices.end()) {
                 bool loopFound =
                     strongConnection(visitedVertices, verticesOnStack, graphRepresentation, graph, nextVertex);
-                if (loopFound) {
-                    return true;
-                }
+                if (loopFound) { return true; }
             } else if (verticesOnStack.find(nextVertex.x) != verticesOnStack.end()) {
                 return true;
             }
@@ -144,7 +124,9 @@ bool TarjanLoopDetection(ChcDirectedGraph const & graph) {
     std::unordered_set<int> verticesOnStack;
     for (uint i = 1; i < vertices.size() - 1; i++) {
         if (visitedVertices.find(vertices[i].x) == visitedVertices.end()) {
-            if (strongConnection(visitedVertices, verticesOnStack, graphRepresentation, graph, vertices[i])) {
+            bool loop_detected =
+                strongConnection(visitedVertices, verticesOnStack, graphRepresentation, graph, vertices[i]);
+            if (loop_detected) {
                 return true;
             }
         }
@@ -177,8 +159,6 @@ bool isTransitionSystemDAG(ChcDirectedGraph const & graph) {
     return not canReachExit;
 }
 
-
-// TODO: SOMETHING WEIRD WITH NEWLY INTROD VARS
 EdgeVariables getVariablesFromEdge(Logic & logic, ChcDirectedGraph const & graph, EId eid) {
     EdgeVariables res;
     TermUtils utils(logic);

src/Witnesses.cc

@@ -113,6 +113,7 @@ InvalidityWitness InvalidityWitness::fromErrorPath(ErrorPath const & errorPath,
 
     InvalidityWitness witness;
     witness.setDerivation(std::move(derivation));
+    witness.ep = errorPath;
     return witness;
 }
 
@@ -182,19 +183,29 @@ 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 = utils.predicateArgsInOrder(graph.getStateVersion(vertex));
+    auto graphVars = getVariablesFromEdge(logic, graph, loop).stateVars;
+    auto origVars = 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) {
-        unversionedVars.push(timeMachine.getUnversioned(graphVars[i]));
-        subs.insert({systemVars[i], unversionedVars.last()});
+        subs.insert({systemVars[i], timeMachine.getUnversioned(graphVars[i])});
     }
     PTRef graphInvariant = utils.varSubstitute(inductiveInvariant, subs);
 //    std::cout << "Graph invariant: " << logic.printTerm(graphInvariant) << std::endl;

src/Witnesses.h

@@ -72,6 +72,7 @@ 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

@@ -49,7 +49,13 @@ VerificationResult TPAEngine::solve(ChcDirectedHyperGraph const & graph) {
         auto normalGraph = transformedGraph->toNormalGraph();
         if (options.hasOption(Options::SIMPLIFY_NESTED)) {
             NestedLoopTransformation transformation;
-            transformation.transform(*normalGraph);
+            auto preTranslator = transformation.transform(*normalGraph);
+            auto res = solve(*normalGraph);
+            if( shouldComputeWitness()){
+                auto prewit = preTranslator->translate(res);
+                return shouldComputeWitness() ? translator->translate(std::move(prewit)) : std::move(prewit);
+            }
+            return std::move(res);
         }
         auto res = solve(*normalGraph);
         return shouldComputeWitness() ? translator->translate(std::move(res)) : std::move(res);
@@ -58,9 +64,7 @@ VerificationResult TPAEngine::solve(ChcDirectedHyperGraph const & graph) {
 }
 
 VerificationResult TPAEngine::solve(const ChcDirectedGraph & graph) {
-    auto newGraph = graph;
     if (isTrivial(graph)) { return solveTrivial(graph); }
-
     if (isTransitionSystem(graph)) {
         auto ts = toTransitionSystem(graph);
         auto solver = mkSolver();
@@ -1589,6 +1593,7 @@ VerificationResult TransitionSystemNetworkManager::solve() && {
                     activePath.push(nextEdge);
                     current = next;
                     break; // Information has been propagated to the next node, switch to the new node
+
                 } else { // Edge cannot propagate forward
                     addRestrictions(current, logic.mkNot(edgeExplanation));
                     continue; // Repeat the query for the same TS with stronger query
@@ -1697,7 +1702,6 @@ TransitionSystemNetworkManager::QueryResult TransitionSystemNetworkManager::quer
         ModelBasedProjection mbp(logic);
         PTRef query = logic.mkAnd({sourceCondition, label, target});
         auto targetVars = getVariablesFromEdge(logic, graph, eid);
-//            TermUtils(logic).predicateArgsInOrder(graph.getNextStateVersion(graph.getTarget(eid)));
         PTRef eliminated = mbp.keepOnly(query, targetVars.nextStateVars, *model);
         getVariablesFromEdge(logic, graph, eid);
         eliminated = TimeMachine(logic).sendFlaThroughTime(eliminated, -1);

src/graph/ChcGraph.h

@@ -123,6 +123,19 @@ class ChcDirectedGraph {
     void mergeMultiEdges();
 
 public:
+    ChcDirectedGraph(const ChcDirectedGraph& graph) :
+          predicates(graph.predicates), logic(graph.logic),
+          simplified_vars(graph.simplified_vars){
+        for(auto el: graph.edges){
+            edges.insert(el);
+        }
+        std::size_t maxId = 0;
+        for (auto & edge : edges) {
+            maxId = std::max(maxId, std::get<1>(edge).id.id);
+        }
+        this->freeId = maxId + 1;
+    };
+
     ChcDirectedGraph(std::vector<DirectedEdge> edges, LinearCanonicalPredicateRepresentation predicates,
                      Logic & logic) :
          predicates(std::move(predicates)), logic(logic) {
@@ -142,7 +155,7 @@ class ChcDirectedGraph {
     ChcDirectedGraph reverse() const;
     DirectedEdge reverseEdge(DirectedEdge const & edge, TermUtils & utils) const;
 
-    LinearCanonicalPredicateRepresentation getPredicateRepresentation() const { return predicates; }
+    LinearCanonicalPredicateRepresentation & getPredicateRepresentation() { return predicates; }
 
     SymRef getEntry() const { return logic.getSym_true(); }
     SymRef getExit() const { return logic.getSym_false(); }
@@ -200,7 +213,6 @@ class ChcDirectedGraph {
         return edges.at(eid);
     }
 
-
     std::vector<PTRef> const & getAuxVars(SymRef sym) const {
         if(simplified_vars.find(sym.x)!=simplified_vars.end()){
             return simplified_vars.at(sym.x);
@@ -209,6 +221,7 @@ class ChcDirectedGraph {
             return empty;
         }
     };
+
     void addAuxVars(SymRef sym, std::vector<PTRef> & vars) {
         simplified_vars[sym.x].insert(simplified_vars[sym.x].end(), vars.begin(), vars.end());
     };
@@ -228,8 +241,6 @@ class ChcDirectedGraph {
 
     EId freshId() const { return EId{freeId++};}
 
-
-
 };