souffle::ast::transform::PartitionBodyLiteralsTransformer Class Reference

Transformation pass to move literals into new clauses if they are independent of remaining literals. More...

#include <PartitionBodyLiterals.h>

Inheritance diagram for souffle::ast::transform::PartitionBodyLiteralsTransformer:

Collaboration diagram for souffle::ast::transform::PartitionBodyLiteralsTransformer:

Public Member Functions
PartitionBodyLiteralsTransformer *	clone () const override
std::string	getName () const override
Public Member Functions inherited from souffle::ast::transform::Transformer
bool	apply (TranslationUnit &translationUnit)
virtual	~Transformer ()=default

Private Member Functions
bool	transform (TranslationUnit &translationUnit) override

Detailed Description

Transformation pass to move literals into new clauses if they are independent of remaining literals.

E.g. a(x) :- b(x), c(y), d(y), e(z). is transformed into:

• a(x) :- b(x), newrel1(), newrel2().
• newrel1() :- c(y), d(y).
• newrel2() :- e(z).

Definition at line 49 of file PartitionBodyLiterals.h.

Member Function Documentation

clone()

PartitionBodyLiteralsTransformer* souffle::ast::transform::PartitionBodyLiteralsTransformer::clone ( ) const

inlineoverridevirtual

Implements souffle::ast::transform::Transformer.

Definition at line 66 of file PartitionBodyLiterals.h.

getName()

std::string souffle::ast::transform::PartitionBodyLiteralsTransformer::getName ( ) const

inlineoverridevirtual

Implements souffle::ast::transform::Transformer.

Definition at line 62 of file PartitionBodyLiterals.h.

transform()

bool souffle::ast::transform::PartitionBodyLiteralsTransformer::transform ( TranslationUnit &  translationUnit )

overrideprivatevirtual

Implements souffle::ast::transform::Transformer.

