souffle::ast::transform::MagicSetTransformer::AdornDatabaseTransformer Class Reference

Database adornment. More...

#include <MagicSet.h>

Inheritance diagram for souffle::ast::transform::MagicSetTransformer::AdornDatabaseTransformer:

Collaboration diagram for souffle::ast::transform::MagicSetTransformer::AdornDatabaseTransformer:

Public Member Functions
AdornDatabaseTransformer *	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 Types
using	adorned_predicate = std::pair< QualifiedName, std::string >

Private Member Functions
Own< Clause >	adornClause (const Clause *clause, const std::string &adornmentMarker)
	Returns the adorned version of a clause. More...
bool	hasAdornmentToProcess () const
	Check if any more relations need to be adorned. More...
adorned_predicate	nextAdornmentToProcess ()
	Pop off the next predicate adornment to process. More...
void	queueAdornment (const QualifiedName &relName, const std::string &adornmentMarker)
	Add an adornment to the ToDo queue if it hasn't been processed before. More...
bool	transform (TranslationUnit &translationUnit) override

Static Private Member Functions
static QualifiedName	getAdornmentID (const QualifiedName &relName, const std::string &adornmentMarker)
	Get the unique identifier corresponding to an adorned predicate. More...

Private Attributes
VecOwn< Clause >	adornedClauses
std::set< QualifiedName >	headAdornmentsSeen
std::set< adorned_predicate >	headAdornmentsToDo
VecOwn< Clause >	redundantClauses
std::set< QualifiedName >	weaklyIgnoredRelations

Detailed Description

Database adornment.

Adorns the rules of a database with variable flow and binding information. Prerequisite for the magic set transformation.

Definition at line 230 of file MagicSet.h.

Member Typedef Documentation

adorned_predicate

using souffle::ast::transform::MagicSetTransformer::AdornDatabaseTransformer::adorned_predicate = std::pair<QualifiedName, std::string>

private

Definition at line 241 of file MagicSet.h.

Member Function Documentation

adornClause()

Own< Clause > souffle::ast::transform::AdornDatabaseTransformer::adornClause ( const Clause *  clause, const std::string &  adornmentMarker  )

private

Returns the adorned version of a clause.

