Logo Search packages:      
Sourcecode: maria version File versions

Constraint.C

Go to the documentation of this file.
// Type constraint class -*- c++ -*-

#ifdef __GNUC__
# pragma implementation
#endif // __GNUC__
#include "Constraint.h"
#include "Range.h"
#include "Value.h"
#include "Type.h"
#include "Printer.h"

/** @file Constraint.C
 * Constraint that limits the domain of a data type
 */

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

00036 Constraint::Constraint () :
  myList ()
{
}

00041 Constraint::Constraint (const class Constraint& old, const class Type& type) :
  myList ()
{
  assert (!type.getConstraint () || this == type.getConstraint ());

  for (const_iterator i = old.begin (); i != old.end (); i++) {
    class Range* range = new class Range (**i);
    myList.push_back (range);
    range->setType (type);
  }
}

00053 Constraint::~Constraint ()
{
  for (iterator i = begin (); i != end (); i++)
    delete *i;
}

void
00060 Constraint::setType (const class Type& type)
{
  for (iterator i = begin (); i != end (); i++)
    (*i)->setType (type);
}

const class Value&
00067 Constraint::getFirstValue () const
{
  assert (!empty ());
  return (*begin ())->getLow ();
}

const class Value&
00074 Constraint::getLastValue () const
{
  assert (!empty ());
  return (*--end ())->getHigh ();
}

const class Value&
00081 Constraint::getNextHigh (const class Value& value) const
{
  const_iterator i;
  for (i = begin (); assert (i != end ()), !(*i)->check (value); i++);
  return (*i)->getHigh ();
}

const class Value*
00089 Constraint::getNextLow (const class Value& value) const
{
  const_iterator i;
  for (i = begin (); assert (i != end ()), !((*i)->getHigh () == value); i++);
  return ++i == end () ? 0 : &(*i)->getLow ();
}

const class Value&
00097 Constraint::getPrevLow (const class Value& value) const
{
  const_iterator i;
  for (i = begin (); assert (i != end ()), !(*i)->check (value); i++);
  return (*i)->getLow ();
}

const class Value*
00105 Constraint::getPrevHigh (const class Value& value) const
{
  const_iterator i = begin (), j = end ();
  for (; assert (i != end ()), !((*i)->getLow () == value); j = i++);
  return j == end () ? 0 : &(*j)->getHigh ();
}

void
00113 Constraint::append (class Range& r)
{
  class Range* range = &r;
  iterator i;
  for (i = begin (); i != end (); ) {
    if (class Range* rn = (*i)->combine (*range)) {
      delete *i; delete range;
      range = rn;

      if (i == begin ()) {
      myList.erase (i);
      if ((i = begin ()) == end ())
        break;
      else
        continue;
      }
      else {
      iterator j = i;
      j--; myList.erase (i);
      i = j;
      }
    }
    else if (!((*i)->getHigh () < range->getHigh ()))
      break;

    i++;
  }

  myList.insert (i, range);
}

void
00145 Constraint::restrict (const class Constraint& constraint,
                  const class Type& type)
{
  assert (!type.getConstraint () || this == type.getConstraint ());
  assert (!isDisjoint (constraint) || !constraint.isDisjoint (*this));
  List l = myList;
  myList.clear ();

  for (iterator j = l.begin (); j != l.end (); j++) {
    for (const_iterator k = constraint.begin ();
       k != constraint.end (); k++) {
      if (class Range* range = (*j)->cut (**k)) {
      range->setType (type);
      myList.push_back (range);
      }
    }

    delete *j;
  }
}

bool
00167 Constraint::isSuperset (const class Constraint& other) const
{
  // This is an ugly O(n^2) algorithm,
  // but it's only used during static analysis.

  // The algorithm does not consider (1..3,4,5) to be a superset of (2..4).
  // Neighbouring ranges will have been combined by Constraint::append ().
  for (const_iterator i = other.begin (); i != other.end (); i++) {
    const class Value& low = (*i)->getLow ();
    const class Value& high = (*i)->getHigh ();

    for (const_iterator j = begin (); j != end (); j++)
      if (!(low < (*j)->getLow ()) && !((*j)->getHigh () < high))
      goto match;
    return false;
  match:
    continue;
  }

  return true;
}

bool
00190 Constraint::isDisjoint (const class Constraint& other) const
{
  // This is an ugly O(n^2) algorithm,
  // but it's only used during static analysis.
  for (const_iterator i = other.begin (); i != other.end (); i++) {
    const class Value& low = (*i)->getLow ();
    const class Value& high = (*i)->getHigh ();

    for (const_iterator j = begin (); j != end (); j++)
      if ((*j)->check (low) || (*j)->check (high))
      return false;
  }

  return true;
}

bool
00207 Constraint::isConstrained (const class Value& value) const
{
  for (const_iterator i = begin (); i != end (); i++)
    if ((*i)->check (value))
      return true;
  return false;
}

card_t
00216 Constraint::getNumValues () const
{
  card_t numValues = 0;
  for (const_iterator i = begin (); i != end (); i++) {
    const class Range* r = *i;
    card_t num = r->getHigh () - r->getLow ();

    if (num != CARD_T_MAX && ++num < CARD_T_MAX - numValues)
      numValues += num;
    else
      return CARD_T_MAX;
  }
  return numValues;
}

