---

scv_constraint.cpp

Go to the documentation of this file.

//  -*- C++ -*- <this line is for emacs to recognize it as C++ code>
/*****************************************************************************
  The following code is derived, directly or indirectly, from the SystemC
  source code Copyright (c) 1996-2002 by all Contributors.
  All Rights reserved.

  The contents of this file are subject to the restrictions and limitations
  set forth in the SystemC Open Source License Version 2.3 (the "License");
  You may not use this file except in compliance with such restrictions and
  limitations. You may obtain instructions on how to receive a copy of the
  License at http://www.systemc.org/. Software distributed by Contributors
  under the License is distributed on an "AS IS" basis, WITHOUT WARRANTY OF
  ANY KIND, either express or implied. See the License for the specific
  language governing rights and limitations under the License.

 *****************************************************************************/

/*****************************************************************************

  scv_constraint.cpp -- The public interface for the constraint facility.

  Original Authors (Cadence Design Systems, Inc):
  Norris Ip, Dean Shea, John Rose, Jasvinder Singh, William Paulsen,
  John Pierce, Rachida Kebichi, Ted Elkind, David Bailey
  2002-09-23

 *****************************************************************************/

/*****************************************************************************

  MODIFICATION LOG - modifiers, enter your name, affiliation, date and
  changes you are making here.

      Name, Affiliation, Date:
  Description of Modification:

 *****************************************************************************/
#include "scv/scv_util.h"
#include "scv/scv_constraint.h"

#include "cuddObj.hh"
#include "cudd.h"
#include "cuddInt.h"
#include "util.h"

#include <float.h>

// Class : scv_constraint_base
//   - Implementation of the scv_constraint_base class methods
//   - scv_constraint_base is base class constraints

static int sDebugLevel = 0;
static void _scv_push_constraint(scv_constraint_base * c);

scv_constraint_base::scv_constraint_base() : 
  mode_(scv_extensions_if::RANDOM), scan_counter_(-1), ignore_(0)
{ 
  _scv_push_constraint(this); 
}

scv_constraint_base::~scv_constraint_base() {}

void scv_constraint_base::next() 
{ 
  uninitialize(); 
  scv_constraint_manager::set_value(this, true);
}

void scv_constraint_base::set_mode(scv_extensions_if::mode_t m) 
{
  if (m == scv_extensions_if::DISTRIBUTION) {
    _scv_message::message(_scv_message::CONSTRAINT_INVALID_MODE, 
      get_name());
  } else {
    if (mode_ == scv_extensions_if::SCAN) {
      scan_counter_ = -1;
      _scv_message::message(_scv_message::NOT_IMPLEMENTED_YET, "SCAN mode for complex constraints (will treat as RANDOM).");
      mode_ = scv_extensions_if::RANDOM;
    } else {
      mode_ = m;
    }
    list<scv_smart_ptr_if*>::iterator i;
    for (i= get_members().begin(); i != get_members().end(); ++i) {
      scv_extensions_if* e = (*i)->get_extensions_ptr();
      e->get_constraint_data()->set_ext_mode(m, 0, 0);
    }
  }
}

scv_extensions_if::mode_t scv_constraint_base::get_mode(void) const 
{
  return mode_;
}

void scv_constraint_base::set_random(scv_shared_ptr<scv_random> g) 
{
  gen_ = g;
  list<scv_smart_ptr_if*>::iterator i;
  for (i= get_members().begin(); i != get_members().end(); ++i) {
    scv_extensions_if* e = (*i)->get_extensions_ptr();
    e->set_random(g);
  }
}

scv_shared_ptr<scv_random> scv_constraint_base::get_random(void) 
{
  if (gen_.isNull())  {
    gen_ = new scv_random(get_name());
    scv_shared_ptr<scv_random> g(gen_);
    gen_ = g; 
  }
  return gen_;
}

void scv_constraint_base::get_members(list<scv_smart_ptr_if*>& vlist) 
{
  list<scv_smart_ptr_if*>::iterator i;
  for (i = pointers_.begin(); i != pointers_.end(); i++) {
    vlist.push_back(*i);
  }
}

list<scv_smart_ptr_if*>& scv_constraint_base::get_members(void) 
{
  return pointers_;
}

int scv_constraint_base::debug_ = scv_debug::INITIAL_DEBUG_LEVEL;

int scv_constraint_base::get_debug()
{
  return debug_;
}

const char *scv_constraint_base::get_name() const
{
  return name_.c_str();
}

const string& scv_constraint_base::get_name_string() const
{
  return name_;
}

const char *scv_constraint_base::kind() const
{
  static const char *name = "scv_constraint_base";
  return name;
}

void scv_constraint_base::print(ostream& o, int details, int indent) const
{
  int local_indent = indent;
  string spaces="";

  for (int i=0; i < indent; i++) spaces += " ";

  if (details == 0 || details == 1) {
    o << spaces << kind() << " Name: " << name_ << endl;
    o << spaces << "  Hard constraints: " << _hard_constraints << endl;
    o << spaces << "  Soft constraints: " << _soft_constraints << endl;
  }

  if (details == 0 || details == 2) {
    o << spaces << "  Number of elements: " << pointers_.size() << endl;
    o << spaces << "  Current value of elements: " << endl;
    list<scv_smart_ptr_if*>::const_iterator i;
    for (i= pointers_.begin(); i != pointers_.end(); ++i) {
      o << spaces << "    " << (*i)->get_name() << ":  " ;
      if ((*i)->get_extensions_ptr()->is_record() || 
          (*i)->get_extensions_ptr()->is_array()) {
        o << endl;
        local_indent = indent + 4;
      } else {
        local_indent = indent;
      }
      (*i)->print(o, details, local_indent);
    }
  }
}

void scv_constraint_base::set_debug(int debug)
{
  if ( debug_ == debug ) return;
  debug_ = debug;
  scv_debug::set_facility_level(scv_debug::RANDOMIZATION, debug);
}

void scv_constraint_base::show(int details, int indent) const
{
  print(scv_out, details, indent);
}

scv_expression scv_constraint_base::get_constraint() const 
{
  return scv_constraint_base::eh() && scv_constraint_base::ebh();
}

scv_expression scv_constraint_base::get_soft_constraint() const 
{
  return scv_constraint_base::es() && scv_constraint_base::ebs();
}

scv_constraint_base* scv_constraint_base::get_copy(scv_constraint_base * from) 
{
  assert(0);
  return NULL;
}

void scv_constraint_base::uninitialize() 
{
  list<scv_smart_ptr_if*>::iterator i;
  for (i= pointers_.begin(); i != pointers_.end(); ++i)
    (*i)->get_extensions_ptr()->uninitialize();
}

