/*
 * 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)
 */

#include "Util.h"
#include <iostream>
#include <sstream>

namespace prismparser {
  using namespace std;

  std::string intToString(int i) {
    stringstream str;
    
    str << i;
    
    return str.str();
  }
  
  std::string floatToString(double f) {
    stringstream str;
    
    str << f;
    
    return str.str();
  }

  template <class C>
  void Signature<C>::Disjunction
  (boolVector& arg1, const boolVector& arg2) {
    for (unsigned i=0; i<arg1.size(); ++i) {
      arg1[i] = arg1[i] || arg2[i];
    }
  }

  template <class C>
  bool Signature<C>::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;
  }

  template <class C>
  Signature<C>::Signature(unsigned size) : s(size, false) {
  }

  template <class C>
  Signature<C>::Signature(const Signature<C>& sig) {
    *this = sig;
  }
  
  template <class C>
  Signature<C>& Signature<C>::operator=(const Signature<C>& sig) {
    s = sig.s;
    cset = sig.cset;
    return *this;
  }

  template <class C>
  Signature<C>::Signature(const boolVector& __s) : s(__s) {
  }

  template <class C>  
  void Signature<C>::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);
    }
  }
  
  template <class C>
  void Signature<C>::insert(const C &c) {
    cset.insert(c);
  }

  template class Signature<unsigned int>;


  prismparser_error::~prismparser_error() throw() {
  }

  prismparser_error::prismparser_error(const std::string& s)
  : runtime_error(s), msg(s) {
  }

  std::ostream& prismparser_error::message(std::ostream& o) const {
    return o << msg << std::endl;
  }
  
  const std::string& prismparser_error::toString() const {
    return msg;
  }

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