/daten/ahuesgen/projects/vhist/code/vhistlib/include/vhistfindlib/cnf.h

/* $HEADERS
 $Id: cnf.h 2168 2011-05-30 09:09:54Z ahuesgen $
 */

#ifndef CONJUNCTIVENORMALFORM_H
#define CONJUNCTIVENORMALFORM_H

#include "../shared/misc_defines.h"

#include <QString>
#include <QList>
#include <QSet>

namespace vhist
{

enum CNFOperandType
{
    OPERAND_TYPE_INVALID = 0,
    OPERAND_TYPE_STRING = 1,
    OPERAND_TYPE_VAR = 2
};

class VHIST_EXTERN CNFLiteralIndex
{
public:
    CNFLiteralIndex(int disjunctionIndex, int literalIndex);

public:
    int disjunctionIndex() const;
    int literalIndex() const;

private:
    int m_disjunctionIndex;
    int m_literalIndex;
};


class VHIST_EXTERN CNFOperand
{
private:
    CNFOperand();
public:
    ~CNFOperand();

public:
    static CNFOperand fromInvalid();
    static CNFOperand fromString(const QString& str);
    static CNFOperand fromVariable(const QString& var, const QString& attr);

public:
    bool isString() const;
    bool isVariable() const;
    bool isInvalid() const;

    QString string() const;
    QString variableName() const;
    QString variableAttribute() const;

private:
    CNFOperandType m_type;
    QString m_variable;
    QString m_attribute;
    QString m_string;
};


enum LiteralType
{
    LITERAL_TYPE_BOOL_VARIABLE,
    LITERAL_TYPE_TWO_PARAMTER_PREDICATE
};


class VHIST_EXTERN CNFLiteral
{
public:
    CNFLiteral(bool negated, const CNFOperand& boolVariable);
    CNFLiteral(bool negated, const CNFOperand& left, const QString& op,
            const CNFOperand& right);
    ~CNFLiteral();

public:
    bool isPredicate() const;
    bool isBoolVariable() const;

    bool isNegated() const;
    CNFOperand left() const;
    CNFOperand right() const;
    QString op() const;

    CNFOperand boolVariable() const;

    QSet<QString> variableNames() const;

public:
    void setNegated(bool negate);

public:
    static CNFLiteral fromInvalid();

private:
    LiteralType m_type;
    bool m_negated;
    QString m_operator;
    CNFOperand m_left;
    CNFOperand m_right;
};


class VHIST_EXTERN CNFDisjunction
{
public:
    void addLiteral(const CNFLiteral& literal);
    QMultiHash<QString, int> variableLocations() const;
    int numLiterals() const;
    const CNFLiteral* literalAt(int i) const;

private:
    QList<CNFLiteral> m_literals;
};


class VHIST_EXTERN ConjunctiveNormalForm
{
public:
    void clear();

public:
    void addDisjunction(const CNFDisjunction& disjunction);
    CNFDisjunction* lastDisjunction();
    QMultiHash<QString, CNFLiteralIndex> variableLocations() const;
    int numDisjunctions() const;
    const CNFDisjunction* disjunctionAt(int i) const;
    const CNFLiteral* literalAt(CNFLiteralIndex index) const;

private:
    QList<CNFDisjunction> m_disjunctions;
};

}

#endif // CONJUNCTIVENORMALFORM_H