void scv_constraint_base::initialize() 
{
  scv_constraint_manager::set_value(this, true);
}

bddNodeT& scv_constraint_base::get_bdd() 
{
  static bddNodeT& bh = scv_constraint_manager::get_bdd(
    scv_constraint_base::get_constraint(), this, true);
  static bddNodeT& bs = scv_constraint_manager::get_bdd(
    scv_constraint_base::get_soft_constraint(), this, false);
  static bddNodeT& b = _scv_bdd_and(bh, bs, this);
  if (ignore_) {
    return bh;
  } else {
    return b;
  }
}

void scv_constraint_base::init_bdd() 
{
  return;
}

scv_expression& scv_constraint_base::eh() const
{ 
  static scv_expression e = true; 
  return e; 
}

scv_expression& scv_constraint_base::es() const 
{ 
  static scv_expression e = true; 
  return e; 
}

scv_expression& scv_constraint_base::ebh() const 
{ 
  static scv_expression e = true; 
  return e; 
}

scv_expression& scv_constraint_base::ebs() const 
{
  static scv_expression e = true; 
  return e; 
}

void scv_constraint_base::set_up_members(list<scv_smart_ptr_if*>& members) 
{
  pointers_ = members;
  scv_constraint_manager::reset();
  list<scv_smart_ptr_if*>::iterator i;
  for (i= pointers_.begin(); i != pointers_.end(); ++i) {
    (*i)->get_extensions_ptr()->set_constraint(this);
    //scv_constraint_manager::add_extension((*i)->get_extensions_ptr());
  }
}

void scv_constraint_base::ignore_soft_constraint(void) 
{
  ignore_ = true;
}

bool scv_constraint_base::is_ignored_soft_constraint(void) 
{
  return ignore_;
}

int scv_constraint_base::get_scan_counter(void) 
{
  return ++scan_counter_;
}

void scv_constraint_base::set_expression_string(const char * e, bool hard_constraint)  
{
  if (hard_constraint) {
    _hard_constraints = e;
  } else {
    _soft_constraints = e;
  }
}

// Class : scv_constraint_manager
//   - Implementation of scv_constraint_manager
//   - External interface for the _scv_constraint_manager class.
//   - Provides static methods to manipulate constraints and
//     generate random values

void _scv_remove(_scv_expr* e);
static void _scv_remove_data(_scv_expr* e); 
static void _scv_remove_if_bdd(_scv_expr* e); 
static bool _scv_is_avoid_duplicate(scv_constraint_base * c);
static bool _scv_is_scan(scv_constraint_base * c); 

_scv_constraint_manager* scv_constraint_manager::globalConstraintManagerP=NULL;
static _scv_expr* errorExprP;

bddNodeT& scv_constraint_manager::get_bdd(scv_expression e, scv_constraint_base* c, bool hard_constraint)
{
  return getConstraintManagerP()->get_bdd(e, c, hard_constraint);
}

void scv_constraint_manager::init_bdd(scv_expression e, scv_constraint_base* c, bool hard_constraint)
{
  getConstraintManagerP()->init_bdd(e, c, hard_constraint);
}

void scv_constraint_manager::init_maxvar(const scv_expression& he, const scv_expression& se)
{
  getConstraintManagerP()->countMaxVar(he);
  getConstraintManagerP()->countMaxVar(se);
}

void scv_constraint_manager::set_value(scv_extensions_if* s, bddNodeT *b, 
  _scv_constraint_data *cdata_)
{
  getConstraintManagerP()->assignRandomValue(s, b, cdata_);
}

void scv_constraint_manager::set_value(scv_constraint_base* c, bool simplify)
{
  getConstraintManagerP()->assignRandomValue(c, simplify);
}

void scv_constraint_manager::wrapup(scv_extensions_if* s, void *argP)
{
  getConstraintManagerP()->wrapup(s);
}

void scv_constraint_manager::reset(void)
{
  getConstraintManagerP()->reset();
}

void scv_constraint_manager::add_extension(scv_extensions_if *s)
{
  getConstraintManagerP()->add_extension(s);
}

_scv_constraint_manager* scv_constraint_manager::getConstraintManagerP(void)
{
  SCV_STARTUP();
  return globalConstraintManagerP;
}

// Class :  _scv_expr
//   - Implementation for the internal expression representation 
//   - Used in the BDD based constraint solver 

_scv_expr::_scv_expr()
{
  type = _scv_expr::EMPTY;
  bit_width = 0;
  vecsize = 0;
  sigLsb = 0;
  sigMsb = 0;
  value.uvalue = 0; 
  isVar = 0;
}

_scv_expr::_scv_expr(const _scv_expr& other)
{
  type = other.type;
  bit_width = other.bit_width;
  vecsize = other.vecsize;
  sigLsb = other.sigLsb;
  sigMsb = other.sigMsb;
  value = other.value;
  isVar = other.isVar;
  sc_data = other.sc_data;
}

_scv_expr::~_scv_expr() {}

_scv_expr& _scv_expr::operator=(const _scv_expr& rhs)
{
  type = rhs.type;
  bit_width = rhs.bit_width;
  vecsize = rhs.vecsize;
  sigLsb = rhs.sigLsb;
  sigMsb = rhs.sigMsb;
  value = rhs.value;
  isVar = rhs.isVar;
  sc_data = rhs.sc_data;

  return *this;
}

void _scv_expr::setType(ExprValueType t)
{
  type = t;
}

void _scv_expr::setBddNodeP(bddNodeT* b)
{
  value.bdd = b;
}

void _scv_expr::setIntValue(long long i)
{
  value.ivalue = i;
}

void _scv_expr::setBooleanValue(bool b)
{
  value.bvalue = b;
}

void _scv_expr::setUnsignedValue(unsigned long long u)
{
  value.uvalue = u;
}

void _scv_expr::setBigValue(sc_bv_base& v, int bw)
{
  scv_shared_ptr<sc_bv_base> tmp(new sc_bv_base(bw));
  sc_data = tmp;
  *sc_data = v;
}

void _scv_expr::setDoubleValue(double d)
{
  value.dvalue = d;
}

void _scv_expr::setStringValue(const char* s) 
{
  value.cvalue = new char[strlen(s)+1];
  strcpy(value.cvalue, s);
}

void _scv_expr::setBddVectorP(bddVectorT* v)
{
  value.bddvec = v;
}

void _scv_expr::setExtensionP(scv_extensions_if* s)
{
  value.ext = s;
}

void _scv_expr::setVecSize(int vsize)
{
  vecsize = vsize;
}

void _scv_expr::setBitWidth(int bw)
{
  bit_width = bw;
}

