bddSymTab.h

Go to the documentation of this file.

/*
 * CrocoPat is a tool for relational programming.
 * This file is part of CrocoPat. 
 *
 * Copyright (C) 2002-2008  Dirk Beyer
 *
 * CrocoPat is free software; you can redistribute it and/or
 * modify it under the terms of the GNU Lesser General Public License
 * as published by the Free Software Foundation; either
 * version 2.1 of the License, or (at your option) any later version.
 *
 * CrocoPat 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
 * Lesser General Public License for more details.
 *
 * You should have received a copy of the GNU Lesser General Public License
 * along with CrocoPat; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 *
 * Please find the GNU Lesser General Public License in file
 * License_LGPL.txt or at http://www.gnu.org/licenses/lgpl.txt
 *
 * Author:
 * Dirk Beyer (firstname.lastname@sfu.ca)
 * Simon Fraser University
 *
 * With contributions of: Andreas Noack, Michael Vogel
 */

#ifndef _bddSymTab_h_
#define _bddSymTab_h_

#include "reprNUMBER.h"
#include "relObject.h"

#include <string>
#include <map>
#include <set>
#include <vector>
#include <cassert>
using namespace std;


class bddSymTab : private relObject
{
private: // Attributes.

  unsigned mBitNr;

  map<string, unsigned> mAttributes;
  map<unsigned, string> mPositions;

  map<string, unsigned> mAttributeNumbers;
  vector<string> mAttributeValues;

  set<string> mIsQuoted;

private:
  void operator,(const bddSymTab&);
  void operator=(const bddSymTab&);
  bddSymTab(const bddSymTab&);

public: // Constructors.
  
  bddSymTab()
  {}

  ~bddSymTab()
  {}  
  

public: // Initializers.

  void
  initValueUniverse(set<string>& pValueUniverse) 
  {
    if (pValueUniverse.size() <= 1) {
      mBitNr = 1;        // We need at least one bit for technical reasons.
    } 
    else {
      // Compute bit width (mBitNr).
      mBitNr = 0;
      unsigned lMaxValueCopy = pValueUniverse.size() - 1;
      while (lMaxValueCopy > 0)
      {
        lMaxValueCopy /= 2;
        ++mBitNr;
      }
    }
    
    // Prepare value-encoding mappings. Sort.
    mAttributeValues.clear();
    for( set<string>::const_iterator
           lIt = pValueUniverse.begin();
         lIt != pValueUniverse.end();
         ++lIt)
    {
      mAttributeNumbers[*lIt] = mAttributeValues.size();
      mAttributeValues.push_back(*lIt);
    }   
  }
  

public: // Accessors.

  unsigned
  getBitNr() const 
  { return mBitNr; }

  unsigned
  getUniverseSize() const
  { return mAttributeValues.size(); }

  void
  setQuoted(const string pAttribute)
  { mIsQuoted.insert(pAttribute); }

  bool
  isQuoted(const string pAttribute) const
  { return mIsQuoted.find(pAttribute) != mIsQuoted.end(); }

  bool
  isValueGood(const string& pAttributeValue) const
  {
    return mAttributeNumbers.find(pAttributeValue) != mAttributeNumbers.end();
  }

  unsigned
  getAttributePos(const string& pAttribute) const
  {
    map<string, unsigned>::const_iterator it = mAttributes.find(pAttribute);
    // Otherwise access for invalid attribute.
    assert(it != mAttributes.end());
    return it->second * getBitNr();
  }

  unsigned
  getValueNum(const string& pAttributeValue) const
  {
    map<string, unsigned>::const_iterator
      lIt = mAttributeNumbers.find(pAttributeValue);
    // Value not found in symbol table.
    assert(lIt != mAttributeNumbers.end());
    return lIt->second;
  }

  string
  getAttributeValue(unsigned pNum) const
  {
    assert(pNum < mAttributeValues.size());
    return mAttributeValues[pNum];
  }

public: // Service methods.
  
  void
  addAttribute(const string& pAttribute)
  {
    assert(pAttribute != "");           // Avoid empty string as name.
    // Add only if new.
    if( mAttributes.find(pAttribute) == mAttributes.end() ) {
      unsigned lAttrNum = mAttributes.size();
      // Ensure that lAttrNum is new.
      while (mPositions.find(lAttrNum) != mPositions.end()) {
        if (lAttrNum < UINT_MAX) {
          ++lAttrNum;
        } else {
          cerr << "Error: Maximum number of attributes exceeded." 
               << endl;
          exit(EXIT_FAILURE);
        }
      }
      mAttributes[pAttribute] = lAttrNum;
      mPositions[lAttrNum] = pAttribute;
    }
  }

  void
  removeAttribute(const string& pAttribute) 
  {
    assert(mAttributes.find(pAttribute) != mAttributes.end());
    mPositions.erase(mAttributes[pAttribute]);
    mAttributes.erase(pAttribute);
  }

  void
  removeUserAttributes(const char pAttributePrefix)
  {
    vector<string> lToRemove;
    // Collect attributes to remove.
    for(map<unsigned, string>::const_iterator lIt = mPositions.begin();
        lIt != mPositions.end();
        ++lIt)
    {
      if( (lIt->second)[0] != pAttributePrefix ) 
      {
        lToRemove.push_back(lIt->second);
      }
    }
    // Actually remove the collected attributes.
    for(vector<string>::const_iterator lIt = lToRemove.begin();
        lIt != lToRemove.end();
        ++lIt)
    {
      removeAttribute(*lIt);
    }
  }  

  const map<unsigned,string>
  computeVariableOrder(const set<string>& pAttributes) const
  { 
    map<unsigned,string> result;
    for (set<string>::const_iterator it = pAttributes.begin();  
         it != pAttributes.end();  
         ++it) 
    {
      result[getAttributePos(*it)] = *it;
    }
    return result;
  }
  
public: // IO.

  void printValueNames(ostream& pS) const
  {
    pS << "VALUES -> NUMBERS :" << endl
       << "{" << endl;
    for (map<string, unsigned>::const_iterator 
         lValueIt = mAttributeNumbers.begin();
         lValueIt != mAttributeNumbers.end();
         ++lValueIt)
    {
      pS << "(\"" << lValueIt->first << "\" -> " 
         << lValueIt->second << "), ";
    }
    pS << "}" << endl;

    // Reverse mapping.
    pS << "NUMBERS -> VALUES :" << endl
       << "{" << endl;
    for (vector<string>::const_iterator 
           lValueIt = mAttributeValues.begin();
           lValueIt != mAttributeValues.end();
           ++lValueIt)
    {
      pS << "(" << lValueIt - mAttributeValues.begin() << " -> \""
         << *lValueIt << "\"), ";
    }
    pS << "}" << endl;
  }

};

#endif // _bddSymTab_h_

---