Skip to content

Preprocessing nested loops #88

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 1 commit into from
Closed

Preprocessing nested loops #88

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions .clang-files
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,9 @@ src/transformers/SingleLoopTransformation.cc
src/transformers/SingleLoopTransformation.h
src/transformers/TrivialEdgePruner.cc
src/transformers/TrivialEdgePruner.h
src/transformers/NodeEliminator.h
src/transformers/NodeEliminator.cc
src/transformers/BasicTransformationPipelines.h

src/utils/SmtSolver.h
src/utils/SmtSolver.cc
Expand Down
16 changes: 16 additions & 0 deletions src/graph/ChcGraph.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -581,6 +581,22 @@ bool isNonLoopNode(
return std::none_of(outgoing.begin(), outgoing.end(), [&](EId eid){ return graph.getTarget(eid) == vertex; });
}

bool isNonNestedLoopNode(SymRef vertex, AdjacencyListsGraphRepresentation const & adjacencyRepresentation,
ChcDirectedHyperGraph const & graph, SymRef toCheck) {
auto const & outgoing = adjacencyRepresentation.getOutgoingEdgesFor(vertex);
for (auto edge : outgoing) {
SymRef target = graph.getTarget(edge);
if (target == toCheck) {
return true;
} else if (target == vertex || target == graph.getExit()) {
continue;
} else {
if (isNonNestedLoopNode(target, adjacencyRepresentation, graph, toCheck)) break;
}
}
return false;
}

