souffle::ast::transform::AddNullariesToAtomlessAggregatesTransformer Class Reference

Transformation pass to add artificial nullary atom (+Tautology()) to aggregate bodies that have no atoms. More...

#include <AddNullariesToAtomlessAggregates.h>

Inheritance diagram for souffle::ast::transform::AddNullariesToAtomlessAggregatesTransformer:

Collaboration diagram for souffle::ast::transform::AddNullariesToAtomlessAggregatesTransformer:

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

Transformation pass to add artificial nullary atom (+Tautology()) to aggregate bodies that have no atoms.

Definition at line 45 of file AddNullariesToAtomlessAggregates.h.

Member Function Documentation

clone()

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

inlineoverridevirtual

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

Definition at line 62 of file AddNullariesToAtomlessAggregates.h.

getName()

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

inlineoverridevirtual

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

Definition at line 58 of file AddNullariesToAtomlessAggregates.h.

transform()

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

overrideprivatevirtual

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

Definition at line 38 of file AddNullariesToAtomlessAggregates.cpp.

                     {false};
        for (const auto& literal : agg.getBodyLiterals()) {
            if (isA<Atom>(literal)) {
                seenAtom = true;
            }
        }
        if (seenAtom) {
            return;
        }
        // We will add in the Tautology atom to the body of this aggregate now
        changed = true;
        // +Tautology()
        auto nullaryAtom = mk<Atom>();
        std::string relName = "+Tautology";
        nullaryAtom->setQualifiedName(relName);
 
        if (getRelation(program, relName) == nullptr) {
            // +Tautology().
            auto fact = mk<Clause>();
            fact->setHead(souffle::clone(nullaryAtom));
            // .decl +Tautology()
            auto tautologyRel = mk<Relation>();
            tautologyRel->setQualifiedName(relName);
            program.addRelation(std::move(tautologyRel));
            program.addClause(std::move(fact));
        }
        VecOwn<Literal> newBody;
        for (const auto& lit : agg.getBodyLiterals()) {
            newBody.push_back(souffle::clone(lit));
        }
        newBody.push_back(souffle::clone(nullaryAtom));
        const_cast<Aggregator&>(agg).setBody(std::move(newBody));
    });
    return changed;
}
}  // namespace souffle::ast::transform

---

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

• ast/transform/AddNullariesToAtomlessAggregates.h
• ast/transform/AddNullariesToAtomlessAggregates.cpp