/*
 * This file is part of Model2X.
 *
 * Model2X is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * Model2X is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.

 * You should have received a copy of the GNU General Public License
 * along with Model2X.  If not, see <http://www.gnu.org/licenses/>.
 *
 * Copyright 2010 Ernst Moritz Hahn (emh@cs.uni-sb.de)
 */

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

namespace model2x {
  using namespace std;
  std::tr1::unordered_map<unsigned,string>
  expr2lua::kindToString(prepareKindToString());
  
  /**
   * Prints CVC3 expression to @a stream as Lua expression.
   *
   * @param expr CVC3 expression to print
   */
  void expr2lua::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 << "(function() if ";
        printExprC(stream, expr[0]);
	stream << " then return ";
        printExprC(stream, expr[1]);
	stream << " else return ";
        printExprC(stream, expr[2]);
	stream << " end end)()";
      } else if (CVC3::POW == expr.getKind()) {
        stream << "math.pow( ";
        printExprC(stream, expr[1]);
        stream << ",  ";
        printExprC(stream, expr[0]);
        stream << ")";
      } else {
        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;
	} else {
	  stream << "(" << numerator << " / " << denominator << ")";
	}
      } else {
        stream << expr;
      }
    }      
  }
  
  /**
   * Prepares the hash-table mapping CVC3 to C operators.
   */
  std::tr1::unordered_map<unsigned,std::string>
  expr2lua::prepareKindToString() {
    std::tr1::unordered_map<unsigned,std::string> kindToString;

    kindToString[CVC3::AND] = "and";
    kindToString[CVC3::OR] = "or";
    kindToString[CVC3::NOT] = "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;
  }
}
