#ifndef __CLAUSE_H__
#define __CLAUSE_H__

#include "Assignment.h"

//-----------------------------------------------------------------------------
//  struct ClauseEntry
//      Represents one variable entry in a clause
//-----------------------------------------------------------------------------
typedef struct __ClauseEntry
{
    int var_num;
    bool pos_neg;
} ClauseEntry;

//-----------------------------------------------------------------------------
//  class Clause
//      Encapsulates the clauses in a CNF formula and all the operations that
//      one might want to perform on a clause
//-----------------------------------------------------------------------------
class Clause
{
    protected:
        int iNumVars;           // Number of entries in this clause
        ClauseEntry* pAttribs;  // The entries in this clause

    public:
        // Constructor/Destructor
        Clause();
        Clause( int num_vars );
        void Create( int num_vars );
        void Clear();
        ~Clause();

        // Returns the number of entries in the clause
        int NumVariables() { return this->iNumVars; }

        // Set the value of one of the clause entries
        void SetValue( int num, int var, bool pos );
        // Get the value of one of the clause entries
        ClauseEntry* GetValue( int num );

        // Determine if a specific assignment satisfies this clause
        bool IsSatisfiedBy( Assignment* a );
        // Returns true if this clause is always true
        bool AlwaysTrue();

        // Removes any duplicate variables
        void RemoveDuplicates();

        // Print the clause
        void Print();
};

#endif