#ifndef EXPR2C_H
#define EXPR2C_H

#include <tr1/unordered_map>
#include <expr.h>
#include "lang/ExprManager.h"

namespace infamation {
  class expr2c {
    friend std::ostream &operator<<(std::ostream &, const expr2c &);
  public:
  expr2c(const CVC3::Expr &__expr): expr(lang::vc.simplify(__expr)) {
    }
  private:
    static std::tr1::unordered_map<unsigned,std::string>
      prepareKindToString();
    void printExprC(std::ostream &, const CVC3::Expr &) const;
    static std::tr1::unordered_map<unsigned,std::string> kindToString;
    const CVC3::Expr expr;
  };

  inline std::ostream &operator<<(std::ostream &os, const expr2c &expr2c) {
    expr2c.printExprC(os, expr2c.expr);
    return os;
  }
}

#endif
