// Marking cardinality/multiplicity expression class -*- c++ -*-

#ifdef __GNUC__
# pragma implementation
#endif // __GNUC__
#include "CardinalityExpression.h"
#include "PlaceMarking.h"
#include "Net.h"
#include "CardType.h"
#include "LeafValue.h"
#include "Valuation.h"
#include "Printer.h"

/** @file CardinalityExpression.C
 * Aggregate operations on multi-sets
 */

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

CardinalityExpression::CardinalityExpression (enum Op op,
					      class Expression& expr) :
  Expression (),
  myOp (op), myExpr (&expr)
{
  assert (myExpr && !myExpr->isTemporal ());
  setType (Net::getCardType ());
}

CardinalityExpression::~CardinalityExpression ()
{
  myExpr->destroy ();
}

class Value*
CardinalityExpression::do_eval (const class Valuation& valuation) const
{
  if (class PlaceMarking* p = myExpr->meval (valuation)) {
    card_t count = myOp == cMin ? CARD_T_MAX : 0;
    for (PlaceMarking::const_iterator i = p->begin (); i != p->end (); i++) {
      card_t add = PlaceMarking::getCount (i);
      switch (myOp) {
      case cCard:
	if (CARD_T_MAX - count < add) {
	  valuation.flag (errOver, *this);
	  delete p;
	  return NULL;
	}
	else
	  count += add;
	break;
      case cMin:
	if (count > add) count = add;
	break;
      case cMax:
	if (count < add) count = add;
	break;
      }
    }
    delete p;
    return constrain (valuation, new class LeafValue (*getType (), count));
  }
  return NULL;
}

class Expression*
CardinalityExpression::ground (const class Valuation& valuation,
			       class Transition* transition,
			       bool declare)
{
  class Expression* e = myExpr->ground (valuation, transition, declare);
  if (!e)
    return NULL;

  assert (valuation.isOK ());

  if (e == myExpr) {
    e->destroy ();
    return copy ();
  }
  else
    return static_cast<class Expression*>
      (new class CardinalityExpression (myOp, *e))->ground (valuation);
}

class Expression*
CardinalityExpression::substitute (class Substitution& substitution)
{
  class Expression* e = myExpr->substitute (substitution);
  if (!e)
    return NULL;
  if (e == myExpr) {
    e->destroy ();
    return copy ();
  }
  else
    return (new class CardinalityExpression (myOp, *e))->cse ();
}

bool
CardinalityExpression::depends (const class VariableSet& vars,
				bool complement) const
{
  return myExpr->depends (vars, complement);
}

bool
CardinalityExpression::forExpressions (bool (*operation)
				       (const class Expression&,void*),
				       void* data) const
{
  return
    (*operation) (*this, data) &&
    myExpr->forExpressions (operation, data);
}

#ifdef EXPR_COMPILE
# include "CExpression.h"
# include "PlaceContents.h"
# include "Place.h"

void
CardinalityExpression::compile (class CExpression& cexpr,
				unsigned indent,
				const char* lvalue,
				const class VariableSet* vars) const
{
  class StringBuffer& out = cexpr.getOut ();

  if (myExpr->getKind () == Expression::ePlaceContents) {
    const class PlaceContents& p =
      *static_cast<const class PlaceContents*>(myExpr);
    if (!p.getPlace ().getCapacityBits ()) {
      out.indent (indent);
      out.append (lvalue);
      out.append ("=");
      out.append (p.getPlace ().getMaxNumTokens ());
      out.append (";\n");
      return;
    }
    if (p.getPlace ().getMaxNumTokens () == 1) {
      out.indent (indent);
      out.append (lvalue);
      out.append ("=");
      out.append (cexpr.getMultiset ());
      out.append (".p");
      out.append (p.getPlace ().getIndex ());
      out.append (myOp == cMin ? "?1:UINT_MAX" : "?1:0;\n");
      return;
    }
  }
  char* expr;
  if (cexpr.getVariable (*myExpr, expr))
    myExpr->compileMset (cexpr, indent, 0, expr, vars);

  char* iter = cexpr.getLabel ();
  out.indent (indent);
  out.append ("{\n");
  out.indent (indent + 2);
  out.append ("register const ");
  myExpr->getType ()->appendMSetName (out);
  out.append ("* ");
  out.append (iter);
  out.append (" = ");
  out.append (expr);
  out.append (";\n");
  out.indent (indent + 2);
  out.append ("FIRST (");
  out.append (iter);
  out.append (");\n");
  out.indent (indent + 2);
  out.append ("for (");
  out.append (lvalue);
  out.append (myOp == cMin ? "=UINT_MAX; " : "=0; ");
  out.append (iter);
  out.append ("; ) {\n");
  switch (myOp) {
  case cCard:
    out.indent (indent + 4);
    out.append ("if ("), out.append (lvalue), out.append (">UINT_MAX-");
    out.append (iter), out.append ("->count)\n");
    cexpr.compileError (indent + 6, errOver);
    out.indent (indent + 4);
    out.append (lvalue);
    out.append ("+=");
    out.append (iter);
    out.append ("->count;\n");
    break;
  case cMin:
  case cMax:
    out.indent (indent + 4);
    out.append ("if ("), out.append (lvalue);
    out.append (myOp == cMin ? ">" : "<");
    out.append (iter), out.append ("->count) ");
    out.append (lvalue), out.append ("=");
    out.append (iter), out.append ("->count;\n");
    break;
  }
  out.indent (indent + 4);
  out.append ("NEXT (");
  out.append (iter);
  out.append (");\n");
  out.indent (indent + 2);
  out.append ("}\n");
  out.indent (indent);
  out.append ("}\n");
  delete[] iter;
  delete[] expr;
  compileConstraint (cexpr, indent, lvalue);
}

#endif // EXPR_COMPILE

void
CardinalityExpression::display (const class Printer& printer) const
{
  switch (myOp) {
  case cCard:
    printer.printRaw ("cardinality");
    break;
  case cMin:
    printer.printRaw ("min");
    break;
  case cMax:
    printer.printRaw ("max");
    break;
  }
  printer.delimiter (' ');

  if (myExpr->getKind () == Expression::eMarking) {
    printer.delimiter ('(')++;
    myExpr->display (printer);
    --printer.delimiter (')');
  }
  else
    myExpr->display (printer);
}