#include "Model2C.h"
#include <iostream>
#include <fstream>
#include <stdexcept>
#include "cvc3/include/lang.h"
#include "cvc3/include/theory_arith.h"
#include <boost/shared_ptr.hpp>
#include "util/Util.h"
#include "lang/SymbolTable.h"
#include "lang/ExprManager.h"
#include "lang/Node.h"
#include "lang/Property.h"
#include "lang/Model.h"
#include "lang/Property.h"
#include "lang/PRISMParser.h"
#include "dp/SMT.h"
#include "dp/CVC3SMT.h"
#include <dlfcn.h>
#include <limits>
#include "expr2c.h"
#ifdef WITH_PARAM
#include "rationalFunction/RationalFunction.h"
#include "rationalFunction/CVC3Converter.h"
#endif

using namespace std;
using namespace lang;
#ifdef WITH_PARAM
using namespace Rational;
#endif

namespace infamation {

  dp::SMT &smt(dp::SMT::getSMT());

  /**
   * Construct new Model-to-C converter.
   *
   * @param __model model to be converted
   */
  Model2C::Model2C(Model &__model)
    : streamP(new ostream(cout.rdbuf())),
      stream(*streamP) {
    model = &__model;
    init();
  }

  /**
   * Construct new Model-to-C converter.
   *
   * @param modelFn model file
   */
  Model2C::Model2C(const string &modelFn)
    : streamP(new ostream(cout.rdbuf())),
      stream(*streamP) {
    model = new Model();
    PRISM::PRISMParser parser;
    parser.run(modelFn, *model);
    model->Flatten();
    init();
    internalModel = true;
  }

  /**
   * Construct new Model-to-C converter.
   *
   * @param modelFn model file
   * @param propFn properties file
   */
  Model2C::Model2C(const string &modelFn, const string &propFn)
    : streamP(new ostream(cout.rdbuf())),
      stream(*streamP) {
    model = new Model();
    PRISM::PRISMParser parser;
    parser.run(modelFn, *model);
    parser.run(propFn, *model);
    model->Flatten();
    init();
    exprNumbers = new CVC3::ExprHashMap<unsigned>();
    prepareStateFormulasFromPropertyStructure();
    internalModel = true;
  }

  string Model2C::getVarName(unsigned varNr) {
    return variablesInC[varNr].toString();
  }

  void Model2C::prepareStateFormulasFromPropertyStructure
  (const Property &prop) {
    if (expr == prop.kind) {
      const PropExpr &propExpr(dynamic_cast<const PropExpr &>(prop));
      addStateSet(propExpr.getExpr());
      (*exprNumbers)[propExpr.getExpr()] = stateSets.size() - 1;
    } else {
      for (unsigned childNr(0); childNr < prop.arity(); childNr++) {
        prepareStateFormulasFromPropertyStructure(prop[childNr]);
      }
    }
  }

  void Model2C::prepareStateFormulasFromPropertyStructure() {
    const Properties &props(model->getProperties());
    for (Properties::const_iterator iter(props.begin()); iter != props.end();
         iter++) {
      const Property &prop(*((*iter).get()));
      prepareStateFormulasFromPropertyStructure(prop);
    }
  }

  bool Model2C::fileExists(const string &fileName) const {
    std::fstream fin;
    fin.open(fileName.c_str(),std::ios::in);
    if (fin.is_open()) {
      fin.close();
      return true;
    }
    fin.close();
    return false;
  }