Definition at line 628 of file MagicSet.cpp.

                    : Suppose a new variable Y is marked as bound because of its appearance in a functor
     * Y=X+1, and X was already found to be bound:
     *  (1) If X was bound through a body atom, then the behaviour of typical magic-set is exhibited, where
     * the magic-set of Y is bounded by the values that X can take, which is bounded by induction.
     *  (2) If X was bound only through the head atom, then Y is only fixed to an appearance in a magic-atom.
     * In the presence of recursion, this can potentially lead to an infinitely-sized magic-set for an atom.
     *
     * Therefore, bound head atom vars should be marked as weakly bound.
     */
    for (size_t i = 0; i < adornmentMarker.length(); i++) {
        const auto* var = dynamic_cast<ast::Variable*>(headArgs[i]);
        assert(var != nullptr && "expected only variables in head");
        if (adornmentMarker[i] == 'b') {
            variableBindings.bindVariableWeakly(var->getName());
        }
    }
 
    // Create the adorned clause with an empty body
    auto adornedClause = mk<Clause>();
 
    // Copy over plans if needed
    if (clause->getExecutionPlan() != nullptr) {
        assert(contains(weaklyIgnoredRelations, clause->getHead()->getQualifiedName()) &&
                "clauses with plans should be ignored");
        adornedClause->setExecutionPlan(souffle::clone(clause->getExecutionPlan()));
    }
 
    // Create the head atom
    auto adornedHeadAtom = mk<Atom>(getAdornmentID(relName, adornmentMarker));
    assert((adornmentMarker == "" || headArgs.size() == adornmentMarker.length()) &&
            "adornment marker should correspond to head atom variables");
    for (const auto* arg : headArgs) {
        const auto* var = dynamic_cast<const ast::Variable*>(arg);
        assert(var != nullptr && "expected only variables in head");
        adornedHeadAtom->addArgument(souffle::clone(var));
    }
    adornedClause->setHead(std::move(adornedHeadAtom));
 
    // Add in adorned body literals
    std::vector<Own<Literal>> adornedBodyLiterals;
    for (const auto* lit : clause->getBodyLiterals()) {
        if (const auto* negation = dynamic_cast<const Negation*>(lit)) {
            // Negated atoms should not be adorned, but their clauses should be anyway
            const auto negatedAtomName = negation->getAtom()->getQualifiedName();
            assert(contains(weaklyIgnoredRelations, negatedAtomName) &&
                    "negated atoms should not be adorned");
            queueAdornment(negatedAtomName, "");
        }
 
        if (!isA<Atom>(lit)) {
            // Non-atoms are added directly
            adornedBodyLiterals.push_back(souffle::clone(lit));
            continue;
        }
 
        const auto* atom = dynamic_cast<const Atom*>(lit);
        assert(atom != nullptr && "expected atom");
 
        // Form the appropriate adornment marker
        std::stringstream atomAdornment;
        if (!contains(weaklyIgnoredRelations, atom->getQualifiedName())) {
            for (const auto* arg : atom->getArguments()) {
                const auto* var = dynamic_cast<const ast::Variable*>(arg);
                assert(var != nullptr && "expected only variables in atom");
                atomAdornment << (variableBindings.isBound(var->getName()) ? "b" : "f");
            }
        }
        auto currAtomAdornmentID = getAdornmentID(atom->getQualifiedName(), atomAdornment.str());
 
        // Add to the ToDo queue if needed
        queueAdornment(atom->getQualifiedName(), atomAdornment.str());
 
        // Add the adorned version to the clause
        auto adornedBodyAtom = souffle::clone(atom);
        adornedBodyAtom->setQualifiedName(currAtomAdornmentID);
        adornedBodyLiterals.push_back(std::move(adornedBodyAtom));
 
        // All arguments are now bound
        for (const auto* arg : atom->getArguments()) {
            const auto* var = dynamic_cast<const ast::Variable*>(arg);
            assert(var != nullptr && "expected only variables in atom");
            variableBindings.bindVariableStrongly(var->getName());
        }
    }
    adornedClause->setBodyLiterals(std::move(adornedBodyLiterals));
 
    return adornedClause;
}
 
