souffle::ast::transform::MinimiseProgramTransformer Class Reference

Transformation pass to remove equivalent rules. More...

#include <MinimiseProgram.h>

Inheritance diagram for souffle::ast::transform::MinimiseProgramTransformer:

Collaboration diagram for souffle::ast::transform::MinimiseProgramTransformer:

Public Member Functions
MinimiseProgramTransformer *	clone () const override
std::string	getName () const override
Public Member Functions inherited from souffle::ast::transform::Transformer
bool	apply (TranslationUnit &translationUnit)
virtual	~Transformer ()=default

Static Public Member Functions
static bool	areBijectivelyEquivalent (const analysis::NormalisedClause &left, const analysis::NormalisedClause &right)

Private Member Functions
bool	transform (TranslationUnit &translationUnit) override

Static Private Member Functions
static bool	existsValidPermutation (const analysis::NormalisedClause &left, const analysis::NormalisedClause &right, const std::vector< std::vector< unsigned int >> &permutationMatrix)
static bool	isValidPermutation (const analysis::NormalisedClause &left, const analysis::NormalisedClause &right, const std::vector< unsigned int > &permutation)
	– Bijective Equivalence Helper Methods – More...
static bool	reduceClauseBodies (TranslationUnit &translationUnit)
	Remove redundant literals within a clause. More...
static bool	reduceLocallyEquivalentClauses (TranslationUnit &translationUnit)
	– Sub-Transformations – More...
static bool	reduceSingletonRelations (TranslationUnit &translationUnit)
	Removes redundant singleton relations. More...
static bool	removeRedundantClauses (TranslationUnit &translationUnit)
	Remove clauses that are only satisfied if they are already satisfied. More...

Detailed Description

Transformation pass to remove equivalent rules.

Definition at line 36 of file MinimiseProgram.h.

Member Function Documentation

areBijectivelyEquivalent()

bool souffle::ast::transform::MinimiseProgramTransformer::areBijectivelyEquivalent ( const analysis::NormalisedClause &  left, const analysis::NormalisedClause &  right  )

static

Definition at line 190 of file MinimiseProgram.cpp.

                                                                 {
        return false;
    }
 
    // rules must be the same length to be equal
    if (leftElements.size() != rightElements.size()) {
        return false;
    }
 
    // head atoms must have the same arity (names do not matter)
    if (leftElements[0].params.size() != rightElements[0].params.size()) {
        return false;
    }
 
    // rules must have the same number of distinct variables
    if (leftVars.size() != rightVars.size()) {
        return false;
    }
 
    // rules must have the exact same set of constants
    if (left.getConstants() != right.getConstants()) {
        return false;
    }
 
    // set up the n x n permutation matrix, where n is the number of clause elements
    size_t size = leftElements.size();
    auto permutationMatrix = std::vector<std::vector<unsigned int>>(size);
    for (auto& i : permutationMatrix) {
        i = std::vector<unsigned int>(size);
    }
 
    // create permutation matrix
    for (size_t i = 0; i < size; i++) {
        for (size_t j = 0; j < size; j++) {
            if (leftElements[i].name == rightElements[j].name) {
                permutationMatrix[i][j] = 1;
            }
        }
    }
 
    // check if any of these permutations have valid variable mappings
    return existsValidPermutation(left, right, permutationMatrix);
}
 
