souffle::ast::transform::ReduceExistentialsTransformer Class Reference

Transformation pass to reduce unnecessary computation for relations that only appear in the form A(_,...,_). More...

#include <ReduceExistentials.h>

Inheritance diagram for souffle::ast::transform::ReduceExistentialsTransformer:

Collaboration diagram for souffle::ast::transform::ReduceExistentialsTransformer:

Public Member Functions
ReduceExistentialsTransformer *	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 reduce unnecessary computation for relations that only appear in the form A(_,...,_).

Definition at line 37 of file ReduceExistentials.h.

Member Function Documentation

clone()

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

inlineoverridevirtual

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

Definition at line 50 of file ReduceExistentials.h.

getName()

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

inlineoverridevirtual

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

Definition at line 46 of file ReduceExistentials.h.

transform()

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

overrideprivatevirtual

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

Definition at line 48 of file ReduceExistentials.cpp.

                                                   {
        for (Argument* arg : atom.getArguments()) {
            if (!isA<UnnamedVariable>(arg)) {
                return false;
            }
        }
        return true;
    };
 
    // Construct a dependency graph G where:
    // - Each relation is a node
    // - An edge (a,b) exists iff a uses b "non-existentially" in one of its *recursive* clauses
    // This way, a relation can be transformed into an existential form
    // if and only if all its predecessors can also be transformed.
    Graph<QualifiedName> relationGraph = Graph<QualifiedName>();
 
    // Add in the nodes
    for (Relation* relation : program.getRelations()) {
        relationGraph.insert(relation->getQualifiedName());
    }
 
    // Keep track of all relations that cannot be transformed
    std::set<QualifiedName> minimalIrreducibleRelations;
 
    auto* ioType = translationUnit.getAnalysis<analysis::IOTypeAnalysis>();
 
    for (Relation* relation : program.getRelations()) {
        // No I/O relations can be transformed
        if (ioType->isIO(relation)) {
            minimalIrreducibleRelations.insert(relation->getQualifiedName());
        }
        for (Clause* clause : getClauses(program, *relation)) {
            bool recursive = isRecursiveClause(*clause);
            visitDepthFirst(*clause, [&](const Atom& atom) {
                if (atom.getQualifiedName() == clause->getHead()->getQualifiedName()) {
                    return;
                }
 
                if (!isExistentialAtom(atom)) {
                    if (recursive) {
                        // Clause is recursive, so add an edge to the dependency graph
                        relationGraph.insert(clause->getHead()->getQualifiedName(), atom.getQualifiedName());
                    } else {
                        // Non-existential apperance in a non-recursive clause, so
                        // it's out of the picture
                        minimalIrreducibleRelations.insert(atom.getQualifiedName());
                    }
                }
            });
        }
    }
 
    // TODO (see issue #564): Don't transform relations appearing in aggregators
    //                        due to aggregator issues with unnamed variables.
    visitDepthFirst(program, [&](const Aggregator& aggr) {
        visitDepthFirst(
                aggr, [&](const Atom& atom) { minimalIrreducibleRelations.insert(atom.getQualifiedName()); });
    });
 
    // Run a DFS from each 'bad' source
    // A node is reachable in a DFS from an irreducible node if and only if it is
    // also an irreducible node
    std::set<QualifiedName> irreducibleRelations;
    for (QualifiedName relationName : minimalIrreducibleRelations) {
        relationGraph.visitDepthFirst(
                relationName, [&](const QualifiedName& subRel) { irreducibleRelations.insert(subRel); });
    }
 
    // All other relations are necessarily existential
    std::set<QualifiedName> existentialRelations;
    for (Relation* relation : program.getRelations()) {
        if (!getClauses(program, *relation).empty() && relation->getArity() != 0 &&
                irreducibleRelations.find(relation->getQualifiedName()) == irreducibleRelations.end()) {
            existentialRelations.insert(relation->getQualifiedName());
        }
    }
 
    // Reduce the existential relations
    for (QualifiedName relationName : existentialRelations) {
        Relation* originalRelation = getRelation(program, relationName);
 
        std::stringstream newRelationName;
        newRelationName << "+?exists_" << relationName;
 
        auto newRelation = mk<Relation>();
        newRelation->setQualifiedName(newRelationName.str());
        newRelation->setSrcLoc(originalRelation->getSrcLoc());
 
        // EqRel relations require two arguments, so remove it from the qualifier
        if (newRelation->getRepresentation() == RelationRepresentation::EQREL) {
            newRelation->setRepresentation(RelationRepresentation::DEFAULT);
        }
 
        // Keep all non-recursive clauses
        for (Clause* clause : getClauses(program, *originalRelation)) {
            if (!isRecursiveClause(*clause)) {
                auto newClause = mk<Clause>();
 
                newClause->setSrcLoc(clause->getSrcLoc());
                if (const ExecutionPlan* plan = clause->getExecutionPlan()) {
                    newClause->setExecutionPlan(souffle::clone(plan));
                }
                newClause->setHead(mk<Atom>(newRelationName.str()));
                for (Literal* lit : clause->getBodyLiterals()) {
                    newClause->addToBody(souffle::clone(lit));
                }
 
                program.addClause(std::move(newClause));
            }
        }
 
        program.addRelation(std::move(newRelation));
    }
 
    // Mapper that renames the occurrences of marked relations with their existential
    // counterparts
    struct renameExistentials : public NodeMapper {
        const std::set<QualifiedName>& relations;
 
        renameExistentials(std::set<QualifiedName>& relations) : relations(relations) {}
 
        Own<Node> operator()(Own<Node> node) const override {
            if (auto* clause = dynamic_cast<Clause*>(node.get())) {
                if (relations.find(clause->getHead()->getQualifiedName()) != relations.end()) {
                    // Clause is going to be removed, so don't rename it
                    return node;
                }
            } else if (auto* atom = dynamic_cast<Atom*>(node.get())) {
                if (relations.find(atom->getQualifiedName()) != relations.end()) {
                    // Relation is now existential, so rename it
                    std::stringstream newName;
                    newName << "+?exists_" << atom->getQualifiedName();
                    return mk<Atom>(newName.str());
                }
            }
            node->apply(*this);
            return node;
        }
    };
 
    renameExistentials update(existentialRelations);
    program.apply(update);
 
    bool changed = !existentialRelations.empty();
    return changed;
}
 
}  // namespace souffle::ast::transform

---

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

• ast/transform/ReduceExistentials.h
• ast/transform/ReduceExistentials.cpp