  void Model2C::init() {
    valueType = doubleVal;
    guardedTransitions = &model->getCommands();
    enumerateVariables();
    maxSuccStates = 0;
    for (unsigned gt_nr = 0; gt_nr < guardedTransitions->size(); gt_nr++) {
      Command &gt = *((*guardedTransitions)[gt_nr]);
      const Alternatives &asss = gt.getAlternatives();
      for (unsigned ass_nr = 0; ass_nr < asss.size(); ass_nr++) {
        maxSuccStates++;
      }
    }
    externCleanup = NULL;
    file = NULL;
    libHandle = NULL;
    rewards = false;
    compress = false;
    stateMapType = hash_map;
    internalModel = false;
    gccOptimizationLevel = 0;
    exprNumbers = NULL;
#if __APPLE__
    cppCompiler = "g++-mp-4.3";
#else
    const string CIPGPP432("/usr/local/lang/gcc-4.3.2/bin/g++");
    if (fileExists(CIPGPP432)) {
      cppCompiler = CIPGPP432;
    } else {
      cppCompiler = "g++";
    }
#endif
  }

#ifdef WITH_PARAM
  void Model2C::preparePARAMSpecific() {
    rateToNumber = new RationalToNumber();
    numberToRate = new NumberToRational();
    cvc3converter = new CVC3Converter();
    succRatesListRational = new RationalFunction[maxSuccStates];
    succRewardsListRational = new RationalFunction[maxSuccStates];
    typedef RationalToNumber::iterator RationalToNumberIter;
    for (unsigned gt_nr = 0; gt_nr < guardedTransitions->size(); gt_nr++) {
      Command &gt = *((*guardedTransitions)[gt_nr]);
      const Alternatives &asss = gt.getAlternatives();
      for (unsigned ass_nr = 0; ass_nr < asss.size(); ass_nr++) {
        Alternative &ass = *asss[ass_nr];
        RationalFunction weight((*cvc3converter)(ass.getWeight()));
        RationalToNumberIter it(rateToNumber->find(weight));
        if (it == rateToNumber->end()) {
          rateToNumber->insert(make_pair(weight, numberToRate->size()));
          numberToRate->push_back(weight);
        }
      }
    }
    if (rewards) {
      numberToTransReward = new NumberToRational();
      vector<pair<pair<string,CVC3::Expr>,CVC3::Expr> >
        &transRew(model->getTransRewards());
      for (unsigned rewNr(0); rewNr < transRew.size(); rewNr++) {
        CVC3::Expr rewardExpr(transRew[rewNr].second);
        const RationalFunction rewardRat((*cvc3converter)(rewardExpr));
        numberToTransReward->push_back(rewardRat);
      }

      numberToStateReward = new NumberToRational();
      vector<pair<CVC3::Expr,CVC3::Expr> > &stateRew(model->getStateRewards());
      for (unsigned rewNr(0); rewNr < stateRew.size(); rewNr++) {
        CVC3::Expr rewardExpr(stateRew[rewNr].second);
        const RationalFunction rewardRat((*cvc3converter)(rewardExpr));
        numberToStateReward->push_back(rewardRat);
      }
    }
  }
#endif

  /**
   * Compile model->
   * Call after all relevant options have been set. Will write out
   * the C++ code, compile it with given compiler, load the dynamic
   * library and prepare the model for usage.
   */
  void Model2C::build() {
#ifdef WITH_PARAM
    preparePARAMSpecific();
#endif
    print();
    compileAndLoad();
    externAddInitialStates();
    numSuccStates = externGetNumSuccStates();
    numActiveCommands = externGetNumActiveCommands();    
    succStatesList = externGetSuccStatesList();
    initialStates = externGetInitialStates();
    if (doubleVal == valueType) {
      succRatesList = externGetSuccRatesList();
    } else if (paramVal == valueType) {
#ifdef WITH_PARAM
      succRatesListUnsigned  = externGetSuccRatesListUnsigned();
#endif
    }
    if (rewards) {
      if (doubleVal == valueType) {
        succRewardsList = externGetSuccRewardsList();
      } else if (paramVal == valueType) {
#ifdef WITH_PARAM
        succRewardsListUnsigned  = externGetSuccRewardsListUnsigned();
#endif
      }
    }
    if (isNonDet()) {
      nonDetBounds = externGetNonDetBounds();
    }
  }

  /**
   * Destroy Model-to-C converter and cleanup.
   */
  Model2C::~Model2C() {
    if (NULL != externCleanup) {
      externCleanup();
    }
    if (NULL != file) {
      file->close();
      delete file;
    }
    if (NULL != libHandle) {
      dlclose(libHandle);
    }
#ifdef NDEBUG
#if 0
    if (0 != system("rm -f temp__.cpp temp__.so")) {
      throw runtime_error("Error while deleting file.");
    }
#endif
#endif
    if (NULL != exprNumbers) {
      delete exprNumbers;
    }
    if (internalModel) {
      delete model;
    }
    delete streamP;
#ifdef WITH_PARAM
    delete rateToNumber;
    delete numberToRate;
    delete cvc3converter;
    delete [] succRatesListRational;
    delete [] succRewardsListRational;
#endif
  }

  /**
   * Add distinguished set of states.
   * To check whether a state is element of a given set of states, the
   * function @a inStateSet() may be used. State sets will be given
   * ascending numbers stating with 0.
   *
   * @param stateSet state set to be specified
   */
  void Model2C::addStateSet(const CVC3::Expr &stateSet) {
    stateSets.push_back(stateSet);
  }

  /**
   * Resets output stream to @a stream.
   *
   * @param stream stream to write to
   */
  void Model2C::setOutput(ostream &__stream) {
    streambuf *psbuf = __stream.rdbuf();
    stream.rdbuf(psbuf);
  }

  /**
   * Resets output to file @a filename
   *
   * @param filename file to write to
   */
  void Model2C::setOutput(const string &filename) {
    if (NULL != file) {
      file->close();
      delete file;
      file = NULL;
    }
    file = new ofstream(filename.c_str (), ios::out);
    setOutput(*file);
  }
  
  /**
   * Writes C++ source code of model to "temp__.cpp".
   */
  void Model2C::print() {
    setOutput("temp__.cpp");
    printFileHeader();
    printStatePropType();
    printNewStateProp();
    printStateBuffer();
    printStateMapDef();
    printGetStateSuccessors();
    printAddInitialStates();
    printGetters();
    printInStateSet();
    printCleanup();
    printGetReward();
#ifdef WITH_PARAM
    printGetRationalReward();
#endif
    printGetValue();
    printGetStateList();
  }