bool MinimiseProgramTransformer::reduceLocallyEquivalentClauses(TranslationUnit& translationUnit) {
    Program& program = translationUnit.getProgram();
    const auto& normalisations = *translationUnit.getAnalysis<analysis::ClauseNormalisationAnalysis>();
 
    std::vector<Clause*> clausesToDelete;

clone()

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

inlineoverridevirtual

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

Definition at line 52 of file MinimiseProgram.h.

existsValidPermutation()

bool souffle::ast::transform::MinimiseProgramTransformer::existsValidPermutation ( const analysis::NormalisedClause &  left, const analysis::NormalisedClause &  right, const std::vector< std::vector< unsigned int >> &  permutationMatrix  )

staticprivate

Definition at line 53 of file MinimiseProgram.cpp.

                                                {
            if (permutationMatrix[i][j] == 1) {
                currentRow.push_back(j);
            }
        }
        validMoves.push_back(currentRow);
    }
 
    // extract the possible permutations, DFS style
    std::vector<unsigned int> seen(clauseSize);
    std::vector<unsigned int> currentPermutation;
    std::stack<std::vector<unsigned int>> todoStack;
 
    todoStack.push(validMoves[0]);
 
    size_t currentIdx = 0;
    while (!todoStack.empty()) {
        if (currentIdx == clauseSize) {
            // permutation is complete, check if it's valid
            if (isValidPermutation(left, right, currentPermutation)) {
                // valid permutation with valid mapping
                // therefore, the two clauses are equivalent!
                return true;
            }
 
            // Not valid yet, keep checking for more permutations
            if (currentIdx == 0) {
                // already at starting position, so no more permutations possible
                break;
            }
 
            // undo the last number added to the permutation
            currentIdx--;
            seen[currentPermutation[currentIdx]] = 0;
            currentPermutation.pop_back();
 
            // see if we can pick up other permutations
            continue;
        }
 
        // pull out the possibilities for the current point of the permutation
        std::vector<unsigned int> possibilities = todoStack.top();
        todoStack.pop();
        if (possibilities.empty()) {
            // no more possibilities at this point, so undo our last move
 
            if (currentIdx == 0) {
                // already at starting position, so no more permutations possible
                break;
            }
 
            currentIdx--;
            seen[currentPermutation[currentIdx]] = 0;
            currentPermutation.pop_back();
 
            // continue looking for permutations
            continue;
        }
 
        // try the next possibility
        unsigned int nextNum = possibilities[0];
 
        // update the possibility vector for the current position
        possibilities.erase(possibilities.begin());
        todoStack.push(possibilities);
 
        if (seen[nextNum] != 0u) {
            // number already seen in this permutation
            continue;
        } else {
            // number can be used
            seen[nextNum] = 1;
            currentPermutation.push_back(nextNum);
            currentIdx++;
 
            // if we havent reached the end of the permutation,
            // push up the valid moves for the next position
            if (currentIdx < clauseSize) {
                todoStack.push(validMoves[currentIdx]);
            }
        }
    }
 
    // checked all permutations, none were valid
    return false;
}
 
bool MinimiseProgramTransformer::isValidPermutation(const NormalisedClause& left,
        const NormalisedClause& right, const std::vector<unsigned int>& permutation) {
    const auto& leftElements = left.getElements();
    const auto& rightElements = right.getElements();
 

References i, and j.

getName()

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

inlineoverridevirtual

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

Definition at line 44 of file MinimiseProgram.h.

       :
    bool transform(TranslationUnit& translationUnit) override;
 

isValidPermutation()

bool souffle::ast::transform::MinimiseProgramTransformer::isValidPermutation ( const analysis::NormalisedClause &  left, const analysis::NormalisedClause &  right, const std::vector< unsigned int > &  permutation  )

staticprivate

– Bijective Equivalence Helper Methods –

Definition at line 147 of file MinimiseProgram.cpp.

                         : left.getConstants()) {
        variableMap[cst] = cst;
    }
 
    // Variables start off mapping to nothing
    for (const auto& var : left.getVariables()) {
        variableMap[var] = "";
    }
 
    // Pass through the all arguments in the first clause in sequence, mapping each to the corresponding
    // argument in the second clause under the literal permutation
    for (size_t i = 0; i < size; i++) {
        const auto& leftArgs = leftElements[i].params;
        const auto& rightArgs = rightElements[permutation[i]].params;
        for (size_t j = 0; j < leftArgs.size(); j++) {
            auto leftArg = leftArgs[j];
            auto rightArg = rightArgs[j];
            std::string currentMap = variableMap[leftArg];
            if (currentMap.empty()) {
                // unassigned yet, so assign it appropriately
                variableMap[leftArg] = rightArg;
            } else if (currentMap != rightArg) {
                // inconsistent mapping!
                // clauses cannot be equivalent under this permutation
                return false;
            }
        }
    }
 
    return true;
}
 
