#ifndef __FORMULA_H__
#define __FORMULA_H__

#include "Assignment.h"
#include "Clause.h"

//-----------------------------------------------------------------------------
//  class Formula
//      Encapsulates a CNF formula and the operations that one might want
//      to perform on such a formula
//-----------------------------------------------------------------------------
class Formula
{
    protected:
        int iNumClauses;    // Number of clauses in the formula
        Clause* pClauses;   // The clauses in the formula

        int iNumVariables;  // Number of variables in the formula

    public:
        // Default Constructor/Destructor
        Formula();
        ~Formula();

        // Load from Stdin or File
        void Load();
        void Load( char* filename );

        // Print the formula
        void Print();

        // Reduce a formula by eliminating always true clauses and duplicate 
        // variables
        void Reduce();

        // Return the number of variables
        int NumVariables(void) { return this->iNumVariables; }
        // Return the number of clauses
        int NumClauses(void) { return this->iNumClauses; }

        // Returns a specific clause
        Clause* GetClause( int i );

        // Returns whether an assignment satisifes this formula
        bool IsSatisfiedBy( Assignment* a );
        // Returns the number of satisfied clauses by the assignment
        int NumSatisfiedBy( Assignment* a );
        // Returns a random unsatisifed clause
        Clause* GetRandomUnsatisfiedClause( Assignment* a );
};

#endif