bool AdornDatabaseTransformer::transform(TranslationUnit& translationUnit) {
    Program& program = translationUnit.getProgram();
    const auto& ioTypes = *translationUnit.getAnalysis<analysis::IOTypeAnalysis>();
    weaklyIgnoredRelations = getWeaklyIgnoredRelations(translationUnit);
 

References souffle::ast::BindingStore::bindVariableWeakly(), and i.

Here is the call graph for this function:

clone()

AdornDatabaseTransformer* souffle::ast::transform::MagicSetTransformer::AdornDatabaseTransformer::clone ( ) const

inlineoverridevirtual

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

Definition at line 236 of file MagicSet.h.

                                                     {
        return new AdornDatabaseTransformer();
    }

getAdornmentID()

QualifiedName souffle::ast::transform::AdornDatabaseTransformer::getAdornmentID ( const QualifiedName &  relName, const std::string &  adornmentMarker  )

staticprivate

Get the unique identifier corresponding to an adorned predicate.

Definition at line 618 of file MagicSet.cpp.

                                                                                                        {
    const auto& relName = clause->getHead()->getQualifiedName();
    const auto& headArgs = clause->getHead()->getArguments();
    BindingStore variableBindings(clause);
 

Referenced by queueAdornment().

getName()

std::string souffle::ast::transform::MagicSetTransformer::AdornDatabaseTransformer::getName ( ) const

inlineoverridevirtual

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

Definition at line 232 of file MagicSet.h.

                                       {
        return "AdornDatabaseTransformer";
    }

hasAdornmentToProcess()

bool souffle::ast::transform::MagicSetTransformer::AdornDatabaseTransformer::hasAdornmentToProcess ( ) const

inlineprivate

Check if any more relations need to be adorned.

Definition at line 265 of file MagicSet.h.

                                       {
        return !headAdornmentsToDo.empty();
    }

References headAdornmentsToDo.

Referenced by nextAdornmentToProcess().

nextAdornmentToProcess()

adorned_predicate souffle::ast::transform::MagicSetTransformer::AdornDatabaseTransformer::nextAdornmentToProcess ( )

inlineprivate

Pop off the next predicate adornment to process.

Definition at line 270 of file MagicSet.h.

                                               {
        assert(hasAdornmentToProcess() && "no adornment to pop");
        auto headAdornment = *(headAdornmentsToDo.begin());
        headAdornmentsToDo.erase(headAdornmentsToDo.begin());
        return headAdornment;
    }

References hasAdornmentToProcess(), and headAdornmentsToDo.

Here is the call graph for this function:

queueAdornment()

void souffle::ast::transform::MagicSetTransformer::AdornDatabaseTransformer::queueAdornment ( const QualifiedName &  relName, const std::string &  adornmentMarker  )

inlineprivate

Add an adornment to the ToDo queue if it hasn't been processed before.

Definition at line 256 of file MagicSet.h.

                                                                                        {
        auto adornmentID = getAdornmentID(relName, adornmentMarker);
        if (!contains(headAdornmentsSeen, adornmentID)) {
            headAdornmentsToDo.insert(std::make_pair(relName, adornmentMarker));
            headAdornmentsSeen.insert(adornmentID);
        }
    }

References souffle::contains(), getAdornmentID(), headAdornmentsSeen, and headAdornmentsToDo.

Here is the call graph for this function:

transform()

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

overrideprivatevirtual

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

Definition at line 730 of file MagicSet.cpp.

                         : program.getRelations()) {
        if (ioTypes.isOutput(rel) || ioTypes.isPrintSize(rel)) {
            queueAdornment(rel->getQualifiedName(), "");
        }
    }
 
    // Keep going while there's things to adorn
    while (hasAdornmentToProcess()) {
        // Pop off the next head adornment to do
        const auto& [relName, adornmentMarker] = nextAdornmentToProcess();
 
        // Add the adorned relation if needed
        if (adornmentMarker != "") {
            const auto* rel = getRelation(program, relName);
            assert(rel != nullptr && "relation does not exist");
 
            auto adornedRelation = mk<Relation>(getAdornmentID(relName, adornmentMarker));
            for (const auto* attr : rel->getAttributes()) {
                adornedRelation->addAttribute(souffle::clone(attr));
            }
            program.addRelation(std::move(adornedRelation));
        }
 
        // Adorn every clause correspondingly
        for (const auto* clause : getClauses(program, relName)) {
            if (adornmentMarker == "") {
                redundantClauses.push_back(souffle::clone(clause));
            }
            auto adornedClause = adornClause(clause, adornmentMarker);
            adornedClauses.push_back(std::move(adornedClause));
        }
    }
 
    // Swap over the redundant clauses with the adorned clauses
    for (const auto& clause : redundantClauses) {
        program.removeClause(clause.get());
    }
 
    for (auto& clause : adornedClauses) {
        program.addClause(souffle::clone(clause));
    }
 
    return !adornedClauses.empty() || !redundantClauses.empty();
}
 
QualifiedName NegativeLabellingTransformer::getNegativeLabel(const QualifiedName& name) {
    QualifiedName newName(name);
    newName.prepend("@neglabel");
    return newName;
}

References rel().

Here is the call graph for this function:

Field Documentation

adornedClauses

VecOwn<Clause> souffle::ast::transform::MagicSetTransformer::AdornDatabaseTransformer::adornedClauses

private

Definition at line 246 of file MagicSet.h.

headAdornmentsSeen

std::set<QualifiedName> souffle::ast::transform::MagicSetTransformer::AdornDatabaseTransformer::headAdornmentsSeen

private

Definition at line 244 of file MagicSet.h.

Referenced by queueAdornment().

headAdornmentsToDo

std::set<adorned_predicate> souffle::ast::transform::MagicSetTransformer::AdornDatabaseTransformer::headAdornmentsToDo

private

Definition at line 243 of file MagicSet.h.

Referenced by hasAdornmentToProcess(), nextAdornmentToProcess(), and queueAdornment().

redundantClauses

VecOwn<Clause> souffle::ast::transform::MagicSetTransformer::AdornDatabaseTransformer::redundantClauses

private

Definition at line 247 of file MagicSet.h.

weaklyIgnoredRelations

std::set<QualifiedName> souffle::ast::transform::MagicSetTransformer::AdornDatabaseTransformer::weaklyIgnoredRelations

private

Definition at line 248 of file MagicSet.h.

---

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

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