/*
 * This file is part of a parser for an extension of the PRISM language.
 *
 * This 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.
 *
 * The parser 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 the program this parser part of.
 * If not, see <http://www.gnu.org/licenses/>.
 *
 * Copyright 2007-2010 Bjoern Wachter (Bjoern.Wachter@comlab.ox.ac.uk)
 * Copyright 2009-2010 Ernst Moritz Hahn (emh@cs.uni-sb.de)
 */

#ifndef __UTIL_H__
#define __UTIL_H__

#include <cmath>
#include <algorithm>
#include <iostream>
#include <fstream>
#include <cstdio>
#include <cassert>
#include <string>
#include <list>
#include <set>
#include <map>
#include <vector>
#include <stack>
#include <typeinfo>
#include <valarray>
#include <stdexcept>

#include <boost/shared_ptr.hpp>
#include <boost/foreach.hpp>

#include <tr1/unordered_map>
#include <tr1/unordered_set>


/*! \typedef true, false and don't care */
typedef enum { l_false=-1, l_undef, l_true } lbool;

typedef std::vector<lbool> Cube;

namespace prismparser {
  std::string intToString(int i);
  std::string floatToString(double f);
  template <class C>
    struct Signature {
      typedef std::vector<bool> boolVector;
      boolVector s;
      typedef std::set<C> CSet;
      CSet cset;

      static void Disjunction(boolVector &, const boolVector &);
      static bool Implies(const boolVector &, const boolVector &);
      Signature(unsigned);
      Signature(const Signature<C> &);
      Signature<C>& operator=(const Signature<C> &);
      Signature(const boolVector &);

      static void partitionRefinement2(std::vector<Signature<C> >&,
				       std::vector<Signature<C> >&);
      void insert(const C &);
    };

  class prismparser_error : public std::runtime_error {
  public:
    ~prismparser_error() throw();
    explicit prismparser_error(const std::string& s);
    std::ostream& message(std::ostream &) const;
    const std::string& toString() const;
  private:
    const std::string msg;
  };

  std::ostream& operator<<(std::ostream &, const class Error& e);
}

#endif
