#include "literal.hpp"
#include <boost/foreach.hpp>
#include <iostream>

std::map<Variable*, Literal*> Literal::true_literal_map;
std::map<Variable*, Literal*> Literal::false_literal_map;

Literal::Literal(bool t, Variable* v)
    : truth(t), var(v)
{
}

Literal::~Literal(void)
{
}

boost::logic::tribool Literal::eval()
{
    return value;
//    return truth ? var->value : !(var->value);
}

Literal* Literal::get_literal(bool t, Variable* v)
{
    if(t == true) {
	std::map<Variable*, Literal*>::iterator iter = true_literal_map.find(v);
	if(iter != true_literal_map.end()) {
	    return iter->second;
	}
	else {
	    Literal *new_one = new Literal(t, v);
	    v->true_literal = new_one;
	    true_literal_map.insert(std::make_pair(v, new_one));
	    return new_one;
	}
    }
    else {
	std::map<Variable*, Literal*>::iterator iter = false_literal_map.find(v);
	if(iter != false_literal_map.end()) {
	    return iter->second;
	}
	else {
	    Literal *new_one = new Literal(t, v);
	    v->false_literal = new_one;
	    false_literal_map.insert(std::make_pair(v, new_one));
	    return new_one;
	}
    }    
}

void Literal::add_parent(QBF_Literal* p)
{
    parent_list.push_back(p);
}

void Literal::propagate(unsigned long assigner_id, bool b)
{
    BOOST_FOREACH(QBF_Literal* q, parent_list) {
	q->propagate(assigner_id, b);
    }
}