void _scv_expr::setSigWidth(int lsb, int msb)
{
  sigLsb = lsb;
  sigMsb = msb;
}

void _scv_expr::setSigMsb(int msb)
{
  sigMsb = msb;
}

void _scv_expr::setSigLsb(int lsb)
{
  sigLsb = lsb;
}

const _scv_expr::ExprValueType _scv_expr::get_type(void) const
{
  return type;
}

bddNodeT* _scv_expr::getBddNodeP(void) const
{
  return value.bdd;
}

long long _scv_expr::getIntValue(void) const
{
  return value.ivalue;  
}

unsigned long long _scv_expr::getUnsignedValue(void) const
{
  return value.uvalue;
}

sc_bv_base _scv_expr::getBigValue(void) const
{
  return *sc_data;
}

bool _scv_expr::getBoolValue(void) const
{
  return value.bvalue;
}

double _scv_expr::getDoubleValue(void) const
{
  return value.dvalue;
}

char* _scv_expr::getStringValue(void) const
{
  return value.cvalue;
}

bddVectorT* _scv_expr::getBddVectorP(void) const
{
  return value.bddvec;
}

scv_extensions_if* _scv_expr::getExtensionP(void) const
{
  return value.ext;
}

int _scv_expr::getVecSize(void) const
{
  if (type == BDDVECTOR || type == BDDVECTOR_SIGNED) {
    return vecsize;
  } else { 
    _scv_constraint_error::internalError(
      "Accessing vector size for non-vector expression");
    return 0;
  }
}

int _scv_expr::getBitWidth(void) const
{
  return bit_width;
}

int _scv_expr::getSigMsb(void) const
{
  if (type == BDDVECTOR || type == BDDVECTOR_SIGNED) {
    return sigMsb;
  } else {
    _scv_constraint_error::internalError(
      "Accessing lsb for non-vector expression.");
    return 0;
  }
}

int _scv_expr::getSigLsb(void) const
{
  if (type == BDDVECTOR || type == BDDVECTOR_SIGNED) {
    return sigLsb;
  } else {
    _scv_constraint_error::internalError(
      "Accessing lsb for non-vector expression.");
    return 0;
  }
}

// _scv_constraint_manager: 
//  Class which implements the BDD constraint solver.
//  There is a single object of this type which is controlled
//  via the scv_constraint_manager class static methods
//  scv_constraint_manager provides external interface.

_scv_constraint_manager::_scv_constraint_manager():maxTime(300),
  maxMemory(0), verboseLevel(0) 
{
  _mgr = new Cudd();
  nthvar = 0;
  multiple = 0;
  iteration = 1;
  maxvar = 1;
  numBddVar = 0;
  maxNumBits = 0;
  eProb = new int;
  mode = scv_extensions_if::RANDOM;
  numBitsUnsigned = 8 * sizeof(unsigned);
  numBitsSigned = 8 * sizeof(int);
  valueIndex = new unsigned[CUDD_MAXINDEX];
  oneNode = _mgr->bddOne().getNode();
  zeroNode = _mgr->bddZero().getNode();
  exprRepOne = new _scv_expr;
  exprRepZero = new _scv_expr;

  extHash = new _scv_open_table<_smartDataRecordT>(SIZE_HINT);
  countExtHash = new _scv_associative_array<scv_extensions_if*, int>
    ("countExtHash", 0);
  avoidDuplicateHash = new _scv_associative_array<scv_constraint_base*, 
    bddNodeT*> ("avoidDuplicateHash", 0);
  avoidDuplicateExtHash = new _scv_associative_array<scv_extensions_if*,
    bddNodeT*> ("avoidDuplicateExtHash", 0);
  nodeHashP = new _scv_open_table<int>(SIZE_HINT);
  nodeWeightHash = new _scv_associative_array<ddNodeT*, double> 
    ("nodeWeightHash", 0);
  wasVisited = new _scv_associative_array<ddNodeT*, int> 
    ("wasVisited", 0);
  enumVarList = new list<scv_extensions_if*>;
}

 _scv_constraint_manager::~ _scv_constraint_manager()
{
  delete eProb;
  delete[] valueIndex;
  delete extHash;
  delete countExtHash;
  delete avoidDuplicateHash;
  delete avoidDuplicateExtHash;
  delete nodeHashP;
  delete nodeWeightHash;
  delete wasVisited;
}

void _scv_constraint_manager::reset(void) 
{
  nthvar = 0;
  maxvar = 0;
  maxNumBits = 0;
  numBddVar = 0;
  countExtHash->clear();
  enumVarList->clear();
}

bddNodeT& _scv_constraint_manager::get_bdd(scv_expression e,  scv_constraint_base * c, bool hard_constraint)
{
  bddNodeT* b = NULL;
  _scv_expr t1 = getExpressionRep(e);
  _scv_expr t2 = getBasicEnumConstraint();
  _scv_expr t = exprAnd(t1, t2);
  _scv_remove_data(&t1);
  _scv_remove_data(&t2);
  if (isOverConstrained(t)) {
    _scv_constraint_error::cannotMeetConstraint(c->get_name());
    b = getExprRepOne().getBddNodeP();
  } else {
    b = t.getBddNodeP();
    check_sparse_var(c, b);
  }
  return *b;
}

void _scv_constraint_manager::add_sparse_var(scv_extensions_if* e, bddNodeT* b)
{
  int size;

  if (e->is_record()) {
    size = e->get_num_fields();
    for (int j=0; j<size; ++j) {
      scv_extensions_if *ef = e->get_field(j);
      add_sparse_var(ef, b);
    }
  } else if (e->is_array()) {
    size = e->get_array_size();
    for (int j=0; j<size; ++j) {
      scv_extensions_if *ef = e->get_array_elt(j);
      add_sparse_var(ef, b);
    }
  } else {
    int bitWidth=0;
    _smartDataRecordT * sDataP;

    bitWidth = e->get_bitwidth();
  
    if (verboseLevel > 3) {
      scv_out << "Extension: " << e << " BitWidth : " << bitWidth << " Has Extension: " << extHash->get(e, sDataP) << endl;
    }
  
    if (extHash->get(e, sDataP)) {
      if (bitWidth < maxNumBits) {
        for (int j = bitWidth; j < maxNumBits; j++) {
          *b = (*b &  (!_mgr->bddVar((maxvar*j)+sDataP->startIndex)));
          if (verboseLevel > 3) {
            scv_out << "  EXTRA FOR SIZE: " << ((maxvar*j)+sDataP->startIndex) << endl;
          }
        } 
      }
    }
  }
}