  /**
   * Prints function to allocate and (partially) init state prop object.
   */
  void Model2C::printNewStateProp() {
    stream << "extern \"C\"\n"
           << "StateProp *newStateProp() {\n"
           << "  StateProp *stateProp = new StateProp();\n"
           << "  unsigned numInts = sizeof(StateProp) / sizeof(unsigned);\n"
           << "  unsigned *array = (unsigned *)(stateProp);\n"
           << "  array[numInts-1] = 0;\n"
           << "  return stateProp;\n"
           << "}\n\n";
  }

  /**
   * Prints struct definition of state property vector.
   */
  void Model2C::printStatePropType() {
    stream << "typedef struct {\n";
    for (unsigned varNr = 0; varNr < variablesInC.size(); varNr++) {
      if (isInfVariable(varNr)) {
        stream << "  int " << variablesInC[varNr];
      } else {
        stream << (compress ? "  unsigned " : "  int ")
	       << variablesInC[varNr];
        if (compress) {
          stream << " : " << numVariableBits(varNr);
        }
      }
      stream << ";\n";
    }
    stream << "} StateProp;\n\n";
  }

  /**
   * Print out function to check whether a state is in a given state set.
   */
  void Model2C::printInStateSet() {
    stream << "extern \"C\"\n";
    stream << "bool inStateSet(unsigned setNr, unsigned state) {\n";
    printDecodeState();
    for (unsigned setNr = 0; setNr < stateSets.size(); setNr++) {
      stream << "  if ((setNr == " << setNr << ") && ("
	     << expr2c(stateSets[setNr].substExpr(variables, variablesInC))
	     << ")) {\n"
	     << "    return true;\n"
	     << "  }\n";
    }
    stream << "  return false;\n"
	   << "}\n\n";
  }

  /**
   */
  void Model2C::printGetStateList() {
    stream << "extern \"C\"\n";
    stream << "vector<void *> *getStateList() {\n";
    stream << "  return (vector<void *> *) &stateList;\n"
           << "}\n\n";
  }

  /**
   * Print methods to get number of states, etc.
   */
  void Model2C::printGetters() {
    stream
      << "extern \"C\"\n"
      "unsigned *getNumSuccStates() {\n"
      "  return &numSuccStates;\n"
      "}\n\n"
      "extern \"C\"\n"
      "unsigned *getNumActiveCommands() {\n"
      "  return &numActiveCommands;\n"
      "}\n\n"
      "extern \"C\"\n"
      "unsigned *getSuccStatesList() {\n"
      "  return succStatesList;\n"
      "}\n\n"
      "extern \"C\"\n"
      << valueTypeString() << " *getSuccRatesList() {\n"
      "  return succRatesList;\n"
      "}\n\n";
    if (rewards) {
      stream << "extern \"C\"\n"
             << valueTypeString() << " *getSuccRewardsList() {\n"
	"  return succRewardsList;\n"
	"}\n\n";
    }
    stream << "extern \"C\"\n"
      "unsigned getNumStates() {\n"
      "  return stateList.size();\n"
      "}\n\n"
      "extern \"C\"\n"
      "vector<unsigned> *getInitialStates() {\n"
      "  return &initialStates;\n"
      "}\n\n";
    if (isNonDet()) {
      stream << "extern \"C\"\n"
	"unsigned *getNonDetBounds() {\n"
	"  return nonDetBounds;\n"
	"}\n\n";
    }
  }

  /**
   * Computes string with which to call the C++ compiler.
   */
  string Model2C::computeCallString() {
    std::ostringstream numberAsString;
    numberAsString << gccOptimizationLevel;

    return cppCompiler + " -O" + numberAsString.str() + " -fPIC"
#ifndef NDEBUG
      + " -ggdb"
#else
      + " -DNDEBUG"
#endif
      + " -shared -o temp__.so temp__.cpp";
}

