souffle::ast::transform Namespace Reference

Namespaces
	test

Data Structures
class	AddNullariesToAtomlessAggregatesTransformer
	Transformation pass to add artificial nullary atom (+Tautology()) to aggregate bodies that have no atoms. More...
class	ComponentChecker
class	ComponentInstantiationTransformer
class	ConditionalTransformer
	Transformer that executes a sub-transformer iff a condition holds. More...
class	DebugReporter
	Transformation pass which wraps another transformation pass and generates a debug report section for the stage after applying the wrapped transformer, and adds it to the translation unit's debug report. More...
class	ExecutionPlanChecker
class	FixpointTransformer
	Transformer that repeatedly executes a sub-transformer until no changes are made. More...
class	FoldAnonymousRecords
	Transformation pass that removes (binary) constraints on the anonymous records. More...
class	GroundedTermsChecker
class	GroundWitnessesTransformer
	Apply a grounding so that the witness of a selection aggregate (min/max) can be transferred to the outer scope. More...
class	InlineRelationsTransformer
	Transformation pass to inline marked relations. More...
class	IOAttributesTransformer
	Transformation pass to set attribute names and types in IO operations. More...
class	IODefaultsTransformer
	Transformation pass to set defaults for IO operations. More...
class	MagicSetTransformer
	Magic Set Transformation. More...
class	MaterializeAggregationQueriesTransformer
	Transformation pass to create artificial relations for bodies of aggregation functions consisting of more than a single atom. More...
class	MaterializeSingletonAggregationTransformer
	Replaces literals containing single-valued aggregates with a synthesised relation. More...
class	MetaTransformer
	Transformer that coordinates other sub-transformations. More...
class	MinimiseProgramTransformer
	Transformation pass to remove equivalent rules. More...
class	NameUnnamedVariablesTransformer
	Transformation pass to replace unnamed variables with singletons. More...
class	NormaliseMultiResultFunctorsTransformer
	Uniquely names all appearances of ranges. More...
class	NullableVector
class	NullTransformer
	Transformer that does absolutely nothing. More...
class	PartitionBodyLiteralsTransformer
	Transformation pass to move literals into new clauses if they are independent of remaining literals. More...
class	PipelineTransformer
	Transformer that holds an arbitrary number of sub-transformations. More...
class	PragmaChecker
class	ProvenanceTransformer
	Transformation pass to add provenance information. More...
class	ReduceExistentialsTransformer
	Transformation pass to reduce unnecessary computation for relations that only appear in the form A(_,...,_). More...
class	RemoveBooleanConstraintsTransformer
	Transformation pass to remove constant boolean constraints Should be called after any transformation that may generate boolean constraints. More...
class	RemoveEmptyRelationsTransformer
	Transformation pass to remove all empty relations and rules that use empty relations. More...
class	RemoveRedundantRelationsTransformer
	Transformation pass to remove relations which are redundant (do not contribute to output). More...
