diff --git a/src/TransformationUtils.cc b/src/TransformationUtils.cc index 14582e30..ddf67da7 100644 --- a/src/TransformationUtils.cc +++ b/src/TransformationUtils.cc @@ -126,9 +126,7 @@ bool TarjanLoopDetection(ChcDirectedGraph const & graph) { if (visitedVertices.find(vertices[i].x) == visitedVertices.end()) { bool loop_detected = strongConnection(visitedVertices, verticesOnStack, graphRepresentation, graph, vertices[i]); - if (loop_detected) { - return true; - } + if (loop_detected) { return true; } } } return false; @@ -165,13 +163,7 @@ EdgeVariables getVariablesFromEdge(Logic & logic, ChcDirectedGraph const & graph PTRef sourcePred = graph.getStateVersion(graph.getSource(eid)); PTRef targetPred = graph.getNextStateVersion(graph.getTarget(eid)); res.stateVars = utils.predicateArgsInOrder(sourcePred); - auto auxSource = graph.getAuxVars(graph.getSource(eid)); - res.stateVars.insert(res.stateVars.end(), auxSource.begin(), auxSource.end()); - auto auxTarget = graph.getAuxVars(graph.getTarget(eid)); res.nextStateVars = utils.predicateArgsInOrder(targetPred); - for(auto var: auxTarget){ - res.nextStateVars.push_back(TimeMachine(logic).sendFlaThroughTime(var, 1)); - } PTRef edgeLabel = graph.getEdgeLabel(eid); auto allVars = TermUtils(logic).getVars(edgeLabel); for (PTRef var : allVars) { diff --git a/src/engine/TPA.cc b/src/engine/TPA.cc index 195cc4c3..bb06fa09 100644 --- a/src/engine/TPA.cc +++ b/src/engine/TPA.cc @@ -14,8 +14,8 @@ #include "TransitionSystem.h" #include "Witnesses.h" #include "transformers/BasicTransformationPipelines.h" -#include "transformers/SingleLoopTransformation.h" #include "transformers/NestedLoopTransformation.h" +#include "transformers/SingleLoopTransformation.h" #include "utils/SmtSolver.h" #define TRACE_LEVEL 0 @@ -51,11 +51,11 @@ VerificationResult TPAEngine::solve(ChcDirectedHyperGraph const & graph) { NestedLoopTransformation transformation; auto preTranslator = transformation.transform(*normalGraph); auto res = solve(*normalGraph); - if( shouldComputeWitness()){ + if (shouldComputeWitness()) { auto prewit = preTranslator->translate(res); return shouldComputeWitness() ? translator->translate(std::move(prewit)) : std::move(prewit); } - return std::move(res); + return res; } auto res = solve(*normalGraph); return shouldComputeWitness() ? translator->translate(std::move(res)) : std::move(res); diff --git a/src/graph/ChcGraph.h b/src/graph/ChcGraph.h index eef18c96..b1d43bd5 100644 --- a/src/graph/ChcGraph.h +++ b/src/graph/ChcGraph.h @@ -109,7 +109,6 @@ struct VertexHasher { class ChcDirectedGraph { std::map edges; - std::map> simplified_vars; LinearCanonicalPredicateRepresentation predicates; Logic & logic; mutable std::size_t freeId {0}; @@ -124,8 +123,7 @@ class ChcDirectedGraph { public: ChcDirectedGraph(const ChcDirectedGraph& graph) : - predicates(graph.predicates), logic(graph.logic), - simplified_vars(graph.simplified_vars){ + predicates(graph.predicates), logic(graph.logic){ for(auto el: graph.edges){ edges.insert(el); } @@ -213,19 +211,6 @@ class ChcDirectedGraph { return edges.at(eid); } - std::vector const & getAuxVars(SymRef sym) const { - if(simplified_vars.find(sym.x)!=simplified_vars.end()){ - return simplified_vars.at(sym.x); - } else { - std::vector empty; - return empty; - } - }; - - void addAuxVars(SymRef sym, std::vector & vars) { - simplified_vars[sym.x].insert(simplified_vars[sym.x].end(), vars.begin(), vars.end()); - }; - private: template diff --git a/src/transformers/NestedLoopTransformation.cc b/src/transformers/NestedLoopTransformation.cc index 6b323fbb..d9c5b368 100644 --- a/src/transformers/NestedLoopTransformation.cc +++ b/src/transformers/NestedLoopTransformation.cc @@ -89,8 +89,7 @@ std::unique_ptr NestedLoopTrans LocationVarMap locationVars; PositionVarMap argVars; while(loop.size()>1){ - simplifiedNodes.push_back(graph.getSource(loop[loop.size()-1])); - simplifyLoop(graph, loop, locationVars, argVars); + simplifiedNodes.push_back(simplifyLoop(graph, loop, locationVars, argVars)); loop = detectLoop(graph); } // auto backTranslator = @@ -149,7 +148,7 @@ std::vector NestedLoopTransformation::detectLoop(const ChcDirectedGraph & g return loop; } -void NestedLoopTransformation::simplifyLoop( ChcDirectedGraph & graph, std::vector loop, LocationVarMap& locationVars, PositionVarMap& argVars) { +SymRef NestedLoopTransformation::simplifyLoop( ChcDirectedGraph & graph, std::vector loop, LocationVarMap& locationVars, PositionVarMap& argVars) { Logic & logic = graph.getLogic(); TimeMachine timeMachine(logic); TermUtils utils(logic); @@ -210,11 +209,14 @@ void NestedLoopTransformation::simplifyLoop( ChcDirectedGraph & graph, std::vect } return ret; }(); + vec args; + for(auto arg: stateVars){ + args.push(logic.getSortRef(arg)); + } PTRef transitionRelation = logic.mkOr(std::move(transitionRelationComponent)); - SymRef newRef = logic.getSymRef(transitionRelation); - + SymRef newRef = logic.declareFun("hello", logic.getSort_bool(), args); std::vector vars; for (PTRef var : stateVars) { vars.push_back(timeMachine.getUnversioned(var)); @@ -240,7 +242,7 @@ void NestedLoopTransformation::simplifyLoop( ChcDirectedGraph & graph, std::vect conds = logic.mkAnd(conds, logic.mkEq(oldEdgeVars.stateVars[i], argVars[{graph.getSource(edge), i}])); // argVars[{graph.getTarget(edge), i}]; } - graph.updateEdgeSource(edge, vertices[0]); + graph.updateEdgeSource(edge, newRef); auto newEdgeVars = getVariablesFromEdge(logic, graph, edge); PTRef label = utils.varSubstitute(logic.mkAnd(graph.getEdgeLabel(edge), badStates), subMap); std::transform(oldEdgeVars.stateVars.begin(), oldEdgeVars.stateVars.end(), newEdgeVars.stateVars.begin(), @@ -272,7 +274,7 @@ void NestedLoopTransformation::simplifyLoop( ChcDirectedGraph & graph, std::vect conds = logic.mkAnd(conds, logic.mkEq(oldEdgeVars.nextStateVars[i], timeMachine.sendVarThroughTime(argVars[{graph.getTarget(edge), i}],1))); // argVars[{graph.getTarget(edge), i}]; } - graph.updateEdgeTarget(edge, vertices[0]); + graph.updateEdgeTarget(edge, newRef); auto newEdgeVars = getVariablesFromEdge(logic, graph, edge); PTRef label = utils.varSubstitute(graph.getEdgeLabel(edge), subMap); std::transform(oldEdgeVars.nextStateVars.begin(), oldEdgeVars.nextStateVars.end(), newEdgeVars.nextStateVars.begin(), @@ -284,10 +286,8 @@ void NestedLoopTransformation::simplifyLoop( ChcDirectedGraph & graph, std::vect } } - - - graph.newEdge(vertices[0], vertices[0],InterpretedFla{transitionRelation}); - graph.addAuxVars(vertices[0], stateVars); + graph.newEdge(newRef, newRef,InterpretedFla{transitionRelation}); + return newRef; } @@ -297,7 +297,7 @@ void NestedLoopTransformation::simplifyLoop( ChcDirectedGraph & graph, std::vect VerificationResult NestedLoopTransformation::WitnessBackTranslator::translate(VerificationResult & result) { if (result.getAnswer() == VerificationAnswer::UNSAFE) { - auto witness = translateErrorPath(result.getInvalidityWitness().ep.getEdges()); + auto witness = translateErrorPath(result.getInvalidityWitness()); if (std::holds_alternative(witness)) { return {result.getAnswer(), std::get(std::move(witness))}; } @@ -315,13 +315,13 @@ NestedLoopTransformation::WitnessBackTranslator::translate(VerificationResult & NestedLoopTransformation::WitnessBackTranslator::ErrorOr -NestedLoopTransformation::WitnessBackTranslator::translateErrorPath(std::vector errorPath) { +NestedLoopTransformation::WitnessBackTranslator::translateErrorPath(InvalidityWitness wtns) { // We need to get the CEX path, which will define the locations in the graph Logic & logic = graph.getLogic(); TimeMachine tm(logic); - + auto errorPath = wtns.getDerivation(); std::vector pathVertices; - pathVertices.push_back(graph.getEntry()); + pathVertices.push_back(initialGraph.getEntry()); auto newVertices = graph.getVertices(); auto allVertices = initialGraph.getVertices(); @@ -329,8 +329,8 @@ NestedLoopTransformation::WitnessBackTranslator::translateErrorPath(std::vector< auto model = [&]() { SMTSolver solverWrapper(logic, SMTSolver::WitnessProduction::ONLY_MODEL); auto & solver = solverWrapper.getCoreSolver(); - for (std::size_t i = 0; i < errorPath.size(); ++i) { - PTRef fla = graph.getEdgeLabel(errorPath[i]); + for (std::size_t i = 1; i < errorPath.size(); ++i) { + PTRef fla = graph.getEdgeLabel(errorPath[i].clauseId); fla = TimeMachine(logic).sendFlaThroughTime(fla, i); solver.insertFormula(fla); } @@ -338,11 +338,14 @@ NestedLoopTransformation::WitnessBackTranslator::translateErrorPath(std::vector< if (res != s_True) { throw std::logic_error("Error in computing model for the error path"); } return solver.getModel(); }(); - for (auto i = 0u; i < errorPath.size(); ++i) { - if(graph.getTarget(errorPath[i]) == graph.getSource(errorPath[i])){ - if (std::find(loopNodes.begin(), loopNodes.end(), graph.getTarget(errorPath[i])) != loopNodes.end()) { + + for (std::size_t i = 1; i < errorPath.size(); ++i) { + if(graph.getTarget(errorPath[i].clauseId) == graph.getSource(errorPath[i].clauseId)){ + if (std::find(loopNodes.begin(), loopNodes.end(), graph.getTarget(errorPath[i].clauseId)) != loopNodes.end()) { auto it = std::find_if(allVertices.begin(), allVertices.end(), [&](auto vertex) { - if (vertex == graph.getEntry()) { return false; } + if(locationVarMap.find(vertex) == locationVarMap.end()){ + return false; + } auto varName = ".loc_" + std::to_string(vertex.x); auto vertexVar = logic.mkBoolVar(varName.c_str()); vertexVar = tm.getVarVersionZero(vertexVar); @@ -352,10 +355,10 @@ NestedLoopTransformation::WitnessBackTranslator::translateErrorPath(std::vector< assert(it != allVertices.end()); pathVertices.push_back(*it); } else { - pathVertices.push_back(graph.getTarget(errorPath[i])); + pathVertices.push_back(initialGraph.getTarget(errorPath[i].clauseId)); }; } else { - pathVertices.push_back(graph.getTarget(errorPath[i])); + pathVertices.push_back(initialGraph.getTarget(errorPath[i].clauseId)); } } @@ -363,7 +366,7 @@ NestedLoopTransformation::WitnessBackTranslator::translateErrorPath(std::vector< // Build error path from the vertices std::vector errorEdges; auto adj = AdjacencyListsGraphRepresentation::from(initialGraph); - for (auto i = 1u; i < pathVertices.size(); ++i) { + for (auto i = 1; i < pathVertices.size(); ++i) { auto source = pathVertices[i - 1]; auto target = pathVertices[i]; auto const & outgoing = adj.getOutgoingEdgesFor(source); diff --git a/src/transformers/NestedLoopTransformation.h b/src/transformers/NestedLoopTransformation.h index a52c3929..9c1dc1bb 100644 --- a/src/transformers/NestedLoopTransformation.h +++ b/src/transformers/NestedLoopTransformation.h @@ -67,20 +67,12 @@ class NestedLoopTransformation { std::vector loopNodes; public: -// WitnessBackTranslator(ChcDirectedGraph const & initialGraph, ChcDirectedGraph const & graph, -// LocationVarMap locationVarMap, PositionVarMap positionVarMap, std::vector & loopNodes) -// : graph(graph), initialGraph(initialGraph), loopNodes(loopNodes), locationVarMap(locationVarMap), positionVarMap(positionVarMap){ -// } WitnessBackTranslator(ChcDirectedGraph initialGraph, ChcDirectedGraph const & graph, LocationVarMap && locationVarMap, PositionVarMap && positionVarMap, std::vector & loopNodes) - : graph(graph), initialGraph(initialGraph), - locationVarMap(std::move(locationVarMap)), - positionVarMap(std::move(positionVarMap)), - loopNodes(loopNodes) { -// initialGraph = std::make_unique(initialGraph); - } + : initialGraph(initialGraph), graph(graph), locationVarMap(std::move(locationVarMap)), + positionVarMap(std::move(positionVarMap)), loopNodes(loopNodes) {} VerificationResult translate(VerificationResult & result); @@ -88,7 +80,7 @@ class NestedLoopTransformation { template using ErrorOr = std::variant; - ErrorOr translateErrorPath(std::vector errorPath); + ErrorOr translateErrorPath(InvalidityWitness errorPath); ErrorOr translateInvariant(ValidityWitness wtns); @@ -97,7 +89,7 @@ class NestedLoopTransformation { std::vector detectLoop(ChcDirectedGraph const & graph); - void simplifyLoop(ChcDirectedGraph & graph, std::vector loop, LocationVarMap& locationVars, PositionVarMap& argVars); + SymRef simplifyLoop(ChcDirectedGraph & graph, std::vector loop, LocationVarMap& locationVars, PositionVarMap& argVars); std::unique_ptr transform(ChcDirectedGraph & graph); diff --git a/test/test_TransformationUtils.cc b/test/test_TransformationUtils.cc index b0803c63..01bb9a71 100644 --- a/test/test_TransformationUtils.cc +++ b/test/test_TransformationUtils.cc @@ -40,6 +40,6 @@ TEST_F(TransformationUtils_Test, test_DAGWithExtraEdge) { ASSERT_TRUE(hypergraph->isNormalGraph()); auto graph = hypergraph->toNormalGraph(); EXPECT_FALSE(isTransitionSystem(*graph)); -// EXPECT_FALSE(isTransitionSystemDAG(*graph)); // Because of the extra edge from entry to exit + EXPECT_FALSE(isTransitionSystemDAG(*graph)); // Because of the extra edge from entry to exit }