#include "qbf_parser.hpp"
#include "qbf_quantified.hpp"
#include "qbf_logical.hpp"
#include "qbf_literal.hpp"
#include "literal.hpp"
#include "variable.hpp"

QBF_Parser::QBF_Parser(QBF_Lexer* l)
    : lexer(l)
{
}

QBF* QBF_Parser::parse()
{
    QBF *q = NULL;
    std::vector<Variable*>* var_vector = NULL;
    std::vector<QBF*>* qbf_vector = NULL;
    QBF::logical_operator op_type = QBF::OR;
    QBF::quantifier q_type = QBF::EXISTS;
    bool literal_truth = true;
    QBF_Lexer::token t = lexer->get_next();
    switch(t) {
	// Universal & Existential
    case QBF_Lexer::FORALL:
	q_type = QBF::FORALL;
    case QBF_Lexer::EXISTS:
	t = lexer->get_next();
	if(t != QBF_Lexer::LBRACKET) return NULL;
	var_vector = parse_var_vector();
	if(var_vector == NULL) return NULL;
	q = parse();
	if(q == NULL) return NULL;
	return new QBF_Quantified(q_type, var_vector, q);
	// (Q)
    case QBF_Lexer::LPAREN:
	q = parse();
	if(q == NULL) return NULL;
	t = lexer->get_next();
	if(t != QBF_Lexer::RPAREN) return NULL;
	return q;
	// And & Or
    case QBF_Lexer::AND:
	op_type = QBF::AND;
	qbf_vector = parse_qbf_vector();
	if(qbf_vector == NULL) return NULL;
	return new QBF_Logical(op_type, qbf_vector);
    case QBF_Lexer::EQU:
	op_type = QBF::EQU;
	qbf_vector = parse_qbf_vector();
	if(qbf_vector == NULL) return NULL;
	return new QBF_Logical(op_type, qbf_vector);
    case QBF_Lexer::XOR:
	op_type = QBF::XOR;
	qbf_vector = parse_qbf_vector();
	if(qbf_vector == NULL) return NULL;
	return new QBF_Logical(op_type, qbf_vector);
    case QBF_Lexer::OR:
	op_type = QBF::OR;
	qbf_vector = parse_qbf_vector();
	if(qbf_vector == NULL) return NULL;
	return new QBF_Logical(op_type, qbf_vector);
    case QBF_Lexer::NEG:
	literal_truth = false;
	t = lexer->get_next();
	if(t != QBF_Lexer::VAR) return NULL;
    case QBF_Lexer::VAR:	
	return new QBF_Literal(Literal::get_literal(literal_truth, 
						     Variable::get_variable(lexer->buffer)));
    default:
	return NULL;
    }
}

std::vector<Variable*>* QBF_Parser::parse_var_vector()
{
    std::vector<Variable*>* var_vector = new std::vector<Variable*>();
    QBF_Lexer::token t = lexer->get_next();
    while(t == QBF_Lexer::VAR) {
	var_vector->push_back(Variable::get_variable(lexer->buffer));
	t = lexer->get_next();
    }
    if(t != QBF_Lexer::RBRACKET)
	return NULL;
    else
	return var_vector;
}

std::vector<QBF*>* QBF_Parser::parse_qbf_vector()
{
    std::vector<QBF*>* qbf_vector = new std::vector<QBF*>();
    QBF_Lexer::token t;
    while(true) {
	qbf_vector->push_back(parse());
	t = lexer->get_next();
	lexer->push_back(t);
	if(t == QBF_Lexer::RPAREN || 
	   t  == QBF_Lexer::END) {
	    break;
	}
    }
    return qbf_vector;
}
