/*
 * 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& arg1, const boolVector& arg2) {
	for(unsigned i=0; i<arg1.size(); ++i) {
	  arg1[i] = arg1[i] || arg2[i];
	}
      }
      static bool Implies(const boolVector& arg1, const boolVector& arg2) {
	bool result (true);
	for(unsigned i=0; result && i<arg1.size(); ++i) {
	  result = result && (!arg1[i] || arg2[i]);
	}
	return result;
      }


    Signature(unsigned size) : s(size, false) { }
      Signature(const Signature<C>& sig) { *this = sig; }
      Signature<C>& operator=(const Signature<C>& sig) { s = sig.s; cset = sig.cset; return *this;}

    Signature(const boolVector& __s) : s(__s) {}

      static void partitionRefinement2(std::vector<Signature<C> >& partition,
				       std::vector<Signature<C> >& new_partition ) {
	if(partition.size()==0) return;

	typedef std::list<boolVector*> List;

	List characteristic;

	unsigned N = partition[0].s.size();

	BOOST_FOREACH(Signature<C>& sig, partition) {
	  assert(sig.s.size() == N);
	  characteristic.push_back(&sig.s);
	}


	for(unsigned i = 0; i<N; ++i) {
	  List::iterator first (characteristic.end());
	  for(List::iterator it = characteristic.begin() ; it!=characteristic.end() ; ) {
	    assert((*it)->size() == N);
	    if((**it)[i]) {
	      if(first == characteristic.end() ) {
		first = it;
		++it;
	      } else {
		List::iterator dit = it;
		boolVector v(**first);
		Disjunction(**first,**dit);
		++it;
		characteristic.erase(dit);
	      }
	    } else {
	      ++it;
	    }
	  }

	}
	new_partition.resize(characteristic.size(),N);

	unsigned i=0;
	BOOST_FOREACH(boolVector* vec, characteristic) {
	  new_partition[i].s = *vec;
	  new_partition[i].cset.clear();
	  ++i;
	}

	BOOST_FOREACH(const Signature<C>& sig1, partition) {
	  assert(sig1.cset.size()== 1);
	  bool result = false;
	  BOOST_FOREACH(Signature<C>& sig2, new_partition) {
	    assert(sig1.s.size() == N);
	    assert(sig2.s.size() == N);
	    if(Implies(sig1.s,sig2.s)) {
	      sig2.cset.insert(sig1.cset.begin(),sig1.cset.end());
	      result = true;
	      break;
	    }
	  }
	  assert(result);
	}
      }
      inline void insert(const C& c) { cset.insert(c); }
    };

  class Error : public std::runtime_error {
  public:
    ~Error() throw() {
    }
    explicit Error(const std::string& s) : runtime_error(s), msg(s)  {
    }
    inline std::ostream& message(std::ostream& o) const {
      return o << msg << std::endl;
    }
    const std::string& toString() const {
      return msg;
    }
  private:
    const std::string msg;
  };

inline std::ostream& operator<<(std::ostream &o, const class Error& e) { return e.message( o ); }

/*! \class ParseError parse error
    \ingroup util
*/
struct ParseError : public Error {
    ParseError( const std::string& s ) : Error( "parse error: " + s) {}
};

/*! \class InternalError internal error
    \ingroup util
*/
struct InternalError: public Error {
    InternalError( const std::string& s ) : Error( "internal error: " + s ) {}
};

/*! \class RuntimeError runtime error
    \ingroup util
*/
struct RuntimeError: public Error {
   RuntimeError( const std::string& s ) : Error(s) {}
   RuntimeError() : Error( "runtime error: ") {}
};

/*! \class TypeError failed type check
    \ingroup util
*/
struct TypeError : public Error {
  TypeError( const std::string& s ) : Error(s ) {}
  TypeError() : Error("type error: ") {}
};

}

#endif