class	RemoveRedundantSumsTransformer
	Transformation pass to remove expressions of the form sum k : { ... More...
class	RemoveRelationCopiesTransformer
	Transformation pass to replaces copy of relations by their origin. More...
class	ReorderLiteralsTransformer
	Transformation pass to reorder body literals. More...
class	ReplaceSingletonVariablesTransformer
	Transformation pass to replace singleton variables with unnamed variables. More...
class	ResolveAliasesTransformer
	Transformation pass to eliminate grounded aliases. More...
class	ResolveAnonymousRecordAliasesTransformer
	Transformer resolving aliases for anonymous records. More...
class	SemanticChecker
struct	SemanticCheckerImpl
class	SimplifyAggregateTargetExpressionTransformer
	Transformation pass to rename aggregation variables to make them unique. More...
class	Transformer
class	TypeChecker
class	TypeCheckerImpl
class	TypeDeclarationChecker
class	UniqueAggregationVariablesTransformer
	Transformation pass to rename aggregation variables to make them unique. More...
class	WhileTransformer
	Transformer that repeatedly executes a sub-transformer while a condition is met. More...

Typedefs
using	AdornDatabaseTransformer = MagicSetTransformer::AdornDatabaseTransformer
using	LabelDatabaseTransformer = MagicSetTransformer::LabelDatabaseTransformer
using	MagicSetCoreTransformer = MagicSetTransformer::MagicSetCoreTransformer
using	NegativeLabellingTransformer = MagicSetTransformer::LabelDatabaseTransformer::NegativeLabellingTransformer
using	NormaliseDatabaseTransformer = MagicSetTransformer::NormaliseDatabaseTransformer
using	PositiveLabellingTransformer = MagicSetTransformer::LabelDatabaseTransformer::PositiveLabellingTransformer

Functions
Argument *	combineAggregators (std::vector< Aggregator * > aggrs, std::string fun)
std::vector< std::vector< Literal * > >	combineNegatedLiterals (std::vector< std::vector< Literal * >> litGroups)
	Return the negated version of a disjunction of conjunctions. More...
bool	containsInlinedAtom (const Program &program, const Clause &clause)
	Checks if a given clause contains an atom that should be inlined. More...
std::vector< QualifiedName >	findInlineCycle (const PrecedenceGraphAnalysis &precedenceGraph, std::map< const Relation *, const Relation * > &origins, const Relation *current, RelationSet &unvisited, RelationSet &visiting, RelationSet &visited)
	Find a cycle consisting entirely of inlined relations. More...
std::vector< std::vector< Literal * > >	formNegatedLiterals (Program &program, Atom *atom)
	Forms the bodies that will replace the negation of a given inlined atom. More...
NullableVector< Argument * >	getInlinedArgument (Program &program, const Argument *arg)
	Returns a vector of arguments that should replace the given argument after one step of inlining. More...
NullableVector< Atom * >	getInlinedAtom (Program &program, Atom &atom)
	Returns a vector of atoms that should replace the given atom after one step of inlining. More...
std::vector< Clause * >	getInlinedClause (Program &program, const Clause &clause)
	Returns a list of clauses that should replace the given clause after one step of inlining. More...
NullableVector< std::vector< Literal * > >	getInlinedLiteral (Program &program, Literal *lit)
	Tries to perform a single step of inlining on the given literal. More...
std::pair< NullableVector< Literal * >, std::vector< BinaryConstraint * > >	inlineBodyLiterals (Atom *atom, Clause *atomInlineClause)
	Inlines the given atom based on a given clause. More...
Own< Relation >	makeInfoRelation (Clause &originalClause, size_t originalClauseNum, TranslationUnit &translationUnit)
QualifiedName	makeRelationName (const QualifiedName &orig, const std::string &type, int num=-1)
	Helper functions. More...
bool	nameInlinedUnderscores (Program &program)
	Removes all underscores in all atoms of inlined relations. More...
Literal *	negateLiteral (Literal *lit)
	Returns the negated version of a given literal. More...
bool	normaliseInlinedHeads (Program &program)
	Replace constants in the head of inlined clauses with (constrained) variables. More...
bool	reduceSubstitution (std::vector< std::pair< Argument *, Argument * >> &sub)
	Reduces a vector of substitutions. More...
void	renameVariables (Argument *arg)
	Renames all variables in a given argument uniquely. More...
void	transformEqrelRelation (Program &program, Relation &rel)
	Transform eqrel relations to explicitly define equivalence relations. More...
NullableVector< std::pair< Argument *, Argument * > >	unifyAtoms (Atom *first, Atom *second)
	Returns the nullable vector of substitutions needed to unify the two given atoms. More...
static const std::vector< SrcLocation >	usesInvalidWitness (TranslationUnit &tu, const Clause &clause, const Aggregator &aggregate)
	A witness is considered "invalid" if it is trying to export a witness out of a count, sum, or mean aggregate. More...

Typedef Documentation

AdornDatabaseTransformer

using souffle::ast::transform::AdornDatabaseTransformer = typedef MagicSetTransformer::AdornDatabaseTransformer

Definition at line 62 of file MagicSet.cpp.

LabelDatabaseTransformer

using souffle::ast::transform::LabelDatabaseTransformer = typedef MagicSetTransformer::LabelDatabaseTransformer

Definition at line 61 of file MagicSet.cpp.

MagicSetCoreTransformer

using souffle::ast::transform::MagicSetCoreTransformer = typedef MagicSetTransformer::MagicSetCoreTransformer

Definition at line 63 of file MagicSet.cpp.

NegativeLabellingTransformer

using souffle::ast::transform::NegativeLabellingTransformer = typedef MagicSetTransformer::LabelDatabaseTransformer::NegativeLabellingTransformer

Definition at line 66 of file MagicSet.cpp.

NormaliseDatabaseTransformer

using souffle::ast::transform::NormaliseDatabaseTransformer = typedef MagicSetTransformer::NormaliseDatabaseTransformer

Definition at line 60 of file MagicSet.cpp.

PositiveLabellingTransformer

using souffle::ast::transform::PositiveLabellingTransformer = typedef MagicSetTransformer::LabelDatabaseTransformer::PositiveLabellingTransformer

Definition at line 68 of file MagicSet.cpp.

Function Documentation

combineAggregators()

Argument* souffle::ast::transform::combineAggregators	(	std::vector< Aggregator * >	aggrs,
		std::string	fun
	)

Definition at line 521 of file InlineRelations.cpp.

                                                                                    {

Referenced by getInlinedArgument().

combineNegatedLiterals()

std::vector<std::vector<Literal*> > souffle::ast::transform::combineNegatedLiterals

(

std::vector< std::vector< Literal * >>

litGroups

)

Return the negated version of a disjunction of conjunctions.

E.g. (a1(x) ^ a2(x) ^ ...) v (b1(x) ^ b2(x) ^ ...) –into-> (!a1(x) ^ !b1(x)) v (!a2(x) ^ !b2(x)) v ...

Definition at line 385 of file InlineRelations.cpp.

                               {
        // !(a1 ^ a2 ^ a3 ^ ...) --into-> !a1 v !a2 v !a3 v ...
        for (auto& i : litGroup) {
            std::vector<Literal*> newVec;
            newVec.push_back(negateLiteral(i));
            negation.push_back(newVec);
        }
 
        // Done!
        return negation;
    }
 
    // Produce the negated versions of all disjunctions ignoring the first recursively
    std::vector<std::vector<Literal*>> combinedRHS = combineNegatedLiterals(
            std::vector<std::vector<Literal*>>(litGroups.begin() + 1, litGroups.end()));
 
    // We now just need to add the negation of a single literal from the untouched LHS
    // to every single conjunction on the RHS to finalise creating every possible combination
    for (Literal* lhsLit : litGroup) {
        for (std::vector<Literal*> rhsVec : combinedRHS) {
            std::vector<Literal*> newVec;
            newVec.push_back(negateLiteral(lhsLit));
 
            for (Literal* lit : rhsVec) {
                newVec.push_back(lit->clone());
            }
 
            negation.push_back(newVec);
        }
    }
 
    for (std::vector<Literal*> rhsVec : combinedRHS) {
        for (Literal* lit : rhsVec) {
            delete lit;
        }
    }
 
    return negation;
}
 
/**
 * Forms the bodies that will replace the negation of a given inlined atom.
 * E.g. a(x) <- (a11(x), a12(x)) ; (a21(x), a22(x)) => !a(x) <- (!a11(x), !a21(x)) ; (!a11(x), !a22(x)) ; ...
 * Essentially, produce every combination (m_1 ^ m_2 ^ ...) where m_i is the negation of a literal in the
 * ith rule of a.

containsInlinedAtom()

bool souffle::ast::transform::containsInlinedAtom	(	const Program &	program,
		const Clause &	clause
	)

Checks if a given clause contains an atom that should be inlined.

Definition at line 202 of file InlineRelations.cpp.

                                                                       {

findInlineCycle()

std::vector<QualifiedName> souffle::ast::transform::findInlineCycle	(	const PrecedenceGraphAnalysis &	precedenceGraph,
		std::map< const Relation *, const Relation * > &	origins,
		const Relation *	current,
		RelationSet &	unvisited,
		RelationSet &	visiting,
		RelationSet &	visited
	)

Find a cycle consisting entirely of inlined relations.

If no cycle exists, then an empty vector is returned.

Definition at line 713 of file SemanticChecker.cpp.

                               {
            // Nothing left to visit - so no cycles exist!
            return result;
        }
 
        // Choose any element from the unvisited set
        current = *unvisited.begin();
        origins[current] = nullptr;
 
        // Move it to "currently visiting"
        unvisited.erase(current);
        visiting.insert(current);
 
        // Check if we can find a cycle beginning from this node
        std::vector<QualifiedName> subresult =
                findInlineCycle(precedenceGraph, origins, current, unvisited, visiting, visited);
 
        if (subresult.empty()) {
            // No cycle found, try again from another node
            return findInlineCycle(precedenceGraph, origins, nullptr, unvisited, visiting, visited);
        } else {
            // Cycle found! Return it
            return subresult;
        }
    }
 
    // Check neighbours
    const RelationSet& successors = precedenceGraph.graph().successors(current);
    for (const Relation* successor : successors) {
        // Only care about inlined neighbours in the graph
        if (successor->hasQualifier(RelationQualifier::INLINE)) {
            if (visited.find(successor) != visited.end()) {
                // The neighbour has already been visited, so move on
                continue;
            }
 
            if (visiting.find(successor) != visiting.end()) {
                // Found a cycle!!
                // Construct the cycle in reverse
                while (current != nullptr) {
                    result.push_back(current->getQualifiedName());
                    current = origins[current];
                }
                return result;
            }
 
            // Node has not been visited yet
            origins[successor] = current;
 
            // Move from unvisited to visiting
            unvisited.erase(successor);
            visiting.insert(successor);
 
            // Visit recursively and check if a cycle is formed
            std::vector<QualifiedName> subgraphCycle =
                    findInlineCycle(precedenceGraph, origins, successor, unvisited, visiting, visited);
 
            if (!subgraphCycle.empty()) {
                // Found a cycle!
                return subgraphCycle;
            }
        }
    }
 
    // Visited all neighbours with no cycle found, so done visiting this node.
    visiting.erase(current);
    visited.insert(current);
    return result;
}
 
void SemanticCheckerImpl::checkInlining() {
    auto isInline = [&](const Relation* rel) { return rel->hasQualifier(RelationQualifier::INLINE); };
 
    // Find all inlined relations
    RelationSet inlinedRelations;

formNegatedLiterals()

std::vector<std::vector<Literal*> > souffle::ast::transform::formNegatedLiterals	(	Program &	program,
		Atom *	atom
	)

Forms the bodies that will replace the negation of a given inlined atom.

E.g. a(x) <- (a11(x), a12(x)) ; (a21(x), a22(x)) => !a(x) <- (!a11(x), !a21(x)) ; (!a11(x), !a22(x)) ; ... Essentially, produce every combination (m_1 ^ m_2 ^ ...) where m_i is the negation of a literal in the ith rule of a.

Definition at line 440 of file InlineRelations.cpp.

                          : getClauses(program, *getRelation(program, atom->getQualifiedName()))) {
        // Form the replacement clause by inlining based on the current clause
        std::pair<NullableVector<Literal*>, std::vector<BinaryConstraint*>> inlineResult =
                inlineBodyLiterals(atom, inClause);
        NullableVector<Literal*> replacementBodyLiterals = inlineResult.first;
        std::vector<BinaryConstraint*> currConstraints = inlineResult.second;
 
        if (!replacementBodyLiterals.isValid()) {
            // Failed to unify, so just move on
            continue;
        }
 
        addedBodyLiterals.push_back(replacementBodyLiterals.getVector());
        addedConstraints.push_back(currConstraints);
    }
 
    // We now have a list of bodies needed to inline the given atom.
    // We want to inline the negated version, however, which is done using De Morgan's Law.
    std::vector<std::vector<Literal*>> negatedAddedBodyLiterals = combineNegatedLiterals(addedBodyLiterals);
 
    // Add in the necessary constraints to all the body literals
    for (auto& negatedAddedBodyLiteral : negatedAddedBodyLiterals) {
        for (std::vector<BinaryConstraint*> constraintGroup : addedConstraints) {
            for (BinaryConstraint* constraint : constraintGroup) {
                negatedAddedBodyLiteral.push_back(constraint->clone());
            }
        }
    }
 
    // Free up the old body literals and constraints
    for (std::vector<Literal*> litGroup : addedBodyLiterals) {
        for (Literal* lit : litGroup) {
            delete lit;
        }
    }
    for (std::vector<BinaryConstraint*> consGroup : addedConstraints) {
        for (Constraint* cons : consGroup) {
            delete cons;
        }
    }
 
    return negatedAddedBodyLiterals;
}
 
/**
 * Renames all variables in a given argument uniquely.
 */
void renameVariables(Argument* arg) {
    static int varCount = 0;

References inlineBodyLiterals().

Here is the call graph for this function:

getInlinedArgument()

NullableVector<Argument*> souffle::ast::transform::getInlinedArgument	(	Program &	program,
		const Argument *	arg
	)

Returns a vector of arguments that should replace the given argument after one step of inlining.

Note: This function is currently generalised to perform any required inlining within aggregators as well, making it simple to extend to this later on if desired (and the semantic check is removed).

Definition at line 543 of file InlineRelations.cpp.

                                                                 {
        // First try inlining the target expression if necessary
        if (aggr->getTargetExpression() != nullptr) {
            NullableVector<Argument*> argumentVersions =
                    getInlinedArgument(program, aggr->getTargetExpression());
 
            if (argumentVersions.isValid()) {
                // An element in the target expression can be inlined!
                changed = true;
 
                // Create a new aggregator per version of the target expression
                for (Argument* newArg : argumentVersions.getVector()) {
                    auto* newAggr = new Aggregator(aggr->getBaseOperator(), Own<Argument>(newArg));
                    VecOwn<Literal> newBody;
                    for (Literal* lit : aggr->getBodyLiterals()) {
                        newBody.push_back(souffle::clone(lit));
                    }
                    newAggr->setBody(std::move(newBody));
                    versions.push_back(newAggr);
                }
            }
        }
 
        // Try inlining body arguments if the target expression has not been changed.
        // (At this point we only handle one step of inlining at a time)
        if (!changed) {
            std::vector<Literal*> bodyLiterals = aggr->getBodyLiterals();
            for (size_t i = 0; i < bodyLiterals.size(); i++) {
                Literal* currLit = bodyLiterals[i];
 
                NullableVector<std::vector<Literal*>> literalVersions = getInlinedLiteral(program, currLit);
 
                if (literalVersions.isValid()) {
                    // Literal can be inlined!
                    changed = true;
 
                    AggregateOp op = aggr->getBaseOperator();
 
                    // Create an aggregator (with the same operation) for each possible body
                    std::vector<Aggregator*> aggrVersions;
                    for (std::vector<Literal*> inlineVersions : literalVersions.getVector()) {
                        Own<Argument> target;
                        if (aggr->getTargetExpression() != nullptr) {
                            target = souffle::clone(aggr->getTargetExpression());
                        }
                        auto* newAggr = new Aggregator(aggr->getBaseOperator(), std::move(target));
 
                        VecOwn<Literal> newBody;
                        // Add in everything except the current literal being replaced
                        for (size_t j = 0; j < bodyLiterals.size(); j++) {
                            if (i != j) {
                                newBody.push_back(souffle::clone(bodyLiterals[j]));
                            }
                        }
 
                        // Add in everything new that replaces that literal
                        for (Literal* addedLit : inlineVersions) {
                            newBody.push_back(Own<Literal>(addedLit));
                        }
 
                        newAggr->setBody(std::move(newBody));
                        aggrVersions.push_back(newAggr);
                    }
 
                    // Utility lambda: get functor used to tie aggregators together.
                    auto aggregateToFunctor = [](AggregateOp op) {
                        switch (op) {
                            case AggregateOp::MIN:
                            case AggregateOp::FMIN:
                            case AggregateOp::UMIN: return "min";
                            case AggregateOp::MAX:
                            case AggregateOp::FMAX:
                            case AggregateOp::UMAX: return "max";
                            case AggregateOp::SUM:
                            case AggregateOp::FSUM:
                            case AggregateOp::USUM:
                            case AggregateOp::COUNT: return "+";
                            case AggregateOp::MEAN: fatal("no translation");
                        }
 
                        UNREACHABLE_BAD_CASE_ANALYSIS
                    };
                    // Create the actual overall aggregator that ties the replacement aggregators together.
                    // example: min x : { a(x) }. <=> min ( min x : { a1(x) }, min x : { a2(x) }, ... )
                    if (op != AggregateOp::MEAN) {
                        versions.push_back(combineAggregators(aggrVersions, aggregateToFunctor(op)));
                    }
                }
 
                // Only perform one stage of inlining at a time.
                if (changed) {
                    break;
                }
            }
        }
    } else if (const auto* functor = dynamic_cast<const Functor*>(arg)) {
        size_t i = 0;
        for (auto funArg : functor->getArguments()) {
            // TODO (azreika): use unique pointers
            // try inlining each argument from left to right
            NullableVector<Argument*> argumentVersions = getInlinedArgument(program, funArg);
            if (argumentVersions.isValid()) {
                changed = true;
                for (Argument* newArgVersion : argumentVersions.getVector()) {
                    // same functor but with new argument version
                    VecOwn<Argument> argsCopy;
                    size_t j = 0;
                    for (auto& functorArg : functor->getArguments()) {
                        if (j == i) {
                            argsCopy.emplace_back(newArgVersion);
                        } else {
                            argsCopy.emplace_back(functorArg->clone());
                        }
                        ++j;
                    }
                    if (const auto* intrFunc = dynamic_cast<const IntrinsicFunctor*>(arg)) {
                        auto* newFunctor =
                                new IntrinsicFunctor(intrFunc->getBaseFunctionOp(), std::move(argsCopy));
                        newFunctor->setSrcLoc(functor->getSrcLoc());
                        versions.push_back(newFunctor);
                    } else if (const auto* userFunc = dynamic_cast<const UserDefinedFunctor*>(arg)) {
                        auto* newFunctor = new UserDefinedFunctor(userFunc->getName(), std::move(argsCopy));
                        newFunctor->setSrcLoc(userFunc->getSrcLoc());
                        versions.push_back(newFunctor);
                    }
                }
                // only one step at a time
                break;
            }
            ++i;
        }
    } else if (const auto* cast = dynamic_cast<const ast::TypeCast*>(arg)) {
        NullableVector<Argument*> argumentVersions = getInlinedArgument(program, cast->getValue());
        if (argumentVersions.isValid()) {
            changed = true;
            for (Argument* newArg : argumentVersions.getVector()) {
                Argument* newTypeCast = new ast::TypeCast(Own<Argument>(newArg), cast->getType());
                versions.push_back(newTypeCast);
            }
        }
    } else if (const auto* record = dynamic_cast<const RecordInit*>(arg)) {
        std::vector<Argument*> recordArguments = record->getArguments();
        for (size_t i = 0; i < recordArguments.size(); i++) {
            Argument* currentRecArg = recordArguments[i];
            NullableVector<Argument*> argumentVersions = getInlinedArgument(program, currentRecArg);
            if (argumentVersions.isValid()) {
                changed = true;
                for (Argument* newArgumentVersion : argumentVersions.getVector()) {
                    auto* newRecordArg = new RecordInit();
                    for (size_t j = 0; j < recordArguments.size(); j++) {
                        if (i == j) {
                            newRecordArg->addArgument(Own<Argument>(newArgumentVersion));
                        } else {
                            newRecordArg->addArgument(souffle::clone(recordArguments[j]));
                        }
                    }
                    versions.push_back(newRecordArg);
                }
            }
 
            // Only perform one stage of inlining at a time.
            if (changed) {
                break;
            }
        }
    }
 
    if (changed) {
        // Return a valid vector - replacements need to be made!
        return NullableVector<Argument*>(versions);
    } else {
        // Return an invalid vector - no inlining has occurred
        return NullableVector<Argument*>();
    }
}
 
/**
 * Returns a vector of atoms that should replace the given atom after one step of inlining.
 * Assumes the relation the atom belongs to is not inlined itself.
 */
NullableVector<Atom*> getInlinedAtom(Program& program, Atom& atom) {

References souffle::clone(), combineAggregators(), souffle::COUNT, souffle::fatal(), souffle::FMAX, souffle::FMIN, souffle::FSUM, getInlinedLiteral(), i, j, souffle::MAX, souffle::MEAN, souffle::MIN, souffle::SUM, souffle::UMAX, souffle::UMIN, UNREACHABLE_BAD_CASE_ANALYSIS, and souffle::USUM.

Referenced by getInlinedAtom().

Here is the call graph for this function:

getInlinedAtom()

NullableVector<Atom*> souffle::ast::transform::getInlinedAtom	(	Program &	program,
		Atom &	atom
	)

Returns a vector of atoms that should replace the given atom after one step of inlining.

Assumes the relation the atom belongs to is not inlined itself.

Definition at line 729 of file InlineRelations.cpp.

                                                  {
        Argument* arg = arguments[i];
 
        NullableVector<Argument*> argumentVersions = getInlinedArgument(program, arg);
 
        if (argumentVersions.isValid()) {
            // Argument has replacements
            changed = true;
 
            // Create a new atom per new version of the argument
            for (Argument* newArgument : argumentVersions.getVector()) {
                auto args = atom.getArguments();
                VecOwn<Argument> newArgs;
                for (size_t j = 0; j < args.size(); j++) {
                    if (j == i) {
                        newArgs.emplace_back(newArgument);
                    } else {
                        newArgs.emplace_back(args[j]->clone());
                    }
                }
                auto* newAtom = new Atom(atom.getQualifiedName(), std::move(newArgs), atom.getSrcLoc());
                versions.push_back(newAtom);
            }
        }
 
        // Only perform one stage of inlining at a time.
        if (changed) {
            break;
        }
    }
 
    if (changed) {
        // Return a valid vector - replacements need to be made!
        return NullableVector<Atom*>(versions);
    } else {
        // Return an invalid vector - no replacements need to be made
        return NullableVector<Atom*>();
    }
}
 
/**
 * Tries to perform a single step of inlining on the given literal.
 * Returns a pair of nullable vectors (v, w) such that:
 *    - v is valid if and only if the literal can be directly inlined, whereby it
 *      contains the bodies that replace it

References souffle::clone(), getInlinedArgument(), i, and j.

Referenced by getInlinedLiteral().

Here is the call graph for this function:

getInlinedClause()

std::vector<Clause*> souffle::ast::transform::getInlinedClause	(	Program &	program,
		const Clause &	clause
	)

Returns a list of clauses that should replace the given clause after one step of inlining.

If no inlining can occur, the list will only contain a clone of the original clause.

Definition at line 911 of file InlineRelations.cpp.

                                {
        // The head atom can be inlined!
        changed = true;
 
        // Produce the new clauses with the replacement head atoms
        for (Atom* newHead : headVersions.getVector()) {
            auto* newClause = new Clause();
            newClause->setSrcLoc(clause.getSrcLoc());
 
            newClause->setHead(Own<Atom>(newHead));
 
            // The body will remain unchanged
            for (Literal* lit : clause.getBodyLiterals()) {
                newClause->addToBody(souffle::clone(lit));
            }
 
            versions.push_back(newClause);
        }
    }
 
    // Only perform one stage of inlining at a time.
    // If the head atoms did not need inlining, try inlining atoms nested in the body.
    if (!changed) {
        std::vector<Literal*> bodyLiterals = clause.getBodyLiterals();
        for (size_t i = 0; i < bodyLiterals.size(); i++) {
            Literal* currLit = bodyLiterals[i];
 
            // Three possible cases when trying to inline a literal:
            //  1) The literal itself may be directly inlined. In this case, the atom can be replaced
            //    with multiple different bodies, as the inlined atom may have several rules.
            //  2) Otherwise, the literal itself may not need to be inlined, but a subnode (e.g. an argument)
            //    may need to be inlined. In this case, an altered literal must replace the original.
            //    Again, several possible versions may exist, as the inlined relation may have several rules.
            //  3) The literal does not depend on any inlined relations, and so does not need to be changed.
            NullableVector<std::vector<Literal*>> litVersions = getInlinedLiteral(program, currLit);
 
            if (litVersions.isValid()) {
                // Case 1 and 2: Inlining has occurred!
                changed = true;
 
                // The literal may be replaced with several different bodies.
                // Create a new clause for each possible version.
                std::vector<std::vector<Literal*>> bodyVersions = litVersions.getVector();
 
                // Create the base clause with the current literal removed
                auto baseClause = Own<Clause>(cloneHead(&clause));
                for (Literal* oldLit : bodyLiterals) {
                    if (currLit != oldLit) {
                        baseClause->addToBody(souffle::clone(oldLit));
                    }
                }
 
                for (std::vector<Literal*> body : bodyVersions) {
                    Clause* replacementClause = baseClause->clone();
 
                    // Add in the current set of literals replacing the inlined literal
                    // In Case 2, each body contains exactly one literal
                    for (Literal* newLit : body) {
                        replacementClause->addToBody(Own<Literal>(newLit));
                    }
 
                    versions.push_back(replacementClause);
                }
            }
 
            // Only replace at most one literal per iteration
            if (changed) {
                break;
            }
        }
    }
 
    if (!changed) {
        // Case 3: No inlining changes, so a clone of the original should be returned
        std::vector<Clause*> ret;
        ret.push_back(clause.clone());
        return ret;
    } else {
        // Inlining changes, so return the replacement clauses.
        return versions;
    }
}
 
bool InlineRelationsTransformer::transform(TranslationUnit& translationUnit) {
    bool changed = false;
    Program& program = translationUnit.getProgram();
 
    // Replace constants in the head of inlined clauses with (constrained) variables.

getInlinedLiteral()

NullableVector< std::vector< Literal * > > souffle::ast::transform::getInlinedLiteral	(	Program &	program,
		Literal *	lit
	)

Tries to perform a single step of inlining on the given literal.

Returns a pair of nullable vectors (v, w) such that:

• v is valid if and only if the literal can be directly inlined, whereby it contains the bodies that replace it
• if v is not valid, then w is valid if and only if the literal cannot be inlined directly, but contains a subargument that can be. In this case, it will contain the versions that will replace it.
• If both are invalid, then no more inlining can occur on this literal and we are done.

Definition at line 785 of file InlineRelations.cpp.

                                               {
        // Check if this atom is meant to be inlined
        Relation* rel = getRelation(program, atom->getQualifiedName());
 
        if (rel->hasQualifier(RelationQualifier::INLINE)) {
            // We found an atom in the clause that needs to be inlined!
            // The clause needs to be replaced
            inlined = true;
 
            // N new clauses should be formed, where N is the number of clauses
            // associated with the inlined relation
            for (Clause* inClause : getClauses(program, *rel)) {
                // Form the replacement clause
                std::pair<NullableVector<Literal*>, std::vector<BinaryConstraint*>> inlineResult =
                        inlineBodyLiterals(atom, inClause);
                NullableVector<Literal*> replacementBodyLiterals = inlineResult.first;
                std::vector<BinaryConstraint*> currConstraints = inlineResult.second;
 
                if (!replacementBodyLiterals.isValid()) {
                    // Failed to unify the atoms! We can skip this one...
                    continue;
                }
 
                // Unification successful - the returned vector of literals represents one possible body
                // replacement We can add in the unification constraints as part of these literals.
                std::vector<Literal*> bodyResult = replacementBodyLiterals.getVector();
 
                for (BinaryConstraint* cons : currConstraints) {
                    bodyResult.push_back(cons);
                }
 
                addedBodyLiterals.push_back(bodyResult);
            }
        } else {
            // Not meant to be inlined, but a subargument may be
            NullableVector<Atom*> atomVersions = getInlinedAtom(program, *atom);
            if (atomVersions.isValid()) {
                // Subnode needs to be inlined, so we have a vector of replacement atoms
                changed = true;
                for (Atom* newAtom : atomVersions.getVector()) {
                    versions.push_back(newAtom);
                }
            }
        }
    } else if (auto neg = dynamic_cast<Negation*>(lit)) {
        // For negations, check the corresponding atom
        Atom* atom = neg->getAtom();
        NullableVector<std::vector<Literal*>> atomVersions = getInlinedLiteral(program, atom);
 
        if (atomVersions.isValid()) {
            // The atom can be inlined
            inlined = true;
 
            if (atomVersions.getVector().empty()) {
                // No clauses associated with the atom, so just becomes a true literal
                addedBodyLiterals.push_back({new BooleanConstraint(true)});
            } else {
                // Suppose an atom a(x) is inlined and has the following rules:
                //  - a(x) :- a11(x), a12(x).
                //  - a(x) :- a21(x), a22(x).
                // Then, a(x) <- (a11(x) ^ a12(x)) v (a21(x) ^ a22(x))
                //  => !a(x) <- (!a11(x) v !a12(x)) ^ (!a21(x) v !a22(x))
                //  => !a(x) <- (!a11(x) ^ !a21(x)) v (!a11(x) ^ !a22(x)) v ...
                // Essentially, produce every combination (m_1 ^ m_2 ^ ...) where m_i is a
                // negated literal in the ith rule of a.
                addedBodyLiterals = formNegatedLiterals(program, atom);
            }
        }
        if (atomVersions.isValid()) {
            for (const auto& curVec : atomVersions.getVector()) {
                for (auto* cur : curVec) {
                    delete cur;
                }
            }
        }
    } else if (auto* constraint = dynamic_cast<BinaryConstraint*>(lit)) {
        NullableVector<Argument*> lhsVersions = getInlinedArgument(program, constraint->getLHS());
        if (lhsVersions.isValid()) {
            changed = true;
            for (Argument* newLhs : lhsVersions.getVector()) {
                Literal* newLit = new BinaryConstraint(constraint->getBaseOperator(), Own<Argument>(newLhs),
                        souffle::clone(constraint->getRHS()));
                versions.push_back(newLit);
            }
        } else {
            NullableVector<Argument*> rhsVersions = getInlinedArgument(program, constraint->getRHS());
            if (rhsVersions.isValid()) {
                changed = true;
                for (Argument* newRhs : rhsVersions.getVector()) {
                    Literal* newLit = new BinaryConstraint(constraint->getBaseOperator(),
                            souffle::clone(constraint->getLHS()), Own<Argument>(newRhs));
                    versions.push_back(newLit);
                }
            }
        }
    }
 
    if (changed) {
        // Not inlined directly but found replacement literals
        // Rewrite these as single-literal bodies
        for (Literal* version : versions) {
            std::vector<Literal*> newBody;
            newBody.push_back(version);
            addedBodyLiterals.push_back(newBody);
        }
        inlined = true;
    }
 
    if (inlined) {
        return NullableVector<std::vector<Literal*>>(addedBodyLiterals);
    } else {
        return NullableVector<std::vector<Literal*>>();
    }
}
 
/**
 * Returns a list of clauses that should replace the given clause after one step of inlining.
 * If no inlining can occur, the list will only contain a clone of the original clause.
 */
std::vector<Clause*> getInlinedClause(Program& program, const Clause& clause) {

References souffle::ast::getClauses(), getInlinedAtom(), souffle::ast::getRelation(), souffle::INLINE, inlineBodyLiterals(), and rel().

Referenced by getInlinedArgument().

Here is the call graph for this function:

inlineBodyLiterals()

std::pair<NullableVector<Literal*>, std::vector<BinaryConstraint*> > souffle::ast::transform::inlineBodyLiterals	(	Atom *	atom,
		Clause *	atomInlineClause
	)

Inlines the given atom based on a given clause.

Returns the vector of replacement literals and the necessary constraints. If unification is unsuccessful, the vector of literals is marked as invalid.

Definition at line 304 of file InlineRelations.cpp.

                           : public NodeMapper {
        int varnum;
        VariableRenamer(int varnum) : varnum(varnum) {}
        Own<Node> operator()(Own<Node> node) const override {
            if (auto* var = dynamic_cast<ast::Variable*>(node.get())) {
                // Rename the variable
                auto newVar = souffle::clone(var);
                std::stringstream newName;
                newName << "<inlined_" << var->getName() << "_" << varnum << ">";
                newVar->setName(newName.str());
                return newVar;
            }
            node->apply(*this);
            return node;
        }
    };
 
    VariableRenamer update(inlineCount);
    atomClause->apply(update);
 
    inlineCount++;
 
    // Get the constraints needed to unify the two atoms
    NullableVector<std::pair<Argument*, Argument*>> res = unifyAtoms(atomClause->getHead(), atom);
    if (res.isValid()) {
        changed = true;
        for (std::pair<Argument*, Argument*> pair : res.getVector()) {
            // FIXME: float equiv (`FEQ`)
            constraints.push_back(new BinaryConstraint(
                    BinaryConstraintOp::EQ, souffle::clone(pair.first), souffle::clone(pair.second)));
        }
 
        // Add in the body of the current clause of the inlined atom
        for (Literal* lit : atomClause->getBodyLiterals()) {
            addedLits.push_back(lit->clone());
        }
    }
 
    if (changed) {
        return std::make_pair(NullableVector<Literal*>(addedLits), constraints);
    } else {
        return std::make_pair(NullableVector<Literal*>(), constraints);
    }
}
 
/**
 * Returns the negated version of a given literal
 */
Literal* negateLiteral(Literal* lit) {
    if (auto* atom = dynamic_cast<Atom*>(lit)) {

Referenced by formNegatedLiterals(), and getInlinedLiteral().

makeInfoRelation()

Own<Relation> souffle::ast::transform::makeInfoRelation	(	Clause &	originalClause,
		size_t	originalClauseNum,
		TranslationUnit &	translationUnit
	)

Definition at line 78 of file Provenance.cpp.

                                                      {
        if (auto* var = dynamic_cast<ast::Variable*>(arg)) {
            return toString(*var);
        } else if (auto* constant = dynamic_cast<Constant*>(arg)) {
            return toString(*constant);
        }
        if (isA<UnnamedVariable>(arg)) {
            return "_";
        }
        if (isA<Functor>(arg)) {
            return tfm::format("functor_%d", functorNumber++);
        }
        if (isA<Aggregator>(arg)) {
            return tfm::format("agg_%d", aggregateNumber++);
        }
 
        fatal("Unhandled argument type");
    };
 
    // add head arguments
    for (auto& arg : originalClause.getHead()->getArguments()) {
        headVariables.push_back(getArgInfo(arg));
    }
 
    // join variables in the head with commas
    std::stringstream headVariableString;
    headVariableString << join(headVariables, ",");
 
    // add an attribute to infoRelation for the head of clause
    infoRelation->addAttribute(mk<Attribute>(std::string("head_vars"), QualifiedName("symbol")));
    infoClauseHead->addArgument(mk<StringConstant>(toString(join(headVariables, ","))));
 
    // visit all body literals and add to info clause head
    for (size_t i = 0; i < originalClause.getBodyLiterals().size(); i++) {
        auto lit = originalClause.getBodyLiterals()[i];
 
        const Atom* atom = nullptr;
        if (isA<Atom>(lit)) {
            atom = static_cast<Atom*>(lit);
        } else if (isA<Negation>(lit)) {
            atom = static_cast<Negation*>(lit)->getAtom();
        } else if (isA<ProvenanceNegation>(lit)) {
            atom = static_cast<ProvenanceNegation*>(lit)->getAtom();
        }
 
        // add an attribute for atoms and binary constraints
        if (atom != nullptr || isA<BinaryConstraint>(lit)) {
            infoRelation->addAttribute(
                    mk<Attribute>(std::string("rel_") + std::to_string(i), QualifiedName("symbol")));
        }
 
        if (atom != nullptr) {
            std::string relName = toString(atom->getQualifiedName());
 
            // for an atom, add its name and variables (converting aggregates to variables)
            if (isA<Atom>(lit)) {
                std::string atomDescription = relName;
 
                for (auto& arg : atom->getArguments()) {
                    atomDescription.append("," + getArgInfo(arg));
                }
 
                infoClauseHead->addArgument(mk<StringConstant>(atomDescription));
                // for a negation, add a marker with the relation name
            } else if (isA<Negation>(lit)) {
                infoClauseHead->addArgument(mk<StringConstant>("!" + relName));
            }
        }
    }
 
    // visit all body constraints and add to info clause head
    for (size_t i = 0; i < originalClause.getBodyLiterals().size(); i++) {
        auto lit = originalClause.getBodyLiterals()[i];
 
        if (auto con = dynamic_cast<BinaryConstraint*>(lit)) {
            // for a constraint, add the constraint symbol and LHS and RHS
            std::string constraintDescription = toBinaryConstraintSymbol(con->getBaseOperator());
 
            constraintDescription.append("," + getArgInfo(con->getLHS()));
            constraintDescription.append("," + getArgInfo(con->getRHS()));
 
            infoClauseHead->addArgument(mk<StringConstant>(constraintDescription));
        }
    }
 
    infoRelation->addAttribute(mk<Attribute>("clause_repr", QualifiedName("symbol")));
    infoClauseHead->addArgument(mk<StringConstant>(toString(originalClause)));
 
    // set clause head and add clause to info relation
    infoClause->setHead(Own<Atom>(infoClauseHead));
    Program& program = translationUnit.getProgram();
    program.addClause(Own<Clause>(infoClause));
 
    return Own<Relation>(infoRelation);
}
 
/** Transform eqrel relations to explicitly define equivalence relations */
void transformEqrelRelation(Program& program, Relation& rel) {
    assert(rel.getRepresentation() == RelationRepresentation::EQREL &&
            "attempting to transform non-eqrel relation");
    assert(rel.getArity() == 2 && "eqrel relation not binary");

makeRelationName()

QualifiedName souffle::ast::transform::makeRelationName ( const QualifiedName &  orig, const std::string &  type, int  num = -1  )

inline

Helper functions.

Definition at line 68 of file Provenance.cpp.

                                                                                            {
    QualifiedName name =
            makeRelationName(originalClause.getHead()->getQualifiedName(), "@info", originalClauseNum);
 

nameInlinedUnderscores()

bool souffle::ast::transform::nameInlinedUnderscores

(

Program &

program

)

Removes all underscores in all atoms of inlined relations.

Definition at line 146 of file InlineRelations.cpp.

                : inlinedRelations(std::move(inlinedRelations)), replaceUnderscores(replaceUnderscores) {}
 
        Own<Node> operator()(Own<Node> node) const override {
            static int underscoreCount = 0;
 
            if (!replaceUnderscores) {
                // Check if we should start replacing underscores for this node's subnodes
                if (auto* atom = dynamic_cast<Atom*>(node.get())) {
                    if (inlinedRelations.find(atom->getQualifiedName()) != inlinedRelations.end()) {
                        // Atom associated with an inlined relation, so replace the underscores
                        // in all of its subnodes with named variables.
                        M replace(inlinedRelations, true);
                        node->apply(replace);
                        changed |= replace.changed;
                        return node;
                    }
                }
            } else if (isA<UnnamedVariable>(node.get())) {
                // Give a unique name to the underscored variable
                // TODO (azreika): need a more consistent way of handling internally generated variables in
                // general
                std::stringstream newVarName;
                newVarName << "<underscore_" << underscoreCount++ << ">";
                changed = true;
                return mk<ast::Variable>(newVarName.str());
            }
 
            node->apply(*this);
            return node;
        }
    };
 
    // Store the names of all relations to be inlined
    std::set<QualifiedName> inlinedRelations;
    for (Relation* rel : program.getRelations()) {
        if (rel->hasQualifier(RelationQualifier::INLINE)) {
            inlinedRelations.insert(rel->getQualifiedName());
        }
    }
 
    // Apply the renaming procedure to the entire program
    M update(inlinedRelations, false);
    program.apply(update);
    return update.changed;
}
 
/**
 * Checks if a given clause contains an atom that should be inlined.
 */
bool containsInlinedAtom(const Program& program, const Clause& clause) {
    bool foundInlinedAtom = false;

negateLiteral()

Literal* souffle::ast::transform::negateLiteral

(

Literal *

lit

)

Returns the negated version of a given literal.

Definition at line 365 of file InlineRelations.cpp.

                                                            {
        Constraint* newCons = cons->clone();
        negateConstraintInPlace(*newCons);
        return newCons;
    }
 
    fatal("unsupported literal type: %s", *lit);
}
 
/**
 * Return the negated version of a disjunction of conjunctions.
 * E.g. (a1(x) ^ a2(x) ^ ...) v (b1(x) ^ b2(x) ^ ...) --into-> (!a1(x) ^ !b1(x)) v (!a2(x) ^ !b2(x)) v ...
 */
std::vector<std::vector<Literal*>> combineNegatedLiterals(std::vector<std::vector<Literal*>> litGroups) {

normaliseInlinedHeads()

bool souffle::ast::transform::normaliseInlinedHeads

(

Program &

program

)

Replace constants in the head of inlined clauses with (constrained) variables.

Definition at line 93 of file InlineRelations.cpp.

                                                         {
            continue;
        }
 
        for (Clause* clause : getClauses(program, *rel)) {
            // Set up the new clause with an empty body and no arguments in the head
            auto newClause = mk<Clause>();
            newClause->setSrcLoc(clause->getSrcLoc());
            auto clauseHead = mk<Atom>(clause->getHead()->getQualifiedName());
 
            // Add in everything in the original body
            for (Literal* lit : clause->getBodyLiterals()) {
                newClause->addToBody(souffle::clone(lit));
            }
 
            // Set up the head arguments in the new clause
            for (Argument* arg : clause->getHead()->getArguments()) {
                if (auto* constant = dynamic_cast<Constant*>(arg)) {
                    // Found a constant in the head, so replace it with a variable
                    std::stringstream newVar;
                    newVar << "<new_var_" << newVarCount++ << ">";
                    clauseHead->addArgument(mk<ast::Variable>(newVar.str()));
 
                    // Add a body constraint to set the variable's value to be the original constant
                    newClause->addToBody(mk<BinaryConstraint>(BinaryConstraintOp::EQ,
                            mk<ast::Variable>(newVar.str()), souffle::clone(constant)));
                } else {
                    // Already a variable
                    clauseHead->addArgument(souffle::clone(arg));
                }
            }
 
            newClause->setHead(std::move(clauseHead));
 
            // Replace the old clause with this one
            program.addClause(std::move(newClause));
            program.removeClause(clause);
            changed = true;
        }
    }
 
    return changed;
}
 
/**
 * Removes all underscores in all atoms of inlined relations
 */
bool nameInlinedUnderscores(Program& program) {
    struct M : public NodeMapper {

reduceSubstitution()

bool souffle::ast::transform::reduceSubstitution

(

std::vector< std::pair< Argument *, Argument * >> &

sub

)

Reduces a vector of substitutions.

Returns false only if matched argument pairs are found to be incompatible.

Definition at line 219 of file InlineRelations.cpp.

                                                {
            auto currPair = sub[i];
            Argument* lhs = currPair.first;
            Argument* rhs = currPair.second;
 
            // Start trying to reduce the substitution
            // Note: Can probably go further with this substitution reduction
            if (*lhs == *rhs) {
                // Get rid of redundant `x = x`
                sub.erase(sub.begin() + i);
                done = false;
            } else if (isA<Constant>(lhs) && isA<Constant>(rhs)) {
                // Both are constants but not equal (prev case => !=)
                // Failed to unify!
                return false;
            } else if (isA<RecordInit>(lhs) && isA<RecordInit>(rhs)) {
                // Note: we will not deal with the case where only one side is
                // a record and the other is a variable, as variables can be records
                // on a deeper level.
                std::vector<Argument*> lhsArgs = static_cast<RecordInit*>(lhs)->getArguments();
                std::vector<Argument*> rhsArgs = static_cast<RecordInit*>(rhs)->getArguments();
 
                if (lhsArgs.size() != rhsArgs.size()) {
                    // Records of unequal size can't be equated
                    return false;
                }
 
                // Equate all corresponding arguments
                for (size_t i = 0; i < lhsArgs.size(); i++) {
                    sub.push_back(std::make_pair(lhsArgs[i], rhsArgs[i]));
                }
 
                // Get rid of the record equality
                sub.erase(sub.begin() + i);
                done = false;
            } else if ((isA<RecordInit>(lhs) && isA<Constant>(rhs)) ||
                       (isA<Constant>(lhs) && isA<RecordInit>(rhs))) {
                // A record =/= a constant
                return false;
            }
        }
    }
 
    return true;
}
 
/**
 * Returns the nullable vector of substitutions needed to unify the two given atoms.
 * If unification is not successful, the returned vector is marked as invalid.
 * Assumes that the atoms are both of the same relation.
 */

References i, lhs, rhs, and souffle::ast::analysis::sub().

Here is the call graph for this function:

renameVariables()

void souffle::ast::transform::renameVariables

(

Argument *

arg

)

Renames all variables in a given argument uniquely.

Definition at line 494 of file InlineRelations.cpp.

                      : varnum(varnum) {}
        Own<Node> operator()(Own<Node> node) const override {
            if (auto* var = dynamic_cast<ast::Variable*>(node.get())) {
                auto newVar = souffle::clone(var);
                std::stringstream newName;
                newName << var->getName() << "-v" << varnum;
                newVar->setName(newName.str());
                return newVar;
            }
            node->apply(*this);
            return node;
        }
    };
 
    M update(varCount);
    arg->apply(update);
}
 
