souffle::RuleBody Class Reference

#include <ParserUtils.h>

Collaboration diagram for souffle::RuleBody:

Data Structures
struct	literal

Public Member Functions
void	conjunct (RuleBody other)
void	disjunct (RuleBody other)
RuleBody	negated () const
RuleBody &	operator= (RuleBody &&)=default
	RuleBody ()=default
	RuleBody (RuleBody &&)=default
VecOwn< ast::Clause >	toClauseBodies () const

Static Public Member Functions
static RuleBody	atom (Own< ast::Atom > atom)
static RuleBody	constraint (Own< ast::Constraint > constraint)
static RuleBody	getFalse ()
static RuleBody	getTrue ()

Private Types
using	clause = std::vector< literal >

Static Private Member Functions
static bool	equal (const clause &a, const clause &b)
static bool	equal (const literal &a, const literal &b)
static void	insert (clause &cl, literal &&lit)
static void	insert (std::vector< clause > &cnf, clause &&cls)
static bool	isSubsetOf (const clause &a, const clause &b)

Private Attributes
std::vector< clause >	dnf

Friends
std::ostream &	operator<< (std::ostream &out, const RuleBody &body)

Detailed Description

Definition at line 36 of file ParserUtils.h.

Member Typedef Documentation

clause

using souffle::RuleBody::clause = std::vector<literal>

private

Definition at line 84 of file ParserUtils.h.

Constructor & Destructor Documentation

RuleBody() [1/2]

souffle::RuleBody::RuleBody ( )

default

Referenced by getTrue().

RuleBody() [2/2]

souffle::RuleBody::RuleBody ( RuleBody &&  )

default

Member Function Documentation

atom()

RuleBody souffle::RuleBody::atom ( Own< ast::Atom >  atom )

static

Definition at line 139 of file ParserUtils.cpp.

                                                           {
    RuleBody body;
    body.dnf.push_back(clause());
    body.dnf.back().emplace_back(literal{false, std::move(constraint)});
    return body;

References constraint(), and dnf.

Referenced by getFalse(), and toClauseBodies().

Here is the call graph for this function:

conjunct()

void souffle::RuleBody::conjunct

(

RuleBody

other

)

Definition at line 58 of file ParserUtils.cpp.

                             : dnf) {
        for (const auto& clauseB : other.dnf) {
            clause cur;
 
            for (const auto& lit : clauseA) {
                cur.emplace_back(lit.clone());
            }
            for (const auto& lit : clauseB) {
                insert(cur, lit.clone());
            }
 
            insert(res, std::move(cur));
        }
    }
 
    dnf = std::move(res);
}
 
