// Buffer value class -*- c++ -*-

#include "snprintf.h"

#ifdef __GNUC__
# pragma implementation
#endif // __GNUC__
#include "BufferValue.h"
#include "BufferType.h"
#include "Constraint.h"

/** @file BufferValue.C
 * The contents of a queue or stack
 */

/* Copyright  1999-2002 Marko Mkel (msmakela@tcs.hut.fi).

   This file is part of MARIA, a reachability analyzer and model checker
   for high-level Petri nets.

   MARIA 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 2, or (at your option)
   any later version.

   MARIA 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.

   The GNU General Public License is often shipped with GNU software, and
   is generally kept in a file called COPYING or LICENSE.  If you do not
   have a copy of the license, write to the Free Software Foundation,
   59 Temple Place, Suite 330, Boston, MA 02111 USA. */

BufferValue::BufferValue (const class Type& type) :
  Value (type),
  myComponents (static_cast<const class BufferType&>(type).getSize ())
{
  assert (getType ().getKind () == Type::tBuffer);
}

BufferValue::BufferValue (const class BufferValue& old) :
  Value (old.getType ()),
  myComponents (old.myComponents)
{
  assert (getType ().getKind () == Type::tBuffer);
}

BufferValue::~BufferValue ()
{
}

bool
BufferValue::operator< (const class BufferValue& other) const
{
  assert (other.myComponents.getSize () == myComponents.getSize ());

  card_t size = getCapacity (), osize = other.getCapacity ();
  if (size < osize)
    return true;
  else if (osize < size)
    return false;

  while (size--)
    if (*myComponents[size] < *other.myComponents[size])
      return true;
    else if (*other.myComponents[size] < *myComponents[size])
      return false;

  return false;
}

bool
BufferValue::operator== (const class BufferValue& other) const
{
  assert (other.myComponents.getSize () == myComponents.getSize ());

  for (card_t i = 0; i < myComponents.getSize (); i++) {
    if (!myComponents[i])
      return !other.myComponents[i];
    if (!other.myComponents[i] ||
	!(*myComponents[i] == *other.myComponents[i]))
      return false;
  }

  return true;
}

card_t
BufferValue::operator- (const class BufferValue& other) const
{
  if (!getSize ())
    return 0;

  const class Type& itemType =
    static_cast<const class BufferType&>(getType ()).getItemType ();
  card_t numItemValues = itemType.getNumValues ();
  card_t offset = 0, i = 0;
  for (card_t mult = 1; i < getSize () && myComponents[i];
       mult *= numItemValues, i++)
    if (!other.myComponents[i])
      offset += mult;
  assert (i == getSize () || !other.myComponents[i]);

  card_t diff = 0;
  while (i--) {
    diff *= numItemValues;
    if (!other.myComponents[i])
      diff += itemType.convert (*myComponents[i]);
    else if (*other.myComponents[i] < *myComponents[i])
      diff += *myComponents[i] - *other.myComponents[i];
    else
      diff -= *other.myComponents[i] - *myComponents[i];
  }
  return diff + offset;
}

void
BufferValue::bottom ()
{
  assert (getSize () ==
	  static_cast<const class BufferType&>(getType ()).getSize ());

  if (const class Constraint* c = getType ().getConstraint ()) {
    const class Value& v = c->getFirstValue ();
    assert (&v.getType () == &getType () && v.getKind () == getKind ());
    const class BufferValue& bv = static_cast<const class BufferValue&>(v);

    for (card_t i = getSize (); i--; ) {
      delete myComponents[i];
      myComponents[i] = bv[i] ? bv[i]->copy () : NULL;
    }

    return;
  }

  for (card_t i = 0; i < getSize (); i++)
    delete myComponents[i], myComponents[i] = NULL;
}

