souffle::ast::BindingStore Class Reference

#include <BindingStore.h>

Collaboration diagram for souffle::ast::BindingStore:

Public Member Functions
	BindingStore (const Clause *clause)
void	bindVariableStrongly (std::string varName)
	Mark the given variable as strongly bound. More...
void	bindVariableWeakly (std::string varName)
	Mark the given variable as weakly bound. More...
bool	isBound (const Argument *arg) const
	Check if an argument is bound. More...
bool	isBound (std::string varName) const
	Check if a variable is bound. More...
size_t	numBoundArguments (const Atom *atom) const
	Counts the number of bound arguments in the given atom. More...

Private Types
using	ConjBindingSet = std::set< std::string >
using	DisjBindingSet = std::set< ConjBindingSet >

Private Member Functions
void	addBindingDependency (std::string variable, ConjBindingSet dependency)
	Add a new conjunction of variables as a potential binder for a given variable. More...
void	generateBindingDependencies (const Clause *clause)
	Generate all binding dependencies implied by the constraints within a given clause. More...
void	processEqualityBindings (const Argument *lhs, const Argument *rhs)
	Add binding dependencies formed on lhs by a <lhs> = <rhs> equality constraint. More...
bool	reduceDependencies ()
	Reduce the full set of dependencies for all tracked variables, binding whatever needs to be bound. More...
ConjBindingSet	reduceDependency (const ConjBindingSet &origDependency)
	Reduce a conjunctive set of dependencies based on the current bound variable set. More...
DisjBindingSet	reduceDependency (const DisjBindingSet &origDependency)
	Reduce a disjunctive set of variable dependencies based on the current bound variable set. More...

Private Attributes
std::set< std::string >	stronglyBoundVariables {}
std::map< std::string, DisjBindingSet >	variableDependencies {}
std::set< std::string >	weaklyBoundVariables {}

Detailed Description

Definition at line 38 of file BindingStore.h.

Member Typedef Documentation

ConjBindingSet

using souffle::ast::BindingStore::ConjBindingSet = std::set<std::string>

private

Definition at line 83 of file BindingStore.h.

DisjBindingSet

using souffle::ast::BindingStore::DisjBindingSet = std::set<ConjBindingSet>

private

Definition at line 84 of file BindingStore.h.

Constructor & Destructor Documentation

BindingStore()

souffle::ast::BindingStore::BindingStore

(

const Clause *

clause

)

Definition at line 42 of file BindingStore.cpp.

                                                             {
        bool containsAggregators = false;
        visitDepthFirst(bc, [&](const Aggregator& /* aggr */) { containsAggregators = true; });

References souffle::ast::BinaryConstraint::getBaseOperator(), souffle::isEqConstraint(), and souffle::ast::visitDepthFirst().

Here is the call graph for this function:

Member Function Documentation

addBindingDependency()

void souffle::ast::BindingStore::addBindingDependency ( std::string  variable, ConjBindingSet  dependency  )

inlineprivate

Add a new conjunction of variables as a potential binder for a given variable.

The variable is considered bound if all variables in the conjunction are bound.

Definition at line 94 of file BindingStore.h.

bindVariableStrongly()

void souffle::ast::BindingStore::bindVariableStrongly ( std::string  varName )

inline

Mark the given variable as strongly bound.

Strongly bound variables can be used to bind functor arguments. This is the usual case, e.g. body atom appearances

Definition at line 54 of file BindingStore.h.

                                          {
        return contains(stronglyBoundVariables, varName) || contains(weaklyBoundVariables, varName);
    }

bindVariableWeakly()

void souffle::ast::BindingStore::bindVariableWeakly ( std::string  varName )

inline

Mark the given variable as weakly bound.

Weakly bound variables cannot be used to bind functor arguments. E.g. bound head arguments in MST adorned relations

Definition at line 66 of file BindingStore.h.

       :
    // Helper types to represent a disjunction of several dependency sets

Referenced by souffle::ast::transform::MagicSetTransformer::AdornDatabaseTransformer::adornClause().

generateBindingDependencies()

void souffle::ast::BindingStore::generateBindingDependencies ( const Clause *  clause )

private

Generate all binding dependencies implied by the constraints within a given clause.

Definition at line 47 of file BindingStore.cpp.

                                  : relevantEqConstraints) {
        processEqualityBindings(eqConstraint->getLHS(), eqConstraint->getRHS());
        processEqualityBindings(eqConstraint->getRHS(), eqConstraint->getLHS());
    }
}
 
void BindingStore::processEqualityBindings(const Argument* lhs, const Argument* rhs) {
    // Only care about equalities affecting the bound status of variables
    const auto* var = dynamic_cast<const Variable*>(lhs);
    if (var == nullptr) return;
 
    // If all variables on the rhs are bound, then lhs is also bound

isBound() [1/2]

bool souffle::ast::BindingStore::isBound

(

const Argument *

arg

)

const

Check if an argument is bound.

Definition at line 149 of file BindingStore.cpp.

                                   {
        return true;
    } else {
        return false;
    }
}
 