void _scv_constraint_manager::check_sparse_var(scv_constraint_base * c, bddNodeT* b) 
{
  list<scv_smart_ptr_if*>::iterator i;
  list<scv_smart_ptr_if*>& pointers_ = c->get_members();
  scv_extensions_if* e = NULL;

  for (i= pointers_.begin(); i != pointers_.end(); ++i) {
    e = (*i)->get_extensions_ptr();
    add_sparse_var(e, b);
  }
}

void _scv_constraint_manager::init_bdd(scv_expression e, scv_constraint_base* c, bool hard_constraint)
{
  c->set_expression_string(e.get_expression_string(), hard_constraint);
  initExpression(e);
}

_scv_expr _scv_constraint_manager::simplifyMember(scv_extensions_if* e, _scv_expr t1, scv_constraint_base* c, bool& remove_, bool& over_constraint) 
{
  int size;
  _scv_expr tmp;
  if (e->is_record()) {
    size = e->get_num_fields();
    for (int j=0; j<size; ++j) {
      scv_extensions_if *ef = e->get_field(j);
      t1 = simplifyMember(ef, t1, c, remove_, over_constraint);
      if (over_constraint) break;
    }
  } else if (e->is_array()) {
    size = e->get_array_size();
    for (int j=0; j<size; ++j) {
      scv_extensions_if *ef = e->get_array_elt(j);
      t1 = simplifyMember(ef, t1, c, remove_, over_constraint);
      if (over_constraint) break;
    }
  } else {
    bool tmp_remove = false;

    tmp = simplifyField(t1, e, tmp_remove);
    if (isOverConstrained(tmp)) { 
      if (!c->is_ignored_soft_constraint()) {
        _scv_constraint_error::ignoredLevel(c->get_name());
        c->ignore_soft_constraint();
        if (tmp_remove) {
          _scv_remove_data(&tmp);
        }
        tmp.setBddNodeP(simplifyConstraint(c, remove_ ));
      } else {
        _scv_constraint_error::cannotMeetConstraint(c->get_name());
        over_constraint = true;
      }
    }
    if (tmp_remove && (t1.getBddNodeP() != &c->get_bdd())) {
      _scv_remove_data(&t1);
    }
    remove_ = tmp_remove;
    t1 = tmp;
  }
  return t1;
}

bddNodeT* _scv_constraint_manager::simplifyConstraint(scv_constraint_base* c, bool& remove_, bddNodeT* b)
{ 
  _scv_expr t1;

  remove_ = false;
  bool over_constraint = false;

  if (b) {
    t1.setBddNodeP(b);
  } else {
    t1.setBddNodeP(&(c->get_bdd()));
  }
  t1.setType(_scv_expr::BDD);
  list<scv_smart_ptr_if*>::iterator i;
  for (i= c->get_members().begin(); i != c->get_members().end(); ++i) {
    scv_extensions_if* e = (*i)->get_extensions_ptr();
    t1 = simplifyMember(e, t1, c, remove_, over_constraint);
    if (over_constraint) break;
  }
  return t1.getBddNodeP();
}

_scv_expr _scv_constraint_manager::simplifyField(_scv_expr t1, scv_extensions_if* s, bool & remove_)
{
  _scv_expr expr;

   _smartDataRecordT * sDataP;

  if (!extHash->get(s, sDataP)) {
    return t1;
  } 
 
  if (s->is_initialized()) {
    switch(s->get_type()) {
    case scv_extensions_if::INTEGER: 
    case scv_extensions_if::ENUMERATION: 
    {
      int bitwidth = s->get_bitwidth();
      if (bitwidth <= 64) {
        long long value = s->get_integer();
        expr = exprEqual(createExprRep(s), createExprRep(value, bitwidth));
      } else {
        sc_bv_base value(bitwidth);
        s->get_value(value);
        expr = exprEqual(createExprRep(s), createExprRep(value, bitwidth));
      }
      t1 = exprAnd(t1, expr);
      _scv_remove_data(&expr);
      remove_ = true;
      break;
    }
    case scv_extensions_if::UNSIGNED:
    case scv_extensions_if::BIT_VECTOR:
    case scv_extensions_if::LOGIC_VECTOR:
    {
      int bitwidth = s->get_bitwidth();
      if (bitwidth <= 64) {
        unsigned long long value = s->get_unsigned();
        expr = exprEqual(createExprRep(s), createExprRep(value, bitwidth));
      } else {
        sc_bv_base value(bitwidth);
        s->get_value(value);
        expr = exprEqual(createExprRep(s), createExprRep(value, bitwidth));
      }
      t1 = exprAnd(t1, expr);
      _scv_remove_data(&expr);
      remove_ = true;
      break;
    }
    case scv_extensions_if::BOOLEAN:
    {
      bool value = s->get_bool();
      int bitwidth = s->get_bitwidth();
      expr = exprEqual(createExprRep(s), createExprRep(value, bitwidth));
      t1 = exprAnd(t1, expr);
      _scv_remove_data(&expr);
      remove_ = true;
      break;
    }
    default: {
        _scv_constraint_error::notImplementedYet(s->get_type_name());
        break;
      }
    }
  }
  return t1;
}

void _scv_constraint_manager::assignRandomValue(scv_extensions_if* s, bddNodeT * b, scv_shared_ptr<scv_random> g)
{
   _smartDataRecordT * sDataP;

  setRandomGen(g); 

  if (!extHash->get(s, sDataP)) {
    if (!s->is_initialized()) {
      s->next();
    }
  } else {
    int msize = getSizeOfBddVec(s);
    for (int i=0; i<msize; i++) {
      valueIndex[i*sDataP->numvar+sDataP->startIndex] = 2;
    }
    getVectorFromBdd(b->getNode());
    setValue(s, sDataP->startIndex, msize, sDataP->numvar);
  }
}

