souffle::ast::transform::FoldAnonymousRecords Class Reference

Transformation pass that removes (binary) constraints on the anonymous records. More...

#include <FoldAnonymousRecords.h>

Inheritance diagram for souffle::ast::transform::FoldAnonymousRecords:

Collaboration diagram for souffle::ast::transform::FoldAnonymousRecords:

Public Member Functions
FoldAnonymousRecords *	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	containsValidRecordConstraint (const Clause &)
	Determine if the clause contains at least one binary constraint which can be expanded. More...
VecOwn< Literal >	expandRecordBinaryConstraint (const BinaryConstraint &)
	Expand constraint on records position-wise. More...
bool	isValidRecordConstraint (const Literal *literal)
	Determine if binary constraint can be expanded. More...
bool	transform (TranslationUnit &translationUnit) override
void	transformClause (const Clause &clause, VecOwn< Clause > &newClauses)
	Process a single clause. More...

Detailed Description

Transformation pass that removes (binary) constraints on the anonymous records.

After resolving aliases this is equivalent to completely removing anonymous records.

e.g. [a, b, c] = [x, y, z] → a = x, b = y, c = z. [a, b, c] != [x, y, z] → a != x b != y c != z (expanded to three new clauses)

In a single pass, in case of equalities a transformation expands a single level of records in every clause. (e.g. [[a]] = [[1]] => [a] = [1]) In case of inequalities, it expands at most a single inequality in every clause

This transformation does not resolve aliases. E.g. A = [a, b], A = [c, d] Thus it should be called in conjunction with ResolveAnonymousRecordAliases.

Definition at line 54 of file FoldAnonymousRecords.h.

Member Function Documentation

clone()

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

inlineoverridevirtual

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

Definition at line 66 of file FoldAnonymousRecords.h.

containsValidRecordConstraint()

bool souffle::ast::transform::FoldAnonymousRecords::containsValidRecordConstraint ( const Clause &  clause )

private

Determine if the clause contains at least one binary constraint which can be expanded.

Definition at line 70 of file FoldAnonymousRecords.cpp.

                                                                                                     {
    VecOwn<Literal> replacedContraint;
 

Referenced by transform().

expandRecordBinaryConstraint()

VecOwn< Literal > souffle::ast::transform::FoldAnonymousRecords::expandRecordBinaryConstraint ( const BinaryConstraint &  constraint )

private

Expand constraint on records position-wise.

eg. [1, 2, 3] = [a, b, c] => vector(1 = a, 2 = b, 3 = c) [x, y, z] != [a, b, c] => vector(x != a, x != b, z != c)

Procedure assumes that argument has a valid operation, that children are of type RecordInit and that the size of both sides is the same

Definition at line 78 of file FoldAnonymousRecords.cpp.

                                                     {
        auto newConstraint = mk<BinaryConstraint>(constraint.getBaseOperator(),
                souffle::clone(leftChildren[i]), souffle::clone(rightChildren[i]));
        replacedContraint.push_back(std::move(newConstraint));
    }
 
    // Handle edge case. Empty records.
    if (leftChildren.size() == 0) {
        if (isEqConstraint(constraint.getBaseOperator())) {
            replacedContraint.emplace_back(new BooleanConstraint(true));
        } else {
            replacedContraint.emplace_back(new BooleanConstraint(false));
        }
    }
 
    return replacedContraint;
}
 
void FoldAnonymousRecords::transformClause(const Clause& clause, VecOwn<Clause>& newClauses) {
    // If we have an inequality constraint, we need to create new clauses
    // At most one inequality constraint will be expanded in a single pass.

Referenced by transformClause().

getName()

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

inlineoverridevirtual

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

Definition at line 62 of file FoldAnonymousRecords.h.

isValidRecordConstraint()

bool souffle::ast::transform::FoldAnonymousRecords::isValidRecordConstraint ( const Literal *  literal )

private

Determine if binary constraint can be expanded.

Definition at line 41 of file FoldAnonymousRecords.cpp.

                                                             {
        return false;
    }
 
    // Check if records are of the same size.
    if (leftRecord->getChildNodes().size() != rightRecord->getChildNodes().size()) {
        return false;
    }
 
    // Check if operator is "=" or "!="
    auto op = constraint->getBaseOperator();
 
    return isEqConstraint(op) || isEqConstraint(negatedConstraintOp(op));
}
 