  /**
   * Converts model to shared C library and loads its functions.
   */
  void Model2C::compileAndLoad() {
    stream << endl;

    string callstring(computeCallString());
    if (0 != system(callstring.c_str())) {
      throw runtime_error("Error while calling C++ compiler");
    }
    libHandle = dlopen("./temp__.so", RTLD_LAZY);
    if (!libHandle) {
      throw runtime_error("Cannot open library: " + string(dlerror()) + "\n");
    }
    dlerror();
    fetchExtFunction("addInitialStates", &externAddInitialStates);
    fetchExtFunction("getStateSuccessors", &externGetStateSuccessors);
    fetchExtFunction("getNumSuccStates", &externGetNumSuccStates);
    fetchExtFunction("getNumActiveCommands", &externGetNumActiveCommands);
    fetchExtFunction("getSuccStatesList", &externGetSuccStatesList);
    if (doubleVal == valueType) {
      fetchExtFunction("getSuccRatesList", &externGetSuccRatesList);
    } else if (paramVal == valueType) {
#ifdef WITH_PARAM
      fetchExtFunction("getSuccRatesList", &externGetSuccRatesListUnsigned);
#endif
    }
    if (rewards) {
      if (doubleVal == valueType) {
        fetchExtFunction("getSuccRewardsList", &externGetSuccRewardsList);
      } else if (paramVal == valueType) {
#ifdef WITH_PARAM
        fetchExtFunction("getSuccRewardsList", &externGetSuccRewardsListUnsigned);
#endif
      }
    }
    fetchExtFunction("getNumStates", &externGetNumStates);
    fetchExtFunction("cleanup", &externCleanup);
    fetchExtFunction("getReward", &externGetReward);
#ifdef WITH_PARAM
    fetchExtFunction("getRationalReward", &externGetRationalReward);
#endif
    fetchExtFunction("inStateSet", &externInStateSet);
    fetchExtFunction("getInitialStates", &externGetInitialStates);
    if (isNonDet()) {
      fetchExtFunction("getNonDetBounds", &externGetNonDetBounds);
    }
    fetchExtFunction("getValue", &externGetValue);
    fetchExtFunction("getStateList", &externGetStateList);
  }

  /**
   * Obtain string representation of @a state.
   * String will consist of the combination of variable assignments
   * the state represents.
   *
   * @param state state to obtain string representation of
   * @return string representing @a state
   */
  string Model2C::getStateString(unsigned state) {
    std::ostringstream stateStringStream;
    for (unsigned varNr(0); varNr < variables.size(); varNr++) {
      int varValue(getValue(state, variables[varNr].toString()));
      stateStringStream << variables[varNr] << " = "<< varValue << "\n";
    }

    return stateStringStream.str();
  }

  /**
   * Enumerate model variables.
   * Also compute position in state vector, number of bits neeed, etc. if
   * this is neccessary.
   */
  void Model2C::enumerateVariables() {
    /* for performance reasons, have "infinite" variables first. */
    
    for (HashMap<string, CVC3::Expr>::iterator i = model->variables.begin();
         i != model->variables.end(); ++i) {
      if (!model->isParameterVariable(i->second)) {
        CVC3::Type valType = i->second.getType();
        if (CVC3::isInt(valType)) {
          if (!model->hasBounds(i->second)) {
	    CVC3::Expr &var(i->second);
	    const string varName(var.toString());
            variables.push_back(var);
	    CVC3::Expr varInC(vc.varExpr("__modelVar" + varName
					 + "_", var.getType()));
	    variablesInC.push_back(varInC);
            lowerBounds.push_back(numeric_limits<int>::min());
            upperBounds.push_back(numeric_limits<int>::max());
          }
        } else if (valType.isBool()) {
        } else {
          throw runtime_error("Variable \"" + i->second.toString()
                              + "\" has unsupported data type.");
        }
      }
    }

    for (HashMap<string, CVC3::Expr>::iterator i = model->variables.begin();
         i != model->variables.end(); ++i) {
      if (!model->isParameterVariable(i->second)) {
        CVC3::Type valType = i->second.getType();
        if (CVC3::isInt(valType)) {
          if (model->hasBounds(i->second)) {
	    CVC3::Expr &var(i->second);
	    const string varName(var.toString());
            variables.push_back(var);
            CVC3::Expr rLower =
              vc.simplify(model->getBounds(i->second).first);
            CVC3::Expr rUpper =
              vc.simplify(model->getBounds(i->second).second);
	    CVC3::Expr varInC(vc.varExpr("__modelVar" + varName
					 + "_", var.getType()));
	    variablesInC.push_back(varInC);
            lowerBounds.push_back(rLower.getRational().getInt());
            upperBounds.push_back(rUpper.getRational().getInt());
          }
        } else if (valType.isBool()) {
	  CVC3::Expr &var(i->second);
          variables.push_back(var);
	  const string varName(var.toString());
	  CVC3::Expr varInC(vc.varExpr("__modelVar" + varName
				       + "_", var.getType()));
	  variablesInC.push_back(varInC);
          lowerBounds.push_back(0);
          upperBounds.push_back(1);
        } else {
          throw runtime_error("Variable \"" + i->second.toString()
                              + "\" has unsupported data type.");
        }
      }
    }
  }

  /**
   * Print C code to divide state vector into different variables.
   */
  void Model2C::printDecodeState() {
    stream << "  StateProp *stateProp = stateList[state];\n";
    for (unsigned varNr = 0; varNr < variablesInC.size(); varNr++) {
      CVC3::Expr &var = variablesInC[varNr];
      stream << "  int " << var << " = " << "stateProp->"
	     << var << ";\n";
      if (compress && !isInfVariable(varNr)) {
        stream << "  " << var << " += " << lowerBounds[varNr] << ";\n";
      }
    }
  }