bool MinimiseProgramTransformer::areBijectivelyEquivalent(
        const NormalisedClause& left, const NormalisedClause& right) {
    const auto& leftElements = left.getElements();
    const auto& rightElements = right.getElements();
 

reduceClauseBodies()

bool souffle::ast::transform::MinimiseProgramTransformer::reduceClauseBodies ( TranslationUnit &  translationUnit )

staticprivate

Remove redundant literals within a clause.

Definition at line 394 of file MinimiseProgram.cpp.

                                                         {
            for (size_t j = 0; j < i; j++) {
                if (*bodyLiterals[i] == *bodyLiterals[j]) {
                    redundantPositions.insert(j);
                    break;
                }
            }
        }
 
        if (!redundantPositions.empty()) {
            auto minimisedClause = mk<Clause>();
            minimisedClause->setHead(souffle::clone(clause->getHead()));
            for (size_t i = 0; i < bodyLiterals.size(); i++) {
                if (!contains(redundantPositions, i)) {
                    minimisedClause->addToBody(souffle::clone(bodyLiterals[i]));
                }
            }
            clausesToAdd.insert(std::move(minimisedClause));
            clausesToRemove.insert(souffle::clone(clause));
        }
    }
 
    for (auto& clause : clausesToRemove) {
        program.removeClause(clause.get());
    }
    for (auto& clause : clausesToAdd) {
        program.addClause(souffle::clone(clause));
    }
 
    return !clausesToAdd.empty();
}
 
bool MinimiseProgramTransformer::transform(TranslationUnit& translationUnit) {
    bool changed = false;
    changed |= reduceClauseBodies(translationUnit);
    if (changed) translationUnit.invalidateAnalyses();
    changed |= removeRedundantClauses(translationUnit);

References i, and j.

reduceLocallyEquivalentClauses()

bool souffle::ast::transform::MinimiseProgramTransformer::reduceLocallyEquivalentClauses ( TranslationUnit &  translationUnit )

staticprivate

– Sub-Transformations –

Reduces locally-redundant clauses. A clause is locally-redundant if there is another clause within the same relation that computes the same set of tuples.

Definition at line 243 of file MinimiseProgram.cpp.

                       : program.getRelations()) {
        std::vector<std::vector<Clause*>> equivalenceClasses;
 
        for (Clause* clause : getClauses(program, *rel)) {
            bool added = false;
 
            for (std::vector<Clause*>& eqClass : equivalenceClasses) {
                const auto& normedRep = normalisations.getNormalisation(eqClass[0]);
                const auto& normedClause = normalisations.getNormalisation(clause);
                if (areBijectivelyEquivalent(normedRep, normedClause)) {
                    // clause belongs to an existing equivalence class, so delete it
                    eqClass.push_back(clause);
                    clausesToDelete.push_back(clause);
                    added = true;
                    break;
                }
            }
 
            if (!added) {
                // clause does not belong to any existing equivalence class, so keep it
                std::vector<Clause*> clauseToAdd = {clause};
                equivalenceClasses.push_back(clauseToAdd);
            }
        }
    }
 
    // remove non-representative clauses
    for (auto clause : clausesToDelete) {
        program.removeClause(clause);
    }
 
    // changed iff any clauses were deleted
    return !clausesToDelete.empty();
}
 