bool FoldAnonymousRecords::containsValidRecordConstraint(const Clause& clause) {
    bool contains = false;
    visitDepthFirst(clause, [&](const BinaryConstraint& binary) {

Referenced by transformClause().

transform()

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

overrideprivatevirtual

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

Definition at line 164 of file FoldAnonymousRecords.cpp.

                            : program.getClauses()) {
        if (containsValidRecordConstraint(*clause)) {
            changed = true;
            transformClause(*clause, newClauses);
        } else {
            newClauses.emplace_back(clause->clone());
        }
    }
 
    // Update Program.
    if (changed) {
        program.setClauses(std::move(newClauses));
    }
    return changed;
}
 
}  // namespace souffle::ast::transform

References containsValidRecordConstraint(), and transformClause().

Here is the call graph for this function:

transformClause()

void souffle::ast::transform::FoldAnonymousRecords::transformClause ( const Clause &  clause, VecOwn< Clause > &  newClauses  )

private

Process a single clause.

@parem clause Clause to be processed.

Parameters

newClauses

a destination for the newly produced clauses.

Definition at line 110 of file FoldAnonymousRecords.cpp.

                       : clause.getBodyLiterals()) {
        if (isValidRecordConstraint(literal)) {
            const BinaryConstraint& constraint = dynamic_cast<BinaryConstraint&>(*literal);
 
            // Simple case, [a_0, ..., a_n] = [b_0, ..., b_n]
            if (isEqConstraint(constraint.getBaseOperator())) {
                auto transformedLiterals = expandRecordBinaryConstraint(constraint);
                std::move(std::begin(transformedLiterals), std::end(transformedLiterals),
                        std::back_inserter(newBody));
 
                // else if: Case [a_0, ..., a_n] != [b_0, ..., b_n].
                // track single such case, it will be expanded in the end.
            } else if (neqConstraint == nullptr) {
                neqConstraint = dynamic_cast<BinaryConstraint*>(literal);
 
                // Else: repeated inequality.
            } else {
                newBody.push_back(souffle::clone(literal));
            }
 
            // else, we simply copy the literal.
        } else {
            newBody.push_back(souffle::clone(literal));
        }
    }
 
    // If no inequality: create a single modified clause.
    if (neqConstraint == nullptr) {
        auto newClause = souffle::clone(&clause);
        newClause->setBodyLiterals(std::move(newBody));
        newClauses.emplace_back(std::move(newClause));
 
        // Else: For each pair in negation, we need an extra clause.
    } else {
        auto transformedLiterals = expandRecordBinaryConstraint(*neqConstraint);
 
        for (auto it = begin(transformedLiterals); it != end(transformedLiterals); ++it) {
            auto newClause = souffle::clone(&clause);
            auto copyBody = souffle::clone(newBody);
            copyBody.push_back(std::move(*it));
 
            newClause->setBodyLiterals(std::move(copyBody));
 
            newClauses.push_back(std::move(newClause));
        }
    }
}
 
bool FoldAnonymousRecords::transform(TranslationUnit& translationUnit) {
    bool changed = false;
    Program& program = translationUnit.getProgram();

References souffle::clone(), expandRecordBinaryConstraint(), souffle::ast::BinaryConstraint::getBaseOperator(), souffle::isEqConstraint(), and isValidRecordConstraint().

Referenced by transform().

Here is the call graph for this function:

---

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

• ast/transform/FoldAnonymousRecords.h
• ast/transform/FoldAnonymousRecords.cpp