  void Model2C::printAdjustNextStateProbabilities() {
    if (DTMC == model->getModelType()) {
      if (doubleVal == valueType) {
      stream << "    for (unsigned stateNr(0); stateNr < numSuccStates; "
        "stateNr++) {\n"
        "      succRatesList[stateNr] /= numActiveCommands;"
        "    }\n";
      }
    }
  }

  /**
   * Print C function to obtain successors of a state.
   */
  void Model2C::printGetStateSuccessors() {
    vector<pair<pair<string,CVC3::Expr>,CVC3::Expr> > &transRew
      = model->getTransRewards();
    stream << "extern \"C\"\n"
      "void getStateSuccessors(unsigned state) {\n"
      "  numSuccStates = 0;\n";
    if (isNonDet() || (DTMC == model->getModelType())) {
      stream << "  numActiveCommands = 0;\n";
    }
    printDecodeState();
    printSuccVarDefinition();
    stream << "  unsigned succNr;\n";
    for (unsigned gt_nr = 0; gt_nr < guardedTransitions->size(); gt_nr++) {
      Command &gt = *((*guardedTransitions)[gt_nr]);
      const CVC3::Expr &guard = gt.getGuard();
      stream << "  if (" << expr2c(guard.substExpr(variables, variablesInC))
	     << ") {\n";
      if (isNonDet()) {
        stream << "    nonDetActions[numActiveCommands] = " << gt_nr << ";\n";
      }
      if (isNonDet() || (DTMC == model->getModelType())) {
        stream << "    numActiveCommands++;\n";
      }
      const Alternatives &asss = gt.getAlternatives();
      stream << "    " << valueTypeString() << " rate__;\n";
      if (rewards) {
        stream << "    " << valueTypeString() << " reward__ = 0;\n";
        string action = gt.getAction();
        for (unsigned i = 0; i < transRew.size(); i++) {
          string &rewardAction = transRew[i].first.first;
          CVC3::Expr &guard = transRew[i].first.second;
          if (action == rewardAction) {
            stream << "    if (" << expr2c(guard) << ") {\n";
            if (doubleVal == valueType) {
              CVC3::Expr &reward = transRew[i].second;
              stream << "      reward__ += " << expr2c(reward) << ";\n";
            } else if (paramVal == valueType) {
              stream << "      reward__ |= 1 << " << i << ";\n";
            }
            stream << "    }\n";
          }
        }
      }
      for (unsigned ass_nr = 0; ass_nr < asss.size(); ass_nr++) {
        Alternative &ass = *asss[ass_nr];
        stream << "    rate__ = ";
        if (doubleVal == valueType) {
          stream << expr2c(ass.getWeight().substExpr(variables, variablesInC));
        } else if (paramVal == valueType) {
#ifdef WITH_PARAM
          RationalFunction weight((*cvc3converter)(ass.getWeight()));
          unsigned number((*rateToNumber)[weight]);
          stream << number;
#endif
        }
        stream << ";\n";
        printSuccStateAssignments(ass);
        printSafeSuccState();
      }
      if (isNonDet()) {
        stream << "    nonDetBounds[numActiveCommands] = numSuccStates;\n";
      }
      stream << "  }\n";
      printAdjustNextStateProbabilities();
    }
    stream << "}\n";
  }

  /**
   * Print C sequence to assign values to variables of successor state.
   *
   * @param ass alternative from which successor results
   */
  void Model2C::printSuccStateAssignments(Alternative &ass) {
    const Alternative::Map& map(ass.getMap());
    for (Alternative::Map::const_iterator i = map.begin(); i!=map.end(); ++i) {
      CVC3::Expr var(i->first.substExpr(variables, variablesInC));
      CVC3::Expr assExpr(i->second.substExpr(variables, variablesInC));

      stream << "    " << var.toString() << "P = ";
      stream << expr2c(assExpr);
      stream << ";\n";
    }
    for (unsigned varNr = 0; varNr < variablesInC.size(); varNr++) {
      CVC3::Expr &var(variablesInC[varNr]);
      if (0 == map.count(variables[varNr])) {
        stream << "    " << var << "P = " << var << ";\n";
      }
    }
  }

  /**
   * Print C code to define variables of successor state.
   */
  void Model2C::printSuccVarDefinition() {
    for (unsigned varNr = 0; varNr < variablesInC.size(); varNr++) {
      stream << "  int " << variablesInC[varNr] << "P;\n";
    }
  }

  bool Model2C::isInfVariable(unsigned var) {
    const CVC3::Type varType(variables[var].getType());
    if (varType.isBool()) {
      return false;
    }
    return !model->hasBounds(variables[var]);
  }

  unsigned Model2C::numVariableBits(unsigned var) {
    if (isInfVariable(var)) {
      return 32;
    } else {
      const unsigned numPossibleValues(1 + upperBounds[var] - lowerBounds[var]);
      unsigned numBits = 1;
      unsigned roundedSize = 2;
      while (roundedSize < numPossibleValues) {
        numBits++;
        roundedSize *= 2;
      }
      
      return numBits;
    }
  }