bool isSimpleNode(
SymRef vertex,
AdjacencyListsGraphRepresentation const & adjacencyRepresentation
Expand Down
2 changes: 2 additions & 0 deletions src/graph/ChcGraph.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -352,6 +352,8 @@ class ReverseDFS {

bool isNonLoopNode(SymRef, AdjacencyListsGraphRepresentation const &, ChcDirectedHyperGraph const & graph);

bool isNonNestedLoopNode(SymRef, AdjacencyListsGraphRepresentation const &, ChcDirectedHyperGraph const &, SymRef);

bool hasHyperEdge(SymRef, AdjacencyListsGraphRepresentation const &, ChcDirectedHyperGraph const & graph);

bool isSimpleNode(SymRef, AdjacencyListsGraphRepresentation const &);
Expand Down
7 changes: 4 additions & 3 deletions src/transformers/BasicTransformationPipelines.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,8 @@ namespace Transformations {
inline TransformationPipeline towardsTransitionSystems() {
TransformationPipeline::pipeline_t stages;
stages.push_back(std::make_unique<MultiEdgeMerger>());
stages.push_back(std::make_unique<NonLoopEliminator>());
// stages.push_back(std::make_unique<NonLoopEliminator>());
stages.push_back(std::make_unique<NonLoopNestedEliminator>());
stages.push_back(std::make_unique<FalseClauseRemoval>());
stages.push_back(std::make_unique<RemoveUnreachableNodes>());
stages.push_back(std::make_unique<MultiEdgeMerger>());
Expand All @@ -28,6 +29,6 @@ inline TransformationPipeline towardsTransitionSystems() {
return pipeline;
}

}
} // namespace Transformations

#endif //GOLEM_BASICTRANSFORMATIONPIPELINES_H
#endif // GOLEM_BASICTRANSFORMATIONPIPELINES_H
70 changes: 39 additions & 31 deletions src/transformers/NodeEliminator.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,13 +17,15 @@ void NodeEliminator::BackTranslator::notifyRemovedVertex(SymRef sym, Contraction

Transformer::TransformationResult NodeEliminator::transform(std::unique_ptr<ChcDirectedHyperGraph> graph) {
auto backTranslator = std::make_unique<BackTranslator>(graph->getLogic(), graph->predicateRepresentation());
while(true) {
while (true) {
auto adjancencyRepresentation = AdjacencyListsGraphRepresentation::from(*graph);
auto vertices = adjancencyRepresentation.getNodes();
// ignore entry and exit, those should never be removed
vertices.erase(std::remove_if(vertices.begin(), vertices.end(),[&graph](SymRef vertex) {
return vertex == graph->getEntry() or vertex == graph->getExit();
}), vertices.end());
vertices.erase(std::remove_if(vertices.begin(), vertices.end(),
[&graph](SymRef vertex) {
return vertex == graph->getEntry() or vertex == graph->getExit();
}),
vertices.end());
auto predicateWrapper = [&](SymRef vertex) {
return this->shouldEliminateNode(vertex, adjancencyRepresentation, *graph);
};
Expand All @@ -36,23 +38,26 @@ Transformer::TransformationResult NodeEliminator::transform(std::unique_ptr<ChcD
return {std::move(graph), std::move(backTranslator)};
}

bool NonLoopEliminatorPredicate::operator()(
SymRef vertex,
AdjacencyListsGraphRepresentation const & ar,
ChcDirectedHyperGraph const & graph) const {
bool NonLoopEliminatorPredicate::operator()(SymRef vertex, AdjacencyListsGraphRepresentation const & ar,
ChcDirectedHyperGraph const & graph) const {
// TODO: Remove the constraint about hyperEdge
return not hasHyperEdge(vertex, ar, graph) and isNonLoopNode(vertex, ar, graph);
}

bool SimpleNodeEliminatorPredicate::operator()(
SymRef vertex,
AdjacencyListsGraphRepresentation const & ar,
ChcDirectedHyperGraph const & graph) const {
bool NonLoopNestedEliminatorPredicate::operator()(SymRef vertex, AdjacencyListsGraphRepresentation const & ar,
ChcDirectedHyperGraph const & graph) const {
// TODO: Remove the constraint about hyperEdge
return not hasHyperEdge(vertex, ar, graph) and isNonLoopNode(vertex, ar, graph) and
isNonNestedLoopNode(vertex, ar, graph, vertex);
}

bool SimpleNodeEliminatorPredicate::operator()(SymRef vertex, AdjacencyListsGraphRepresentation const & ar,
ChcDirectedHyperGraph const & graph) const {
if (isSimpleNode(vertex, ar) and isNonLoopNode(vertex, ar, graph)) {
if (not hasHyperEdge(vertex, ar, graph)) { return true; }
// We eliminate the node also if it has outgoing hyperedges, but only if it has single normal incoming edge
auto const & incoming = ar.getIncomingEdgesFor(vertex);
if (not (incoming.size() == 1 and graph.getSources(incoming[0]).size() == 1)) { return false; }
if (not(incoming.size() == 1 and graph.getSources(incoming[0]).size() == 1)) { return false; }
// And these additional constraints hold
// 1. Candidate vertex must not be the target
// 2. Candidate vertex must be present exactly once in the sources.
Expand All @@ -61,9 +66,8 @@ bool SimpleNodeEliminatorPredicate::operator()(
auto const & outgoing = ar.getOutgoingEdgesFor(vertex);
return std::all_of(outgoing.begin(), outgoing.end(), [&](EId edge) {
auto const & sources = graph.getSources(edge);
return vertex != graph.getTarget(edge)
and std::count(sources.begin(), sources.end(), vertex) == 1
and std::find(sources.begin(), sources.end(), incomingSource) == sources.end();
return vertex != graph.getTarget(edge) and std::count(sources.begin(), sources.end(), vertex) == 1 and
std::find(sources.begin(), sources.end(), incomingSource) == sources.end();
});
}
return false;
Expand All @@ -76,16 +80,14 @@ InvalidityWitness NodeEliminator::BackTranslator::translate(InvalidityWitness wi
for (auto && [node, contractionResult] : nodeInfo) {
for (auto const & [replacing, inout] : contractionResult.replacing) {
if (replacing.id == eid) {
return std::make_pair(replacing,
std::make_pair(contractionResult.incoming[inout.first],
contractionResult.outgoing[inout.second])
);
return std::make_pair(replacing, std::make_pair(contractionResult.incoming[inout.first],
contractionResult.outgoing[inout.second]));
}
}
}
return std::nullopt;
};
while(true) {
while (true) {
auto & derivation = witness.getDerivation();
// For each step, check if it uses one of the newly created edges
bool stepReplaced = false;
Expand Down Expand Up @@ -114,24 +116,25 @@ InvalidityWitness NodeEliminator::BackTranslator::translate(InvalidityWitness wi
break;
}
}
if (not stepReplaced) {
break;
}
if (not stepReplaced) { break; }
}
return witness;
}

#define SANITY_CHECK(cond) if (not (cond)) { assert(false); return ValidityWitness{}; }
#define SANITY_CHECK(cond) \
if (not(cond)) { \
assert(false); \
return ValidityWitness{}; \
}
ValidityWitness NodeEliminator::BackTranslator::translate(ValidityWitness witness) {
if (this->removedNodes.empty()) { return witness; }
auto definitions = witness.getDefinitions();

auto definitionFor = [&](SymRef vertex) {
if (vertex == logic.getSym_false()) { return logic.getTerm_false(); }
if (vertex == logic.getSym_true()) { return logic.getTerm_true(); }
auto it = std::find_if(definitions.begin(), definitions.end(), [&](auto const & entry){
return logic.getSymRef(entry.first) == vertex;
});
auto it = std::find_if(definitions.begin(), definitions.end(),
[&](auto const & entry) { return logic.getSymRef(entry.first) == vertex; });
return it != definitions.end() ? it->second : PTRef_Undef;
};
VersionManager manager(logic);
Expand All @@ -142,7 +145,9 @@ ValidityWitness NodeEliminator::BackTranslator::translate(ValidityWitness witnes
auto const & info = nodeInfo.at(vertex);
vec<PTRef> incomingFormulas;
for (auto const & edge : info.incoming) {
if (edge.from.size() != 1) { throw std::logic_error("NonLoopEliminator should not have processed hyperEdges!"); }
if (edge.from.size() != 1) {
throw std::logic_error("NonLoopEliminator should not have processed hyperEdges!");
}
PTRef sourceDef = definitionFor(edge.from[0]);
SANITY_CHECK(sourceDef != PTRef_Undef); // Missing definition, cannot backtranslate
sourceDef = manager.baseFormulaToSource(sourceDef);
Expand Down Expand Up @@ -173,7 +178,8 @@ ValidityWitness NodeEliminator::BackTranslator::translate(ValidityWitness witnes
outgoingFormulas.push(logic.mkAnd(std::move(components)));
}
TermUtils::substitutions_map substitutionsMap;
utils.mapFromPredicate(predicateRepresentation.getSourceTermFor(vertex), predicateRepresentation.getTargetTermFor(vertex), substitutionsMap);
utils.mapFromPredicate(predicateRepresentation.getSourceTermFor(vertex),
predicateRepresentation.getTargetTermFor(vertex), substitutionsMap);
PTRef incomingPart = logic.mkOr(std::move(incomingFormulas));
PTRef outgoingPart = logic.mkOr(std::move(outgoingFormulas));
outgoingPart = utils.varSubstitute(outgoingPart, substitutionsMap);
Expand All @@ -191,7 +197,9 @@ ValidityWitness NodeEliminator::BackTranslator::translate(ValidityWitness witnes
PTRef vertexSolution = manager.targetFormulaToBase(itps[0]);
PTRef predicateSourceRepresentation = predicateRepresentation.getSourceTermFor(vertex);
// TODO: Fix handling of 0-ary predicates
PTRef predicate = logic.isVar(predicateSourceRepresentation) ? predicateSourceRepresentation : manager.sourceFormulaToBase(predicateSourceRepresentation);
PTRef predicate = logic.isVar(predicateSourceRepresentation)
? predicateSourceRepresentation
: manager.sourceFormulaToBase(predicateSourceRepresentation);
assert(definitions.count(predicate) == 0);
definitions.insert({predicate, vertexSolution});
}
Expand Down
18 changes: 15 additions & 3 deletions src/transformers/NodeEliminator.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,9 @@
* The predicate determining the nodes to eliminate is passed to the constructor.
*/
class NodeEliminator : public Transformer {
using predicate_t = std::function<bool(SymRef,AdjacencyListsGraphRepresentation const &, ChcDirectedHyperGraph const &)>;
using predicate_t =
std::function<bool(SymRef, AdjacencyListsGraphRepresentation const &, ChcDirectedHyperGraph const &)>;

public:
NodeEliminator(predicate_t shouldEliminateNode) : shouldEliminateNode(std::move(shouldEliminateNode)) {}

Expand All @@ -26,13 +28,14 @@ class NodeEliminator : public Transformer {
using ContractionResult = ChcDirectedHyperGraph::VertexContractionResult;

BackTranslator(Logic & logic, NonlinearCanonicalPredicateRepresentation predicateRepresentation)
: logic(logic), predicateRepresentation(std::move(predicateRepresentation)) {}
: logic(logic), predicateRepresentation(std::move(predicateRepresentation)) {}

InvalidityWitness translate(InvalidityWitness witness) override;

ValidityWitness translate(ValidityWitness witness) override;

void notifyRemovedVertex(SymRef sym, ContractionResult && edges);

private:
std::unordered_map<SymRef, ContractionResult, SymRefHash> nodeInfo;
std::vector<SymRef> removedNodes;
Expand All @@ -52,6 +55,15 @@ class NonLoopEliminator : public NodeEliminator {
NonLoopEliminator() : NodeEliminator(NonLoopEliminatorPredicate{}) {}
};

struct NonLoopNestedEliminatorPredicate {
bool operator()(SymRef, AdjacencyListsGraphRepresentation const &, ChcDirectedHyperGraph const & graph) const;
};

class NonLoopNestedEliminator : public NodeEliminator {
public:
NonLoopNestedEliminator() : NodeEliminator(NonLoopNestedEliminatorPredicate{}) {}
};

struct SimpleNodeEliminatorPredicate {
bool operator()(SymRef, AdjacencyListsGraphRepresentation const &, ChcDirectedHyperGraph const & graph) const;
};
Expand All @@ -61,4 +73,4 @@ class SimpleNodeEliminator : public NodeEliminator {
SimpleNodeEliminator() : NodeEliminator(SimpleNodeEliminatorPredicate()) {}
};

#endif //GOLEM_NODEELIMINATOR_H
#endif // GOLEM_NODEELIMINATOR_H