// Structure value class -*- c++ -*-

#include "snprintf.h"

#ifdef __GNUC__
# pragma implementation
#endif // __GNUC__
#include "StructValue.h"
#include "StructType.h"
#include "Constraint.h"

/** @file StructValue.C
 * Structure 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. */

StructValue::StructValue (const class Type& type) :
  Value (type),
  myComponents (static_cast<const class StructType&>(type).getSize ())
{
  assert (getType ().getKind () == Type::tStruct);
}

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

StructValue::~StructValue ()
{
}

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

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

  return false;
}

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

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

  return true;
}

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

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

    for (card_t i = getSize (); i--; ) {
      delete myComponents[i];
      myComponents[i] = sv[i].copy ();
    }
  }
  else
    for (card_t i = 0; i < getSize (); i++)
      myComponents[i]->bottom ();
}

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

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

    for (card_t i = getSize (); i--; ) {
      delete myComponents[i];
      myComponents[i] = sv[i].copy ();
    }
  }
  else
    for (card_t i = 0; i < getSize (); i++)
      myComponents[i]->top ();
}

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

  card_t i, numValues;

  for (i = numValues = 1; i < getSize (); i++)
    numValues *= myComponents[i - 1]->getType ().getNumValues ();

  card_t diff = 0;

  for (i = getSize (); --i;
       numValues /= myComponents[i - 1]->getType ().getNumValues ())
    if (*myComponents[i] < *other.myComponents[i])
      diff -= (*other.myComponents[i] - *myComponents[i]) * numValues;
    else
      diff += (*myComponents[i] - *other.myComponents[i]) * numValues;

  assert (numValues == 1);

  if (*myComponents[0] < *other.myComponents[0])
    diff -= *other.myComponents[0] - *myComponents[0];
  else
    diff += *myComponents[0] - *other.myComponents[0];

  return diff;
}

bool
StructValue::increment ()
{
  assert (getSize () ==
	  static_cast<const class StructType&>(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 StructValue*>(v)) {
      if (!(v = c->getNextLow (*this))) {
	bottom ();
	return false;
      }
      assert (&v->getType () == &getType () && v->getKind () == getKind ());
      const class StructValue& sv = *static_cast<const class StructValue*>(v);
      for (card_t i = getSize (); i--; ) {
	delete myComponents[i];
	myComponents[i] = sv[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
StructValue::decrement ()
{
  assert (getSize () ==
	  static_cast<const class StructType&>(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 StructValue*>(v)) {
      if (!(v = c->getPrevHigh (*this))) {
	top ();
	return false;
      }
      assert (&v->getType () == &getType () && v->getKind () == getKind ());
      const class StructValue& sv = *static_cast<const class StructValue*>(v);
      for (card_t i = getSize (); i--; ) {
	delete myComponents[i];
	myComponents[i] = sv[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*
StructValue::cast (const class Type& type)
{
  assert (getType ().isAssignable (type));
  if (type.getKind () != Type::tStruct)
    return Value::cast (type);
  const class StructType& st = static_cast<const class StructType&>(type);
  assert (getSize () == st.getSize ());

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

#include "Printer.h"

void
StructValue::display (const class Printer& printer) const
{
  if (getSize ()) {
    printer.delimiter ('{')++;
    for (card_t i = 0;;) {
      myComponents[i]->display (printer);
      if (++i == getSize ())
	break;
      else
	printer.delimiter (',');
    }
    printer--.delimiter ('}');
  }
  else
    printer.delimiter ('{').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 = 23;

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

void
StructValue::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, ".s%u", i);
    myComponents[i]->compileInit (ixname, indent, out);
    if (++i < getSize () && !indent) out.append (", ");
  }

  delete[] ixname;
}

bool
StructValue::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, ".s%u", i);
    if (myComponents[i]->compileEqual (out, indent, ixname, equal, first, !i))
      first = false;
  }

  delete[] ixname;

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

  return true;
}

unsigned
StructValue::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, ".s%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 (getSize ()) {
    if (!last)
      out.append ("||\n");
  }
  else if (last)
    out.append (equal ? "1" : "0");
  delete[] ixname;
  return 0;
}

#endif // EXPR_COMPILE