// Performs a given binary op on a list of aggregators recursively.
// E.g. ( <aggr1, aggr2, aggr3, ...>, o > = (aggr1 o (aggr2 o (agg3 o (...))))
// TODO (azreika): remove aggregator support
Argument* combineAggregators(std::vector<Aggregator*> aggrs, std::string fun) {
    // Due to variable scoping issues with aggregators, we rename all variables uniquely in the

transformEqrelRelation()

void souffle::ast::transform::transformEqrelRelation	(	Program &	program,
		Relation &	rel
	)

Transform eqrel relations to explicitly define equivalence relations.

Definition at line 203 of file Provenance.cpp.

          {
Own<Argument> getNextLevelNumber(const std::vector<Argument*>& levels) {
    if (levels.empty()) return mk<NumericConstant>(0);
 
    auto max = levels.size() == 1

unifyAtoms()

NullableVector<std::pair<Argument*, Argument*> > souffle::ast::transform::unifyAtoms	(	Atom *	first,
		Atom *	second
	)

Returns the nullable vector of substitutions needed to unify the two given atoms.

If unification is not successful, the returned vector is marked as invalid. Assumes that the atoms are both of the same relation.

Definition at line 278 of file InlineRelations.cpp.

                                                  {
        substitution.push_back(std::make_pair(firstArgs[i], secondArgs[i]));
    }
 
    // Reduce the substitutions
    bool success = reduceSubstitution(substitution);
    if (success) {
        return NullableVector<std::pair<Argument*, Argument*>>(substitution);
    } else {
        // Failed to unify the two atoms
        return NullableVector<std::pair<Argument*, Argument*>>();
    }
}
 
/**
 * Inlines the given atom based on a given clause.
 * Returns the vector of replacement literals and the necessary constraints.
 * If unification is unsuccessful, the vector of literals is marked as invalid.
 */

References i.

usesInvalidWitness()

static const std::vector<SrcLocation> souffle::ast::transform::usesInvalidWitness ( TranslationUnit &  tu, const Clause &  clause, const Aggregator &  aggregate  )

static

A witness is considered "invalid" if it is trying to export a witness out of a count, sum, or mean aggregate.

However we need to be careful: Sometimes a witness variables occurs within the body of a count, sum, or mean aggregate, but this is valid, because the witness actually belongs to an inner min or max aggregate.

We just need to check that that witness only occurs on this level.

Definition at line 647 of file SemanticChecker.cpp.

                            : aggregate.getBodyLiterals()) {
        aggregateSubclause->addToBody(souffle::clone(lit));
    }
    struct InnerAggregateMasker : public NodeMapper {
        mutable int numReplaced = 0;
        Own<Node> operator()(Own<Node> node) const override {
            if (isA<Aggregator>(node.get())) {
                std::string newVariableName = "+aggr_var_" + toString(numReplaced++);
                return mk<Variable>(newVariableName);
            }
            node->apply(*this);
            return node;
        }
    };
    InnerAggregateMasker update;
    aggregateSubclause->apply(update);
 
    // Find the witnesses of the original aggregate.
    // If we can find occurrences of the witness in
    // this masked version of the aggregate subclause,
    // AND the aggregate is a sum / count / mean (we know this because
    // of the early exit for a min/max aggregate)
    // then we have an invalid witness and we'll add the source location
    // of the variable to the invalidWitnessLocations vector.
    auto witnesses = analysis::getWitnessVariables(tu, clause, aggregate);
    for (const auto& witness : witnesses) {
        visitDepthFirst(*aggregateSubclause, [&](const Variable& var) {
            if (var.getName() == witness) {
                invalidWitnessLocations.push_back(var.getSrcLoc());
            }
        });
    }
    return invalidWitnessLocations;
}
 
void SemanticCheckerImpl::checkWitnessProblem() {
    // Check whether there is the use of a witness in
    // an aggregate where it doesn't make sense to use it, i.e.
    // count, sum, mean
    visitDepthFirst(program, [&](const Clause& clause) {