void _scv_constraint_manager::assignRandomValue(scv_extensions_if* s, bddNodeT * b, _scv_constraint_data * cdata_)
{
   scv_shared_ptr<scv_random> g = cdata_->get_random(s);
   _smartDataRecordT * sDataP;

  setRandomGen(g); 

  if (!extHash->get(s, sDataP)) {
    if (!s->is_initialized()) {
      generate_value_range_constraint(s, cdata_);
    }  
  } else {
    int msize = getSizeOfBddVec(s);
    bool _avoid_duplicate = false;
    bool remove_ = false;
    bddNodeT* sb;
    _scv_expr t, expr, expr_n, expr_f;
  
    scv_constraint_base* c = cdata_->get_constraint();
  
    if (cdata_->is_scan_mode()) {
      mode = scv_extensions_if::SCAN;
      randomnext = cdata_->prev_val_.unsigned_;
      randomnext = randomnext << 1;
      cdata_->prev_val_.unsigned_ += cdata_->lb_scan_;
    } else if (cdata_->is_avoid_duplicate_mode()) {
      _avoid_duplicate = true;
      // Remove the previous bdd if it is not the constraint expression bdd 
      sb = avoidDuplicateHash->getValue(c);
      if (sb != &c->get_bdd()) {
        remove_ = true;
      }
      t.setBddNodeP(sb);
      t.setType(_scv_expr::BDD);
  
    } else {
      mode = scv_extensions_if::RANDOM;
    }
   
    for (int i=0; i<msize; i++) {
      valueIndex[i*sDataP->numvar+sDataP->startIndex] = 2;
    }
  
    getVectorFromBdd(b->getNode());
  
    if (_avoid_duplicate) {
      expr = assignValueMember(s, _avoid_duplicate);
  
      expr_n = exprNot(expr);
      expr_f = exprAnd(t, expr_n);
      
      _scv_remove_data(&expr_n);
      _scv_remove_data(&expr);
      if (isOverConstrained(expr_f)) {
        avoidDuplicateHash->insert(c, 0); 
      } else {
        avoidDuplicateHash->insert(c, expr_f.getBddNodeP());
      }
      if (remove_) {
        _scv_remove_data(&t);
      }
    } else {
      setValue(s, sDataP->startIndex, msize, sDataP->numvar);
    }
  }
}

void _scv_constraint_manager::initMember(scv_extensions_if* e)
{
  _smartDataRecordT * sDataP=NULL;
  if (e->is_record()) {
    int size = e->get_num_fields();

    for (int j=0; j < size; j++) {
      scv_extensions_if* ef = e->get_field(j);
      initMember(ef);
    }
  } else if (e->is_array()) {
    int size = e->get_array_size();

    for (int j=0; j < size; j++) {
      scv_extensions_if* ef = e->get_array_elt(j);
      initMember(ef);
    }
  } else {
    _scv_constraint_data::gen_mode gen_mode = 
      e->get_constraint_data()->get_mode();

    if ( (gen_mode == _scv_constraint_data::DISTRIBUTION) ||
         (gen_mode == _scv_constraint_data::DISTRIBUTION_RANGE) ||
         (gen_mode == _scv_constraint_data::RANGE_CONSTRAINT)) {

        if (verboseLevel > 3) {
          scv_out << "  Doing Initialize on: " << e->get_name() << endl;
        }
        e->initialize();
    } 
    if (extHash->get(e, sDataP)) {

      if ( !(gen_mode == _scv_constraint_data::DISTRIBUTION) ||
           (gen_mode == _scv_constraint_data::DISTRIBUTION_RANGE) ||
           (gen_mode == _scv_constraint_data::RANGE_CONSTRAINT)) {
        int msize = getSizeOfBddVec(e);
        for (int k=0; k<msize; k++) {
          valueIndex[k*sDataP->numvar+sDataP->startIndex] = 2;
        }
      }
    } 
  }
  return;
}

_scv_expr _scv_constraint_manager::assignValueMember(scv_extensions_if* e, bool _avoid_duplicate)
{
  _smartDataRecordT * sDataP=NULL;
  _scv_expr expr;
  _scv_expr tmp;
  _scv_expr tmp1;

  if (_avoid_duplicate) {
    expr = getExprRepOne();
  }

  if (e->is_record()) {
    int size = e->get_num_fields();

    for (int j=0; j < size; j++) {
      scv_extensions_if* ef = e->get_field(j);
      if (_avoid_duplicate) {
        tmp1 = expr;
      }
      tmp = assignValueMember(ef, _avoid_duplicate);
      if (_avoid_duplicate) {
        expr = exprAnd(expr, tmp);
        _scv_remove_data(&tmp); 
        _scv_remove_data(&tmp1); 
      }
    }
  } else if (e->is_array()) {
    int size = e->get_array_size();
    for (int j=0; j < size; j++) {
      scv_extensions_if* ef = e->get_array_elt(j);
      if (_avoid_duplicate) {
        tmp1 = expr;
      }
      tmp = assignValueMember(ef, _avoid_duplicate);
      if (_avoid_duplicate) {
        expr = exprAnd(expr, tmp);
        _scv_remove_data(&tmp); 
        _scv_remove_data(&tmp1); 
      }
    }
  } else {
    bool should_remove=false;

    if (extHash->get(e, sDataP)) {
      if (!e->is_initialized()) {
        int msize = getSizeOfBddVec(e);
        setValue(e, sDataP->startIndex, msize, sDataP->numvar);
        if (_avoid_duplicate) {
          tmp = simplifyField(expr, e, should_remove);
          _scv_remove_data(&expr);
          expr = tmp;
        }
      }
    } else {
      if (!e->is_initialized()) {
        e->next();
      } 
    }
  }
  return expr;
}

void _scv_constraint_manager::assignRandomValue(scv_constraint_base* c, bool simplify)
{
  list<scv_smart_ptr_if*>::iterator i;

  list<scv_smart_ptr_if*>& pointers_ = c->get_members();

  setRandomGen(c->get_random());

  for (i= pointers_.begin(); i != pointers_.end(); ++i) {
    scv_extensions_if* e = (*i)->get_extensions_ptr();
    initMember(e);
  }

  bool remove_ = false;
  bool _avoid_duplicate = false;
  _scv_expr t;
  bddNodeT* sb;
  _scv_expr expr; 
  _scv_expr tmp, tmp1;

  _avoid_duplicate = _scv_is_avoid_duplicate(c);
  if (_avoid_duplicate) {
    remove_ = true;
    sb = avoidDuplicateHash->getValue(c);
    if (!sb) {
      if (simplify) {
        sb = simplifyConstraint(c, remove_);
      } else {
        sb = &c->get_bdd();
        remove_ = false;
      }
    } 
  } else {
    if (simplify) {
      sb = simplifyConstraint(c, remove_);
    } else {
      sb = &c->get_bdd();
    }
  }
  t.setBddNodeP(sb);
  t.setType(_scv_expr::BDD);

  if (_scv_is_scan(c)) {
    mode = scv_extensions_if::SCAN;
    randomnext = (unsigned int)c->get_scan_counter();
    randomnext = randomnext << 1;
  } else {
    mode = scv_extensions_if::RANDOM;
  } 

  getVectorFromBdd(sb->getNode());
 
  if (_avoid_duplicate) { 
    expr = getExprRepOne();
  }

  for (i= pointers_.begin(); i != pointers_.end(); ++i) {
    scv_extensions_if* e = (*i)->get_extensions_ptr();
    _scv_constraint_data::gen_mode gen_mode = e->get_constraint_data()->get_mode();

    if ( !((gen_mode == _scv_constraint_data::DISTRIBUTION) ||
         (gen_mode == _scv_constraint_data::DISTRIBUTION_RANGE) ||
         (gen_mode == _scv_constraint_data::RANGE_CONSTRAINT)) ) {

      if (_avoid_duplicate) { 
        tmp1 = expr; 
      }
  
      tmp = assignValueMember(e, _avoid_duplicate);
      
      if (_avoid_duplicate) {
        expr = exprAnd(expr, tmp);
        _scv_remove_data(&tmp1);
        _scv_remove_data(&tmp);
      }
    }
  }

  if (_avoid_duplicate) {
    _scv_expr expr_n = exprNot(expr);
    _scv_expr expr_f = exprAnd(t, expr_n);

    _scv_remove_data(&expr_n);
    _scv_remove_data(&expr);
    if (isOverConstrained(expr_f)) {
      avoidDuplicateHash->insert(c, 0); 
      _scv_remove_data(&expr_f);
    } else {
      avoidDuplicateHash->insert(c, expr_f.getBddNodeP());
    }
  }

  if (remove_) {
    _scv_remove_data(&t);
  }

}

