#include "qbf_lexer.hpp"

QBF_Lexer::QBF_Lexer(std::istream& input)
    : in(input)
{
}

QBF_Lexer::token QBF_Lexer::get_next()
{
    char c = in.get();
    while(isspace(c))
	c = in.get();
    switch (c) {
    case '!':
	return NEG;
    case '(':
	return LPAREN;
    case ')':
	return RPAREN;
    case '[':
	return LBRACKET;
    case ']':
	return RBRACKET;
    case '|':
	return OR;
    case '&':
	return AND;
    case '*':
	return XOR;
    case '=':
	return EQU;
    case '@':
	return FORALL;
    case '#':
	return EXISTS;
    case EOF:
	return END;;
    default:
	in.putback(c);
	return process_var();
    }
    return NEG;
}

void QBF_Lexer::push_back(token t)
{
    switch(t) {
    case NEG:
	in.putback('!');
	break;
    case AND:
	in.putback('&');
	break;
    case XOR:
	in.putback('*');
	break;
    case EQU:
	in.putback('=');
	break;
    case OR:
	in.putback('|');
	break;
    case EXISTS:
	in.putback('#');
	break;
    case FORALL:
	in.putback('@');
	break;
    case LPAREN:
	in.putback('(');
	break;
    case RPAREN:
	in.putback(')');
	break;
    case LBRACKET:
	in.putback('[');
	break;
    case RBRACKET:
	in.putback(']');
	break;
    case VAR:
	for(int i = buffer.length() - 1; i >= 0; i--)
	    in.putback(buffer[i]);
	break;
    case END:
	in.putback(EOF);
	break;
    }
}


QBF_Lexer::token QBF_Lexer::process_var()
{
    buffer = std::string();
    char c;
    while(c = in.get(), (isalnum(c) || (c == '_')))
	buffer+=c;
    in.putback(c);
    return VAR;
}

const bool QBF_Lexer::is_special_char(const char c)
{
    switch (c)
    {
    case '!':
    case '(':
    case ')':
    case '[':
    case ']':
    case '|':
    case '&':
    case '*':
    case '=':
    case '@':
    case '#':
    case EOF:
	return true;
    }
    return false;
}
