#include <stdexcept>
#include "cvc3/include/lang.h"
#include "cvc3/include/theory_arith.h"
#include "expr2c.h"

using namespace std;

namespace infamation {
  std::tr1::unordered_map<unsigned,string>
  expr2c::kindToString(prepareKindToString());
  
  /**
   * Prints CVC3 expression to "stream" as C expression.
   *
   * @param expr CVC3 expression to print
   */
  void expr2c::printExprC(std::ostream &stream, const CVC3::Expr &expr)
    const {
    if (0 != expr.arity()) {
      unsigned kind = expr.getKind();
      if (0 != kindToString.count(kind)) {
        string &op = kindToString[kind];
        if (1 == expr.arity()) {
          stream << op << "(";
          printExprC(stream, expr[0]);
          stream << ")";
        } else {
          stream << "(";
          printExprC(stream, expr[0]);
          stream << ")";
          for (unsigned childNr = 1u; childNr < unsigned(expr.arity());
               childNr++) {
            stream << " " << op << " (";
            printExprC(stream, expr[childNr]);
            stream << ")";
          }
        }
      } else if (expr.isITE()) {
        stream << "(";
        printExprC(stream, expr[0]);
        stream << ") ? (";
        printExprC(stream, expr[1]);
        stream << ") : (";
        printExprC(stream, expr[2]);
        stream << ")";
      } else if (CVC3::POW == expr.getKind()) {
        stream << "pow((double) ";
        printExprC(stream, expr[1]);
        stream << ", (double) ";
        printExprC(stream, expr[0]);
        stream << ")";
      } else {
        // TODO possible convert expression to string via strbuffer
        throw runtime_error("Unsupported operator in expression\".");
      }
    } else {
      if (expr.isTrue()) {
        stream << "true";
      } else if (expr.isFalse()) {
        stream << "false";
      } else if (CVC3::isRational(expr)) {
        const CVC3::Rational rational(expr.getRational());
	const int numerator(rational.getNumerator().getInt());
	const int denominator(rational.getDenominator().getInt());
	if (1 == denominator) {
	  stream << numerator << ".0";
	} else {
	  stream << "(" << numerator << ".0 / " << denominator << ".0)";
	}
      } else {
        stream << expr;
      }
    }      
  }
  
  /**
   * Prepares the hash-table mapping CVC3 to C operators.
   */
  std::tr1::unordered_map<unsigned,std::string>
  expr2c::prepareKindToString() {
    std::tr1::unordered_map<unsigned,std::string> kindToString;

    kindToString[CVC3::AND] = "&&";
    kindToString[CVC3::OR] = "||";
    kindToString[CVC3::NOT] = "!";
    kindToString[CVC3::EQ] = "==";
    kindToString[CVC3::NEQ] = "!=";
    kindToString[CVC3::UMINUS] = "-";
    kindToString[CVC3::PLUS] = "+";
    kindToString[CVC3::MINUS] = "-";
    kindToString[CVC3::MULT] = "*";
    kindToString[CVC3::DIVIDE] = "/";
    kindToString[CVC3::LT] = "<";
    kindToString[CVC3::GT] = ">";
    kindToString[CVC3::LE] = "<=";
    kindToString[CVC3::GE] = ">=";
    kindToString[CVC3::IFF] = "==";

    return kindToString;
  }
}
