---

semantics.h

Go to the documentation of this file.

// Semantics implementation -*- C++ -*-

// Copyright (C) 2001-2003 Hermann Schichl
//
// This file is part of the COCONUT API.  This library
// is free software; you can redistribute it and/or modify it under the
// terms of the Library GNU General Public License as published by the
// Free Software Foundation; either version 2, or (at your option)
// any later version.

// This library 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
// Library GNU General Public License for more details.

// As a special exception, you may use this file as part of a free software
// library without restriction.  Specifically, if other files instantiate
// templates or use macros or inline functions from this file, or you compile
// this file and link it with other files to produce an executable, this
// file does not by itself cause the resulting executable to be covered by
// the Library GNU General Public License.  This exception does not however
// invalidate any other reasons why the executable file might be covered by
// the Library GNU General Public License.

#ifndef _SEMANTICS_H_
#define _SEMANTICS_H_

#include <stdint.h>
#include <string>
#include <fstream>
#include <iostream>
#include <coconut_types.h>

typedef enum { c_convex=1, c_linear=0, c_concave=-1, c_maybe=2 } convex_info;

typedef enum { v_exists=0, v_forall=1, v_free=2, v_stochastic=3 }
                                                        type_annotation;

typedef enum { a_redundant=1,
               a_active_lo=2, a_active_lo_red=a_active_lo|a_redundant,
               a_active_hi=4, a_active_hi_red=a_active_hi|a_redundant,
               a_active=a_active_lo|a_active_hi, 
               a_active_red=a_active|a_redundant }      activity_descr;

class convex_e
{
private:
  convex_info e;
  uint16_t tested;
public:
  convex_e() : e(c_maybe), tested(0) {}
  convex_e(const convex_info& __e, uint16_t __t) : e(__e), tested(__t) {}
  convex_e(const convex_e& __e) : e(__e.e), tested(__e.tested) {}
  explicit convex_e(uint16_t __e) : tested(0) { e = (convex_info)__e; }

  ~convex_e() {}

  const convex_info& i() const { return e; }
  uint16_t t() const { return tested; }
  
  convex_e operator-() const
  {
    convex_e __tmp;
    if(e == c_convex)
      __tmp.e = c_concave;
    else if(e == c_concave)
      __tmp.e = c_convex;
    else
      __tmp.e = e;
    return __tmp;
  }

  convex_e& operator=(const convex_e& __c)
  {
    e = __c.e;
    tested = __c.tested;
    return *this;
  }

  convex_e& operator=(const convex_info& __i)
  {
    e = __i;
    return *this;
  }

  convex_e& operator=(unsigned int __t)
  {
    tested = (uint16_t) __t;
    return *this;
  }

  convex_e& operator=(uint16_t __t)
  {
    tested = __t;
    return *this;
  }

  void read(char *c);

  void merge(const convex_e& __c)
  {
    if(e == __c.e)
    {
      if(tested < __c.tested)
        tested = __c.tested;
    }
    else // e != __c.e
    {
      if(tested < __c.tested)
        *this = __c;
      else if(tested == __c.tested) // this is a contradiction
        e = c_maybe;
    }
  }

  friend bool operator==(const convex_e& __c, const convex_e& __d);
  friend bool operator==(const convex_e& __c, const convex_info& __d);
  friend bool operator==(const convex_info& __c, const convex_e& __d);
  friend bool operator!=(const convex_e& __c, const convex_e& __d);
  friend bool operator!=(const convex_e& __c, const convex_info& __d);
  friend bool operator!=(const convex_info& __c, const convex_e& __d);
  friend std::ostream& operator<< (std::ostream& o, const convex_e& __s);
};

inline bool operator==(const convex_e& __c, const convex_e& __d)
{
  return __c.e == __d.e;
}

inline bool operator==(const convex_e& __c, const convex_info& __d)
{
  return __c.e == __d;
}

inline bool operator==(const convex_info& __c, const convex_e& __d)
{
  return __c == __d.e;
}

inline bool operator!=(const convex_e& __c, const convex_e& __d)
{
  return __c.e != __d.e;
}

inline bool operator!=(const convex_e& __c, const convex_info& __d)
{
  return __c.e != __d;
}

inline bool operator!=(const convex_info& __c, const convex_e& __d)
{
  return __c != __d.e;
}

inline std::ostream& operator<< (std::ostream& o, const convex_e& __s)
{
  char c[5] = "VLXM";
  o << c[__s.e+1] << __s.tested;
  return o;
}

class semantics
{
public:
  struct {
    convex_e c_info;
    activity_descr act;                 // activity descriptor
    tristate separable;
    tristate active;
    bool is_at_any_bound;
  } property_flags;                     // mathematical constraint properties

  struct {
    bool kj;                            // is from KJ conditions
    bool integer;                       // is integer / not real
    type_annotation type;               // exists, forall, free, stochastic
    bool hard;                          // hard or soft constraint
  } annotation_flags;

  struct {
    tristate has_0chnbase;
  } info_flags;                         // algorithmic properties

  unsigned int _0chnbase;

  int addinfo;                          // for KJ variables this number
                                        // is the corresponding constraint
                                        // number, -1 if kappa (for obj.)

