souffle::ast::transform::GroundWitnessesTransformer Class Reference

Apply a grounding so that the witness of a selection aggregate (min/max) can be transferred to the outer scope. More...

#include <GroundWitnesses.h>

Inheritance diagram for souffle::ast::transform::GroundWitnessesTransformer:

Collaboration diagram for souffle::ast::transform::GroundWitnessesTransformer:

Public Member Functions
GroundWitnessesTransformer *	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

Detailed Description

Apply a grounding so that the witness of a selection aggregate (min/max) can be transferred to the outer scope.

Here is an example:

Tallest(student) :- _ = max height : { Student(student, height) }.

student occurs ungrounded in the outer scope, but we can fix this by using the aggregate result to figure out which students satisfy this aggregate.

Tallest(student) :- n = max height : { Student(student0, height) }, Student(student, n).

This transformation is really just syntactic sugar.

Definition at line 49 of file GroundWitnesses.h.

Member Function Documentation

clone()

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

inlineoverridevirtual

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

Definition at line 62 of file GroundWitnesses.h.

getName()

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

inlineoverridevirtual

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

Definition at line 58 of file GroundWitnesses.h.

transform()

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

overrideprivatevirtual

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

Definition at line 31 of file GroundWitnesses.cpp.

                : aggregate(agg), originatingClause(clause), witnesses(std::move(witnesses)) {}
    };
 
    std::vector<AggregateWithWitnesses> aggregatesToFix;
 
    visitDepthFirst(program, [&](const Clause& clause) {
        visitDepthFirst(clause, [&](const Aggregator& agg) {
            auto witnessVariables = analysis::getWitnessVariables(translationUnit, clause, agg);
            // remove any witness variables that originate from an inner aggregate
            visitDepthFirst(agg, [&](const Aggregator& innerAgg) {
                if (agg == innerAgg) {
                    return;
                }
                auto innerWitnesses = analysis::getWitnessVariables(translationUnit, clause, innerAgg);
                for (const auto& witness : innerWitnesses) {
                    witnessVariables.erase(witness);
                }
            });
            if (witnessVariables.empty()) {
                return;
            }
            AggregateWithWitnesses instance(
                    const_cast<Aggregator*>(&agg), const_cast<Clause*>(&clause), witnessVariables);
            aggregatesToFix.push_back(instance);
        });
    });
 
    for (struct AggregateWithWitnesses& aggregateToFix : aggregatesToFix) {
        Aggregator* agg = aggregateToFix.aggregate;
        Clause* clause = aggregateToFix.originatingClause;
        std::set<std::string> witnesses = aggregateToFix.witnesses;
        // agg will become invalid when it gets replaced, so we have to be careful
        // not to use it after that point.
        // 1. make a copy of all aggregate body literals, because they will need to
        // be added to the rule body
        std::vector<std::unique_ptr<Literal>> aggregateLiterals;
        for (const auto& literal : agg->getBodyLiterals()) {
            aggregateLiterals.push_back(souffle::clone(literal));
        }
        // 1a. TODO: Be sure to rename any INNER witnesses! They have no meaning here and should just be made
        // into (For now I won't allow multi-leveled witnesses) an anonymous variable.
 
        // 2. Replace witness variables with unique names so they don't clash with the outside
        std::map<std::string, std::string> newWitnessVariableName;
        for (std::string witness : witnesses) {
            newWitnessVariableName[witness] = analysis::findUniqueVariableName(*clause, witness + "_w");
        }
        visitDepthFirst(*agg, [&](const Variable& var) {
            if (witnesses.find(var.getName()) != witnesses.end()) {
                // if this variable is a witness, we need to replace it with its new name
                const_cast<Variable&>(var).setName(newWitnessVariableName[var.getName()]);
            }
        });
 
        // 3. Replace any instance of the target variable with a clone of the aggregate
        struct TargetVariableReplacer : public NodeMapper {
            Aggregator* aggregate;
            std::string targetVariable;
            TargetVariableReplacer(Aggregator* agg, std::string target)
                    : aggregate(agg), targetVariable(std::move(target)) {}
            std::unique_ptr<Node> operator()(std::unique_ptr<Node> node) const override {
                if (auto* variable = dynamic_cast<Variable*>(node.get())) {
                    if (variable->getName() == targetVariable) {
                        auto replacement = souffle::clone(aggregate);
                        return replacement;
                    }
                }
                node->apply(*this);
                return node;
            }
        };
        const auto* targetVariable = dynamic_cast<const Variable*>(agg->getTargetExpression());
        std::string targetVariableName = targetVariable->getName();
        TargetVariableReplacer replacer(agg, targetVariableName);
        for (std::unique_ptr<Literal>& literal : aggregateLiterals) {
            literal->apply(replacer);
            // 4. Finally add these new grounding literals for the witness
            // to the body of the clause and voila! We've grounded
            // the witness(es)! Yay!
            clause->addToBody(souffle::clone(literal));
        }
    }
    return !aggregatesToFix.empty();
}
}  // namespace souffle::ast::transform

---

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

• ast/transform/GroundWitnesses.h
• ast/transform/GroundWitnesses.cpp