Logo Search packages:      
Sourcecode: maria version File versions

IfThenElse.C

Go to the documentation of this file.
// Maria if-then-else expression class -*- c++ -*-

#ifdef __GNUC__
# pragma implementation
#endif // __GNUC__
#include "IfThenElse.h"
#include "Type.h"
#include "Printer.h"

/** @file IfThenElse.C
 * Selection expression
 */

/* Copyright © 1998-2002 Marko Mäkelä (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. */

00034 IfThenElse::IfThenElse (class Expression& condition,
                  class ExpressionList& exprList) :
  Expression (),
  myCondition (&condition), myExprList (&exprList)
{
  assert (myCondition->getType ()->getNumValues () == exprList.size ());
  setType (*myExprList->getType ());
}

00043 IfThenElse::~IfThenElse ()
{
  myCondition->destroy ();
  myExprList->destroy ();
}

bool
00050 IfThenElse::isBasic () const
{
  return
    myCondition->isBasic () &&
    myExprList->isBasic ();
}

bool
00058 IfThenElse::isTemporal () const
{
  return
    myCondition->isTemporal () ||
    myExprList->isTemporal ();
}

bool
00066 IfThenElse::isSet () const
{
  return myExprList->isSet ();
}

void
00072 IfThenElse::setType (const class Type& type)
{
  Expression::setType (type);
  assert (myExprList->getType () == &type);
}

class Value*
00079 IfThenElse::do_eval (const class Valuation& valuation) const
{
  if (class Value* cond = myCondition->eval (valuation)) {
    const card_t i = myCondition->getType ()->convert (*cond);
    delete cond;
    return (*myExprList)[i].eval (valuation);
  }
  else
    return NULL;
}

class PlaceMarking*
00091 IfThenElse::meval (const class Valuation& valuation) const
{
  if (class Value* cond = myCondition->eval (valuation)) {
    const card_t i = myCondition->getType ()->convert (*cond);
    delete cond;
    return (*myExprList)[i].meval (valuation);
  }
  else
    return NULL;
}

class Expression*
00103 IfThenElse::ground (const class Valuation& valuation,
                class Transition* transition,
                bool declare)
{
  class Expression* expr = NULL;
  if (class Value* cond = myCondition->eval (valuation)) {
    const card_t i = myCondition->getType ()->convert (*cond);
    delete cond;
    if (!(expr = (*myExprList)[i].ground (valuation, transition, declare)))
      return NULL;
  }
  else {
    assert (!valuation.isOK ());
    valuation.clearErrors ();
    class Expression* condition =
      myCondition->ground (valuation, transition, declare);
    if (!condition) return NULL;
    class ExpressionList* exprList =
      myExprList->ground (valuation, transition, declare);
    if (!exprList) { condition->destroy (); return NULL; }

    if (condition == myCondition && exprList == myExprList) {
      condition->destroy ();
      exprList->destroy ();

      return copy ();
    }
    else
      expr = (new class IfThenElse (*condition, *exprList))->cse ();
  }

  return expr->ground (valuation);
}

class Expression*
00138 IfThenElse::substitute (class Substitution& substitution)
{
  class Expression* condition = myCondition->substitute (substitution);
  class ExpressionList* exprList = myExprList->substitute (substitution);

  if (condition == myCondition && exprList == myExprList) {
    condition->destroy ();
    exprList->destroy ();

    return copy ();
  }
  else
    return (new class IfThenElse (*condition, *exprList))->cse ();
}

bool
00154 IfThenElse::depends (const class VariableSet& vars,
                 bool complement) const
{
  return
    myCondition->depends (vars, complement) ||
    myExprList->depends (vars, complement);
}

bool
00163 IfThenElse::forVariables (bool (*operation)
                    (const class Expression&,void*),
                    void* data) const
{
  return
    myCondition->forVariables (operation, data) &&
    myExprList->forVariables (operation, data);
}

#ifdef EXPR_COMPILE
# include "CExpression.h"

