From 95c437446c9526ca35608708c57f60cf261c9b49 Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Tue, 22 Oct 2024 16:54:42 +0200 Subject: [PATCH] Preprocessing nested loops: nodes with nested loops are no longer removed --- .clang-files | 3 + src/graph/ChcGraph.cc | 16 +++++ src/graph/ChcGraph.h | 2 + .../BasicTransformationPipelines.h | 7 +- src/transformers/NodeEliminator.cc | 70 +++++++++++-------- src/transformers/NodeEliminator.h | 18 ++++- 6 files changed, 79 insertions(+), 37 deletions(-) diff --git a/.clang-files b/.clang-files index 0f69e59ab..eebb3ebe0 100644 --- a/.clang-files +++ b/.clang-files @@ -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 diff --git a/src/graph/ChcGraph.cc b/src/graph/ChcGraph.cc index bb3a5a55c..76561b387 100644 --- a/src/graph/ChcGraph.cc +++ b/src/graph/ChcGraph.cc @@ -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 diff --git a/src/graph/ChcGraph.h b/src/graph/ChcGraph.h index ebbf348f4..261d384ed 100644 --- a/src/graph/ChcGraph.h +++ b/src/graph/ChcGraph.h @@ -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 &); diff --git a/src/transformers/BasicTransformationPipelines.h b/src/transformers/BasicTransformationPipelines.h index 70d36b571..b92768411 100644 --- a/src/transformers/BasicTransformationPipelines.h +++ b/src/transformers/BasicTransformationPipelines.h @@ -19,7 +19,8 @@ namespace Transformations { inline TransformationPipeline towardsTransitionSystems() { TransformationPipeline::pipeline_t stages; stages.push_back(std::make_unique()); - stages.push_back(std::make_unique()); + // stages.push_back(std::make_unique()); + stages.push_back(std::make_unique()); stages.push_back(std::make_unique()); stages.push_back(std::make_unique()); stages.push_back(std::make_unique()); @@ -28,6 +29,6 @@ inline TransformationPipeline towardsTransitionSystems() { return pipeline; } -} +} // namespace Transformations -#endif //GOLEM_BASICTRANSFORMATIONPIPELINES_H +#endif // GOLEM_BASICTRANSFORMATIONPIPELINES_H diff --git a/src/transformers/NodeEliminator.cc b/src/transformers/NodeEliminator.cc index 336bf7e44..4586f8020 100644 --- a/src/transformers/NodeEliminator.cc +++ b/src/transformers/NodeEliminator.cc @@ -17,13 +17,15 @@ void NodeEliminator::BackTranslator::notifyRemovedVertex(SymRef sym, Contraction Transformer::TransformationResult NodeEliminator::transform(std::unique_ptr graph) { auto backTranslator = std::make_unique(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); }; @@ -36,23 +38,26 @@ Transformer::TransformationResult NodeEliminator::transform(std::unique_ptrremovedNodes.empty()) { return witness; } auto definitions = witness.getDefinitions(); @@ -129,9 +133,8 @@ ValidityWitness NodeEliminator::BackTranslator::translate(ValidityWitness witnes 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); @@ -142,7 +145,9 @@ ValidityWitness NodeEliminator::BackTranslator::translate(ValidityWitness witnes auto const & info = nodeInfo.at(vertex); vec 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); @@ -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); @@ -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}); } diff --git a/src/transformers/NodeEliminator.h b/src/transformers/NodeEliminator.h index 34710c0c6..1151ac2c2 100644 --- a/src/transformers/NodeEliminator.h +++ b/src/transformers/NodeEliminator.h @@ -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; + using predicate_t = + std::function; + public: NodeEliminator(predicate_t shouldEliminateNode) : shouldEliminateNode(std::move(shouldEliminateNode)) {} @@ -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 nodeInfo; std::vector removedNodes; @@ -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; }; @@ -61,4 +73,4 @@ class SimpleNodeEliminator : public NodeEliminator { SimpleNodeEliminator() : NodeEliminator(SimpleNodeEliminatorPredicate()) {} }; -#endif //GOLEM_NODEELIMINATOR_H +#endif // GOLEM_NODEELIMINATOR_H