#include "Formula.h"
#include "rand.h"
#include <stdio.h>

// Default Constructor
Formula::Formula()
{
    this->iNumClauses = 0;
    this->iNumVariables = 0;
    this->pClauses = 0;
}

// Default Destructor
Formula::~Formula()
{
    this->iNumClauses = 0;
    this->iNumVariables = 0;
    if( this->pClauses != 0 )
        delete [] this->pClauses;
    this->pClauses = 0;
}

// Load a formula from stdin
void Formula::Load()
{
    int entries_per_clause = -1;

    // Read the header
    scanf( "%d", &this->iNumVariables );
    scanf( "%d", &this->iNumClauses );
    scanf( "%d", &entries_per_clause );

    // Create the clauses
    this->pClauses = new Clause[this->iNumClauses];
    for( int i=0; i<this->iNumClauses; i++ )
    {
        this->pClauses[i].Create( entries_per_clause );

        // Read the leading parentheses
        scanf( " ( " );

        for( int j=0; j<entries_per_clause; j++ )
        {
            int num = 0;
            scanf( " %d ", &num );
            if( num < 0 )
                this->pClauses[i].SetValue( j, (-num)-1, false );
            else
                this->pClauses[i].SetValue( j, num-1, true );
        }

        // Read the trailing parentheses
        scanf( " ) " );
    }

    // Reduce this formula
    this->Reduce();
}

// Load a formula from file
void Formula::Load( char* filename )
{
}

// Print the formula
void Formula::Print()
{
    printf( "%d %d\n", this->iNumVariables, this->iNumClauses );
    for( int i=0; i<this->iNumClauses; i++ )
    {
        this->pClauses[i].Print();
    }
}

// Reduce a formula by eliminating always true clauses and duplicate 
// variables
void Formula::Reduce()
{
    // Remove Always True Clauses
    for( int i=0; i<this->iNumClauses; i++ )
    {
        if( this->pClauses[i].AlwaysTrue() )
        {
            // Remove the clause
            this->pClauses[i] = this->pClauses[this->iNumClauses-1];
            this->pClauses[this->iNumClauses-1].Clear();
            this->iNumClauses--;
            i--;
        }
    }

    // Remove duplicates from clauses
    for( int k=0; k<this->iNumClauses; k++ )
        (this->pClauses[k]).RemoveDuplicates();
}

// Returns one of the clauses from the formula
Clause* Formula::GetClause( int i )
{
    if( (this->pClauses != 0) &&
        (i >= 0) &&
        (i < this->iNumClauses) )
        return &this->pClauses[i];
    return 0;
}

// Check if the formula is satisfied
bool Formula::IsSatisfiedBy( Assignment* a )
{
    for( int i=0; i<this->iNumClauses; i++ )
        if( !( (this->pClauses[i]).IsSatisfiedBy( a ) ) )
            return false;
    return true;
}

// Check the number of clauses the formula is satisfied in
int Formula::NumSatisfiedBy( Assignment* a )
{
    int count = 0;

    // Count the number of clauses that are satisfied
    for( int i=0; i<this->iNumClauses; i++ )
        if( (this->pClauses[i]).IsSatisfiedBy( a ) )
            count++;

    return count;
}

Clause* Formula::GetRandomUnsatisfiedClause( Assignment* a )
{
    int num_satisfied = this->NumSatisfiedBy( a );
    int random_clause = my_rand( 0, (this->NumClauses()-num_satisfied)-1 );
        
    for( int i=0; i<this->iNumClauses; i++ )
    {
        if( !(this->pClauses[i]).IsSatisfiedBy( a ) )
            random_clause--;

        if( random_clause < 0 )
            return &this->pClauses[i];
    }

    return (Clause*)0;
}