  void Model2C::printSuccToSuccProp() {
    for (unsigned varNr = 0; varNr < variablesInC.size(); varNr++) {
      stream << "    succProp->" << variablesInC[varNr] << " = ";
      if (!compress || isInfVariable(varNr)) {
        stream << variablesInC[varNr] << "P;\n";
      } else {
        stream << "unsigned(" << variablesInC[varNr] << "P - "
               << lowerBounds[varNr] << ");\n";
      }
    }
  }

  /**
   * Print C code to safe successor state.
   * Will create a new state if neccessary and add it to successor list.
   * If state already exists, it will just be added to successor list.
   * Also handles the sink/target state case.
   */
  void Model2C::printSafeSuccState() {
    printSuccToSuccProp();
    
    
    /* successor is a state already seen */
    stream << "if (0 != stateMap.count(succProp)) {\n"
      "      succNr = stateMap[succProp];\n"
      "      succStatesList[numSuccStates] = succNr;\n"
      "      succRatesList[numSuccStates] = rate__;\n";
    if (rewards) {
      stream << "    succRewardsList[numSuccStates] = reward__;\n";
    }
    stream << "    numSuccStates++;\n"
      "    } else {\n";
    /* successor is new state */
    stream << "      stateList.push_back(succProp);\n"
      "      succNr = stateList.size() - 1;\n"
      "      stateMap[succProp] = succNr;\n"
      "      succProp = newStateProp();\n"
      "      succStatesList[numSuccStates] = succNr;\n"
      "      succRatesList[numSuccStates] = rate__;\n";
    if (rewards) {
      stream << "      succRewardsList[numSuccStates] = reward__;\n";
    }
    stream << "    numSuccStates++;\n";
    stream << "    }\n";
  }
  
  /**
   * Print C definitions and helper functions for state hashmap.
   */
  void Model2C::printStateMapDef() {
    if (hash_map == stateMapType) {
      /* SDBM algorithm (from Berkeley DataBase) */
      stream << "struct eqstate {\n"
        "  bool operator()(const StateProp* s1, const StateProp* s2) const {\n"
        "    unsigned numInts = sizeof(StateProp) / sizeof(unsigned);\n"
        "    unsigned *array1 = (unsigned *)(s1);\n"
        "    unsigned *array2 = (unsigned *)(s2);\n"
        "    for (unsigned i = 0; i < numInts; i++) {\n"
        "      if (array1[i] != array2[i]) {\n"
        "        return false;\n"
        "      }\n"
        "    }\n"
        "    return true;\n"
        "  }\n"
        "};\n\n"
        "struct hashstate {\n"
        "  size_t operator()(const StateProp* s) const {\n"
        "    unsigned numInts = sizeof(StateProp) / sizeof(unsigned);\n"
        "    unsigned *array = (unsigned *)(s);\n"
        "    size_t hash = 0;\n\n"
        "    for (unsigned i = 0; i < numInts; i++) {\n"
        "      hash = array[i] + (hash << 6) + (hash << 16) - hash;\n"
        "    }\n"
        "    return hash;\n"
        "  }\n"
        "};\n\n"
        "std::tr1::unordered_map<const StateProp*, unsigned, hashstate,"
        "eqstate> stateMap;\n";
    } else if (map == stateMapType) {
      stream << "struct leqstate {\n"
        "  bool operator()(const StateProp* const &s1, const StateProp* const &s2) const {\n"
        "    unsigned numInts = sizeof(StateProp) / sizeof(unsigned);\n"
        "    unsigned *array1 = (unsigned *)(s1);\n"
        "    unsigned *array2 = (unsigned *)(s2);\n"
        "    for (unsigned i = 0; i < numInts; i++) {\n"
        "      if (array1[i] < array2[i]) {\n"
        "        return true;\n"
        "      } else if (array1[i] > array2[i]) {\n"
        "        return false;\n"
        "      }\n"
        "    }\n"
        "    return false;\n"
        "  }\n"
        "};\n\n"
        "map<const StateProp *, unsigned, leqstate> stateMap;\n";
    } else {
      throw runtime_error("Invalid state map type.");
    }
    stream << "vector<StateProp *> stateList;\n"
      "vector<unsigned> initialStates;\n";
  }

  /**
   * Print header for C file.
   */
  void Model2C::printFileHeader() {
    stream << "#include <cstring>\n"
      "#include <iostream>\n"
      "#include <math.h>\n"
      "#include <vector>\n"
      "#include <assert.h>\n";
    if (hash_map == stateMapType) {
      stream << "#include <tr1/unordered_map>\n";
    } else if (map == stateMapType) {
      stream << "#include <map>\n";
    }
    stream << "using namespace std;\n";
  }

