souffle::ast::transform::MagicSetTransformer::MagicSetCoreTransformer Class Reference

Core section of the magic set transformer. More...

#include <MagicSet.h>

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

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

Public Member Functions
MagicSetCoreTransformer *	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 void	addRelevantVariables (std::set< std::string > &variables, const std::vector< const BinaryConstraint * > eqConstraints)
	Get the closure of the given set of variables under appearance in the given eq constraints. More...
static Own< Atom >	createMagicAtom (const Atom *atom)
	Creates the magic atom associatd with the given (rel, adornment) pair. More...
static Own< Clause >	createMagicClause (const Atom *atom, const VecOwn< Atom > &constrainingAtoms, const std::vector< const BinaryConstraint * > eqConstraints)
	Creates the magic clause centred around the given magic atom. More...
static std::string	getAdornment (const QualifiedName &name)
	Retrieves an adornment encoded in a given relation name. More...
static std::vector< const BinaryConstraint * >	getBindingEqualityConstraints (const Clause *clause)
	Get all potentially-binding equality constraints in a clause. More...
static QualifiedName	getMagicName (const QualifiedName &name)
	Gets a unique magic identifier for a given adorned relation name. More...
static bool	isAdorned (const QualifiedName &name)
	Checks if a given relation name is adorned. More...

Detailed Description

Core section of the magic set transformer.

Creates all magic rules and relations based on the preceding adornment, and adds them into rules as needed. Assumes that Normalisation, Labelling, and Adornment have all been performed.

Definition at line 286 of file MagicSet.h.

Member Function Documentation

addRelevantVariables()

void souffle::ast::transform::MagicSetCoreTransformer::addRelevantVariables ( std::set< std::string > &  variables, const std::vector< const BinaryConstraint * >  eqConstraints  )

staticprivate

Get the closure of the given set of variables under appearance in the given eq constraints.

Definition at line 1046 of file MagicSet.cpp.

                                                  { fullyBound &= contains(variables, var.getName()); });
        return fullyBound;
    };
 
    // Helper method to add all newly relevant variables given a lhs = rhs constraint
    auto addLocallyRelevantVariables = [&](const Argument* lhs, const Argument* rhs) {
        const auto* lhsVar = dynamic_cast<const ast::Variable*>(lhs);
        if (lhsVar == nullptr) return true;
 
        // if the rhs is fully bound, lhs is now bound
        if (!contains(variables, lhsVar->getName())) {
            if (isFullyBound(rhs)) {
                variables.insert(lhsVar->getName());
                return false;
            } else {
                return true;
            }
        }
 
        // if the rhs is a record, and lhs is a bound var, then all rhs vars are bound
        bool fixpointReached = true;
        if (const auto* rhsRec = dynamic_cast<const RecordInit*>(rhs)) {
            for (const auto* arg : rhsRec->getArguments()) {
                const auto* subVar = dynamic_cast<const ast::Variable*>(arg);
                assert(subVar != nullptr && "expected only variable arguments");
                if (!contains(variables, subVar->getName())) {
                    fixpointReached = false;
                    variables.insert(subVar->getName());
                }
            }
        }
 
        return fixpointReached;
    };
 
    // Keep adding in relevant variables until we reach a fixpoint
    bool fixpointReached = false;
    while (!fixpointReached) {
        fixpointReached = true;
        for (const auto* eqConstraint : eqConstraints) {
            assert(isEqConstraint(eqConstraint->getBaseOperator()) && "expected only eq constraints");
            fixpointReached &= addLocallyRelevantVariables(eqConstraint->getLHS(), eqConstraint->getRHS());
            fixpointReached &= addLocallyRelevantVariables(eqConstraint->getRHS(), eqConstraint->getLHS());
        }
    }
}
 
Own<Clause> MagicSetCoreTransformer::createMagicClause(const Atom* atom,
        const std::vector<Own<Atom>>& constrainingAtoms,
        const std::vector<const BinaryConstraint*> eqConstraints) {
    auto magicHead = createMagicAtom(atom);
    auto magicClause = mk<Clause>();

References souffle::contains().

Here is the call graph for this function:

clone()

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

inlineoverridevirtual

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

Definition at line 292 of file MagicSet.h.

                                                    {
        return new MagicSetCoreTransformer();
    }

createMagicAtom()

Own< Atom > souffle::ast::transform::MagicSetCoreTransformer::createMagicAtom ( const Atom *  atom )

staticprivate

Creates the magic atom associatd with the given (rel, adornment) pair.

Definition at line 1030 of file MagicSet.cpp.

                                             {
        if (adornmentMarker[i] == 'b') {
            magicAtom->addArgument(souffle::clone(args[i]));
        }
    }
 
    return magicAtom;
}
 
