/*
 * This file is part of PARAM.
 *
 * PARAM 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.
 *
 * PARAM 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 PARAM.  If not, see <http://www.gnu.org/licenses/>.
 *
 * Copyright 2009 Ernst Moritz Hahn (emh@cs.uni-sb.de)
 */

#ifndef RATIONAL_FUNCTION_H
#define RATIONAL_FUNCTION_H

#include <iostream>
#include <vector>
#include <map>
#include <tr1/unordered_map>
#include "RationalCmp.h"

namespace Rational {
  class RationalFunction;
  class Base;
  class CVC3Converter;

  RationalFunction operator+
    (const RationalFunction &, const RationalFunction &);
  RationalFunction operator-
    (const RationalFunction &, const RationalFunction &);
  RationalFunction operator-
    (const RationalFunction &);
  RationalFunction operator*
    (const RationalFunction &, const RationalFunction &);
  RationalFunction operator/
    (const RationalFunction &, const RationalFunction &);
  bool operator==(const RationalFunction &, const RationalFunction &);
  bool operator!=(const RationalFunction &, const RationalFunction &);
  RationalFunction operator+=
    (RationalFunction &, const RationalFunction &);
  RationalFunction operator-=
    (RationalFunction &, const RationalFunction &);
  RationalFunction operator*=
    (RationalFunction &, const RationalFunction &);
  RationalFunction operator/=
    (RationalFunction &, const RationalFunction &);
  RationalFunction operator+=
    (RationalFunction &, const int);

  class RationalFunction {
    friend std::ostream &operator<<(std::ostream &, const RationalFunction &);
    friend RationalFunction operator+
      (const RationalFunction &, const RationalFunction &);
    friend RationalFunction operator-
      (const RationalFunction &, const RationalFunction &);
    friend RationalFunction operator*
      (const RationalFunction &, const RationalFunction &);
    friend RationalFunction operator/
      (const RationalFunction &, const RationalFunction &);
    friend RationalFunction operator-
      (const RationalFunction &);
    friend RationalFunction operator+=
      (RationalFunction &, const RationalFunction &);
    friend RationalFunction operator-=
      (RationalFunction &, const RationalFunction &);
    friend RationalFunction operator*=
      (RationalFunction &, const RationalFunction &);
    friend RationalFunction operator/=
      (RationalFunction &, const RationalFunction &);
    friend RationalFunction operator+=(RationalFunction &, const int);
    friend RationalFunction operator-=(RationalFunction &, const int);
    friend RationalFunction operator*=(RationalFunction &, const int);
    friend RationalFunction operator/=(RationalFunction &, const int);
    friend bool operator==
      (const RationalFunction &, const RationalFunction &);
    friend bool operator!=
      (const RationalFunction &, const RationalFunction &);
    friend class Base;
    friend class CVC3Converter;
  public:
    typedef std::pair<Polynomial *, Polynomial *> PolyPair;
    typedef std::map<PolyPair, unsigned, RationalCmp> PolyPairMap;
    typedef PolyPairMap::iterator PolyPairIter;
    enum CleanupMethod {never, always, nocache};

    RationalFunction();
    RationalFunction(int, std::vector<unsigned>);
    RationalFunction(int);
    RationalFunction(const RationalFunction &);
    ~RationalFunction();
    RationalFunction &operator=(const RationalFunction &);
    inline PolyPairIter getIndex() const {
      return index;
    }
    static unsigned getNumSymbols();
    static void addSymbol(const std::string &);
    static void addNewSymbolsWhileRunning(const std::vector<std::string> &);
    static void start();
    static void removeUnusedSymbols();
    static void setCleanupMethod(CleanupMethod);
  private:
    PolyPairIter index;
  };

  inline bool operator==
    (const RationalFunction &r1, const RationalFunction &r2) {
    return r1.index == r2.index;
  }

  inline bool operator!=
    (const RationalFunction &r1, const RationalFunction &r2) {
    return r1.index != r2.index;
  }
}

namespace std {
  namespace tr1 {
    template<>
      inline size_t hash<Rational::RationalFunction>::operator()
      (Rational::RationalFunction r) const {
      Rational::RationalFunction::PolyPairIter index(r.getIndex());
      size_t indexUnsigned(reinterpret_cast<size_t>(&*index));
      return std::tr1::hash<size_t>()(indexUnsigned);
    }

    template<>
      inline size_t hash<std::pair<Rational::RationalFunction, Rational::RationalFunction> >::operator()
      (std::pair<Rational::RationalFunction, Rational::RationalFunction> r) const {
      return std::tr1::hash<Rational::RationalFunction>()(r.first)
        + std::tr1::hash<Rational::RationalFunction>()(r.second);
    }
  }
}

#endif