size_t BindingStore::numBoundArguments(const Atom* atom) const {
    size_t count = 0;
    for (const auto* arg : atom->getArguments()) {
        if (isBound(arg)) {
            count++;
        }

isBound() [2/2]

bool souffle::ast::BindingStore::isBound ( std::string  varName ) const

inline

Check if a variable is bound.

Definition at line 71 of file BindingStore.h.

                                            {};
    std::set<std::string> weaklyBoundVariables{};

numBoundArguments()

size_t souffle::ast::BindingStore::numBoundArguments

(

const Atom *

atom

)

const

Counts the number of bound arguments in the given atom.

Definition at line 166 of file BindingStore.cpp.

processEqualityBindings()

void souffle::ast::BindingStore::processEqualityBindings ( const Argument *  lhs, const Argument *  rhs  )

private

Add binding dependencies formed on lhs by a <lhs> = <rhs> equality constraint.

Definition at line 65 of file BindingStore.cpp.

                                                      { depSet.insert(subVar.getName()); });
    addBindingDependency(var->getName(), depSet);
 
    // If the lhs is bound, then all args in the rec on the rhs are also bound
    if (const auto* rec = dynamic_cast<const RecordInit*>(rhs)) {
        for (const auto* arg : rec->getArguments()) {
            const auto* subVar = dynamic_cast<const Variable*>(arg);
            assert(subVar != nullptr && "expected args to be variables");
            addBindingDependency(subVar->getName(), BindingStore::ConjBindingSet({var->getName()}));
        }
    }
}
 
BindingStore::ConjBindingSet BindingStore::reduceDependency(
        const BindingStore::ConjBindingSet& origDependency) {
    BindingStore::ConjBindingSet newDependency;
    for (const auto& var : origDependency) {
        // Only keep unbound variables in the dependency
        if (!contains(stronglyBoundVariables, var)) {

reduceDependencies()

bool souffle::ast::BindingStore::reduceDependencies ( )

private

Reduce the full set of dependencies for all tracked variables, binding whatever needs to be bound.

Definition at line 109 of file BindingStore.cpp.

                                                       {
            changed = true;
            continue;
        }
 
        // Reduce the dependency set based on bound variables
        auto newDependencies = reduceDependency(dependencies);
        if (newDependencies.empty() || newDependencies.size() < dependencies.size()) {
            // At least one dependency has been satisfied, so variable is now bound
            changed = true;
            variablesToBind.insert(headVar);
            continue;
        }
        newVariableDependencies[headVar] = newDependencies;
        changed |= (newDependencies != dependencies);
    }
 
    // Bind variables that need to be bound
    for (auto var : variablesToBind) {
        stronglyBoundVariables.insert(var);
    }
 
    // Repeat it recursively if any changes happened, until we reach a fixpoint
    if (changed) {
        variableDependencies = newVariableDependencies;
        reduceDependencies();
        return true;
    }
    assert(variableDependencies == newVariableDependencies && "unexpected change");
    return false;
}
 
bool BindingStore::isBound(const Argument* arg) const {
    if (const auto* var = dynamic_cast<const Variable*>(arg)) {
        return isBound(var->getName());
    } else if (const auto* term = dynamic_cast<const Term*>(arg)) {
        for (const auto* subArg : term->getArguments()) {
            if (!isBound(subArg)) {

reduceDependency() [1/2]

BindingStore::ConjBindingSet souffle::ast::BindingStore::reduceDependency ( const ConjBindingSet &  origDependency )

private

Reduce a conjunctive set of dependencies based on the current bound variable set.

Definition at line 85 of file BindingStore.cpp.

                                                          {
    BindingStore::DisjBindingSet newDependencies;
    for (const auto& dep : origDependency) {
        auto newDep = reduceDependency(dep);
        if (!newDep.empty()) {

reduceDependency() [2/2]

BindingStore::DisjBindingSet souffle::ast::BindingStore::reduceDependency ( const DisjBindingSet &  origDependency )

private

Reduce a disjunctive set of variable dependencies based on the current bound variable set.

Definition at line 97 of file BindingStore.cpp.

                                      {
    bool changed = false;
    std::map<std::string, BindingStore::DisjBindingSet> newVariableDependencies;
    std::set<std::string> variablesToBind;
 
    // Reduce each variable's set of dependencies one by one

Field Documentation

stronglyBoundVariables

std::set<std::string> souffle::ast::BindingStore::stronglyBoundVariables {}

private

Definition at line 86 of file BindingStore.h.

variableDependencies

std::map<std::string, DisjBindingSet> souffle::ast::BindingStore::variableDependencies {}

private

Definition at line 88 of file BindingStore.h.

weaklyBoundVariables

std::set<std::string> souffle::ast::BindingStore::weaklyBoundVariables {}

private

Definition at line 87 of file BindingStore.h.

---

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

• ast/utility/BindingStore.h
• ast/utility/BindingStore.cpp