void _scv_constraint_manager::wrapup(scv_extensions_if* s)
{
  _smartDataRecordT* sDataP;

  if (s->is_record()) {
    int size = s->get_num_fields();
    for (int i=0; i<size; ++i) {
      scv_extensions_if* ef = s->get_field(i);
      wrapup(ef);
    }
  } else if (s->is_array()) { 
    int size = s->get_array_size();
    for (int i=0; i<size; ++i) {
      scv_extensions_if* ef = s->get_array_elt(i);
      wrapup(ef);
    }
  } else { 
    if (extHash->get(s, sDataP)) {
      extHash->remove(s);
    }
  }
}

void _scv_constraint_manager::add_extension(scv_extensions_if* s)
{
  if (s->is_record()) {
    int size = s->get_num_fields();
    for (int i=0; i<size; ++i) {
      add_extension(s->get_field(i));
    }
  } else if (s->is_array()) {
    int size = s->get_array_size();
    for (int i=0; i<size; ++i) {
      add_extension(s->get_array_elt(i));
    }
  } else {
    createExprRep(s);
  }
}

bool _scv_constraint_manager::has_complex_constraint(scv_extensions_if* s)

{
  _smartDataRecordT * sDataP = NULL;
  return extHash->get(s, sDataP); 
}

_scv_expr _scv_constraint_manager::getConstantExprRep(_scv_expr e, int signExtend) const
{
  unsigned binVal[1024];
  _scv_expr newElem;

  //int msize = getSizeOfBddVec(e);
  int msize = e.getBitWidth();
  int resultSize = msize;

  if (signExtend != -1 && msize != signExtend) {
    resultSize = (msize >= signExtend) ? msize : signExtend;
  }

  bddVectorT *vec = new bddVectorT(resultSize);
  bddVectorT& vecR = *vec;

  switch(e.get_type()) {
  case _scv_expr::UNSIGNED :  
  case _scv_expr::SC_BV_BASE :  
  case _scv_expr::UNSIGNED_64BIT :  {
    getVector(e, binVal);
    for (int i=0; i<resultSize; i++) {
      if (i >= msize) {
        vecR[i] = _mgr->bddZero();
      } else {
        if (binVal[i] == 0) {
          vecR[i] = _mgr->bddZero();
        } else if (binVal[i] == 1) {
          vecR[i] = _mgr->bddOne();
        }
      }
    }
    newElem.setType(_scv_expr::BDDVECTOR);
    newElem.setBddVectorP(vec);
    newElem.setVecSize(resultSize);
    break;
  }
  case _scv_expr::INT :  
  case _scv_expr::BOOLEAN : {
    getVector(e, binVal);
    for (int i=0; i<resultSize; i++) {
      if (i >= msize) {
        if (binVal[msize-1] == 1) {
          vecR[i] = _mgr->bddOne();
        } else {
          vecR[i] = _mgr->bddZero();
        }
      } else {
        if (binVal[i] == 0) {
          vecR[i] = _mgr->bddZero();
        } else if (binVal[i] == 1) {
          vecR[i] = _mgr->bddOne();
        }
      }
    }
    newElem.setType(_scv_expr::BDDVECTOR);
    newElem.setBddVectorP(vec);
    newElem.setVecSize(resultSize);
    break;
  }
  case _scv_expr::DOUBLE : 
  case _scv_expr::STRING : 
  case _scv_expr::RECORD : 
  case _scv_expr::ARRAY : {
    break;
  }
  default:
    _scv_constraint_error::internalError(
      "Unknown expression type- getConstantExprRep.\n");
    break;
  }
  return newElem;
}

void _scv_constraint_manager::countMaxVar(const scv_expression& e)
{
  switch (e.get_operator()) {
  case scv_expression::EMPTY:
    break;
  case scv_expression::INT_CONSTANT:
  case scv_expression::UNSIGNED_CONSTANT:
  case scv_expression::DOUBLE_CONSTANT:
  case scv_expression::BOOLEAN_CONSTANT:
    return;
  case scv_expression::EXTENSION:
    checkExprRep(e.get_extension());
    return;
  case scv_expression::PLUS:
  case scv_expression::MINUS:
  case scv_expression::MULTIPLY:
  case scv_expression::EQUAL:
  case scv_expression::NOT_EQUAL:
  case scv_expression::GREATER_THAN:
  case scv_expression::LESS_THAN:
  case scv_expression::GREATER_OR_EQUAL:
  case scv_expression::LESS_OR_EQUAL:
  case scv_expression::AND:
  case scv_expression::OR:
      countMaxVar(e.get_left());
      countMaxVar(e.get_right());
      return;
  case scv_expression::NOT:
      countMaxVar(e.get_left());
      return;
  default: 
    _scv_constraint_error::internalError(
      "init bdd for unknown operator type in countMaxVar\n");
     break;
  }
  return;
}

void _scv_constraint_manager::initExpression(const scv_expression& e)
{
  switch (e.get_operator()) {
  case scv_expression::EMPTY:
    break;
  case scv_expression::INT_CONSTANT:
  case scv_expression::UNSIGNED_CONSTANT:
  case scv_expression::DOUBLE_CONSTANT:
  case scv_expression::BOOLEAN_CONSTANT:
    return;
  case scv_expression::EXTENSION:
    createExprRep(e.get_extension());
    return;
  case scv_expression::PLUS:
  case scv_expression::MINUS:
  case scv_expression::MULTIPLY:
  case scv_expression::EQUAL:
  case scv_expression::NOT_EQUAL:
  case scv_expression::GREATER_THAN:
  case scv_expression::LESS_THAN:
  case scv_expression::GREATER_OR_EQUAL:
  case scv_expression::LESS_OR_EQUAL:
  case scv_expression::AND:
  case scv_expression::OR:
      initExpression(e.get_left());
      initExpression(e.get_right());
      return;
  case scv_expression::NOT:
      initExpression(e.get_left());
      return;
  default: 
    _scv_constraint_error::internalError(
      "init bdd for unknown operator type in initExpression\n");
     break;
  }
  return;
}