void MagicSetCoreTransformer::addRelevantVariables(
        std::set<std::string>& variables, const std::vector<const BinaryConstraint*> eqConstraints) {
    // Helper method to check if all variables in an argument are bound
    auto isFullyBound = [&](const Argument* arg) {
        bool fullyBound = true;

createMagicClause()

Own< Clause > souffle::ast::transform::MagicSetCoreTransformer::createMagicClause ( const Atom *  atom, const VecOwn< Atom > &  constrainingAtoms, const std::vector< const BinaryConstraint * >  eqConstraints  )

staticprivate

Creates the magic clause centred around the given magic atom.

Definition at line 1099 of file MagicSet.cpp.

                                 : constrainingAtoms) {
        magicClause->addToBody(souffle::clone(bindingAtom));
    }
 
    // Get the set of all variables that will be relevant to the magic clause
    std::set<std::string> relevantVariables;
    visitDepthFirst(
            constrainingAtoms, [&](const ast::Variable& var) { relevantVariables.insert(var.getName()); });
    visitDepthFirst(*magicHead, [&](const ast::Variable& var) { relevantVariables.insert(var.getName()); });
    addRelevantVariables(relevantVariables, eqConstraints);
 
    // Add in all eq constraints containing ONLY relevant variables
    for (const auto* eqConstraint : eqConstraints) {
        bool addConstraint = true;
        visitDepthFirst(*eqConstraint, [&](const ast::Variable& var) {
            if (!contains(relevantVariables, var.getName())) {
                addConstraint = false;
            }
        });
 
        if (addConstraint) magicClause->addToBody(souffle::clone(eqConstraint));
    }
 
    magicClause->setHead(std::move(magicHead));
    return magicClause;
}
 