bool MinimiseProgramTransformer::reduceSingletonRelations(TranslationUnit& translationUnit) {
    // Note: This reduction is particularly useful in conjunction with the
    // body-partitioning transformation
    Program& program = translationUnit.getProgram();
    const auto& ioTypes = *translationUnit.getAnalysis<analysis::IOTypeAnalysis>();

References souffle::ast::getClauses(), and rel().

Here is the call graph for this function:

reduceSingletonRelations()

bool souffle::ast::transform::MinimiseProgramTransformer::reduceSingletonRelations ( TranslationUnit &  translationUnit )

staticprivate

Removes redundant singleton relations.

Singleton relations are relations with a single clause. A singleton relation is redundant if there exists another singleton relation that computes the same set of tuples.

Returns

true iff the program was changed

Definition at line 286 of file MinimiseProgram.cpp.

                       : program.getRelations()) {
        if (!ioTypes.isIO(rel) && getClauses(program, *rel).size() == 1) {
            Clause* clause = getClauses(program, *rel)[0];
            singletonRelationClauses.push_back(clause);
        }
    }
 
    // Keep track of clauses found to be redundant
    std::set<const Clause*> redundantClauses;
 
    // Keep track of canonical relation name for each redundant clause
    std::map<QualifiedName, QualifiedName> canonicalName;
 
    // Check pairwise equivalence of each singleton relation
    for (size_t i = 0; i < singletonRelationClauses.size(); i++) {
        const auto* first = singletonRelationClauses[i];
        if (redundantClauses.find(first) != redundantClauses.end()) {
            // Already found to be redundant, no need to check
            continue;
        }
 
        for (size_t j = i + 1; j < singletonRelationClauses.size(); j++) {
            const auto* second = singletonRelationClauses[j];
 
            // Note: Bijective-equivalence check does not care about the head relation name
            const auto& normedFirst = normalisations.getNormalisation(first);
            const auto& normedSecond = normalisations.getNormalisation(second);
            if (areBijectivelyEquivalent(normedFirst, normedSecond)) {
                QualifiedName firstName = first->getHead()->getQualifiedName();
                QualifiedName secondName = second->getHead()->getQualifiedName();
                redundantClauses.insert(second);
                canonicalName.insert(std::pair(secondName, firstName));
            }
        }
    }
 
    // Remove redundant relation definitions
    for (const auto* clause : redundantClauses) {
        auto relName = clause->getHead()->getQualifiedName();
        Relation* rel = getRelation(program, relName);
        assert(rel != nullptr && "relation does not exist in program");
        removeRelation(translationUnit, relName);
    }
 
    // Replace each redundant relation appearance with its canonical name
    struct replaceRedundantRelations : public NodeMapper {
        const std::map<QualifiedName, QualifiedName>& canonicalName;
 
        replaceRedundantRelations(const std::map<QualifiedName, QualifiedName>& canonicalName)
                : canonicalName(canonicalName) {}
 
        Own<Node> operator()(Own<Node> node) const override {
            // Remove appearances from children nodes
            node->apply(*this);
 
            if (auto* atom = dynamic_cast<Atom*>(node.get())) {
                auto pos = canonicalName.find(atom->getQualifiedName());
                if (pos != canonicalName.end()) {
                    auto newAtom = souffle::clone(atom);
                    newAtom->setQualifiedName(pos->second);
                    return newAtom;
                }
            }
 
            return node;
        }
    };
    replaceRedundantRelations update(canonicalName);
    program.apply(update);
 
    // Program was changed iff a relation was replaced
    return !canonicalName.empty();
}
 
bool MinimiseProgramTransformer::removeRedundantClauses(TranslationUnit& translationUnit) {
    Program& program = translationUnit.getProgram();
    auto isRedundant = [&](const Clause* clause) {
        const auto* head = clause->getHead();
        for (const auto* lit : clause->getBodyLiterals()) {

References souffle::ast::getClauses(), and rel().

Here is the call graph for this function:

removeRedundantClauses()

bool souffle::ast::transform::MinimiseProgramTransformer::removeRedundantClauses ( TranslationUnit &  translationUnit )

staticprivate

Remove clauses that are only satisfied if they are already satisfied.

Definition at line 369 of file MinimiseProgram.cpp.

                            : program.getClauses()) {
        if (isRedundant(clause)) {
            clausesToRemove.insert(souffle::clone(clause));
        }
    }
 
    for (auto& clause : clausesToRemove) {
        program.removeClause(clause.get());
    }
    return !clausesToRemove.empty();
}
 
bool MinimiseProgramTransformer::reduceClauseBodies(TranslationUnit& translationUnit) {
    Program& program = translationUnit.getProgram();
    std::set<Own<Clause>> clausesToAdd;
    std::set<Own<Clause>> clausesToRemove;
 

transform()

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

overrideprivatevirtual

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

Definition at line 434 of file MinimiseProgram.cpp.

---

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

• ast/transform/MinimiseProgram.h
• ast/transform/MinimiseProgram.cpp