  /**
   * Print C definitions for state arrays, number of states, etc.
   */
  void Model2C::printStateBuffer() {
    stream << "unsigned numSuccStates = 0;\n"
      "unsigned succStatesList[" << maxSuccStates << "];\n";
    stream << valueTypeString() << " succRatesList["
           << maxSuccStates << "];\n";
    stream << "unsigned numActiveCommands;\n";
    if (isNonDet()) {
      stream << "unsigned nonDetBounds["
             << guardedTransitions->size() + 1 << "];\n"
             << "unsigned nonDetActions["
             << guardedTransitions->size() << "];\n";
    }
    
    if (rewards) {
      stream << valueTypeString() << " succRewardsList["
             << maxSuccStates << "];\n";
    }
    stream << "StateProp *succProp = newStateProp();\n";
  }
  
  /**
   * Print C code for cleanup function.
   * The function generated should be called before library unloading
   * to free memory etc.
   */
  void Model2C::printCleanup() {
    stream << "extern \"C\"\n"
      "void cleanup() {\n"
      "  delete succProp;\n"
      "  for (unsigned state = 0; state < stateList.size(); "
      "state++) {\n"
      "    delete stateList[state];\n"
      "  }\n"
      "}\n\n";
  }

  /**
   * Print C code for function to obtain state reward.
   */
  void Model2C::printGetReward() {
    stream << "extern \"C\"\n"
      "double getReward(unsigned state) {\n";
    printDecodeState();
    stream << "  double reward = 0.0;\n";
    vector<pair<CVC3::Expr,CVC3::Expr> > &gr = model->getStateRewards();
    for (unsigned i = 0; i < gr.size(); i++) {
      CVC3::Expr &guard = gr[i].first;
      stream << "  if (" << expr2c(guard.substExpr(variables, variablesInC)) << ") {\n"
	"    reward += " << expr2c(gr[i].second.substExpr(variables, variablesInC)) << ";\n"
	     << "  }\n";
    }
    stream << "  return reward;\n"
	   << "}\n\n";
  }

  void Model2C::printGetRationalReward() {
    stream << "extern \"C\"\n"
      "unsigned getRationalReward(unsigned state) {\n";
    printDecodeState();
    stream << "  unsigned reward = 0;\n";
    vector<pair<CVC3::Expr,CVC3::Expr> > &gr = model->getStateRewards();
    for (unsigned i = 0; i < gr.size(); i++) {
      CVC3::Expr &guard = gr[i].first;
      stream << "  if (" << expr2c(guard.substExpr(variables, variablesInC)) << ") {\n"
	"    reward |= 1 << " << i << ";\n"
	     << "  }\n";
    }
    stream << "  return reward;\n"
	   << "}\n\n";
  }

  /**
   * Print C code to get variable value at a state.
   */
  void Model2C::printGetValue() {
    stream << "extern \"C\"\n"
      "int getValue(unsigned state, const std::string &variable) {\n";
    // TODO could be done more efficient, if wanted
    stream << "  StateProp *stateProp = stateList[state];\n";
    for (unsigned varNr = 0; varNr < variablesInC.size(); varNr++) {
      CVC3::Expr &var = variables[varNr];
      stream << "  if (variable == \"" << var.substExpr(variables, variablesInC) << "\") {\n";
      stream << "    int result = stateProp->" << var.substExpr(variables, variablesInC) << ";\n";
      if (compress && !isInfVariable(varNr)) {
        stream << "    result += " << lowerBounds[varNr] << ";\n";
      }
      stream << "    return result;\n";
      stream << "  }\n";
    }
    stream << "  assert(false);\n";
    stream << "  }\n\n";
  }

  /**
   * Restricts expression @a to valid ranges of model variables
   *
   * @param expr expression to be restricted
   */
  void Model2C::restrictExprToValidVariablesRange(CVC3::Expr &expr) {
    for (unsigned varNr(0); varNr < variables.size(); varNr++) {
      const CVC3::Expr &variable(variables[varNr]);
      if (model->hasBounds(variable)) {
        const CVC3::Expr &lowerBound(model->getBounds(variable).first);
        const CVC3::Expr &upperBound(model->getBounds(variable).second);
        const CVC3::Expr varGeqLower(vc.geExpr(variable, lowerBound));
        const CVC3::Expr varLeqUpper(vc.leExpr(variable, upperBound));
        expr = vc.andExpr(expr, varGeqLower);
        expr = vc.andExpr(expr, varLeqUpper);
      }
    }
  }