void
IfThenElse::compile (class CExpression& cexpr,
                 unsigned indent,
                 const char* lvalue,
                 const class VariableSet* vars) const
{
  class StringBuffer& out = cexpr.getOut ();
  char* cond;
  if (cexpr.getVariable (*myCondition, cond))
    myCondition->compile (cexpr, indent, cond, vars);
  char* condconv = 0;
  if (!getType ()->isLeaf () &&
      cexpr.getConverted (*myCondition, condconv))
    myCondition->getType ()->compileConversion (out, indent,
                                    cond, condconv, false);
  bool* checkpoint;
  unsigned checkpointSize = cexpr.getCheckpoint (checkpoint);
  out.indent (indent);
  out.append ("switch (");
  if (getType ()->isLeaf ())
    out.append (cond);
  else
    out.append (condconv);
  out.append (") {\n");
  for (card_t i = 0; i < myExprList->size (); i++) {
    out.indent (indent);
    out.append ("case ");
    if (getType ()->isLeaf ()) {
      class Value* v = myCondition->getType ()->convert (i);
      v->compile (out);
      delete v;
    }
    else
      out.append (i);
    out.append (":\n");
    (*myExprList)[i].compile (cexpr, indent + 2, lvalue, vars);
    cexpr.setCheckpoint (indent + 2, checkpoint, checkpointSize);
    out.indent (indent + 2);
    out.append ("break;\n");
  }
  out.indent (indent);
  out.append ("}\n");
  delete[] checkpoint;
  delete[] cond;
  delete[] condconv;
}

void
IfThenElse::compileMset (class CExpression& cexpr,
                   unsigned indent,
                   const char* resulttype,
                   const char* result,
                   const class VariableSet* vars) const
{
  class StringBuffer& out = cexpr.getOut ();
  char* cond;
  if (cexpr.getVariable (*myCondition, cond))
    myCondition->compile (cexpr, indent, cond, vars);
  char* condconv = 0;
  if (!getType ()->isLeaf () &&
      cexpr.getConverted (*myCondition, condconv))
    myCondition->getType ()->compileConversion (out, indent,
                                    cond, condconv, false);
  bool* checkpoint;
  unsigned checkpointSize = cexpr.getCheckpoint (checkpoint);
  out.indent (indent);
  out.append ("switch (");
  if (getType ()->isLeaf ())
    out.append (cond);
  else
    out.append (condconv);
  out.append (") {\n");
  for (card_t i = 0; i < myExprList->size (); i++) {
    out.indent (indent);
    out.append ("case ");
    if (getType ()->isLeaf ()) {
      class Value* v = myCondition->getType ()->convert (i);
      v->compile (out);
      delete v;
    }
    else
      out.append (i);
    out.append (":\n");
    (*myExprList)[i].compileMset (cexpr, indent + 2, resulttype, result, vars);
    cexpr.setCheckpoint (indent + 2, checkpoint, checkpointSize);
    out.indent (indent + 2);
    out.append ("break;\n");
  }
  out.indent (indent);
  out.append ("}\n");
  delete[] checkpoint;
  delete[] cond;
  delete[] condconv;
}

#endif // EXPR_COMPILE

void
00273 IfThenElse::display (const class Printer& printer) const
{
  myCondition->display (printer);
  printer.delimiter ('?');
  for (card_t i = myExprList->size (); i--; ) {
    const class Expression& expr = (*myExprList)[i];
    switch (expr.getKind ()) {
    case Expression::eVariable:
    case Expression::eUndefined:
    case Expression::eStructComponent:
    case Expression::eStructAssign:
    case Expression::eUnionComponent:
    case Expression::eUnionType:
    case Expression::eVectorIndex:
    case Expression::eVectorAssign:
    case Expression::eVectorShift:
    case Expression::eUnop:
    case Expression::eBinop:
    case Expression::eBooleanBinop:
    case Expression::eNot:
    case Expression::eRelop:
    case Expression::eBufferUnop:
    case Expression::eBufferRemove:
    case Expression::eBufferWrite:
    case Expression::eBufferIndex:
    case Expression::eSet:
    case Expression::eTemporalBinop:
    case Expression::eTemporalUnop:
    case Expression::eTypecast:
    case Expression::eCardinality:
    case Expression::eTransitionQualifier:
    case Expression::ePlaceContents:
    case Expression::eSubmarking:
    case Expression::eMapping:
    case Expression::eEmptySet:
      break;
    case Expression::eIfThenElse:
    case Expression::eMarking:
      printer.delimiter ('(')++;
      expr.display (printer);
      --printer.delimiter (')');
      if (i) printer.delimiter (':');
      continue;
    case Expression::eConstant:
    case Expression::eStruct:
    case Expression::eUnion:
    case Expression::eVector:
    case Expression::eBuffer:
      if (const char* name = expr.getType ()->getName ()) {
      printer.printRaw ("is");
      printer.delimiter (' ');
      printer.print (name);
      printer.delimiter (' ');
      }
      else {
      switch (expr.getType ()->getKind ()) {
      case Type::tInt:
      case Type::tCard:
        printer.printRaw ("is");
        printer.delimiter (' ');
        printer.print (expr.getType ()->getSyntacticName ());
        printer.delimiter (' ');
        break;
      default:
        break;
      }
      }
      break;
    }
    expr.display (printer);
    if (i)
      printer.delimiter (':');
  }
}

Generated by  Doxygen 1.6.0   Back to index