#ifdef EXPR_COMPILE
# include "CExpression.h"
void
Constraint::compileCheck (class CExpression& cexpr,
                    unsigned indent,
                    const char* value) const
{
  class StringBuffer& out = cexpr.getOut ();
  out.indent (indent);
  out.append ("if (!(");
  /** flag: is this the first generated line? */
  bool first = true;
  for (Constraint::const_iterator i = begin ();; ) {
    const class Range* range = *i++;
    const class Value& low = range->getLow ();
    const class Value& high = range->getHigh ();

    if (&low != &high) {
      if (!first)
      out.indent (indent + 6);
      out.append ("(");
      if (low.compileOrder (out, indent + 7, value,
                      false, true, true, true))
      assert (false);
      out.append ("&&\n");
      if (high.compileOrder (out, indent + 7, value,
                       true, true, false, true))
      assert (false);
      out.append (")");
    }
    else if (!low.compileEqual (out, indent + 6, value, true, first, true))
      continue;

    first = false;
    if (i != end ())
      out.append ("||\n");
    else
      break;
  }
  if (first)
    out.append ("1");
  out.append ("))\n");
  cexpr.compileError (indent + 2, errConst);
}

void
Constraint::compileConversion (class StringBuffer& out,
                         unsigned indent,
                         const class Type& type,
                         const char* value,
                         const char* number,
                         bool add,
                         const char* work) const
{
  bool next = false;

  for (Constraint::const_iterator i = end ();; next = true) {
    const class Range* range = *--i;
    const class Value& low = range->getLow ();
    const class Value& high = range->getHigh ();
    const bool notfirst = i != begin ();

    if (notfirst) {
      out.indent (indent);
      if (next)
      out.append ("else ");
      out.append ("if (");
      if (&low == &high)
      low.compileEqual (out, next ? indent + 9 : indent + 4,
                    value, true, true, true);
      else
      low.compileOrder (out, next ? indent + 9 : indent + 4,
                    value, false, true, true, true);
      out.append (")\n");
      indent += 2;
    }
    else if (next)
      out.indent (indent), out.append ("else\n"), indent += 2;

    out.indent (indent);
    if (&low == &high) {
      card_t num = type.convert (low);
      if (num || !add)
      out.append (number), out.append (add ? "+=" : "="), out.append (num);
      out.append (";\n");
    }
    else if (!work) {
      out.append (number), out.append (add ? "+=" : "=");
      out.append ("(card_t) ("), out.append (value);
      out.append (" - ");
      low.compile (out);
      out.append (")");
      if (card_t num = type.convert (low))
      out.append ("+"), out.append (num);
      out.append (";\n");
    }
    else {
      out.append ("for (");
      if (notfirst) {
      out.append (number), out.append (add ? "+=" : "=");
      out.append (type.convert (low));
      out.append (", ");
      }
      else if (!add)
      out.append (number), out.append ("=0, ");

      out.append (work);
      out.append ("="), out.append (value);
      out.append (";\n");
      low.compileEqual (out, indent + 5, work, false, false, true);
      out.append (";\n");
      out.indent (indent + 5), out.append (number), out.append ("++) {\n");
      type.do_compilePredecessor (out, indent + 2, work, work, NULL);
      out.indent (indent), out.append ("}\n");
    }

    if (notfirst || next)
      indent -= 2;
    if (!notfirst)
      break;
  }
}

void
Constraint::compileReverseConversion (class StringBuffer& out,
                              unsigned indent,
                              const class Type& type,
                              const char* number,
                              const char* value,
                              bool leaf) const
{
  bool next = false;
  for (Constraint::const_iterator i = end (); i != begin (); next = true) {
    const class Range* range = *--i;
    const class Value& low = range->getLow ();
    const class Value& high = range->getHigh ();
    card_t num = type.convert (low);
    if (num) {
      out.indent (indent);
      if (next)
      out.append ("else ");
      out.append ("if ("), out.append (number);
      out.append (&low == &high ? "==" : ">="), out.append (num);
      out.append (")");
    }
    else if (next)
      out.indent (indent), out.append ("else");
    if (num || next)
      out.append (" {\n"), indent += 2;

    low.compileInit (value, indent, out);

    if (&low != &high) {
      if (leaf) {
      out.indent (indent);
      out.append (value);
      out.append ("+=");
      out.append (number);
      if (num)
        out.append ("-"), out.append (num);
      out.append (";\n");
      }
      else {
      out.indent (indent), out.append ("for (");
      if (num)
        out.append (number), out.append ("-="), out.append (num);
      out.append ("; "), out.append (number), out.append ("--; ) {\n");
      type.do_compileSuccessor (out, indent + 2, value, value, 0);
      out.indent (indent), out.append ("}\n");
      }
    }

    if (num || next)
      out.indent (indent -= 2), out.append ("}\n");
  }
}
#endif // EXPR_COMPILE

void
00410 Constraint::display (const class Printer& printer) const
{
  printer.delimiter ('(')++;
  for (const_iterator i = begin ();;) {
    (*i)->display (printer);
    if (++i == end ())
      break;
    printer.delimiter (',');
  }
  --printer.delimiter (')');
}

Generated by  Doxygen 1.6.0   Back to index