Skip to content

Commit

Permalink
Merging nested loops: Tests and reformatting
Browse files Browse the repository at this point in the history
  • Loading branch information
@BritikovKI
BritikovKI committed Sep 1, 2024
1 parent 21fca8e commit adcb786
Show file tree
Hide file tree
Showing 6 changed files with 37 additions and 65 deletions.
10 changes: 1 addition & 9 deletions src/TransformationUtils.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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) {
Expand Down
6 changes: 3 additions & 3 deletions src/engine/TPA.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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);
Expand Down
17 changes: 1 addition & 16 deletions src/graph/ChcGraph.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -109,7 +109,6 @@ struct VertexHasher {

class ChcDirectedGraph {
std::map<EId, DirectedEdge> edges;
std::map<uint32_t, std::vector<PTRef>> simplified_vars;
LinearCanonicalPredicateRepresentation predicates;
Logic & logic;
mutable std::size_t freeId {0};
Expand All @@ -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);
}
Expand Down Expand Up @@ -213,19 +211,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);
} else {
std::vector<PTRef> empty;
return empty;
}
};

void addAuxVars(SymRef sym, std::vector<PTRef> & vars) {
simplified_vars[sym.x].insert(simplified_vars[sym.x].end(), vars.begin(), vars.end());
};

private:

template<typename TPred>
Expand Down
51 changes: 27 additions & 24 deletions src/transformers/NestedLoopTransformation.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -89,8 +89,7 @@ std::unique_ptr<NestedLoopTransformation::WitnessBackTranslator> 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 =
Expand Down Expand Up @@ -149,7 +148,7 @@ std::vector<EId> NestedLoopTransformation::detectLoop(const ChcDirectedGraph & g
return loop;
}

void NestedLoopTransformation::simplifyLoop( ChcDirectedGraph & graph, std::vector<EId> loop, LocationVarMap& locationVars, PositionVarMap& argVars) {
SymRef NestedLoopTransformation::simplifyLoop( ChcDirectedGraph & graph, std::vector<EId> loop, LocationVarMap& locationVars, PositionVarMap& argVars) {
Logic & logic = graph.getLogic();
TimeMachine timeMachine(logic);
TermUtils utils(logic);
Expand Down Expand Up @@ -210,11 +209,14 @@ void NestedLoopTransformation::simplifyLoop( ChcDirectedGraph & graph, std::vect
}
return ret;
}();
vec<SRef> 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<PTRef> vars;
for (PTRef var : stateVars) {
vars.push_back(timeMachine.getUnversioned(var));
Expand All @@ -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(),
Expand Down Expand Up @@ -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(),
Expand All @@ -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;
}


Expand All @@ -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<NoWitness>(witness)) {
return {result.getAnswer(), std::get<NoWitness>(std::move(witness))};
}
Expand All @@ -315,34 +315,37 @@ NestedLoopTransformation::WitnessBackTranslator::translate(VerificationResult &


NestedLoopTransformation::WitnessBackTranslator::ErrorOr<InvalidityWitness>
NestedLoopTransformation::WitnessBackTranslator::translateErrorPath(std::vector<EId> 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<SymRef> pathVertices;
pathVertices.push_back(graph.getEntry());
pathVertices.push_back(initialGraph.getEntry());
auto newVertices = graph.getVertices();
auto allVertices = initialGraph.getVertices();

// Compute model for the error path
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);
}
auto res = solver.check();
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);
Expand All @@ -352,18 +355,18 @@ 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));
}

}

// Build error path from the vertices
std::vector<EId> 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);
Expand Down
16 changes: 4 additions & 12 deletions src/transformers/NestedLoopTransformation.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -67,28 +67,20 @@ class NestedLoopTransformation {
std::vector<SymRef> loopNodes;

public:
// WitnessBackTranslator(ChcDirectedGraph const & initialGraph, ChcDirectedGraph const & graph,
// LocationVarMap locationVarMap, PositionVarMap positionVarMap, std::vector<SymRef> & loopNodes)
// : graph(graph), initialGraph(initialGraph), loopNodes(loopNodes), locationVarMap(locationVarMap), positionVarMap(positionVarMap){
// }

WitnessBackTranslator(ChcDirectedGraph initialGraph, ChcDirectedGraph const & graph,
LocationVarMap && locationVarMap, PositionVarMap && positionVarMap,
std::vector<SymRef> & loopNodes)
: graph(graph), initialGraph(initialGraph),
locationVarMap(std::move(locationVarMap)),
positionVarMap(std::move(positionVarMap)),
loopNodes(loopNodes) {
// initialGraph = std::make_unique<ChcDirectedGraph>(initialGraph);
}
: initialGraph(initialGraph), graph(graph), locationVarMap(std::move(locationVarMap)),
positionVarMap(std::move(positionVarMap)), loopNodes(loopNodes) {}

VerificationResult translate(VerificationResult & result);

private:

template<typename T> using ErrorOr = std::variant<NoWitness, T>;

ErrorOr<InvalidityWitness> translateErrorPath(std::vector<EId> errorPath);
ErrorOr<InvalidityWitness> translateErrorPath(InvalidityWitness errorPath);

ErrorOr<ValidityWitness> translateInvariant(ValidityWitness wtns);

Expand All @@ -97,7 +89,7 @@ class NestedLoopTransformation {


std::vector<EId> detectLoop(ChcDirectedGraph const & graph);
void simplifyLoop(ChcDirectedGraph & graph, std::vector<EId> loop, LocationVarMap& locationVars, PositionVarMap& argVars);
SymRef simplifyLoop(ChcDirectedGraph & graph, std::vector<EId> loop, LocationVarMap& locationVars, PositionVarMap& argVars);

std::unique_ptr<WitnessBackTranslator> transform(ChcDirectedGraph & graph);

Expand Down
2 changes: 1 addition & 1 deletion test/test_TransformationUtils.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
}

0 comments on commit adcb786

Please sign in to comment.