#include "qbf_quantified.hpp"
#include "boost/foreach.hpp"
#include <boost/bind.hpp>
#include <cmath>
#include <iostream>

QBF_Quantified::QBF_Quantified(quantifier q_t, std::vector<Variable*>* vl, QBF* q)
    : q_type(q_t), var_vector(vl), qbf(q), variable_ordered(false), preprocessed(false)
{
    q->set_parent(this);
}

QBF_Quantified::~QBF_Quantified(void)
{
}

std::string QBF_Quantified::toString()
{
    std::string result = "(";
    result += (q_type == FORALL) ? "@" : "#";
    result += " [";
    BOOST_FOREACH(Variable* v, *var_vector) {
	result+=v->var_name + " ";
    }
    result += "] ";
    result += " " + qbf->toString() + ")";
    return result;
}

bool mycompare(Variable* v1, Variable* v2)
{
    long double cost_diff_v1 = v1->false_cost - v1->true_cost;
    if(cost_diff_v1 < 0) cost_diff_v1 = - cost_diff_v1;
    long double cost_diff_v2 = v2->false_cost - v2->true_cost;
    if(cost_diff_v2 < 0) cost_diff_v2 = - cost_diff_v2;

    return cost_diff_v1 > cost_diff_v2;

}

void QBF_Quantified::update()
{
    if(boost::logic::indeterminate(qbf->status))
	qbf->update();


    // variable 마다 true / false로 propagate하고,
    // 각각의 cost를 구해서 variable에 저장하고
    // status reset하는 것을 모두 반복한 후에
    // 비로서 update 시작.
    if(preprocessed && !variable_ordered) {
	BOOST_FOREACH(Variable* v, *var_vector) {
	    v->propagate(id, true);
	    qbf->update();
	    QBF::update();
	    v->true_cost = qbf->cost;
	    reset_status();

	    v->propagate(id, false);
	    qbf->update();
	    QBF::update();
	    v->false_cost = qbf->cost;
	    reset_status();

	    v->preference = (v->true_cost < v->false_cost) ? true : false;
	    v->not_preference = ! (v->preference);
/*	    std::cout << v->var_name << " : " << v->preference 
		      << " :: " << v->true_cost << " : " << v->false_cost
		      << std::endl;*/
	}
	sort(var_vector->begin(), var_vector->end(), mycompare);
	variable_ordered = true;
    }
    else
	QBF::update();
    preprocessed = true;
}

bool QBF_Quantified::eval()
{
    return eval(var_vector->begin());
}

bool QBF_Quantified::eval(std::vector<Variable*>::iterator itr)
{
    if(itr != var_vector->end()) {
	// 아직 variable instantiate이 끝나지 않은 경우
	Variable* curr_var = *itr;
	if(q_type == QBF::FORALL) {
	    curr_var->assign_prefered_value();
	    ++itr;
	    if(!eval(itr))
		return false;
	    else {
		curr_var->assign_not_prefered_value();
		return eval(itr);
	    }
	}
	else {
	    curr_var->assign_prefered_value();
	    ++itr;
	    if(eval(itr))
		return true;
	    else {
		curr_var->assign_not_prefered_value();
		return eval(itr);
	    }
	}
    }
    else {
	return qbf->eval();
    }
}

void QBF_Quantified::propagate(unsigned long assigner_id, bool b)
{
    status = b;
    if(parent != NULL && assigner_id != id)
	parent->propagate(assigner_id, b);
}
    
void QBF_Quantified::reset_status()
{
    QBF::reset_status();
    qbf->reset_status();
}


void QBF_Quantified::update_prob()
{
    if(boost::logic::indeterminate(status)) {
	if(q_type == QBF::FORALL) {
	    prob = pow(qbf->prob, (1u << var_vector->size()));
	    if(prob < 0.00001)
		prob = 0.00001;
	} else {
	    prob = 1 - pow((1 - qbf->prob), (1u << var_vector->size()));
	    if(prob > 0.99999)
		prob = 0.99999;
	}
    }
    else if(status == true)
	prob = 0.999999;
    else if(status == false)
	prob = 0.000001;
}

void QBF_Quantified::update_size()
{
    if(!boost::logic::indeterminate(status))
	size = 0;
    else {
	if(q_type == QBF::FORALL) {
	    size = pow(1 + qbf->prob, var_vector->size()) * qbf->size;
	} else {
	    size = pow(2 - qbf->prob, var_vector->size()) * qbf->size;
	}
    }
}

void QBF_Quantified::update_child_cost()
{
    if(!boost::logic::indeterminate(status))
	qbf->cost = 0;
    else {
	if(q_type == QBF::FORALL) {
	    qbf->cost = qbf->prob * qbf->size;
	}
	else {
	    qbf->cost = (1 - qbf->prob) * qbf->size;
	}
    }
}

