/**CFile****************************************************************
FileName [mfsInt.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [The good old minimization with complete don't-cares.]
Synopsis [Internal declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: mfsInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __MFS_INT_H__
#define __MFS_INT_H__
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include "abc.h"
#include "extra.h"
#include "mfs.h"
#include "aig.h"
#include "cnf.h"
#include "satSolver.h"
#include "satStore.h"
#include "bdc.h"
#include "gia.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_HEADER_START
#define MFS_FANIN_MAX 12
typedef struct Mfs_Man_t_ Mfs_Man_t;
struct Mfs_Man_t_
{
// input data
Mfs_Par_t * pPars;
Abc_Ntk_t * pNtk;
Aig_Man_t * pCare;
Vec_Ptr_t * vSuppsInv;
int nFaninMax;
// intermeditate data for the node
Vec_Ptr_t * vRoots; // the roots of the window
Vec_Ptr_t * vSupp; // the support of the window
Vec_Ptr_t * vNodes; // the internal nodes of the window
Vec_Ptr_t * vDivs; // the divisors of the node
Vec_Int_t * vDivLits; // the SAT literals of divisor nodes
Vec_Int_t * vProjVarsCnf; // the projection variables
Vec_Int_t * vProjVarsSat; // the projection variables
// intermediate simulation data
Vec_Ptr_t * vDivCexes; // the counter-example for dividors
int nDivWords; // the number of words
int nCexes; // the numbe rof current counter-examples
int nSatCalls;
int nSatCexes;
/*
// intermediate AIG data
Gia_Man_t * pGia; // replica of the AIG in the new package
// Gia_Obj_t ** pSat2Gia; // mapping of PO SAT var into internal GIA nodes
Tas_Man_t * pTas; // the SAT solver
Vec_Int_t * vCex; // the counter-example
Vec_Ptr_t * vGiaLits; // literals given as assumptions
*/
// used for bidecomposition
Vec_Int_t * vTruth;
Bdc_Man_t * pManDec;
int nNodesDec;
int nNodesGained;
int nNodesGainedLevel;
// solving data
Aig_Man_t * pAigWin; // window AIG with constraints
Cnf_Dat_t * pCnf; // the CNF for the window
sat_solver * pSat; // the SAT solver used
Int_Man_t * pMan; // interpolation manager;
Vec_Int_t * vMem; // memory for intermediate SOPs
Vec_Vec_t * vLevels; // levelized structure for updating
Vec_Ptr_t * vMfsFanins; // the new set of fanins
int nTotConfLim; // total conflict limit
int nTotConfLevel; // total conflicts on this level
// switching activity
Vec_Int_t * vProbs;
// the result of solving
int nFanins; // the number of fanins
int nWords; // the number of words
int nCares; // the number of care minterms
unsigned uCare[(MFS_FANIN_MAX<=5)?1:1<<(MFS_FANIN_MAX-5)]; // the computed care-set
// performance statistics
int nNodesTried;
int nNodesResub;
int nMintsCare;
int nMintsTotal;
int nNodesBad;
int nTotalDivs;
int nTimeOuts;
int nTimeOutsLevel;
int nDcMints;
double dTotalRatios;
// node/edge stats
int nTotalNodesBeg;
int nTotalNodesEnd;
int nTotalEdgesBeg;
int nTotalEdgesEnd;
float TotalSwitchingBeg;
float TotalSwitchingEnd;
// statistics
int timeWin;
int timeDiv;
int timeAig;
int timeGia;
int timeCnf;
int timeSat;
int timeInt;
int timeTotal;
};
static inline float Abc_MfsObjProb( Mfs_Man_t * p, Abc_Obj_t * pObj ) { return (p->vProbs && pObj->Id < Vec_IntSize(p->vProbs))? Abc_Int2Float(Vec_IntEntry(p->vProbs,pObj->Id)) : 0.0; }
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== mfsDiv.c ==========================================================*/
extern Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDivMax );
/*=== mfsInter.c ==========================================================*/
extern sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands, int fInvert );
extern Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands );
extern int Abc_NtkMfsInterplateEval( Mfs_Man_t * p, int * pCands, int nCands );
/*=== mfsMan.c ==========================================================*/
extern Mfs_Man_t * Mfs_ManAlloc( Mfs_Par_t * pPars );
extern void Mfs_ManStop( Mfs_Man_t * p );
extern void Mfs_ManClean( Mfs_Man_t * p );
/*=== mfsResub.c ==========================================================*/
extern void Abc_NtkMfsPrintResubStats( Mfs_Man_t * p );
extern int Abc_NtkMfsEdgeSwapEval( Mfs_Man_t * p, Abc_Obj_t * pNode );
extern int Abc_NtkMfsEdgePower( Mfs_Man_t * p, Abc_Obj_t * pNode );
extern int Abc_NtkMfsResubNode( Mfs_Man_t * p, Abc_Obj_t * pNode );
extern int Abc_NtkMfsResubNode2( Mfs_Man_t * p, Abc_Obj_t * pNode );
/*=== mfsSat.c ==========================================================*/
extern int Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode );
extern int Abc_NtkAddOneHotness( Mfs_Man_t * p );
/*=== mfsStrash.c ==========================================================*/
extern Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode );
extern double Abc_NtkConstraintRatio( Mfs_Man_t * p, Abc_Obj_t * pNode );
/*=== mfsWin.c ==========================================================*/
extern Vec_Ptr_t * Abc_MfsComputeRoots( Abc_Obj_t * pNode, int nWinTfoMax, int nFanoutLimit );
/*=== mfsGia.c ==========================================================*/
extern void Abc_NtkMfsConstructGia( Mfs_Man_t * p );
extern void Abc_NtkMfsDeconstructGia( Mfs_Man_t * p );
extern int Abc_NtkMfsTryResubOnceGia( Mfs_Man_t * p, int * pCands, int nCands );
ABC_NAMESPACE_HEADER_END
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////