semantics.h

Go to the documentation of this file.

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

// $Id: semantics.h 932 2009-11-12 17:23:05Z mihaly $
// 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>
#if defined(COCONUT_WINDOWS)
#include <msc_stdint.h>
#endif
#include <string>
#include <fstream>
#include <iostream>
#include <coconut_types.h>

namespace coco {


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(int16_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;         
    tristate separable;         
    bool is_at_either_bound;    
  } property_flags;

  struct {
    bool kj;                    
    bool integer;               
    type_annotation type;       
    bool hard;                  
  } annotation_flags;

  struct {
    tristate has_0chnbase;      
  } info_flags;

  unsigned int _0chnbase;

  int addinfo;

  int degree;
  int dim;
  int stage;
public:
  semantics();

  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);

  void merge_type_annotation(type_annotation& __o, const type_annotation& __n);

  void merge_activity_descr(activity_descr& __o, const activity_descr& __n);

public:
  void read(char *c);

  void merge(const semantics& __s);

public:
  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_either_bound() const { return property_flags.is_at_either_bound; }
  void is_at_either_bound(bool __c) { property_flags.is_at_either_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)); }
};

inline semantics::semantics()
{
  property_flags.c_info = convex_e(c_maybe,0);
  property_flags.separable = t_maybe;
  property_flags.act = a_active;
  property_flags.is_at_either_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;
}

inline void semantics::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;
  }
}

inline void semantics::merge_type_annotation(type_annotation& __o,
                                             const type_annotation& __n)
{
  if((__o != __n) &&
     (__o == v_exists || __n != v_exists))
    __o = __n;
}

inline void semantics::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;
  }
}

inline void semantics::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_either_bound)
    property_flags.is_at_either_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;
  if(addinfo == 0)
    addinfo = __s.addinfo;
  else if(addinfo != 0 && __s.addinfo != 0)
    addinfo = std::max(addinfo,__s.addinfo);
  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;
}


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

} // namespace coco

#endif // _SEMANTICS_H_

---