/**CFile****************************************************************
Copyright (c) The Regents of the University of California. All rights reserved.

Permission is hereby granted, without written agreement and without license or
royalty fees, to use, copy, modify, and distribute this software and its
documentation for any purpose, provided that the above copyright notice and
the following two paragraphs appear in all copies of this software.

IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF
THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING,
BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS,
AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE,
SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.


  FileName    [darInt.h]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [DAG-aware AIG rewriting.]

  Synopsis    [Internal declarations.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - April 28, 2007.]

  Revision    [$Id: darInt.h,v 1.00 2007/04/28 00:00:00 alanmi Exp $]

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

#ifndef __DAR_INT_H__
#define __DAR_INT_H__

#ifdef __cplusplus
extern "C" {
#endif 

////////////////////////////////////////////////////////////////////////
///                          INCLUDES                                ///
////////////////////////////////////////////////////////////////////////

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include <time.h>

//#include "bar.h"
#include "vec.h"
#include "aig.h"
#include "dar.h"

////////////////////////////////////////////////////////////////////////
///                         PARAMETERS                               ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                         BASIC TYPES                              ///
////////////////////////////////////////////////////////////////////////

typedef struct Dar_Man_t_            Dar_Man_t;
typedef struct Dar_Cut_t_            Dar_Cut_t;

// the AIG 4-cut
struct Dar_Cut_t_  // 6 words
{
    unsigned         uSign;          // cut signature
    unsigned         uTruth  : 16;   // the truth table of the cut function
    unsigned         Value   : 11;   // the value of the cut 
    unsigned         fBest   :  1;   // marks the best cut
    unsigned         fUsed   :  1;   // marks the cut currently in use
    unsigned         nLeaves :  3;   // the number of leaves
    int              pLeaves[4];     // the array of leaves
};

// the AIG manager
struct Dar_Man_t_
{
    // input data
    Dar_RwrPar_t *   pPars;          // rewriting parameters
    Aig_Man_t *      pAig;           // AIG manager 
    // various data members
    Aig_MmFixed_t *  pMemCuts;       // memory manager for cuts
    void *           pManCnf;        // CNF managers
    // current rewriting step
    Vec_Ptr_t *      vLeavesBest;    // the best set of leaves
    int              OutBest;        // the best output (in the library)
    int              OutNumBest;     // the best number of the output
    int              GainBest;       // the best gain
    int              LevelBest;      // the level of node with the best gain
    int              ClassBest;      // the equivalence class of the best replacement
    // function statistics
    int              nTotalSubgs;    // the total number of subgraphs tried
    int              ClassTimes[222];// the runtimes for each class
    int              ClassGains[222];// the gains for each class
    int              ClassSubgs[222];// the graphs for each class
    int              nCutMemUsed;    // memory used for cuts
    // rewriting statistics
    int              nNodesInit;     // the original number of nodes
    int              nNodesTried;    // the number of nodes attempted
    int              nCutsAll;       // all cut pairs
    int              nCutsTried;     // computed cuts
    int              nCutsUsed;      // used cuts
    int              nCutsBad;       // bad cuts due to absent fanin
    int              nCutsGood;      // good cuts
    int              nCutsSkipped;   // skipped bad cuts
    // timing statistics
    int              timeCuts;
    int              timeEval;
    int              timeOther;
    int              timeTotal;
    int              time1;
    int              time2;
};

static inline Dar_Cut_t *  Dar_ObjCuts( Aig_Obj_t * pObj )                         { return pObj->pData;    }
static inline void         Dar_ObjSetCuts( Aig_Obj_t * pObj, Dar_Cut_t * pCuts )   { assert( !Aig_ObjIsNone(pObj) ); pObj->pData = pCuts;   }

////////////////////////////////////////////////////////////////////////
///                      MACRO DEFINITIONS                           ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                          ITERATORS                               ///
////////////////////////////////////////////////////////////////////////

// iterator over all cuts of the node
#define Dar_ObjForEachCutAll( pObj, pCut, i )                                   \
    for ( (pCut) = Dar_ObjCuts(pObj), i = 0; i < (int)(pObj)->nCuts; i++, pCut++ ) 
#define Dar_ObjForEachCut( pObj, pCut, i )                                      \
    for ( (pCut) = Dar_ObjCuts(pObj), i = 0; i < (int)(pObj)->nCuts; i++, pCut++ ) if ( (pCut)->fUsed==0 ) {} else
// iterator over leaves of the cut
#define Dar_CutForEachLeaf( p, pCut, pLeaf, i )                                 \
    for ( i = 0; (i < (int)(pCut)->nLeaves) && (((pLeaf) = Aig_ManObj(p, (pCut)->pLeaves[i])), 1); i++ )

////////////////////////////////////////////////////////////////////////
///                    FUNCTION DECLARATIONS                         ///
////////////////////////////////////////////////////////////////////////

/*=== darBalance.c ========================================================*/
/*=== darCore.c ===========================================================*/
/*=== darCut.c ============================================================*/
extern void            Dar_ManCutsStart( Dar_Man_t * p );
extern void            Dar_ManCutsFree( Dar_Man_t * p );
extern Dar_Cut_t *     Dar_ObjComputeCuts_rec( Dar_Man_t * p, Aig_Obj_t * pObj );
extern Dar_Cut_t *     Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj );
/*=== darData.c ===========================================================*/
extern Vec_Int_t *     Dar_LibReadNodes();
extern Vec_Int_t *     Dar_LibReadOuts();
extern Vec_Int_t *     Dar_LibReadPrios();
/*=== darLib.c ============================================================*/
extern void            Dar_LibStart();
extern void            Dar_LibStop();
extern void            Dar_LibPrepare( int nSubgraphs );
extern void            Dar_LibReturnCanonicals( unsigned * pCanons );
extern void            Dar_LibEval( Dar_Man_t * p, Aig_Obj_t * pRoot, Dar_Cut_t * pCut, int Required );
extern Aig_Obj_t *     Dar_LibBuildBest( Dar_Man_t * p );
/*=== darMan.c ============================================================*/
extern Dar_Man_t *     Dar_ManStart( Aig_Man_t * pAig, Dar_RwrPar_t * pPars );
extern void            Dar_ManStop( Dar_Man_t * p );
extern void            Dar_ManPrintStats( Dar_Man_t * p );
/*=== darPrec.c ============================================================*/
extern char **         Dar_Permutations( int n );
extern void            Dar_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** puPerms, unsigned char ** puMap );

#ifdef __cplusplus
}
#endif

#endif

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////