_scv_expr _scv_constraint_manager::getExpressionRep(const scv_expression& e)
{
  switch (e.get_operator()) {
  case scv_expression::EMPTY:
    _scv_constraint_error::internalError(
      "Generating internal BddRep for an EMPTY scv_expression");
    break;
  case scv_expression::INT_CONSTANT:
    return createExprRep(e.get_int_value(), e.get_bit_width());
  case scv_expression::UNSIGNED_CONSTANT:
    return createExprRep(e.get_unsigned_value(), e.get_bit_width());
  case scv_expression::SC_BIGINT_CONSTANT:
  case scv_expression::SC_BIGUINT_CONSTANT:
  case scv_expression::SC_BV_CONSTANT: {
    sc_bv_base val(e.get_bit_width());
    e.get_value(val);
    return createExprRep(val, e.get_bit_width());
  }
  case scv_expression::BOOLEAN_CONSTANT:
    return createExprRep(e.get_bool_value(), e.get_bit_width());
  case scv_expression::DOUBLE_CONSTANT:
    return createExprRep(e.get_double_value());
  case scv_expression::EXTENSION:
    return createExprRep(e.get_extension());
  case scv_expression::PLUS:
    {
      _scv_expr t1 = getExpressionRep(e.get_left());
      _scv_expr t2 = getExpressionRep(e.get_right());
      _scv_expr t3 = exprPlus(t1, t2);
      _scv_remove_if_bdd(&t1); 
      _scv_remove_if_bdd(&t2); 
      return t3;
    }
  case scv_expression::MINUS:
    {
      _scv_expr t1 = getExpressionRep(e.get_left());
      _scv_expr t2 = getExpressionRep(e.get_right());
      _scv_expr t3 = exprMinus(t1, t2);
      _scv_remove_if_bdd(&t1); 
      _scv_remove_if_bdd(&t2); 
      return t3;
    }
  case scv_expression::MULTIPLY:
    {
      _scv_expr t1 = getExpressionRep(e.get_left());
      _scv_expr t2 = getExpressionRep(e.get_right());
      _scv_expr t3 = exprMultiply(t1, t2);
      _scv_remove_if_bdd(&t1); 
      _scv_remove_if_bdd(&t2); 
      return t3;
    }
  case scv_expression::EQUAL:
    {
      _scv_expr t1 = getExpressionRep(e.get_left());
      _scv_expr t2 = getExpressionRep(e.get_right());
      _scv_expr t3 = exprEqual(t1, t2);
      _scv_remove_if_bdd(&t1); 
      _scv_remove_if_bdd(&t2); 
      return t3;
    }
  case scv_expression::NOT_EQUAL:
    {
      _scv_expr t1 = getExpressionRep(e.get_left());
      _scv_expr t2 = getExpressionRep(e.get_right());
      _scv_expr t3 = exprNEqual(t1, t2);
      _scv_remove_if_bdd(&t1); 
      _scv_remove_if_bdd(&t2); 
      return t3;
    }
  case scv_expression::GREATER_THAN:
    {
      _scv_expr t1 = getExpressionRep(e.get_left());
      _scv_expr t2 = getExpressionRep(e.get_right());
      _scv_expr t3 = exprGThan(t1, t2);
      _scv_remove_if_bdd(&t1); 
      _scv_remove_if_bdd(&t2); 
      return t3;
    }
  case scv_expression::LESS_THAN:
    {
      _scv_expr t1 = getExpressionRep(e.get_left());
      _scv_expr t2 = getExpressionRep(e.get_right());
      _scv_expr t3 = exprLThan(t1, t2);
      _scv_remove_if_bdd(&t1); 
      _scv_remove_if_bdd(&t2); 
      return t3;
    }
  case scv_expression::GREATER_OR_EQUAL:
    {
      _scv_expr t1 = getExpressionRep(e.get_left());
      _scv_expr t2 = getExpressionRep(e.get_right());
      _scv_expr t3 = exprGEq(t1, t2);
      _scv_remove_if_bdd(&t1); 
      _scv_remove_if_bdd(&t2); 
      return t3;
    }
  case scv_expression::LESS_OR_EQUAL:
    {
      _scv_expr t1 = getExpressionRep(e.get_left());
      _scv_expr t2 = getExpressionRep(e.get_right());
      _scv_expr t3 = exprLEq(t1, t2);
      _scv_remove_if_bdd(&t1); 
      _scv_remove_if_bdd(&t2); 
      return t3;
    }
  case scv_expression::AND:
    {
      _scv_expr t1 = getExpressionRep(e.get_left());
      _scv_expr t2 = getExpressionRep(e.get_right());
      _scv_expr t3 = exprAnd(t1, t2);
      _scv_remove_if_bdd(&t1); 
      _scv_remove_if_bdd(&t2); 
      return t3;
    }
  case scv_expression::OR:
    {
      _scv_expr t1 = getExpressionRep(e.get_left());
      _scv_expr t2 = getExpressionRep(e.get_right());
      _scv_expr t3 = exprOr(t1, t2);
      _scv_remove_if_bdd(&t1); 
      _scv_remove_if_bdd(&t2); 
      return t3;
    }
  case scv_expression::NOT:
    {
      _scv_expr t1 = getExpressionRep(e.get_left());
      _scv_expr t3 = exprNot(t1);
      _scv_remove_if_bdd(&t1); 
      return t3;
    }
  default: 
    _scv_constraint_error::internalError(
      "creating bdd for unknown operator type in getExpressionRep\n");
     break;
  }
  return *errorExprP;
}

_scv_expr _scv_constraint_manager::getExprRepZero(void)
{
  bddNodeT* internalZero = new bddNodeT;
  *internalZero = _mgr->bddZero();
  exprRepZero->setType(_scv_expr::BDD);
  exprRepZero->setBddNodeP(internalZero);
  return *exprRepZero;
}

_scv_expr _scv_constraint_manager::getExprRepOne(void)
{
  bddNodeT* internalOne = new bddNodeT;
  *internalOne = _mgr->bddOne();
  exprRepOne->setType(_scv_expr::BDD);
  exprRepOne->setBddNodeP(internalOne);
  return *exprRepOne;
}