  /**
   * Print C code to add initial states to model->
   */
  void Model2C::printAddInitialStates() {
    stream << "extern \"C\"\n"
      "void addInitialStates() {\n";
    if (isNonDet()) {
      stream << "  nonDetBounds[0] = 0;\n";
    }
    stream << "  StateProp *stateProp;\n";

    CVC3::Expr initStatesExpr(model->getInitial());
    restrictExprToValidVariablesRange(initStatesExpr);
    smt.pushContext();    
    smt.Assert(initStatesExpr);
    
    while (true) {
      smt.pushContext();
      lbool smt_result = smt.Solve();
      if (smt_result != l_true ) {
        smt.popContext();
        break;
      }
      CVC3::ExprHashMap<CVC3::Expr> varMap;
      smt.getModel(variables, varMap);
      smt.popContext();

      smt.blockModel(varMap);
      stream << "  stateProp = newStateProp();\n";

      for (unsigned varNr = 0; varNr < variables.size(); varNr++) {
        CVC3::Expr &var = variables[varNr];
        CVC3::Expr &varInC = variablesInC[varNr];
        stream << "  stateProp->" << varInC << " = "
               << expr2c(varMap[var]);
        if (compress && !isInfVariable(varNr)) {
          stream << " - " << lowerBounds[varNr];
        }
        stream << ";\n";
      }
      stream << "  stateList.push_back(stateProp);\n"
        "  stateMap[stateProp] = stateList.size() - 1;\n"
        "  initialStates.push_back(stateList.size() - 1);\n";
    }
    stream << "}\n\n";
    smt.popContext();
  }

  bool Model2C::isNonDet() const {
    return (lang::MDP == model->getModelType())
      || (lang::CTMDP == model->getModelType());
  }

  /**
   * Explores all states of the model.
   * You should not all this, if your model is of infinite size.
   */
  void Model2C::exploreAllStates() {
    unsigned state = 0;

    while (state < getNumStates()) {
      getStateSuccessors(state);
      state++;
    }
  }

  /**
   * Try to obtain an external function by name.
   * As library handle, @a libHandle will be used.
   *
   * @param name name of symbol
   * @param function pointer to be set
   */
  template<typename T>
  void Model2C::fetchExtFunction(const std::string &name, T *function) {
    *function = (T)
      dlsym(libHandle, name.c_str());
    char *dlsym_error = dlerror();
    if (NULL != dlsym_error) {
      std::cerr << "Cannot load symbol '" << name << "': " <<
        dlsym_error << std::endl;
      dlclose(libHandle);
      exit(1);
    }
  }

  const Properties &Model2C::getProperties() {
    return model->getProperties();
  }

  /**
   * Checks whether expression @a expr is valid in @a state.
   * For this to work, expr must have been prepared before the model
   * is actually compiled.
   *
   * @param expr CVC3 expression to check whether valid in state
   * @state state state to check whether CVC3 expession is valid in
   * @return true iff expression is valid in state
   */
  bool Model2C::exprValid(const CVC3::Expr &expr, unsigned state) const {
    assert(NULL != exprNumbers);
    unsigned setNr((*exprNumbers)[expr]);
    return inStateSet(setNr, state);
  }

  /**
   * Checks whether underlying model is continuous time or not.
   *
   * @return true if time model is continuous
   */
  bool Model2C::isContinuousTimeModel() const {
    const ModelType type(model->getModelType());
    if ((CTMC == type) || (CTMDP == type)) {
      return true;
    } else {
      return false;
    }
  }

  void Model2C::setValueType(ValueType valueType__) {
#ifndef WITH_PARAM
      if (paramVal == valueType) {
        std::cerr << "Support for parametric values not compiled in" << endl;
        exit(1);
      }
#endif
      valueType = valueType__;
    }

#ifdef WITH_PARAM
  void Model2C::computeTransRationals() {
    for (unsigned succNr(0); succNr < *numSuccStates; succNr++) {
      const unsigned rateNumber(succRatesListUnsigned[succNr]);
      succRatesListRational[succNr] = (*numberToRate)[rateNumber];
      if (DTMC == model->getModelType()) {
        if (1 != *numActiveCommands) {
          succRatesListRational[succNr] /= *numActiveCommands;
        }
      }
    }

    if (rewards) {
      for (unsigned succNr(0); succNr < *numSuccStates; succNr++) {
        vector<pair<pair<string,CVC3::Expr>,CVC3::Expr> >
          &transRew(model->getTransRewards());
        unsigned rewardBit(1);
        succRewardsListRational[succNr] = RationalFunction(0);
        for (unsigned rewNr(0); rewNr < transRew.size(); rewNr++) {
          if (succRewardsListUnsigned[succNr] & rewardBit) {
            const RationalFunction rewardRat((*numberToTransReward)[rewNr]);
            succRewardsListRational[succNr] += rewardRat;
          }
          rewardBit <<= 1;
        }
      }      
    }
  }
#endif

#ifdef WITH_PARAM
  RationalFunction Model2C::getReward(unsigned state) {
    vector<pair<CVC3::Expr,CVC3::Expr> > &stateRew(model->getStateRewards());
    unsigned rewardBit(1);
    RationalFunction result(0);
    unsigned rewardMask(externGetRationalReward(state));
    for (unsigned rewNr(0); rewNr < stateRew.size(); rewNr++) {
      if (rewardMask & rewardBit) {
	const RationalFunction rewardRat((*numberToStateReward)[rewNr]);
	result += rewardRat;
      }
      rewardBit <<= 1;
    }

    return result;
  }

#endif
}
