souffle::ast::transform::RemoveBooleanConstraintsTransformer Class Reference

Transformation pass to remove constant boolean constraints Should be called after any transformation that may generate boolean constraints. More...

#include <RemoveBooleanConstraints.h>

Inheritance diagram for souffle::ast::transform::RemoveBooleanConstraintsTransformer:

Collaboration diagram for souffle::ast::transform::RemoveBooleanConstraintsTransformer:

Public Member Functions
RemoveBooleanConstraintsTransformer *	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 remove constant boolean constraints Should be called after any transformation that may generate boolean constraints.

Definition at line 31 of file RemoveBooleanConstraints.h.

Member Function Documentation

clone()

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

inlineoverridevirtual

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

Definition at line 41 of file RemoveBooleanConstraints.h.

getName()

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

inlineoverridevirtual

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

Definition at line 37 of file RemoveBooleanConstraints.h.

       :
    bool transform(TranslationUnit& translationUnit) override;
};

transform()

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

overrideprivatevirtual

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

Definition at line 42 of file RemoveBooleanConstraints.cpp.

                                                           { changed = true; });
 
    // Remove true and false constant literals from all aggregators
    struct removeBools : public NodeMapper {
        Own<Node> operator()(Own<Node> node) const override {
            // Remove them from child nodes
            node->apply(*this);
 
            if (auto* aggr = dynamic_cast<Aggregator*>(node.get())) {
                bool containsTrue = false;
                bool containsFalse = false;
 
                // Check if aggregator body contains booleans.
                for (Literal* lit : aggr->getBodyLiterals()) {
                    if (auto* bc = dynamic_cast<BooleanConstraint*>(lit)) {
                        if (bc->isTrue()) {
                            containsTrue = true;
                        } else {
                            containsFalse = true;
                        }
                    }
                }
 
                // Only keep literals that aren't boolean constraints
                if (containsFalse || containsTrue) {
                    auto replacementAggregator = souffle::clone(aggr);
                    VecOwn<Literal> newBody;
 
                    bool isEmpty = true;
 
                    // Don't bother copying over body literals if any are false
                    if (!containsFalse) {
                        for (Literal* lit : aggr->getBodyLiterals()) {
                            // Don't add in boolean constraints
                            if (!isA<BooleanConstraint>(lit)) {
                                isEmpty = false;
                                newBody.push_back(souffle::clone(lit));
                            }
                        }
 
                        // If the body is still empty and the original body contains true add it now.
                        if (containsTrue && isEmpty) {
                            newBody.push_back(mk<BinaryConstraint>(
                                    BinaryConstraintOp::EQ, mk<NumericConstant>(1), mk<NumericConstant>(1)));
 
                            isEmpty = false;
                        }
                    }
 
                    if (containsFalse || isEmpty) {
                        // Empty aggregator body!
                        // Not currently handled, so add in a false literal in the body
                        // E.g. max x : { } =becomes=> max 1 : {0 = 1}
                        newBody.push_back(mk<BinaryConstraint>(
                                BinaryConstraintOp::EQ, mk<NumericConstant>(0), mk<NumericConstant>(1)));
                    }
 
                    replacementAggregator->setBody(std::move(newBody));
                    return replacementAggregator;
                }
            }
 
            // no false or true, so return the original node
            return node;
        }
    };
 
    removeBools update;
    program.apply(update);
 
    // Remove true and false constant literals from all clauses
    for (Relation* rel : program.getRelations()) {
        for (Clause* clause : getClauses(program, *rel)) {
            bool containsTrue = false;
            bool containsFalse = false;
 
            for (Literal* lit : clause->getBodyLiterals()) {
                if (auto* bc = dynamic_cast<BooleanConstraint*>(lit)) {
                    bc->isTrue() ? containsTrue = true : containsFalse = true;
                }
            }
 
            if (containsFalse) {
                // Clause will always fail
                program.removeClause(clause);
            } else if (containsTrue) {
                auto replacementClause = Own<Clause>(cloneHead(clause));
 
                // Only keep non-'true' literals
                for (Literal* lit : clause->getBodyLiterals()) {
                    if (!isA<BooleanConstraint>(lit)) {
                        replacementClause->addToBody(souffle::clone(lit));
                    }
                }
 
                program.removeClause(clause);
                program.addClause(std::move(replacementClause));
            }
        }
    }
 
    return changed;
}
 
}  // namespace souffle::ast::transform

---

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

• ast/transform/RemoveBooleanConstraints.h
• ast/transform/RemoveBooleanConstraints.cpp