void RuleBody::disjunct(RuleBody other) {
    // append the clauses of the other body to this body
    for (auto& cur : other.dnf) {
        insert(dnf, std::move(cur));
    }

constraint()

RuleBody souffle::RuleBody::constraint ( Own< ast::Constraint >  constraint )

static

Definition at line 146 of file ParserUtils.cpp.

                                                              {
    return out << join(body.dnf, ";", [](std::ostream& out, const RuleBody::clause& cur) {
        out << join(cur, ",", [](std::ostream& out, const RuleBody::literal& l) {
            if (l.negated) {
                out << "!";

References dnf, and souffle::join().

Referenced by atom().

Here is the call graph for this function:

disjunct()

void souffle::RuleBody::disjunct

(

RuleBody

other

)

Definition at line 89 of file ParserUtils.cpp.

                                                 {
    // collect clause results
    VecOwn<ast::Clause> bodies;
    for (const clause& cur : dnf) {
        bodies.push_back(mk<ast::Clause>());

References dnf.

equal() [1/2]

bool souffle::RuleBody::equal ( const clause &  a, const clause &  b  )

staticprivate

Definition at line 168 of file ParserUtils.cpp.

                           : b) {
            if (equal(i, j)) {
                found = true;
                break;
            }
        }
        if (!found) {
            return false;
        }
    }
    return true;
}
 
bool RuleBody::isSubsetOf(const clause& a, const clause& b) {
    if (a.size() > b.size()) {
        return false;
    }
    for (const auto& i : a) {

References i, and j.

equal() [2/2]

bool souffle::RuleBody::equal ( const literal &  a, const literal &  b  )

staticprivate

Definition at line 164 of file ParserUtils.cpp.

                       : a) {

getFalse()

RuleBody souffle::RuleBody::getFalse ( )

static

Definition at line 135 of file ParserUtils.cpp.

                                        {false, std::move(atom)});
    return body;

References atom().

Here is the call graph for this function:

getTrue()

RuleBody souffle::RuleBody::getTrue ( )

static

Definition at line 129 of file ParserUtils.cpp.

                            {
    return RuleBody();
}
 
RuleBody RuleBody::atom(Own<ast::Atom> atom) {

References RuleBody().

Here is the call graph for this function:

insert() [1/2]

void souffle::RuleBody::insert ( clause &  cl, literal &&  lit  )

staticprivate

Definition at line 206 of file ParserUtils.cpp.

                                                          {
    for (const auto& cur : cnf) {
        if (isSubsetOf(cur, cls)) {
            return;
        }

insert() [2/2]

void souffle::RuleBody::insert ( std::vector< clause > &  cnf, clause &&  cls  )

staticprivate

Definition at line 215 of file ParserUtils.cpp.

                   : cnf) {
        if (!isSubsetOf(cls, cur)) {
            res.push_back(std::move(cur));
        }
    }
    res.swap(cnf);
    cnf.push_back(std::move(cls));
}
 
}  // end of namespace souffle

isSubsetOf()

bool souffle::RuleBody::isSubsetOf ( const clause &  a, const clause &  b  )

staticprivate

Definition at line 187 of file ParserUtils.cpp.

                           : b) {
            if (equal(i, j)) {
                found = true;
                break;
            }
        }
        if (!found) {
            return false;
        }
    }
    return true;
}
 
void RuleBody::insert(clause& cl, literal&& lit) {
    for (const auto& cur : cl) {
        if (equal(cur, lit)) {
            return;
        }

References i, and j.

negated()

RuleBody souffle::RuleBody::negated

(

)

const

Definition at line 42 of file ParserUtils.cpp.

                                                {!lit.negated, clone(lit.atom)});
        }
 
        res.conjunct(std::move(step));
    }
 
    return res;
}
 
void RuleBody::conjunct(RuleBody other) {
    // avoid making clones if possible
    if (dnf.size() == 1 && other.dnf.size() == 1) {
        for (auto&& rhs : other.dnf[0]) {
            insert(dnf[0], std::move(rhs));

References souffle::clone(), and souffle::RuleBody::literal::negated.

Here is the call graph for this function:

operator=()

RuleBody& souffle::RuleBody::operator= ( RuleBody &&  )

default

toClauseBodies()

VecOwn< ast::Clause > souffle::RuleBody::toClauseBodies

(

)

const

Definition at line 96 of file ParserUtils.cpp.

                                : cur) {
            // extract literal
            auto base = clone(lit.atom);
            // negate if necessary
            if (lit.negated) {
                // negate
                if (auto* atom = dynamic_cast<ast::Atom*>(&*base)) {
                    base.release();
                    base = mk<ast::Negation>(Own<ast::Atom>(atom));
                    base->setSrcLoc(atom->getSrcLoc());
                } else if (auto* cstr = dynamic_cast<ast::Constraint*>(&*base)) {
                    negateConstraintInPlace(*cstr);
                }
            }
 
            // add to result
            clause.addToBody(std::move(base));
        }
    }
 
    // done
    return bodies;
}
 
// -- factory functions --
 
RuleBody RuleBody::getTrue() {
    RuleBody body;
    body.dnf.push_back(clause());

References atom(), base, souffle::clone(), and souffle::ast::negateConstraintInPlace().

Here is the call graph for this function:

Friends And Related Function Documentation

operator<<

std::ostream& operator<< ( std::ostream &  out, const RuleBody &  body  )

friend

Definition at line 153 of file ParserUtils.cpp.

                                                       {
    return a.negated == b.negated && *a.atom == *b.atom;
}
 
bool RuleBody::equal(const clause& a, const clause& b) {

Field Documentation

dnf

std::vector<clause> souffle::RuleBody::dnf

private

Definition at line 86 of file ParserUtils.h.

Referenced by atom(), constraint(), and disjunct().

---

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

• parser/ParserUtils.h
• parser/ParserUtils.cpp