void
BufferValue::top ()
{
  assert (getSize () ==
	  static_cast<const class BufferType&>(getType ()).getSize ());

  if (const class Constraint* c = getType ().getConstraint ()) {
    const class Value& v = c->getLastValue ();
    assert (&v.getType () == &getType () && v.getKind () == getKind ());
    const class BufferValue& bv = static_cast<const class BufferValue&>(v);

    for (card_t i = getSize (); i--; ) {
      delete myComponents[i];
      myComponents[i] = bv[i] ? bv[i]->copy () : NULL;
    }

    return;
  }

  for (card_t i = 0; i < getSize (); i++)
    delete myComponents[i], myComponents[i] =
      &static_cast<const class BufferType&>(getType ()).getItemType ()
      .getLastValue ();
}

bool
BufferValue::increment ()
{
  assert (getSize () ==
	  static_cast<const class BufferType&>(getType ()).getSize ());

  if (const class Constraint* c = getType ().getConstraint ()) {
    const class Value* v = &c->getNextHigh (*this);
    assert (&v->getType () == &getType () && v->getKind () == getKind ());
    if (*this == *static_cast<const class BufferValue*>(v)) {
      if (!(v = c->getNextLow (*this))) {
	bottom ();
	return false;
      }
      assert (&v->getType () == &getType () && v->getKind () == getKind ());
      const class BufferValue& bv = *static_cast<const class BufferValue*>(v);
      for (card_t i = getSize (); i--; ) {
	delete myComponents[i];
	myComponents[i] = bv[i] ? bv[i]->copy () : NULL;
      }
      return true;
    }
  }

  for (card_t i = 0; i < getSize (); i++) {
    if (!myComponents[i]) {
      myComponents[i] =
	&static_cast<const class BufferType&>(getType ()).getItemType ()
	.getFirstValue ();
      return true;
    }

    if (myComponents[i]->increment ())
      return true;
  }

  bottom ();
  return false;
}

bool
BufferValue::decrement ()
{
  assert (getSize () ==
	  static_cast<const class BufferType&>(getType ()).getSize ());

  if (const class Constraint* c = getType ().getConstraint ()) {
    const class Value* v = &c->getPrevLow (*this);
    assert (&v->getType () == &getType () && v->getKind () == getKind ());
    if (*this == *static_cast<const class BufferValue*>(v)) {
      if (!(v = c->getPrevHigh (*this))) {
	top ();
	return false;
      }
      assert (&v->getType () == &getType () && v->getKind () == getKind ());
      const class BufferValue& bv = *static_cast<const class BufferValue*>(v);
      for (card_t i = getSize (); i--; ) {
	delete myComponents[i];
	myComponents[i] = bv[i] ? bv[i]->copy () : NULL;
      }
      return true;
    }
  }

  card_t i;
  for (i = 0; i < getSize (); i++)
    if (!myComponents[i])
      break;
    else if (myComponents[i]->decrement ())
      return true;

  if (i--) {
    delete myComponents[i];
    myComponents[i] = NULL;
    return true;
  }
  else {
    top ();
    return false;
  }
}

class Value*
BufferValue::cast (const class Type& type)
{
  assert (getType ().isAssignable (type));
  if (&type == &getType () || type.getKind () != Type::tBuffer)
    return Value::cast (type);
  const class BufferType& bt = static_cast<const class BufferType&>(type);
  const class Type& itemType = bt.getItemType ();

  card_t i;
  for (i = 0; i < getSize () && (*this)[i]; i++);

  if (i > bt.getSize ()) {
    delete this;
    return NULL;
  }

  class BufferValue* value = new class BufferValue (type);
  for (i = 0; i < getSize () && (*this)[i]; i++)
    (*value)[i] = (*this)[i], (*this)[i] = NULL;
  delete this;

  while (i--) {
    if (!((*value)[i] = (*value)[i]->cast (itemType))) {
      delete value;
      return NULL;
    }
  }
  return value->cast (type);
}

#include "Printer.h"