Definition at line 41 of file PartitionBodyLiterals.cpp.

                                                       {
        // Create the variable dependency graph G
        Graph<std::string> variableGraph = Graph<std::string>();
        std::set<std::string> ruleVariables;
 
        // Add in the nodes
        // The nodes of G are the variables in the rule
        visitDepthFirst(clause, [&](const ast::Variable& var) {
            variableGraph.insert(var.getName());
            ruleVariables.insert(var.getName());
        });
 
        // Add in the edges
        // Since we are only looking at reachability in the final graph, it is
        // enough to just add in an (undirected) edge from the first variable
        // in the literal to each of the other variables.
        std::vector<Literal*> literalsToConsider = clause.getBodyLiterals();
        literalsToConsider.push_back(clause.getHead());
 
        for (Literal* clauseLiteral : literalsToConsider) {
            std::set<std::string> literalVariables;
 
            // Store all variables in the literal
            visitDepthFirst(*clauseLiteral,
                    [&](const ast::Variable& var) { literalVariables.insert(var.getName()); });
 
            // No new edges if only one variable is present
            if (literalVariables.size() > 1) {
                std::string firstVariable = *literalVariables.begin();
                literalVariables.erase(literalVariables.begin());
 
                // Create the undirected edge
                for (const std::string& var : literalVariables) {
                    variableGraph.insert(firstVariable, var);
                    variableGraph.insert(var, firstVariable);
                }
            }
        }
 
        // Find the connected components of G
        std::set<std::string> seenNodes;
 
        // Find the connected component associated with the head
        std::set<std::string> headComponent;
        visitDepthFirst(
                *clause.getHead(), [&](const ast::Variable& var) { headComponent.insert(var.getName()); });
 
        if (!headComponent.empty()) {
            variableGraph.visitDepthFirst(*headComponent.begin(), [&](const std::string& var) {
                headComponent.insert(var);
                seenNodes.insert(var);
            });
        }
 
        // Compute all other connected components in the graph G
        std::set<std::set<std::string>> connectedComponents;
 
        for (std::string var : ruleVariables) {
            if (seenNodes.find(var) != seenNodes.end()) {
                // Node has already been added to a connected component
                continue;
            }
 
            // Construct the connected component
            std::set<std::string> component;
            variableGraph.visitDepthFirst(var, [&](const std::string& child) {
                component.insert(child);
                seenNodes.insert(child);
            });
            connectedComponents.insert(component);
        }
 
        if (connectedComponents.empty()) {
            // No separate connected components, so no point partitioning
            return;
        }
 
        // Need to extract some disconnected lits!
        changed = true;
        std::vector<Atom*> replacementAtoms;
 
        // Construct the new rules
        for (const std::set<std::string>& component : connectedComponents) {
            // Come up with a unique new name for the relation
            static int disconnectedCount = 0;
            std::stringstream nextName;
            nextName << "+disconnected" << disconnectedCount;
            QualifiedName newRelationName = nextName.str();
            disconnectedCount++;
 
            // Create the extracted relation and clause for the component
            // newrelX() <- disconnectedLiterals(x).
            auto newRelation = mk<Relation>();
            newRelation->setQualifiedName(newRelationName);
            program.addRelation(std::move(newRelation));
 
            auto* disconnectedClause = new Clause();
            disconnectedClause->setSrcLoc(clause.getSrcLoc());
            disconnectedClause->setHead(mk<Atom>(newRelationName));
 
            // Find the body literals for this connected component
            std::vector<Literal*> associatedLiterals;
            for (Literal* bodyLiteral : clause.getBodyLiterals()) {
                bool associated = false;
                visitDepthFirst(*bodyLiteral, [&](const ast::Variable& var) {
                    if (component.find(var.getName()) != component.end()) {
                        associated = true;
                    }
                });
                if (associated) {
                    disconnectedClause->addToBody(souffle::clone(bodyLiteral));
                }
            }
 
            // Create the atom to replace all these literals
            replacementAtoms.push_back(new Atom(newRelationName));
 
            // Add the clause to the program
            clausesToAdd.push_back(disconnectedClause);
        }
 
        // Create the replacement clause
        // a(x) <- b(x), c(y), d(z). --> a(x) <- newrel0(), newrel1(), b(x).
        auto* replacementClause = new Clause();
        replacementClause->setSrcLoc(clause.getSrcLoc());
        replacementClause->setHead(souffle::clone(clause.getHead()));
 
        // Add the new propositions to the clause first
        for (Atom* newAtom : replacementAtoms) {
            replacementClause->addToBody(Own<Literal>(newAtom));
        }
 
        // Add the remaining body literals to the clause
        for (Literal* bodyLiteral : clause.getBodyLiterals()) {
            bool associated = false;
            bool hasVariables = false;
            visitDepthFirst(*bodyLiteral, [&](const ast::Variable& var) {
                hasVariables = true;
                if (headComponent.find(var.getName()) != headComponent.end()) {
                    associated = true;
                }
            });
            if (associated || !hasVariables) {
                replacementClause->addToBody(souffle::clone(bodyLiteral));
            }
        }
 
        // Replace the old clause with the new one
        clausesToRemove.push_back(&clause);
        clausesToAdd.push_back(replacementClause);
    });
 
    // Adjust the program
    for (Clause* newClause : clausesToAdd) {
        program.addClause(Own<Clause>(newClause));
    }
 
    for (const Clause* oldClause : clausesToRemove) {
        program.removeClause(oldClause);
    }
 
    return changed;
}
 
}  // namespace souffle::ast::transform

References souffle::clone(), souffle::ast::Clause::getBodyLiterals(), souffle::ast::Clause::getHead(), souffle::ast::Node::getSrcLoc(), and souffle::ast::visitDepthFirst().

Here is the call graph for this function:

---

The documentation for this class was generated from the following files:

• ast/transform/PartitionBodyLiterals.h
• ast/transform/PartitionBodyLiterals.cpp