// Vector value class -*- c++ -*-

#include "snprintf.h"

#ifdef __GNUC__
# pragma implementation
#endif // __GNUC__
#include "VectorValue.h"
#include "VectorType.h"
#include "Constraint.h"

/** @file VectorValue.C
 * Array value
 */

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

VectorValue::VectorValue (const class Type& type) :
  Value (type),
  myComponents (static_cast<const class VectorType&>(type).getSize ())
{
  assert (getType ().getKind () == Type::tVector);
}

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

VectorValue::~VectorValue ()
{
}

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

  for (card_t i = myComponents.getSize (); i--; ) {
    assert (myComponents[i] && other.myComponents[i]);
    if (*myComponents[i] < *other.myComponents[i])
      return true;
    else if (*other.myComponents[i] < *myComponents[i])
      return false;
  }

  return false;
}

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

  for (card_t i = myComponents.getSize (); i--; ) {
    assert (myComponents[i] && other.myComponents[i]);
    if (!(*myComponents[i] == *other.myComponents[i]))
      return false;
  }

  return true;
}

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

  const class Type& itemType =
    static_cast<const class VectorType&>(getType ()).getItemType ();
  card_t numItemValues = itemType.getNumValues ();
  card_t diff = 0, i = getSize ();

  while (i--) {
    card_t d;
    if (myComponents[i] && other.myComponents[i])
      d = *myComponents[i] < *other.myComponents[i]
	? -(*other.myComponents[i] - *myComponents[i])
	: *myComponents[i] - *other.myComponents[i];
    else
      assert (false), d = 0;
    (diff *= numItemValues) += d;
  }

  return diff;
}

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

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

    for (card_t i = getSize (); i--; ) {
      delete myComponents[i];
      myComponents[i] = vv[i].copy ();
    }

    return;
  }

  for (card_t i = 0; i < getSize (); i++)
    myComponents[i]->bottom ();
}

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

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

    for (card_t i = getSize (); i--; ) {
      delete myComponents[i];
      myComponents[i] = vv[i].copy ();
    }

    return;
  }

  for (card_t i = getSize (); i--; ) {
    delete myComponents[i];
    myComponents[i] =
      &static_cast<const class VectorType&>(getType ()).getItemType ()
      .getLastValue ();
  }
}

bool
VectorValue::increment ()
{
  assert (getSize () ==
	  static_cast<const class VectorType&>(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 VectorValue*>(v)) {
      if (!(v = c->getNextLow (*this))) {
	bottom ();
	return false;
      }
      assert (&v->getType () == &getType () && v->getKind () == getKind ());
      const class VectorValue& vv = *static_cast<const class VectorValue*>(v);
      for (card_t i = getSize (); i--; ) {
	delete myComponents[i];
	myComponents[i] = vv[i].copy ();
      }
      return true;
    }
  }

  for (card_t i = 0; i < getSize (); i++)
    if (myComponents[i]->increment ())
      return true;

  if (getType ().getConstraint ())
    bottom ();

  return false;
}

bool
VectorValue::decrement ()
{
  assert (getSize () ==
	  static_cast<const class VectorType&>(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 VectorValue*>(v)) {
      if (!(v = c->getPrevHigh (*this))) {
	top ();
	return false;
      }
      assert (&v->getType () == &getType () && v->getKind () == getKind ());
      const class VectorValue& vv = *static_cast<const class VectorValue*>(v);
      for (card_t i = getSize (); i--; ) {
	delete myComponents[i];
	myComponents[i] = vv[i].copy ();
      }
      return true;
    }
  }

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

  if (getType ().getConstraint ())
    top ();

  return false;
}

class Value*
VectorValue::cast (const class Type& type)
{
  assert (getType ().isAssignable (type));
  if (type.getKind () != Type::tVector)
    return Value::cast (type);
  const class VectorType& vt = static_cast<const class VectorType&>(type);
  const class Type& itemType = vt.getItemType ();
  assert (getSize () == vt.getSize ());

  for (card_t i = getSize (); i--; ) {
    if ((*this)[i] && !((*this)[i] = (*this)[i]->cast (itemType))) {
      delete this;
      return NULL;
    }
  }
  return Value::cast (type);
}

#include "Printer.h"

void
VectorValue::display (const class Printer& printer) const
{
  printer.delimiter ('{')++;
  for (card_t i = 0;;) {
    if (myComponents[i])
      myComponents[i]->display (printer);
    if (++i == getSize ())
      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
VectorValue::compile (class StringBuffer&) const
{
  assert (false);
}

void
VectorValue::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);

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

  delete[] ixname;
}

bool
VectorValue::compileEqual (class StringBuffer& out,
			   unsigned indent,
			   const char* var,
			   bool equal,
			   bool first,
			   bool last) const
{
  if (!getSize ())
    return false;

  /** length of the supplied name string */
  size_t length = strlen (var);
  /** an extended name */
  char* ixname = new char[length + ixlength];
  memcpy (ixname, var, length);

  for (card_t i = getSize (); i--; ) {
    snprintf (ixname + length, ixlength, ".a[%u]", i);
    if (myComponents[i]->compileEqual (out, indent, ixname, equal, first, !i))
      first = false;
  }

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

  delete[] ixname;
  return true;
}

unsigned
VectorValue::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);
  /** number of opened parentheses */
  unsigned opened = 0;

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

#endif // EXPR_COMPILE