#include "Clause.h"
#include <stdio.h>

// Default Constructor
Clause::Clause()
{
    this->iNumVars = 0;
    this->pAttribs = 0;
}

// Constructor
Clause::Clause( int num_vars )
{
    this->Create( num_vars );
}

// Create the clause object
void Clause::Create( int num_vars )
{
    this->iNumVars = num_vars;
    this->pAttribs = new ClauseEntry[num_vars];
}

// Clear the structure
void Clause::Clear()
{
    this->iNumVars = 0;
    this->pAttribs = 0;
}

// Default Destructor
Clause::~Clause()
{
    this->iNumVars = 0;
    if( this->pAttribs )
        delete [] this->pAttribs;
    this->pAttribs = 0;
}

// Set the value of one of the clause entries
void Clause::SetValue( int num, int var, bool pos )
{
    if( (this->iNumVars != 0) &&
        (num >= 0) &&
        (num < this->iNumVars) )
    {
        this->pAttribs[num].var_num = var;
        this->pAttribs[num].pos_neg = pos;
    }
}

// Get the value of one of the clause entries
ClauseEntry* Clause::GetValue( int num )
{
    if( (this->iNumVars != 0) && 
        (num >= 0) &&
        (num < this->iNumVars) )
        return &this->pAttribs[num];
    return (ClauseEntry*)0;
}

// Determine if a specific assignment satisfies this clause
bool Clause::IsSatisfiedBy( Assignment* a )
{
    for( int i=0; i<this->iNumVars; i++ )
    {
        if( a->GetValue( this->pAttribs[i].var_num ) == this->pAttribs[i].pos_neg )
            return true;
    }

    return false;
}

// Returns true if this clause is always true
bool Clause::AlwaysTrue()
{
    for( int i=0; i<this->iNumVars-1; i++ )
    {
        int var = this->pAttribs[i].var_num;
        bool pos = this->pAttribs[i].pos_neg;

        for( int j=i+1; j<this->iNumVars; j++ )
        {
            if( (this->pAttribs[j].var_num == var) && 
                (this->pAttribs[j].pos_neg != pos) )
                return true;
        }
    }

    return false;
}

// Removes any duplicate variables
void Clause::RemoveDuplicates()
{
    for( int i=0; i<this->iNumVars-1; i++ )
    {
        int var = this->pAttribs[i].var_num;
        bool pos = this->pAttribs[i].pos_neg;

        for( int j=i+1; j<this->iNumVars; j++ )
        {
            if( (this->pAttribs[j].var_num == var) && 
                (this->pAttribs[j].pos_neg == pos) )
            {
                // Duplicate Remove
                this->pAttribs[j] = this->pAttribs[iNumVars-1];
                this->iNumVars--;
                j--;
            }
        }
    }
}

// Print the clause
void Clause::Print()
{
    printf( "(" );
    for( int i=0; i<this->iNumVars; i++ )
    {
        if( this->pAttribs[i].pos_neg )
            printf( " %d", this->pAttribs[i].var_num+1 );
        else
            printf( " -%d", this->pAttribs[i].var_num+1 );
    }
    printf ( " )\n" );
}