std::vector<const BinaryConstraint*> MagicSetCoreTransformer::getBindingEqualityConstraints(
        const Clause* clause) {
    std::vector<const BinaryConstraint*> equalityConstraints;
    for (const auto* lit : clause->getBodyLiterals()) {
        const auto* bc = dynamic_cast<const BinaryConstraint*>(lit);

References souffle::clone().

Here is the call graph for this function:

getAdornment()

std::string souffle::ast::transform::MagicSetCoreTransformer::getAdornment ( const QualifiedName &  name )

staticprivate

Retrieves an adornment encoded in a given relation name.

Definition at line 1012 of file MagicSet.cpp.

                                                                             {
    assert(isAdorned(name) && "cannot magify unadorned predicates");
    QualifiedName magicRelName(name);
    magicRelName.prepend("@magic");
    return magicRelName;

getBindingEqualityConstraints()

std::vector< const BinaryConstraint * > souffle::ast::transform::MagicSetCoreTransformer::getBindingEqualityConstraints ( const Clause *  clause )

staticprivate

Get all potentially-binding equality constraints in a clause.

Definition at line 1133 of file MagicSet.cpp.

                                                                           {
            bool containsAggrs = false;
            visitDepthFirst(*bc, [&](const Aggregator& /* aggr */) { containsAggrs = true; });
            if (!containsAggrs) {
                equalityConstraints.push_back(bc);
            }
        }
    }
    return equalityConstraints;
}
 
bool MagicSetCoreTransformer::transform(TranslationUnit& translationUnit) {
    Program& program = translationUnit.getProgram();
    std::set<Own<Clause>> clausesToRemove;
    std::set<Own<Clause>> clausesToAdd;
 

References souffle::ast::visitDepthFirst().

Here is the call graph for this function:

getMagicName()

QualifiedName souffle::ast::transform::MagicSetCoreTransformer::getMagicName ( const QualifiedName &  name )

staticprivate

Gets a unique magic identifier for a given adorned relation name.

Definition at line 1023 of file MagicSet.cpp.

                                                                   {
    auto origRelName = atom->getQualifiedName();
    auto args = atom->getArguments();
 
    auto magicAtom = mk<Atom>(getMagicName(origRelName));

References souffle::ast::Atom::getArguments(), and souffle::ast::Atom::getQualifiedName().

Here is the call graph for this function:

getName()

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

inlineoverridevirtual

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

Definition at line 288 of file MagicSet.h.

                                       {
        return "MagicSetCoreTransformer";
    }

isAdorned()

bool souffle::ast::transform::MagicSetCoreTransformer::isAdorned ( const QualifiedName &  name )

staticprivate

Checks if a given relation name is adorned.

Definition at line 992 of file MagicSet.cpp.

                              {' && finalQualifier[finalQualifier.length() - 1] == '}') {
        for (size_t i = 1; i < finalQualifier.length() - 1; i++) {
            char curBindingType = finalQualifier[i];
            if (curBindingType != 'b' && curBindingType != 'f') {
                return false;
            }
        }
        return true;
    }
    return false;
}
 
std::string MagicSetCoreTransformer::getAdornment(const QualifiedName& name) {
    assert(isAdorned(name) && "relation not adorned");
    auto qualifiers = name.getQualifiers();
    auto finalQualifier = qualifiers[qualifiers.size() - 1];
    std::stringstream binding;

References i.

transform()

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

overrideprivatevirtual

Perform the Magic Set Transformation

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

Definition at line 1150 of file MagicSet.cpp.

                            : program.getClauses()) {
        clausesToRemove.insert(souffle::clone(clause));
 
        const auto* head = clause->getHead();
        auto relName = head->getQualifiedName();
 
        // (1) Add the refined clause
        if (!isAdorned(relName)) {
            // Unadorned relations need not be refined, as every possible tuple is relevant
            clausesToAdd.insert(souffle::clone(clause));
        } else {
            // Refine the clause with a prepended magic atom
            auto magicAtom = createMagicAtom(head);
            auto refinedClause = mk<Clause>();
            refinedClause->setHead(souffle::clone(head));
            refinedClause->addToBody(souffle::clone(magicAtom));
            for (auto* literal : clause->getBodyLiterals()) {
                refinedClause->addToBody(souffle::clone(literal));
            }
            clausesToAdd.insert(std::move(refinedClause));
        }
 
        // (2) Add the associated magic rules
        std::vector<const BinaryConstraint*> eqConstraints = getBindingEqualityConstraints(clause);
        std::vector<Own<Atom>> atomsToTheLeft;
        if (isAdorned(relName)) {
            // Add the specialising head atom
            // Output relations are not specialised, and so the head will not contribute to specialisation
            atomsToTheLeft.push_back(createMagicAtom(clause->getHead()));
        }
        for (const auto* lit : clause->getBodyLiterals()) {
            const auto* atom = dynamic_cast<const Atom*>(lit);
            if (atom == nullptr) continue;
            if (!isAdorned(atom->getQualifiedName())) {
                atomsToTheLeft.push_back(souffle::clone(atom));
                continue;
            }
 
            // Need to create a magic rule
            auto magicClause = createMagicClause(atom, atomsToTheLeft, eqConstraints);
            atomsToTheLeft.push_back(souffle::clone(atom));
            clausesToAdd.insert(std::move(magicClause));
        }
    }
 
    for (auto& clause : clausesToAdd) {
        program.addClause(souffle::clone(clause));
    }
    for (const auto& clause : clausesToRemove) {
        program.removeClause(clause.get());
    }
 
    // Add in the magic relations
    bool changed = false;
    for (const auto* rel : program.getRelations()) {
        const auto& origName = rel->getQualifiedName();
        if (!isAdorned(origName)) continue;
        auto magicRelation = mk<Relation>(getMagicName(origName));
        auto attributes = getRelation(program, origName)->getAttributes();
        auto adornmentMarker = getAdornment(origName);
        for (size_t i = 0; i < attributes.size(); i++) {
            if (adornmentMarker[i] == 'b') {
                magicRelation->addAttribute(souffle::clone(attributes[i]));
            }
        }
        changed = true;
        program.addRelation(std::move(magicRelation));
    }
    return changed;
}
 
}  // namespace souffle::ast::transform

References souffle::clone().

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