souffle::ast::transform::MagicSetTransformer::LabelDatabaseTransformer::PositiveLabellingTransformer Class Reference

Runs the second stage of the labelling algorithm. More...

#include <MagicSet.h>

Inheritance diagram for souffle::ast::transform::MagicSetTransformer::LabelDatabaseTransformer::PositiveLabellingTransformer:

Collaboration diagram for souffle::ast::transform::MagicSetTransformer::LabelDatabaseTransformer::PositiveLabellingTransformer:

Public Member Functions
PositiveLabellingTransformer *	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

Static Private Member Functions
static QualifiedName	getPositiveLabel (const QualifiedName &name, size_t count)
	Provide a unique name for a positively labelled relation copy. More...

Detailed Description

Runs the second stage of the labelling algorithm.

Separates out the dependencies of negatively labelled atoms from the main SCC graph, preventing them from affecting stratification after magic. Note: Negative labelling must have been run first.

Definition at line 208 of file MagicSet.h.

Member Function Documentation

clone()

PositiveLabellingTransformer* souffle::ast::transform::MagicSetTransformer::LabelDatabaseTransformer::PositiveLabellingTransformer::clone ( ) const

inlineoverridevirtual

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

Definition at line 214 of file MagicSet.h.

                                                         {
        return new PositiveLabellingTransformer();
    }

getName()

std::string souffle::ast::transform::MagicSetTransformer::LabelDatabaseTransformer::PositiveLabellingTransformer::getName ( ) const

inlineoverridevirtual

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

Definition at line 210 of file MagicSet.h.

                                       {
        return "PositiveLabellingTransformer";
    }

getPositiveLabel()

QualifiedName souffle::ast::transform::PositiveLabellingTransformer::getPositiveLabel ( const QualifiedName &  name, size_t  count  )

staticprivate

Provide a unique name for a positively labelled relation copy.

Definition at line 787 of file MagicSet.cpp.

                                                                             {
    auto qualifiers = name.getQualifiers();
    assert(!qualifiers.empty() && "unexpected empty qualifier list");
    return qualifiers[0] == "@neglabel";
}

transform()

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

overrideprivatevirtual

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

Definition at line 868 of file MagicSet.cpp.

                                                                              {
        size_t numNeggedRelations = 0;
        const auto& stratumRels = sccGraph.getInternalRelations(stratum);
 
        // Count how many relations in this node are neglabelled
        for (const auto* rel : stratumRels) {
            if (isNegativelyLabelled(rel->getQualifiedName())) {
                numNeggedRelations++;
            }
        }
        assert((numNeggedRelations == 0 || numNeggedRelations == stratumRels.size()) &&
                "stratum cannot contain a mix of neglabelled and unlabelled relations");
 
        if (numNeggedRelations > 0) {
            // This is a neglabelled stratum that will not be copied
            neglabelledStrata.insert(stratum);
        } else {
            // This is a regular stratum that may be copied
            originalStrataCopyCount[stratum] = 0;
        }
    }
 
    // Keep track of strata that depend on each stratum
    // e.g. T in dependentStrata[S] iff a relation in T depends on a relation in S
    std::map<size_t, std::set<size_t>> dependentStrata;
    for (size_t stratum = 0; stratum < sccGraph.getNumberOfSCCs(); stratum++) {
        dependentStrata[stratum] = std::set<size_t>();
    }
    for (const auto* rel : program.getRelations()) {
        size_t stratum = sccGraph.getSCC(rel);
        precedenceGraph.visitDepthFirst(rel, [&](const auto* dependentRel) {
            dependentStrata[stratum].insert(sccGraph.getSCC(dependentRel));
        });
    }
 
    // Label the positive derived literals in the clauses of neglabelled relations
    // Need a new copy of those relations up to that point for each
    for (size_t stratum = 0; stratum < sccGraph.getNumberOfSCCs(); stratum++) {
        if (!contains(neglabelledStrata, stratum)) continue;
 
        // Rename in the current stratum
        for (const auto* rel : sccGraph.getInternalRelations(stratum)) {
            assert(isNegativelyLabelled(rel->getQualifiedName()) &&
                    "should only be looking at neglabelled strata");
            const auto& clauses = getClauses(program, *rel);
            std::set<QualifiedName> relsToCopy;
 
            // Get the unignored unlabelled relations appearing in the rules
            for (const auto* clause : clauses) {
                visitDepthFirst(*clause, [&](const Atom& atom) {
                    const auto& name = atom.getQualifiedName();
                    if (!contains(relationsToNotLabel, name) && !isNegativelyLabelled(name)) {
                        relsToCopy.insert(name);
                    }
                });
            }
 
            // Positively label them
            for (auto* clause : clauses) {
                std::map<QualifiedName, QualifiedName> labelledNames;
                for (const auto& relName : relsToCopy) {
                    size_t relStratum = sccGraph.getSCC(getRelation(program, relName));
                    size_t copyCount = originalStrataCopyCount.at(relStratum) + 1;
                    labelledNames[relName] = getPositiveLabel(relName, copyCount);
                }
                renameAtoms(*clause, labelledNames);
            }
        }
 
        // Create the rules (from all previous strata) for the newly positive labelled literals
        for (int preStratum = stratum - 1; preStratum >= 0; preStratum--) {
            if (contains(neglabelledStrata, preStratum)) continue;
            if (!contains(dependentStrata[preStratum], stratum)) continue;
 
            for (const auto* rel : sccGraph.getInternalRelations(preStratum)) {
                if (contains(relationsToNotLabel, rel->getQualifiedName())) continue;
 
                for (const auto* clause : getClauses(program, rel->getQualifiedName())) {
                    // Grab the new names for all unignored unlabelled positive atoms
                    std::map<QualifiedName, QualifiedName> labelledNames;
                    visitDepthFirst(*clause, [&](const Atom& atom) {
                        const auto& relName = atom.getQualifiedName();
                        if (contains(relationsToNotLabel, relName) || isNegativelyLabelled(relName)) return;
                        size_t relStratum = sccGraph.getSCC(getRelation(program, relName));
                        size_t copyCount = originalStrataCopyCount.at(relStratum) + 1;
                        labelledNames[relName] = getPositiveLabel(relName, copyCount);
                    });
 
                    // Rename atoms accordingly
                    auto labelledClause = souffle::clone(clause);
                    renameAtoms(*labelledClause, labelledNames);
                    program.addClause(std::move(labelledClause));
                }
            }
 
            originalStrataCopyCount[preStratum]++;
        }
    }
 
    // Add each copy for each relation in
    bool changed = false;
    for (const auto& [stratum, numCopies] : originalStrataCopyCount) {
        const auto& stratumRels = sccGraph.getInternalRelations(stratum);
        for (size_t copy = 0; copy < numCopies; copy++) {
            for (auto* rel : stratumRels) {
                auto newRelation = souffle::clone(rel);
                newRelation->setQualifiedName(getPositiveLabel(newRelation->getQualifiedName(), copy + 1));
                program.addRelation(std::move(newRelation));
                changed = true;
            }
        }
    }
    return changed;
}
 
bool MagicSetCoreTransformer::isAdorned(const QualifiedName& name) {
    // Grab the final qualifier - this is where the adornment is if it exists
    auto qualifiers = name.getQualifiers();
    assert(!qualifiers.empty() && "unexpected empty qualifier list");
    auto finalQualifier = qualifiers[qualifiers.size() - 1];

References rel().

Here is the call graph for this function:

---

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

• ast/transform/MagicSet.h
• ast/transform/MagicSet.cpp