void
BufferValue::display (const class Printer& printer) const
{
  printer.delimiter ('{')++;
  for (card_t i = 0; myComponents[i]; ) {
    myComponents[i]->display (printer);
    if (++i == getSize () || !myComponents[i])
      break;
    else
      printer.delimiter (',');
  }
  printer--.delimiter ('}');
}

#ifdef EXPR_COMPILE
# include "StringBuffer.h"
# include <stdio.h>

/** maximum length of a 64-bit index value, plus delimiters */
static const size_t ixlength = 25;

void
BufferValue::compile (class StringBuffer&) const
{
  assert (false);
}

void
BufferValue::compileInit (const char* name,
			  unsigned indent,
			  class StringBuffer& out) const
{
  /** length of the supplied name string */
  size_t length = strlen (name);
  /** an extended name */
  char* ixname = new char[length + ixlength];
  memcpy (ixname, name, length);

  out.indent (indent);
  out.append (name);
  out.append (".s=");
  out.append (getCapacity ());
  out.append (indent ? ";\n" : ", ");

  // initialized buffer items
  for (card_t i = 0; i < getSize () && myComponents[i]; ) {
    snprintf (ixname + length, ixlength, ".a[%u]", i);
    myComponents[i++]->compileInit (ixname, indent, out);
    if (i < getSize () && myComponents[i] && !indent) out.append (", ");
  }

  delete[] ixname;
}

bool
BufferValue::compileEqual (class StringBuffer& out,
			   unsigned indent,
			   const char* var,
			   bool equal,
			   bool first,
			   bool last) const
{
  /** length of the supplied name string */
  size_t length = strlen (var);
  /** an extended name */
  char* ixname = new char[length + ixlength];
  memcpy (ixname, var, length);
  /** length of the buffer value */
  card_t capacity = getCapacity ();

  if (!first)
    out.indent (indent);
  out.append (var);
  out.append (".s");
  out.append (equal ? "==" : "!=");
  out.append (capacity);
  if (capacity)
    out.append (equal ? "&&\n" : "||\n");

  // initialized buffer items
  for (card_t i = capacity; i--; ) {
    snprintf (ixname + length, ixlength, ".a[%u]", i);
    myComponents[i]->compileEqual (out, indent, ixname, equal, false, !i);
  }

  if (!last)
    out.append (equal ? "&&\n" : "||\n");

  delete[] ixname;
  return true;
}

unsigned
BufferValue::compileOrder (class StringBuffer& out,
			   unsigned indent,
			   const char* var,
			   bool less,
			   bool equal,
			   bool first,
			   bool last) const
{
  assert (!equal || last);
  /** length of the supplied name string */
  size_t length = strlen (var);
  /** an extended name */
  char* ixname = new char[length + ixlength];
  memcpy (ixname, var, length);
  /** length of the buffer value */
  card_t capacity = getCapacity ();

  if (!first)
    out.indent (indent);
  out.openParen (1);
  out.append (var);
  out.append (less ? ".s<" : ".s>");
  out.append (capacity);
  out.append ("||\n");
  out.indent (indent + 1);
  out.openParen (1);
  out.append (var);
  out.append (".s==");
  out.append (capacity);
  if (capacity)
    out.append ("&&\n");

  /** number of opened parentheses */
  unsigned opened = 2;

  // initialized buffer items
  for (card_t i = capacity; i--; ) {
    snprintf (ixname + length, ixlength, ".a[%u]", i);
    if (i) {
      opened += myComponents[i]->compileOrder (out, indent + opened, ixname,
					       less, false, false, false);
      myComponents[i]->compileEqual (out, indent + opened, ixname,
				     true, false, false);
    }
    else
      opened += myComponents[i]->compileOrder (out, indent + opened, ixname,
					       less, equal, false, true);
  }
  out.closeParen (opened);
  if (!last)
    out.append ("||\n");
  delete[] ixname;
  return 0;
}

#endif // EXPR_COMPILE