  int degree;                           // -1: essential non-linearity
  int dim;                              // num of vars involved
  int stage;                            // for multistage problems
public:
  // and others needed
  semantics()
  {
    property_flags.c_info = convex_e(c_maybe,0);
    property_flags.separable = t_maybe;
    property_flags.act = a_active;
    property_flags.is_at_any_bound = false;

    annotation_flags.kj = false;
    annotation_flags.integer = false;
    annotation_flags.hard = true;
    annotation_flags.type = v_exists;

    info_flags.has_0chnbase = t_false;

    _0chnbase = 0;
    addinfo = 0;

    degree = -1;
    dim = 0;
    stage = 0;
  }

  semantics(const semantics& __s) : property_flags(__s.property_flags),
                                    annotation_flags(__s.annotation_flags),
                                    info_flags(__s.info_flags),
                                    _0chnbase(__s._0chnbase),
                                    addinfo(__s.addinfo), degree(__s.degree),
                                    dim(__s.dim), stage(__s.stage) {}

  ~semantics() {}

  friend std::ostream& operator<< (std::ostream& o, const semantics& __s);

private:
  const char* print_tristate(const tristate& x) const;
  tristate read_tristate(char c) const;
  const char* print_type_annotation(const type_annotation& x) const;
  type_annotation read_type_annotation(char c) const;
  const char* print_activity_descr(const activity_descr& x) const;
  activity_descr read_activity_descr(char c) const;

  void merge_tristate(tristate& __o, const tristate& __n)
  {
    if(__o != __n)
    {
      if((__o == t_true && __n == t_false) || (__o == t_false && __n == t_true))
        __o = t_maybe;
      else if(__n == t_true)
        __o = t_true;
      else if(__n == t_false)
        __o = t_false;
    }
  }

  void merge_type_annotation(type_annotation& __o, const type_annotation& __n)
  {
    if(__o != __n)
    {
      if(__o == v_exists)
        __o = __n;
      else if(__o == v_free)
        __o = __n;
      else if(__o == v_forall)
        __o = __n;
    }
  }

  void merge_activity_descr(activity_descr& __o, const activity_descr& __n)
  {
    if(__o != __n)
    {
      unsigned int _n = (unsigned int) __n;
      unsigned int _o = (unsigned int) __o;
      unsigned int _r = _n & ((unsigned int)a_redundant); // rem. redundant bit
      _n |= (unsigned int)a_redundant;   // set redundant bit
      _o &= _n;       // unset all _n bits in _o.
      _o |= _r;       // one is redundant, hence the other one as well
      if(_o == 0) _o = (unsigned int)a_redundant;
      __o = (activity_descr)_o;
    }
  }

public:
  void read(char *c);

  void merge(const semantics& __s)
  {
    property_flags.c_info.merge(__s.property_flags.c_info);
    merge_tristate(property_flags.separable, __s.property_flags.separable);
    merge_activity_descr(property_flags.act, __s.property_flags.act);
    if(__s.property_flags.is_at_any_bound)
      property_flags.is_at_any_bound = true;
    if(!__s.annotation_flags.kj)
      annotation_flags.kj = false;
    if(__s.annotation_flags.integer)
      annotation_flags.integer = true;
    if(__s.annotation_flags.hard)
      annotation_flags.hard = true;
    merge_type_annotation(annotation_flags.type, __s.annotation_flags.type);
    merge_tristate(info_flags.has_0chnbase, __s.info_flags.has_0chnbase);
    if(stage == 0 && __s.stage != 0)
      stage = __s.stage;
  }

public:
  // access and storage methods for flags which are
  // not automatically set by the simplifier
  const convex_e& convexity() const { return property_flags.c_info; }
  void convexity(const convex_e& __c) { property_flags.c_info = __c; }

  const tristate& separability() const { return property_flags.separable; }
  void separability(const tristate& __c) { property_flags.separable = __c; }

  const activity_descr& activity() const { return property_flags.act; }
  void activity(const activity_descr& __c) { property_flags.act = __c; }

  bool kj_flag() const { return annotation_flags.kj; }
  void kj_flag(bool __c) { annotation_flags.kj = __c; }

  bool integer_flag() const { return annotation_flags.integer; }
  void integer_flag(bool __c) { annotation_flags.integer = __c; }

  bool hard_flag() const { return annotation_flags.hard; }
  void hard_flag(bool __c) { annotation_flags.hard = __c; }

  bool is_at_any_bound() const { return property_flags.is_at_any_bound; }
  void is_at_any_bound(bool __c) { property_flags.is_at_any_bound = __c; }

  const type_annotation& type() const { return annotation_flags.type; }
  void type(const type_annotation& __c) { annotation_flags.type = __c; }

  bool redundancy() const
    { return (bool)(((unsigned int)activity()) & (unsigned int)a_redundant); }
  bool inactive_hi() const
    { return (bool)(!((unsigned int)activity() & (unsigned int)a_active_hi)); }
  bool inactive_lo() const
    { return (bool)(!((unsigned int)activity() & (unsigned int)a_active_lo)); }
  bool inactive() const
    { return (bool)(!((unsigned int)activity() & (unsigned int)a_active)); }
};

std::ostream& operator<< (std::ostream& o, const semantics& __s);

#endif // _SEMANTICS_H_

---