#include "qbf_logical.hpp"
#include <boost/bind.hpp>
#include <boost/foreach.hpp>
#include <algorithm>
#include <cassert>
#include <iostream>

QBF_Logical::QBF_Logical(logical_operator log_op, std::vector<QBF*>* q_l)
    : op_type(log_op), qbf_vector(q_l)
{
    for_each(qbf_vector->begin(), 
	     qbf_vector->end(),
	     bind(&QBF::set_parent, _1, this));
}

QBF_Logical::~QBF_Logical(void)
{
}

std::string QBF_Logical::toString()
{
    std::string result = "(";
    result += (op_type == AND) ? "&" : "|";
    result += " ";
    BOOST_FOREACH(QBF* q, *qbf_vector) {
	result+=q->toString() + " ";
    }
    result += ")";
    return result;
}

void QBF_Logical::update()
{
    BOOST_FOREACH(QBF* q, *qbf_vector) {
	if(boost::logic::indeterminate(q->status))
	    q->update();
    }
    QBF::update();
}

bool QBF_Logical::eval()
{
    switch(op_type) {
    case QBF::AND:
	BOOST_FOREACH(QBF* q, *qbf_vector) {
	    if(!q->eval()) {
		return false;
	    }
	}
	return true;
    case QBF::OR:
	BOOST_FOREACH(QBF* q, *qbf_vector) {
	    if(q->eval())
		return true;
	}
	return false;
    case QBF::EQU:
	if((*qbf_vector)[0]->eval() == (*qbf_vector)[1]->eval())
	    return true;
	else 
	    return false;
    case QBF::XOR:
	if((*qbf_vector)[0]->eval() != (*qbf_vector)[1]->eval())
	    return true;
	else 
	    return false;
    }
    assert(false);
    return false;
}
void QBF_Logical::propagate(unsigned long assigner_id, bool b)
{
    switch(op_type) {
    case QBF::AND:
	if(b == false) {
	    status = b;
	    if(parent != NULL)
		parent->propagate(assigner_id, b);
	}
	break;
    case QBF::OR:
	if(b == true) {
	    status = b;
	    if(parent != NULL)
		parent->propagate(assigner_id, b);
	}
    case QBF::EQU:
	break;
    case QBF::XOR:
	break;
    }
}

void QBF_Logical::reset_status()
{
    QBF::reset_status();
    BOOST_FOREACH(QBF* q, *qbf_vector) {
	q->reset_status();
    }
}

void QBF_Logical::update_prob()
{
    prob = 1;
    long double p_0, p_1;
    
    switch(op_type) {
    case QBF::AND:
	BOOST_FOREACH(QBF* q, *qbf_vector) {
	    if(boost::logic::indeterminate(q->status)) {
		prob*= q->prob;
	    }
	    else {
	    }
	}
	if(prob < 0.00001)
	    prob = 0.00001;
	break;
    case QBF::OR:
	BOOST_FOREACH(QBF* q, *qbf_vector) {
	    if(boost::logic::indeterminate(q->status)) {
		prob*= (1 - q->prob);
	    }
	    else {
	    }
	}
	prob = 1 - prob;
	if(prob > 0.99999)
	    prob = 0.99999;
	break;
    case QBF::EQU:
	p_0 = ((*qbf_vector)[0])->prob;
	p_1 = ((*qbf_vector)[1])->prob;
	prob = p_0 * (1 - p_1) + (1 - p_0) * p_1;
	break;
    case QBF::XOR:
	p_0 = ((*qbf_vector)[0])->prob;
	p_1 = ((*qbf_vector)[1])->prob;
	prob = p_0 * p_1 + (1 - p_0) * (1 - p_1);
	break;
    }
}

bool mycompare(QBF* q1, QBF* q2)
{
    return (q1->cost) < (q2->cost);
}

void QBF_Logical::update_size()
{
    if(!qbf_sorted) {
	sort(qbf_vector->begin(), qbf_vector->end(), mycompare);
	qbf_sorted = true;
    }
    
    long double tempP = 1, tempS = 0;
    size = 0;
    switch(op_type) {
    case QBF::AND:
	BOOST_FOREACH(QBF* q, *qbf_vector) {
	    if(boost::logic::indeterminate(q->status)) {
		tempS += q->size;
		size += tempP * (1 - q->prob) * tempS;
		tempP *= q->prob;
	    }
	}
	size += tempP * tempS;
	break;
    case QBF::OR:
	BOOST_FOREACH(QBF* q, *qbf_vector) {
	    if(boost::logic::indeterminate(q->status)) {
		tempS += q->size;
		size += tempP * q->prob * tempS;
		tempP *= (1 - q->prob);
	    }
	}
	size += tempP * tempS;
	break;
    case QBF::EQU:
    case QBF::XOR:
	size = ((*qbf_vector)[0])->size + ((*qbf_vector)[1])->size;
    }
}

void QBF_Logical::update_child_cost()
{
    if(op_type == QBF::AND) {
	BOOST_FOREACH(QBF* q, *qbf_vector) {
	    if(boost::logic::indeterminate(q->status))
		q->cost = q->prob * q->size;
	}
    } else {
	BOOST_FOREACH(QBF* q, *qbf_vector) {
	    if(boost::logic::indeterminate(q->status))
		q->cost = (1 - q->prob) * q->size;
	}
    }
}
