/*************************************************************************
  FILE:  BddHiscHighSub.cpp
  DESCR: Reading high-level DES files and initialze all the BDDs
  AUTH:  Raoguang Song
  Supervisor: Dr. Ryan Leduc
  DATE:  (C) Jan, 2006
*************************************************************************/
#include "BddHiscSub.h"
#include "BddHiscHighSub.h"
#include "BddHiscLowSub.h"
#include <string>
#include "BddHiscErrmsg.h"
#include "BddHiscType.h"
#include <fdd.h>
#include "BddHiscDES.h"
#include "BddHiscProject.h"
#include <fstream>
#include "BddHiscPubfunc.h"
#include <cstdlib>


#include "BddHisc.h"
#include <QString>

#include "DesProject.h"
#include "ProjectEvent.h"
#include "DesTypes.h"
//#include "DesFlatProject.h"
#include "DesHierProject.h"
#include "Des.h"

using namespace std;

namespace BDDHISC
{

extern CProject *pPrj;

/**
 * DESCR:   Constructor
 * PARA:    vsHighFile: subsystem file name with path (.sub)(input)
 *          viSubIndex: subsystem index (high: 0, low: 1,2,...)(input)
 * RETURN:  None
 * ACCESS:  public
 */
CHighSub::CHighSub(const string & vsHighFile, int viSubIndex):
CSub(vsHighFile, viSubIndex)
{
    m_iNumofIntfs = pPrj->GetNumofLows();

    //Uncontrollable event index array --H.I.
    m_piUArr[0] = NULL;
    m_piUArr[1] = NULL;
    m_piUArr[3] = NULL;

    //Controllable event index array --H.I.
    m_piCArr[0] = NULL;
    m_piCArr[1] = NULL;
    m_piCArr[3] = NULL;
    InitBddFields();
}

/**
 * DESCR:   Destructor
 * PARA:    None
 * RETURN:  None
 * ACCESS:  public
 */
CHighSub::~CHighSub()
{
    //Uncontrollable event index array --H.I.
    delete[] m_piUArr[0];
    m_piUArr[0] = NULL;
    delete[] m_piUArr[1];
    m_piUArr[1] = NULL;
    delete[] m_piUArr[3];
    m_piUArr[3] = NULL;

    //Controllable event index array --H.I.
    delete[] m_piCArr[0];
    m_piCArr[0] = NULL;
    delete[] m_piCArr[1];
    m_piCArr[1] = NULL;
    delete[] m_piCArr[3];
    m_piCArr[3] = NULL;

    ClearBddFields();
}

/*
 * DESCR:   Initialize BDD related data members (only those in HighSub.h)
 * PARA:    None
 * RETURN:  0
 * ACCESS:  private
 */
int CHighSub::InitBddFields()
{
    m_pbdd_IVar = NULL;
    m_pbdd_IVarPrim = NULL;
    m_pbdd_UnConATrans = NULL;
    m_pbdd_ConATrans = NULL;
    m_pbdd_UnConLDTrans = NULL;
    m_pbdd_ConLDTrans = NULL;
    return 0;
}

/*
 * DESCR:   Release memory for BDD related data members(only those in Highsub.h)
 * PARA:    None
 * RETURN:  0
 * ACCESS:  private
 */
int CHighSub::ClearBddFields()
{
    delete[] m_pbdd_IVar;
    m_pbdd_IVar = NULL;
    delete[] m_pbdd_IVarPrim;
    m_pbdd_IVarPrim = NULL;
    delete[] m_pbdd_UnConATrans;
    m_pbdd_UnConATrans = NULL;
    delete[] m_pbdd_ConATrans;
    m_pbdd_ConATrans = NULL;
    delete[] m_pbdd_UnConLDTrans;
    m_pbdd_UnConLDTrans = NULL;
    delete[] m_pbdd_ConLDTrans;
    m_pbdd_ConLDTrans = NULL;
    return 0;
}

/**
 * DESCR:   Load high-level
 * PARA:    None
 * RETURN:  0 sucess <0 fail;
 * ACCESS:  public
 */
int CHighSub::LoadSub(const DESpot::DesSubsystem& subSys)
{
    int iRet = 0;
    CDES *pDES = NULL;
    string sDESFile;
    


    //  can I remove this try?
    try
    {


      // set name of subsystem
      QString highName = QString::fromStdWString(subSys.getName());
      // remove spaces from name
      while (highName.contains(" "))
	{
	  highName.remove(' ');
	}
       m_sSubName = highName.toStdString();

       int numPlants = 0;
       int numSups = 0;
       
       // count number of plants
       {
	 DESpot::DesSubsystem::DesIteratorPtr desIt = subSys.createDesIterator(DESpot::ePlantDes);
	 for(desIt->first(); desIt->notDone(); desIt->next())
	   {
	     numPlants++;
	   }
       }

       m_iNumofPlants = numPlants;

       // count number of Sups
       {
	 DESpot::DesSubsystem::DesIteratorPtr desIt = subSys.createDesIterator(DESpot::eSupervisorDes);
	 for(desIt->first(); desIt->notDone(); desIt->next())
	   {
	     numSups++;
	   }
       }

       m_iNumofSpecs = numSups;
       
       m_pDESArr = new CDES *[this->GetNumofDES()];
       for (int i = 0; i < this->GetNumofDES(); i++)
	 m_pDESArr[i] = NULL;

       //Initialize m_piDESOrderArr
       m_piDESOrderArr = new int[this->GetNumofDES()];
       for (int i = 0; i < this->GetNumofDES(); i++)
	 m_piDESOrderArr[i] = i;
       //Initialize m_piDESPosArr
       m_piDESPosArr = new int[this->GetNumofDES()];
       for (int i = 0; i < this->GetNumofDES(); i++)
	 m_piDESPosArr[i] = i;
    



       // process plant components
       int iNumofPlants = 0;

       {
	 DESpot::DesSubsystem::DesIteratorPtr desIt = subSys.createDesIterator(DESpot::ePlantDes);
	 for(desIt->first(); desIt->notDone(); desIt->next())
	   {
	     DESpot::Des& des = desIt->currentItem();
	     QString highDESName = QString::fromStdWString(des.getName());
	     // sDESFile not used with DESpot 
	     sDESFile = highDESName.toStdString();
	     pDES = new CDES(this, sDESFile, PLANT_DES);
	     if (pDES->LoadDES(des, true) < 0)
	       throw -1;   //here LoadDES() will generate the err msg.
	     else
	       {
		 iNumofPlants++;
		 m_pDESArr[iNumofPlants -1] = pDES;
		 pDES = NULL;
	       }
	   }
       }


       // Process specs
        int iNumofSpecs = 0;

       {
	 DESpot::DesSubsystem::DesIteratorPtr desIt = subSys.createDesIterator(DESpot::eSupervisorDes);
	 for(desIt->first(); desIt->notDone(); desIt->next())
	   {
	     DESpot::Des& des = desIt->currentItem();
	     QString highDESName = QString::fromStdWString(des.getName());
	     // sDESFile not used with DESpot 
	     sDESFile = highDESName.toStdString();
	     pDES = new CDES(this, sDESFile, SPEC_DES);
	     if (pDES->LoadDES(des, true) < 0)
	       throw -1;   //here LoadDES() will generate the err msg.
	     else
	       {
		 iNumofSpecs++;
		 m_pDESArr[m_iNumofPlants + iNumofSpecs -1] = pDES;
		 pDES = NULL;
	       }
	   }
       }

       //Get all the interface DES
       for (int i = 0; i < m_iNumofIntfs; i++)
	 {
	   m_pDESArr[m_iNumofPlants + m_iNumofSpecs + i] = 
	     ((CLowSub *)pPrj->GetSub(i + 1))->GetIntfDES();
	 }
   
       
       //Compute the R/A events starting index in Transition precidate arrary
       for (int i = 0; i < 4; i++)
	 {           
            if (i != 2)
            {
               m_piUArr[i] = new int[m_iNumofIntfs];
               m_piCArr[i] = new int[m_iNumofIntfs];

               m_piUArr[i][0] = 0;
               m_piCArr[i][0] = 0;
            }
	 }


       for (int i = 1; i < m_iNumofIntfs; i++)
	 {
	   m_piUArr[0][i] = m_piUArr[0][i-1] + 
                pPrj->GetSub(i)->GetMaxUnCon(R_EVENT) / 2;
	   m_piUArr[1][i] = m_piUArr[1][i-1] + 
                pPrj->GetSub(i)->GetMaxUnCon(A_EVENT) / 2;
           m_piUArr[3][i] = m_piUArr[3][i-1] +
                pPrj->GetSub(i)->GetMaxUnCon(LD_EVENT) / 2;

	   
	   m_usiMaxUnCon[R_EVENT] += pPrj->GetSub(i)->GetMaxUnCon(R_EVENT);
	   m_usiMaxUnCon[A_EVENT] += pPrj->GetSub(i)->GetMaxUnCon(A_EVENT);
           m_usiMaxUnCon[LD_EVENT] += pPrj->GetSub(i)->GetMaxUnCon(LD_EVENT);
	   
	   m_piCArr[0][i] = m_piCArr[0][i-1] + 
                ((unsigned short)(pPrj->GetSub(i)->GetMaxCon(R_EVENT) + 1)) / 2;
	   m_piCArr[1][i] = m_piCArr[1][i-1] + 
                ((unsigned short)(pPrj->GetSub(i)->GetMaxCon(A_EVENT) + 1)) / 2;
           m_piCArr[3][i] = m_piCArr[3][i-1] +
                ((unsigned short)(pPrj->GetSub(i)->GetMaxCon(LD_EVENT) + 1)) / 2;
	   
	   m_usiMaxCon[R_EVENT] += 
                (unsigned short)(pPrj->GetSub(i)->GetMaxCon(R_EVENT) + 1);
	   m_usiMaxCon[A_EVENT] += 
                (unsigned short)(pPrj->GetSub(i)->GetMaxCon(A_EVENT) + 1);
           m_usiMaxCon[LD_EVENT] +=
                (unsigned short)(pPrj->GetSub(i)->GetMaxCon(LD_EVENT) + 1);
	 }
       m_usiMaxUnCon[R_EVENT] += 
            pPrj->GetSub(m_iNumofIntfs)->GetMaxUnCon(R_EVENT);
       m_usiMaxUnCon[A_EVENT] += 
            pPrj->GetSub(m_iNumofIntfs)->GetMaxUnCon(A_EVENT);
       m_usiMaxUnCon[LD_EVENT] +=
            pPrj->GetSub(m_iNumofIntfs)->GetMaxUnCon(LD_EVENT);

       m_usiMaxCon[R_EVENT] += 
            (unsigned short)(pPrj->GetSub(m_iNumofIntfs)->GetMaxCon(R_EVENT) + 1);
       m_usiMaxCon[A_EVENT] += 
            (unsigned short)(pPrj->GetSub(m_iNumofIntfs)->GetMaxCon(A_EVENT) + 1);
       m_usiMaxCon[LD_EVENT] +=
            (unsigned short)(pPrj->GetSub(m_iNumofIntfs)->GetMaxCon(LD_EVENT) + 1);

       //DES Reorder
       this->DESReorder();


    }
    catch (int iError)
    {
        if (pDES != NULL)
        {
            delete pDES;
            pDES = NULL;
        }

        iRet = iError;
    }
    return iRet;
}

/*
 * DESCR:   Initialize BDD data memebers
 * PARA:    None
 * RETURN:  0: sucess -1: fail
 * ACCESS:  private
 */
int CHighSub::MakeBdd()
{
    try
    {
        //Initialize the bdd node table and cache size.
        long long lNumofStates = 1;
        
        for (int i = 0; i < this->GetNumofDES(); i++)
        {
            lNumofStates *= m_pDESArr[i]->GetNumofStates();
            if (lNumofStates >= MAX_INT)
                break;
        }
        if (lNumofStates <= 10000)
            bdd_init(1000, 100);
        else if (lNumofStates <= 1000000)
            bdd_init(10000, 1000);
        else if (lNumofStates <= 10000000)
            bdd_init(100000, 10000);
        else
        {
            bdd_init(2000000, 1000000);
            //bdd_setcacheratio(16);
            bdd_setmaxincrease(1000000);
        }
        
        giNumofBddNodes = 0;
        bdd_gbc_hook(my_bdd_gbchandler);
        
        //define domain variables
        int *piDomainArr = new int[2];
        for (int i = 0; i < 2 * this->GetNumofDES(); i += 2)
        {
            piDomainArr[0] = m_pDESArr[i/2]->GetNumofStates();
            piDomainArr[1] = piDomainArr[0];
            fdd_extdomain(piDomainArr, 2);
        }
        delete[] piDomainArr;
        piDomainArr = NULL;
        
        //compute the number of bdd variables (only for normal variables)
        m_iNumofBddNormVar = 0;
        for (int i = 0; i < 2 * (this->GetNumofDES()); i = i + 2)
            m_iNumofBddNormVar += fdd_varnum(i);
        
        //set the first level block
        int iNumofBddVar = 0;
        int iVarNum = 0;
        bdd bddBlock = bddtrue;
        for (int i = 0; i < 2 * (this->GetNumofDES()); i += 2)
        {
            iVarNum = fdd_varnum(i);
            bddBlock = bddtrue;
            
            for (int j = 0; j < 2 * iVarNum; j++)
            {
                bddBlock &= bdd_ithvar(iNumofBddVar + j);
            }
            bdd_addvarblock(bddBlock, BDD_REORDER_FREE);
            iNumofBddVar += 2 * iVarNum;
        }
                
        //compute initial state predicate
        for (int i = 0; i < this->GetNumofDES(); i++)
            m_bddInit &= fdd_ithvar(i * 2, m_pDESArr[i]->GetInitState());

        //compute marking states predicate
        bdd bddTmp = bddfalse;
        for (int i = 0; i < this->GetNumofDES(); i++)
        {
            bddTmp = bddfalse;
            MARKINGLIST::const_iterator ci = 
                 (m_pDESArr[i]->GetMarkingList()).begin();
                 
            for (int j = 0; j < m_pDESArr[i]->GetNumofMarkingStates(); j++)
            {
                bddTmp |= fdd_ithvar(i * 2, *ci);
                ++ci;
            }
            m_bddMarking &= bddTmp;
        }
        
        //Initialize interface variables predicates
        m_pbdd_IVar = new bdd[m_iNumofIntfs];
        m_pbdd_IVarPrim = new bdd[m_iNumofIntfs];

        if (m_usiMaxUnCon[A_EVENT] != 0) //Answer events
            m_pbdd_UnConATrans = new bdd[m_usiMaxUnCon[A_EVENT]/2];

        if (m_usiMaxCon[A_EVENT] != 0xFFFF) //Answer events
            m_pbdd_ConATrans = new bdd[m_usiMaxCon[A_EVENT] / 2 + 1];

        if (m_usiMaxUnCon[LD_EVENT] != 0) //Low data events
            m_pbdd_UnConLDTrans = new bdd[m_usiMaxUnCon[LD_EVENT]/2];

        if (m_usiMaxCon[LD_EVENT] != 0xFFFF) //Low data events
            m_pbdd_ConLDTrans = new bdd[m_usiMaxCon[LD_EVENT] / 2 + 1];
        
        //Compute transitions predicate
        for (int k = 0; k < 5; k++)
        {
            //High-level only, so ignore low level (k == 3)
            if (k != 3)
            {
                if (m_usiMaxCon[k] != 0xFFFF)
                {
                    m_pbdd_ConTrans[k] = new bdd[m_usiMaxCon[k] / 2 + 1];
                    m_pbdd_ConVar[k] = new bdd[m_usiMaxCon[k] / 2 + 1];
                    m_pbdd_ConVarPrim[k] = new bdd[m_usiMaxCon[k]/ 2 + 1];
                    m_pbdd_ConPhysicVar[k] =
                                        new bdd[m_usiMaxCon[k] / 2 + 1];
                    m_pbdd_ConPhysicVarPrim[k] =
                                        new bdd[m_usiMaxCon[k] / 2 + 1];
                    m_pPair_Con[k] = new bddPair *[m_usiMaxCon[k] / 2 + 1];
                    for (int iPair = 0; iPair < m_usiMaxCon[k] / 2 + 1; iPair++)
                        m_pPair_Con[k][iPair] = NULL;
                    m_pPair_ConPrim[k] = new bddPair *[m_usiMaxCon[k] / 2 + 1];
                    for (int iPair = 0; iPair < m_usiMaxCon[k] / 2 + 1; iPair++)
                        m_pPair_ConPrim[k][iPair] = NULL;
                }
                if (m_usiMaxUnCon[k] != 0)
                {
                    m_pbdd_UnConTrans[k] = new bdd[m_usiMaxUnCon[k]/2];
                    m_pbdd_UnConPlantTrans[k] =
                                            new bdd[m_usiMaxUnCon[k]/2];
                    m_pbdd_UnConVar[k] = new bdd[m_usiMaxUnCon[k]/2];
                    m_pbdd_UnConVarPrim[k] = new bdd[m_usiMaxUnCon[k]/2];
                    m_pbdd_UnConPlantVar[k] = new bdd[m_usiMaxUnCon[k]/2];
                    m_pbdd_UnConPlantVarPrim[k] =
                                              new bdd[m_usiMaxUnCon[k]/2];
                    m_pPair_UnCon[k] = new bddPair *[m_usiMaxUnCon[k]/2];
                    for (int iPair = 0; iPair < m_usiMaxUnCon[k]/2; iPair++)
                        m_pPair_UnCon[k][iPair] = NULL;
                    m_pPair_UnConPrim[k] = new bddPair *[m_usiMaxUnCon[k]/2];
                    for (int iPair = 0; iPair < m_usiMaxUnCon[k]/2; iPair++)
                        m_pPair_UnConPrim[k][iPair] = NULL;
                }
            }
        }
        
        
        map<int, bdd> bddTmpTransMap;  //<event_index, transitions>
        for (int i = 0, iIntf = 0; i < this->GetNumofDES(); i++)
        {
            //before compute transition predicate for each DES, clear it.
            bddTmpTransMap.clear();
            for (int j = 0; j < m_pDESArr[i]->GetNumofEvents(); j++)
            {
                bddTmpTransMap[(m_pDESArr[i]->GetEventsArr())[j]] = bddfalse;
            }
            
            //compute transition predicate for each DES
            for (int j = 0; j < m_pDESArr[i]->GetNumofStates(); j++)
            {
                TRANS::const_iterator ci = 
                                    (*(m_pDESArr[i]->GetTrans() + j)).begin();
                for (; ci != (*(m_pDESArr[i]->GetTrans() + j)).end(); ++ci)
                {
                    bddTmpTransMap[ci->first] |= fdd_ithvar(i * 2, j) &
                        fdd_ithvar(i * 2 + 1, ci->second);
                }
            }

            int iIndex = 0;
            unsigned short usiIndex = 0;
            int iSub = 0;
            EVENTSUB EventSub;
            //combine the current DES transition predicate to 
            //subsystem transition predicate
            map<int, bdd>::const_iterator ciTmp = bddTmpTransMap.begin();
            for (; ciTmp != bddTmpTransMap.end(); ++ciTmp)
            {
                if (ciTmp->first % 2 == 0)  //uncontrollable, start from 2
                {
                    //Compute index
                    pPrj->GenEventInfo(ciTmp->first, EventSub, iSub, usiIndex);
                    usiIndex = (usiIndex - 2) / 2;
                    if (EventSub == R_EVENT || EventSub == A_EVENT || EventSub == LD_EVENT)
                        iIndex = usiIndex + 
                                        m_piUArr[(int)EventSub - 1][iSub - 1];
                    else
                        iIndex = usiIndex;

                    //Compute transition predicates
                    if (m_pbdd_UnConVar[EventSub][iIndex] == bddfalse)
                    {
                        m_pbdd_UnConTrans[EventSub][iIndex] = bddtrue;
                        m_pbdd_UnConVar[EventSub][iIndex] = bddtrue;
                        m_pbdd_UnConVarPrim[EventSub][iIndex] = bddtrue;
                    }
                    
                    m_pbdd_UnConTrans[EventSub][iIndex] &= ciTmp->second; 
                    m_pbdd_UnConVar[EventSub][iIndex] &= fdd_ithset(i * 2);
                    m_pbdd_UnConVarPrim[EventSub][iIndex] &= 
                                                        fdd_ithset(i * 2 + 1);
                    
                    //compute uncontrollable plant vars and varprimes
                    if (m_pDESArr[i]->GetDESType() != SPEC_DES)
                    {
                        if (m_pbdd_UnConPlantVar[EventSub][iIndex] == bddfalse)
                        {
                            m_pbdd_UnConPlantTrans[EventSub][iIndex] = bddtrue; 
                            m_pbdd_UnConPlantVar[EventSub][iIndex] = bddtrue;
                            m_pbdd_UnConPlantVarPrim[EventSub][iIndex]= bddtrue;
                        }
                        m_pbdd_UnConPlantTrans[EventSub][iIndex] &= 
                                                            ciTmp->second; 
                        m_pbdd_UnConPlantVar[EventSub][iIndex] &= 
                                                            fdd_ithset(i * 2);
                        m_pbdd_UnConPlantVarPrim[EventSub][iIndex] &= 
                                                        fdd_ithset(i * 2 + 1);
                    }
                    //compute uncontrollable answer events transitions
                    if (m_pDESArr[i]->GetDESType() == INTERFACE_DES && 
                        EventSub == A_EVENT)
                        m_pbdd_UnConATrans[iIndex] = ciTmp->second; 

                    //compute uncontrollable low data events transitions
                    if (m_pDESArr[i]->GetDESType() == INTERFACE_DES &&
                        EventSub == LD_EVENT)
                        m_pbdd_UnConLDTrans[iIndex] = ciTmp->second;
                }
                else  //controllable, start from 1
                {
                    //Compute index
                    pPrj->GenEventInfo(ciTmp->first, EventSub, iSub, usiIndex);
                    usiIndex = (usiIndex - 1) / 2;
                    if (EventSub == R_EVENT || EventSub == A_EVENT || EventSub == LD_EVENT)
                        iIndex = usiIndex + 
                                    m_piCArr[(int)EventSub - 1][iSub - 1];
                    else
                        iIndex = usiIndex;
                        
                    //Compute transition predicate
                    if (m_pbdd_ConVar[EventSub][iIndex] == bddfalse)
                    {
                        m_pbdd_ConTrans[EventSub][iIndex] = bddtrue; 
                        m_pbdd_ConVar[EventSub][iIndex] = bddtrue;
                        m_pbdd_ConVarPrim[EventSub][iIndex] = bddtrue;
                    }
                    m_pbdd_ConTrans[EventSub][iIndex] &= ciTmp->second; 
                    m_pbdd_ConVar[EventSub][iIndex] &= fdd_ithset(i * 2);
                    m_pbdd_ConVarPrim[EventSub][iIndex] &=fdd_ithset(i * 2 + 1);

                    //compute controllable actual plant vars and varprimes
                    //note: can not use != SPEC_DES
                    if (m_pDESArr[i]->GetDESType() == PLANT_DES)
                    {
                        if (m_pbdd_ConPhysicVar[EventSub][iIndex] == bddfalse)
                        {
                            m_pbdd_ConPhysicVar[EventSub][iIndex] = bddtrue;
                            m_pbdd_ConPhysicVarPrim[EventSub][iIndex] = bddtrue;
                        }
                        m_pbdd_ConPhysicVar[EventSub][iIndex] &= 
                                                            fdd_ithset(i * 2);
                        m_pbdd_ConPhysicVarPrim[EventSub][iIndex] &= 
                                                        fdd_ithset(i * 2 + 1);
                    }
                    //compute controllable answer events transitions
                    if (m_pDESArr[i]->GetDESType() == INTERFACE_DES && 
                                                            EventSub == A_EVENT)
                        m_pbdd_ConATrans[iIndex] = ciTmp->second;

                    //compute controllable low data events transitions
                    if (m_pDESArr[i]->GetDESType() == INTERFACE_DES &&
                                                            EventSub == LD_EVENT)
                        m_pbdd_ConLDTrans[iIndex] = ciTmp->second;
                }
            }
            if (m_pDESArr[i]->GetDESType() == INTERFACE_DES)
            {
                m_pbdd_IVar[iIntf] = fdd_ithset(i * 2);
                m_pbdd_IVarPrim[iIntf] = fdd_ithset(i * 2 + 1);
                iIntf++;
            }
        }
        //compute m_pPair_UnCon, m_pPair_Con
        for (int k = 0; k < 5; k++)
        {       
            if (k != 3)
            {
                for (int j = 0; j < m_usiMaxUnCon[k]; j += 2)
                {
                    m_pPair_UnCon[k][j/2] = bdd_newpair();
                    SetBddPairs(m_pPair_UnCon[k][j/2], m_pbdd_UnConVar[k][j/2],
                                    m_pbdd_UnConVarPrim[k][j/2]);
                    m_pPair_UnConPrim[k][j/2] = bdd_newpair();
                    SetBddPairs(m_pPair_UnConPrim[k][j/2],
                                    m_pbdd_UnConVarPrim[k][j/2],
                                    m_pbdd_UnConVar[k][j/2]);
                }
                for (int j = 1; j < (unsigned short)(m_usiMaxCon[k] + 1); j += 2)
                //m_usiMaxCon[k] might be 0xFFFF
                {
                    m_pPair_Con[k][(j - 1) / 2] = bdd_newpair();
                    SetBddPairs(m_pPair_Con[k][(j - 1) / 2],
                                    m_pbdd_ConVar[k][(j - 1) / 2],
                                    m_pbdd_ConVarPrim[k][(j - 1) / 2]);
                    m_pPair_ConPrim[k][(j - 1) / 2] = bdd_newpair();
                    SetBddPairs(m_pPair_ConPrim[k][(j - 1) / 2],
                                    m_pbdd_ConVarPrim[k][(j - 1) / 2],
                                    m_pbdd_ConVar[k][(j - 1) / 2]);
                }
            }
        }
    }
    catch(...)
    {
        string sErr;
        sErr = "Error happens when initializing high-level ";
        sErr += " BDD!";
        pPrj->SetErr(sErr, HISC_SYSTEM_INITBDD);
        return -1;
    }
    return 0;
}


} //end of namespace BDDHISC
