// Integer value class -*- c++ -*-

#ifdef __GNUC__
# pragma implementation
#endif // __GNUC__
#include "LeafValue.h"
#include "EnumType.h"
#include "IdType.h"
#include "Constraint.h"

/** @file LeafValue.C
 * Non-compound value (representable in a machine word)
 */

/* Copyright  1999-2001 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. */

/** Determine the smallest value of an unconstrained type
 * @param type	the data type
 * @return	the smallest value
 */
inline static card_t
bottomValue (const class Type& type)
{
  switch (type.getKind ()) {
  case Type::tInt:
    return card_t (INT_T_MIN);
  case Type::tEnum:
    return static_cast<const class EnumType&>(type).getFirstEnum ();
  default:
    return 0;
  }
}

/** Determine the largest value of an unconstrained type
 * @param type	the data type
 * @return	the largest value
 */
inline static card_t
topValue (const class Type& type)
{
  switch (type.getKind ()) {
  case Type::tInt:
    return INT_T_MAX;
  case Type::tCard:
    return CARD_T_MAX;
  case Type::tBool:
    return true;
  case Type::tChar:
    return CHAR_T_MAX;
  case Type::tEnum:
    return static_cast<const class EnumType&>(type).getLastEnum ();
  case Type::tId:
    return static_cast<const class IdType&>(type).getSize () - 1;
  case Type::tStruct:
  case Type::tVector:
  case Type::tUnion:
  case Type::tBuffer:
    break;
  }
  assert (false);
  return 0;
}

bool
LeafValue::operator< (const class LeafValue& other) const
{
  assert (getType ().getKind () == other.getType ().getKind ());
  if (getType ().getKind () == Type::tInt)
    return int_t (myValue) < int_t (other.myValue);
  return myValue < other.myValue;
}

card_t
LeafValue::operator- (const class LeafValue& other) const
{
  assert (!(*this < other));
  if (getType ().getKind () == Type::tInt)
    return int_t (myValue) - int_t (other.myValue);
  return myValue - other.myValue;
}

void
LeafValue::bottom ()
{
  if (const class Constraint* c = getType ().getConstraint ()) {
    const class Value& v = c->getFirstValue ();
    assert (&v.getType () == &getType () && v.getKind () == getKind ());
    myValue = static_cast<const class LeafValue&>(v).myValue;
  }
  else
    myValue = ::bottomValue (getType ());
}

void
LeafValue::top ()
{
  if (const class Constraint* c = getType ().getConstraint ()) {
    const class Value& v = c->getLastValue ();
    assert (&v.getType () == &getType () && v.getKind () == getKind ());
    myValue = static_cast<const class LeafValue&>(v).myValue;
  }
  else
    myValue = ::topValue (getType ());
}

bool
LeafValue::increment ()
{
  if (myValue == ::topValue (getType ())) {
    bottom ();
    return false;
  }

  if (const class Constraint* c = getType ().getConstraint ()) {
    const class Value* v = &c->getNextHigh (*this);
    assert (&v->getType () == &getType () && v->getKind () == getKind ());
    if (myValue == static_cast<const class LeafValue*>(v)->myValue) {
      if (!(v = c->getNextLow (*this))) {
	bottom ();
	return false;
      }
      assert (&v->getType () == &getType () && v->getKind () == getKind ());
      myValue = static_cast<const class LeafValue*>(v)->myValue;
      return true;
    }
  }

  myValue++;
  return true;
}

bool
LeafValue::decrement ()
{
  if (myValue == ::bottomValue (getType ())) {
    top ();
    return false;
  }

  if (const class Constraint* c = getType ().getConstraint ()) {
    const class Value* v = &c->getPrevLow (*this);
    assert (&v->getType () == &getType () && v->getKind () == getKind ());
    if (myValue == static_cast<const class LeafValue*>(v)->myValue) {
      if (!(v = c->getPrevHigh (*this))) {
	top ();
	return false;
      }
      assert (&v->getType () == &getType () && v->getKind () == getKind ());
      myValue = static_cast<const class LeafValue*>(v)->myValue;
      return true;
    }
  }

  myValue--;
  return true;
}

#include "Printer.h"

void
LeafValue::display (const class Printer& printer) const
{
  switch (getType ().getKind ()) {
  case Type::tInt:
    printer.print (int_t (myValue));
    break;
  case Type::tBool:
    printer.print (bool (myValue));
    break;
  case Type::tChar:
    printer.print (char_t (myValue));
    break;
  case Type::tEnum:
    if (const char* const comp =
	static_cast<const class EnumType&>(getType ()).getEnumName (myValue)) {
      printer.print (comp);
      break;
    }
  case Type::tId:
  case Type::tCard:
    printer.print (myValue);
    break;
  case Type::tStruct:
  case Type::tVector:
  case Type::tUnion:
  case Type::tBuffer:
    assert (false);
  }
}

#ifdef EXPR_COMPILE
# include "StringBuffer.h"

void
LeafValue::compile (class StringBuffer& out) const
{
  if (getType ().getKind () == Type::tInt) {
    if (int_t (myValue) == INT_T_MIN)
      out.append ("INT_MIN");
    else if (int_t (myValue) == INT_T_MAX)
      out.append ("INT_MAX");
    else
      out.append (int_t (myValue));
  }
  else if (myValue == CARD_T_MAX)
    out.append ("UINT_MAX");
  else
    out.append (myValue);
}

void
LeafValue::compileInit (const char* name,
			unsigned indent,
			class StringBuffer& out) const
{
  if (indent)
    out.indent (indent);
  out.append (name);
  out.append ("=");
  compile (out);
  if (indent)
    out.append (";\n");
}

bool
LeafValue::compileEqual (class StringBuffer& out,
			 unsigned indent,
			 const char* var,
			 bool equal,
			 bool first,
			 bool last) const
{
  if (!first)
    out.indent (indent);
  out.append (var);
  out.append (equal ? "==" : "!=");
  compile (out);
  if (!last)
    out.append (equal ? "&&\n" : "||\n");
  return true;
}

unsigned
LeafValue::compileOrder (class StringBuffer& out,
			 unsigned indent,
			 const char* var,
			 bool less,
			 bool equal,
			 bool first,
			 bool last) const
{
  assert (!equal || last);
  if (!first)
    out.indent (indent);
  if (!last)
    out.openParen (1);
  out.append (var);
  out.append (less
	      ? (equal ? "<=" : "<")
	      : (equal ? ">=" : ">"));
  compile (out);
  if (!last) {
    out.append ("||\n");
    return 1;
  }
  else
    return 0;
}

#endif // EXPR_COMPILE