_scv_expr _scv_constraint_manager::exprAnd(const _scv_expr& e1, const _scv_expr& e2) 
{
  _scv_expr newElem; 
  
  if (e1.isBdd() && e2.isBdd()) {
    bddNodeT *tmp = new bddNodeT;
    *tmp = (*(e1.getBddNodeP()) & *(e2.getBddNodeP())); 
    newElem.setType(_scv_expr::BDD);
    newElem.setBddNodeP(tmp);
  } else if (e1.isBddVector() && e2.isBddVector()) {
    newElem = _exprAnd(e1, e2);
  } else if (e1.isBdd() && e2.isBddVector()) {
    bddNodeT *tmp = new bddNodeT;
    _scv_expr tmpElem; 
    tmpElem = _exprAnd(e2, e2);
    *tmp = (*(e1.getBddNodeP()) & *tmpElem.getBddNodeP());
    newElem.setType(_scv_expr::BDD);
    newElem.setBddNodeP(tmp);
    _scv_remove_data(&tmpElem);
  } else if (e1.isBddVector() && e2.isBdd()) {
    bddNodeT *tmp = new bddNodeT;
    _scv_expr tmpElem; 
    tmpElem = _exprAnd(e1, e1);
    *tmp = (*(e2.getBddNodeP()) & *tmpElem.getBddNodeP());
    newElem.setType(_scv_expr::BDD);
    newElem.setBddNodeP(tmp);
    _scv_remove_data(&tmpElem);
  } else if (e1.isBddVector() && e2.isConstant()) {
    _scv_expr constElem = getConstantExprRep(e2);
    newElem = _exprAnd(e1, constElem);
    delete constElem.getBddVectorP();
  } else if (e1.isConstant() && e2.isBddVector()) {
    _scv_expr constElem = getConstantExprRep(e1);
    newElem = _exprAnd(constElem, e2);
    delete constElem.getBddVectorP();
  } else if (e1.isConstant() && e2.isConstant()) {
    _scv_expr constElem1 = getConstantExprRep(e1);
    _scv_expr constElem2 = getConstantExprRep(e2);
    newElem = _exprAnd(constElem1, constElem2);
    delete constElem1.getBddVectorP();
    delete constElem2.getBddVectorP();
  } else if (e1.isConstant() && e2.isBdd()) {
    newElem = e2;
    bddNodeT *tmp = new bddNodeT;
    *tmp = *e2.getBddNodeP();
    newElem.setBddNodeP(tmp);
  } else if (e1.isBdd() && e2.isConstant()) {
    newElem = e1;
    bddNodeT *tmp = new bddNodeT;
    *tmp = *e1.getBddNodeP();
    newElem.setBddNodeP(tmp);
  } else if (e1.isDouble() || e2.isDouble()) {
    _scv_constraint_error::ignoreDoubleConstraints();
    newElem = getExprRepOne();
  } else if (e1.isString() || e2.isString()) {
    _scv_constraint_error::ignoreDoubleConstraints();
    newElem = getExprRepOne();
  } else if (e1.isEmpty() || e2.isEmpty()) {
  } else {
    _scv_constraint_error::internalError(
                            "Trying exprAnd for unknown types\n");
  }
  return newElem;
}

_scv_expr _scv_constraint_manager::_exprAnd(const _scv_expr& e1, const _scv_expr& e2) 
{
  _scv_expr newElem;
  bddNodeT *tmp = new bddNodeT;
  bddNodeT tmpE1; 
  bddNodeT tmpE2;

  bddVectorT *e1Vec = e1.getBddVectorP();
  bddVectorT *e2Vec = e2.getBddVectorP();
  int e1size = e1.getVecSize();
  int e2size = e2.getVecSize();

  bddVectorT& e1VecR = *e1Vec;
  bddVectorT& e2VecR = *e2Vec;

  tmpE1 = _mgr->bddZero();
  tmpE2 = _mgr->bddZero();

  for (int i=0; i<e1size; ++i) {
    tmpE1 = tmpE1 | e1VecR[i];
  } 
  for (int i=0; i<e2size; ++i) {
    tmpE2 = tmpE2 | e2VecR[i];
  } 
  *tmp = (tmpE1 & tmpE2); 
  newElem.setType(_scv_expr::BDD);
  newElem.setBddNodeP(tmp);
  return newElem;
}

_scv_expr _scv_constraint_manager::exprOr(const _scv_expr& e1, const _scv_expr& e2) 
{
  _scv_expr newElem;

  if (e1.isBdd() && e2.isBdd()) {
    bddNodeT *tmp = new bddNodeT;
    *tmp = (*(e1.getBddNodeP()) | *(e2.getBddNodeP())); 
    newElem.setType(_scv_expr::BDD);
    newElem.setBddNodeP(tmp);
  } else if (e1.isBddVector() && e2.isBddVector()) {
    newElem = _exprOr(e1, e2);
  } else if (e1.isBdd() && e2.isBddVector()) {
    bddNodeT *tmp = new bddNodeT;
    _scv_expr tmpElem; 
    tmpElem = _exprOr(e2, e2);
    *tmp = (*(e1.getBddNodeP()) | *tmpElem.getBddNodeP());
    newElem.setType(_scv_expr::BDD);
    newElem.setBddNodeP(tmp);
    _scv_remove_data(&tmpElem);
  } else if (e1.isBddVector() && e2.isBdd()) {
    bddNodeT *tmp = new bddNodeT;
    _scv_expr tmpElem; 
    tmpElem = _exprOr(e1, e1);
    *tmp = (*(e2.getBddNodeP()) | *tmpElem.getBddNodeP());
    newElem.setType(_scv_expr::BDD);
    newElem.setBddNodeP(tmp);
    _scv_remove_data(&tmpElem);
  } else if (e1.isBddVector() && e2.isConstant()) {
    _scv_expr constElem = getConstantExprRep(e2);  
    newElem = _exprOr(e1, constElem);
    delete constElem.getBddVectorP();
  } else if (e1.isConstant() && e2.isBddVector()) {
    _scv_expr constElem = getConstantExprRep(e1);  
    newElem = _exprOr(constElem, e2);
    delete constElem.getBddVectorP();
  } else if (e1.isConstant() && e2.isConstant()) {
    _scv_expr constElem1 = getConstantExprRep(e1);  
    _scv_expr constElem2 = getConstantExprRep(e2);  
    newElem = _exprOr(constElem1, constElem2);
    delete constElem1.getBddVectorP();
    delete constElem2.getBddVectorP();
  } else if (e1.isDouble() || e2.isDouble()) {
    _scv_constraint_error::ignoreDoubleConstraints();
    newElem = getExprRepOne();
  }