Skip to content

A
abc
Commit 1c26e2d2 by Alan Mishchenko
Options

Version abc70124

parent b1a913fb
Showing with 474 additions and 238 deletions
abc.dsp
...@@ -42,7 +42,7 @@ RSC=rc.exe ...@@ -42,7 +42,7 @@ RSC=rc.exe
# PROP Ignore_Export_Lib 0 # PROP Ignore_Export_Lib 0
# PROP Target_Dir "" # PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c # ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
# ADD CPP /nologo /W3 /GX /O2 /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\bsat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\opt\kit" /I "src\map\fpga" /I "src\map\if" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\aig\ivy" /I "src\aig\hop" /I "src\aig\rwt" /I "src\aig\deco" /I "src\aig\mem" /I "src\temp\esop" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c # ADD CPP /nologo /W3 /GX /O2 /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\bsat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\opt\kit" /I "src\opt\res" /I "src\map\fpga" /I "src\map\if" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\aig\ivy" /I "src\aig\hop" /I "src\aig\rwt" /I "src\aig\deco" /I "src\aig\mem" /I "src\temp\esop" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c
# ADD BASE RSC /l 0x409 /d "NDEBUG" # ADD BASE RSC /l 0x409 /d "NDEBUG"
# ADD RSC /l 0x409 /d "NDEBUG" # ADD RSC /l 0x409 /d "NDEBUG"
BSC32=bscmake.exe BSC32=bscmake.exe
...@@ -66,7 +66,7 @@ LINK32=link.exe ...@@ -66,7 +66,7 @@ LINK32=link.exe
# PROP Ignore_Export_Lib 0 # PROP Ignore_Export_Lib 0
# PROP Target_Dir "" # PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c # ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c
# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\bsat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\opt\kit" /I "src\map\fpga" /I "src\map\if" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\aig\ivy" /I "src\aig\hop" /I "src\aig\rwt" /I "src\aig\deco" /I "src\aig\mem" /I "src\temp\esop" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c # ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\bsat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\opt\kit" /I "src\opt\res" /I "src\map\fpga" /I "src\map\if" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\aig\ivy" /I "src\aig\hop" /I "src\aig\rwt" /I "src\aig\deco" /I "src\aig\mem" /I "src\temp\esop" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c
# SUBTRACT CPP /X # SUBTRACT CPP /X
# ADD BASE RSC /l 0x409 /d "_DEBUG" # ADD BASE RSC /l 0x409 /d "_DEBUG"
# ADD RSC /l 0x409 /d "_DEBUG" # ADD RSC /l 0x409 /d "_DEBUG"
......
abc.rc
...@@ -103,9 +103,11 @@ alias resyn2rs "b; rs -K 6; rw; rs -K 6 -N 2; rf; rs -K 8; b; rs -K 8 -N 2; r ...@@ -103,9 +103,11 @@ alias resyn2rs "b; rs -K 6; rw; rs -K 6 -N 2; rf; rs -K 8; b; rs -K 8 -N 2; r
alias compress2rs "b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; rs -K 8 -N 2 -l; rw -l; rs -K 10 -l; rwz -l; rs -K 10 -N 2 -l; b -l; rs -K 12 -l; rfz -l; rs -K 12 -N 2 -l; rwz -l; b -l" alias compress2rs "b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; rs -K 8 -N 2 -l; rw -l; rs -K 10 -l; rwz -l; rs -K 10 -N 2 -l; b -l; rs -K 12 -l; rfz -l; rs -K 12 -N 2 -l; rwz -l; b -l"
# temporaries # temporaries
#alias test "rvl th/lib.v; rvv th/t2.v" #alias t "rvl th/lib.v; rvv th/t2.v"
#alias test "so c/pure_sat/test.c" #alias t "so c/pure_sat/test.c"
#alias test "r c/14/csat_998.bench; st; ps" #alias t "r c/14/csat_998.bench; st; ps"
alias t0 "r res.blif; aig; mfs"
alias t "r res2.blif; aig; mfs"
src/base/abc/abc.h
...@@ -241,9 +241,9 @@ static inline unsigned Abc_InfoRandom() { return (( ...@@ -241,9 +241,9 @@ static inline unsigned Abc_InfoRandom() { return ((
static inline void Abc_InfoClear( unsigned * p, int nWords ) { memset( p, 0, sizeof(unsigned) * nWords ); } static inline void Abc_InfoClear( unsigned * p, int nWords ) { memset( p, 0, sizeof(unsigned) * nWords ); }
static inline void Abc_InfoFill( unsigned * p, int nWords ) { memset( p, 0xff, sizeof(unsigned) * nWords );} static inline void Abc_InfoFill( unsigned * p, int nWords ) { memset( p, 0xff, sizeof(unsigned) * nWords );}
static inline void Abc_InfoNot( unsigned * p, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = ~p[i]; } static inline void Abc_InfoNot( unsigned * p, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = ~p[i]; }
static inline int Abc_InfoIsZero( unsigned * p, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) if ( p[i] ) return 0; return 1; } static inline int Abc_InfoIsZero( unsigned * p, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) if ( p[i] ) return 0; return 1; }
static inline int Abc_InfoIsOne( unsigned * p, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) if ( !p[i] ) return 0; return 1; } static inline int Abc_InfoIsOne( unsigned * p, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) if ( ~p[i] ) return 0; return 1; }
static inline void Abc_InfoCopy( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = q[i]; } static inline void Abc_InfoCopy( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = q[i]; }
static inline void Abc_InfoAnd( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] &= q[i]; } static inline void Abc_InfoAnd( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] &= q[i]; }
static inline void Abc_InfoOr( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] |= q[i]; } static inline void Abc_InfoOr( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] |= q[i]; }
static inline void Abc_InfoXor( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] ^= q[i]; } static inline void Abc_InfoXor( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] ^= q[i]; }
......
src/base/abc/abcFunc.c
...@@ -830,10 +830,13 @@ Abc_Obj_t * Abc_ConvertAigToAig( Abc_Ntk_t * pNtkAig, Abc_Obj_t * pObjOld ) ...@@ -830,10 +830,13 @@ Abc_Obj_t * Abc_ConvertAigToAig( Abc_Ntk_t * pNtkAig, Abc_Obj_t * pObjOld )
pRoot = pObjOld->pData; pRoot = pObjOld->pData;
// check the case of a constant // check the case of a constant
if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) ) if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
return Abc_ObjNotCond( Abc_AigConst1(pNtkAig->pManFunc), Hop_IsComplement(pRoot) ); return Abc_ObjNotCond( Abc_AigConst1(pNtkAig), Hop_IsComplement(pRoot) );
// assign the fanin nodes // assign the fanin nodes
Abc_ObjForEachFanin( pObjOld, pFanin, i ) Abc_ObjForEachFanin( pObjOld, pFanin, i )
{
assert( pFanin->pCopy != NULL );
Hop_ManPi(pHopMan, i)->pData = pFanin->pCopy; Hop_ManPi(pHopMan, i)->pData = pFanin->pCopy;
}
// construct the AIG // construct the AIG
Abc_ConvertAigToAig_rec( pNtkAig, Hop_Regular(pRoot) ); Abc_ConvertAigToAig_rec( pNtkAig, Hop_Regular(pRoot) );
Hop_ConeUnmark_rec( Hop_Regular(pRoot) ); Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
......
src/base/abci/abc.c
...@@ -25,6 +25,7 @@ ...@@ -25,6 +25,7 @@
#include "cut.h" #include "cut.h"
#include "fpga.h" #include "fpga.h"
#include "if.h" #include "if.h"
#include "res.h"
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// DECLARATIONS /// /// DECLARATIONS ///
...@@ -2565,23 +2566,19 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -2565,23 +2566,19 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
FILE * pOut, * pErr; FILE * pOut, * pErr;
Abc_Ntk_t * pNtk; Abc_Ntk_t * pNtk;
Res_Par_t Pars, * pPars = &Pars;
int c; int c;
int nWindow;
int nSimWords;
int fVerbose;
int fVeryVerbose;
// external functions
extern int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, int nWindow, int nSimWords, int fVerbose, int fVeryVerbose );
pNtk = Abc_FrameReadNtk(pAbc); pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc); pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc); pErr = Abc_FrameReadErr(pAbc);
// set defaults // set defaults
nWindow = 33; pPars->nWindow = 33;
nSimWords = 8; pPars->nCands = 3;
fVerbose = 1; pPars->nSimWords = 8;
fVeryVerbose = 0; pPars->fVerbose = 1;
pPars->fVeryVerbose = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "WSvwh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "WSvwh" ) ) != EOF )
{ {
...@@ -2593,9 +2590,9 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -2593,9 +2590,9 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Command line switch \"-W\" should be followed by an integer.\n" ); fprintf( pErr, "Command line switch \"-W\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
nWindow = atoi(argv[globalUtilOptind]); pPars->nWindow = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
if ( nWindow < 1 || nWindow > 99 ) if ( pPars->nWindow < 1 || pPars->nWindow > 99 )
goto usage; goto usage;
break; break;
case 'S': case 'S':
...@@ -2604,16 +2601,16 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -2604,16 +2601,16 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Command line switch \"-S\" should be followed by an integer.\n" ); fprintf( pErr, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage; goto usage;
} }
nSimWords = atoi(argv[globalUtilOptind]); pPars->nSimWords = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
if ( nSimWords < 2 || nSimWords > 256 ) if ( pPars->nSimWords < 1 || pPars->nSimWords > 256 )
goto usage; goto usage;
break; break;
case 'v': case 'v':
fVerbose ^= 1; pPars->fVerbose ^= 1;
break; break;
case 'w': case 'w':
fVeryVerbose ^= 1; pPars->fVeryVerbose ^= 1;
break; break;
case 'h': case 'h':
goto usage; goto usage;
...@@ -2634,7 +2631,7 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -2634,7 +2631,7 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
} }
// modify the current network // modify the current network
if ( !Abc_NtkResynthesize( pNtk, nWindow, nSimWords, fVerbose, fVeryVerbose ) ) if ( !Abc_NtkResynthesize( pNtk, pPars ) )
{ {
fprintf( pErr, "Resynthesis has failed.\n" ); fprintf( pErr, "Resynthesis has failed.\n" );
return 1; return 1;
...@@ -2642,13 +2639,13 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -2642,13 +2639,13 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: usage:
fprintf( pErr, "usage: mfs [-W <NM>] [-S <n>] [-vwh]\n" ); fprintf( pErr, "usage: mfs [-W <NM>] [-S <num>] [-vwh]\n" );
fprintf( pErr, "\t performs resubstitution-based resynthesis with don't-cares\n" ); fprintf( pErr, "\t performs resubstitution-based resynthesis with don't-cares\n" );
fprintf( pErr, "\t-W <NM> : specifies the windowing paramters (00 < NM <= 99) [default = %d%d]\n", nWindow/10, nWindow%10 ); fprintf( pErr, "\t-W <NM> : specifies the windowing paramters (00 < NM <= 99) [default = %d%d]\n", pPars->nWindow/10, pPars->nWindow%10 );
fprintf( pErr, "\t-S <n> : specifies the number of simulation words (2 <= n <= 256) [default = %d]\n", nSimWords ); fprintf( pErr, "\t-S <num> : specifies the number of simulation words (1 <= n <= 256) [default = %d]\n", pPars->nSimWords );
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( pErr, "\t-w : toggle printout subgraph statistics [default = %s]\n", fVeryVerbose? "yes": "no" ); fprintf( pErr, "\t-w : toggle printout subgraph statistics [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n"); fprintf( pErr, "\t-h : print the command usage\n");
return 1; return 1;
} }
......
src/opt/res/res.h
...@@ -37,50 +37,17 @@ extern "C" { ...@@ -37,50 +37,17 @@ extern "C" {
/// BASIC TYPES /// /// BASIC TYPES ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
typedef struct Res_Win_t_ Res_Win_t; typedef struct Res_Par_t_ Res_Par_t;
struct Res_Win_t_ struct Res_Par_t_
{ {
// the general data // general parameters
int nWinTfiMax; // the fanin levels int nWindow; // window size
int nWinTfoMax; // the fanout levels int nSimWords; // the number of simulation words
int nLevLeaves; // the level where leaves begin int nCands; // the number of candidates to try
int nLevDivMax; // the maximum divisor level int fVerbose; // enable basic stats
Abc_Obj_t * pNode; // the node in the center int fVeryVerbose; // enable detailed stats
// the window data
Vec_Vec_t * vLevels; // nodes by level
Vec_Ptr_t * vLeaves; // leaves of the window
Vec_Ptr_t * vRoots; // roots of the window
Vec_Ptr_t * vDivs; // the candidate divisors of the node
}; };
typedef struct Res_Sim_t_ Res_Sim_t;
struct Res_Sim_t_
{
Abc_Ntk_t * pAig; // AIG for simulation
// simulation parameters
int nWords; // the number of simulation words
int nPats; // the number of patterns
int nWordsOut; // the number of simulation words in the output patterns
int nPatsOut; // the number of patterns in the output patterns
// simulation info
Vec_Ptr_t * vPats; // input simulation patterns
Vec_Ptr_t * vPats0; // input simulation patterns
Vec_Ptr_t * vPats1; // input simulation patterns
Vec_Ptr_t * vOuts; // output simulation info
int nPats0; // the number of 0-patterns accumulated
int nPats1; // the number of 1-patterns accumulated
// resub candidates
Vec_Vec_t * vCands; // resubstitution candidates
};
// adds one node to the window
static inline void Res_WinAddNode( Res_Win_t * p, Abc_Obj_t * pObj )
{
assert( !pObj->fMarkA );
pObj->fMarkA = 1;
Vec_VecPush( p->vLevels, pObj->Level, pObj );
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS /// /// MACRO DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
...@@ -89,26 +56,8 @@ static inline void Res_WinAddNode( Res_Win_t * p, Abc_Obj_t * pObj ) ...@@ -89,26 +56,8 @@ static inline void Res_WinAddNode( Res_Win_t * p, Abc_Obj_t * pObj )
/// FUNCTION DECLARATIONS /// /// FUNCTION DECLARATIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/*=== resDivs.c ==========================================================*/ /*=== resCore.c ==========================================================*/
extern void Res_WinDivisors( Res_Win_t * p, int nLevDivMax ); extern int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, Res_Par_t * pPars );
extern int Res_WinVisitMffc( Res_Win_t * p );
/*=== resFilter.c ==========================================================*/
extern Vec_Vec_t * Res_FilterCandidates( Res_Win_t * pWin, Res_Sim_t * pSim );
/*=== resSat.c ==========================================================*/
extern void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins );
/*=== resSim.c ==========================================================*/
extern Res_Sim_t * Res_SimAlloc( int nWords );
extern void Res_SimFree( Res_Sim_t * p );
extern int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig );
/*=== resStrash.c ==========================================================*/
extern Abc_Ntk_t * Res_WndStrash( Res_Win_t * p );
/*=== resWnd.c ==========================================================*/
extern void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc, Vec_Vec_t * vLevels );
/*=== resWnd.c ==========================================================*/
extern Res_Win_t * Res_WinAlloc();
extern void Res_WinFree( Res_Win_t * p );
extern int Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t * p );
extern void Res_WinVisitNodeTfo( Res_Win_t * p );
#ifdef __cplusplus #ifdef __cplusplus
......
src/opt/res/resDivs.c
...@@ -19,7 +19,7 @@ ...@@ -19,7 +19,7 @@
***********************************************************************/ ***********************************************************************/
#include "abc.h" #include "abc.h"
#include "res.h" #include "resInt.h"
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// DECLARATIONS /// /// DECLARATIONS ///
...@@ -56,11 +56,12 @@ void Res_WinDivisors( Res_Win_t * p, int nLevDivMax ) ...@@ -56,11 +56,12 @@ void Res_WinDivisors( Res_Win_t * p, int nLevDivMax )
// prepare the new trav ID // prepare the new trav ID
Abc_NtkIncrementTravId( p->pNode->pNtk ); Abc_NtkIncrementTravId( p->pNode->pNtk );
// mark the TFO of the node (does not increment trav ID) // mark the TFO of the node (does not increment trav ID)
Res_WinVisitNodeTfo( p ); Res_WinSweepLeafTfo_rec( p->pNode, p->nLevDivMax, NULL );
// mark the MFFC of the node (does not increment trav ID) // mark the MFFC of the node (does not increment trav ID)
Res_WinVisitMffc( p ); Res_WinVisitMffc( p );
// go through all the legal levels and check if their fanouts can be divisors // go through all the legal levels and check if their fanouts can be divisors
p->nDivsPlus = 0;
Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, 0, p->nLevDivMax - 1 ) Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, 0, p->nLevDivMax - 1 )
{ {
// skip nodes in the TFO or in the MFFC of node // skip nodes in the TFO or in the MFFC of node
...@@ -69,15 +70,15 @@ void Res_WinDivisors( Res_Win_t * p, int nLevDivMax ) ...@@ -69,15 +70,15 @@ void Res_WinDivisors( Res_Win_t * p, int nLevDivMax )
// consider fanouts of this node // consider fanouts of this node
Abc_ObjForEachFanout( pObj, pFanout, f ) Abc_ObjForEachFanout( pObj, pFanout, f )
{ {
// skip nodes that are already added
if ( pFanout->fMarkA )
continue;
// skip COs // skip COs
if ( !Abc_ObjIsNode(pFanout) ) if ( !Abc_ObjIsNode(pFanout) )
continue; continue;
// skip nodes in the TFO or in the MFFC of node // skip nodes in the TFO or in the MFFC of node
if ( Abc_NodeIsTravIdCurrent(pFanout) ) if ( Abc_NodeIsTravIdCurrent(pFanout) )
continue; continue;
// skip nodes that are already added
if ( pFanout->fMarkA )
continue;
// skip nodes with large level // skip nodes with large level
if ( (int)pFanout->Level > p->nLevDivMax ) if ( (int)pFanout->Level > p->nLevDivMax )
continue; continue;
...@@ -85,10 +86,11 @@ void Res_WinDivisors( Res_Win_t * p, int nLevDivMax ) ...@@ -85,10 +86,11 @@ void Res_WinDivisors( Res_Win_t * p, int nLevDivMax )
Abc_ObjForEachFanin( pFanout, pFanin, m ) Abc_ObjForEachFanin( pFanout, pFanin, m )
if ( !pFanin->fMarkA ) if ( !pFanin->fMarkA )
break; break;
if ( m < Abc_ObjFaninNum(pFanin) ) if ( m < Abc_ObjFaninNum(pFanout) )
continue; continue;
// add the node // add the node
Res_WinAddNode( p, pFanout ); Res_WinAddNode( p, pFanout );
p->nDivsPlus++;
} }
} }
...@@ -100,8 +102,8 @@ void Res_WinDivisors( Res_Win_t * p, int nLevDivMax ) ...@@ -100,8 +102,8 @@ void Res_WinDivisors( Res_Win_t * p, int nLevDivMax )
// collect the divisors below the line // collect the divisors below the line
Vec_PtrClear( p->vDivs ); Vec_PtrClear( p->vDivs );
// collect the node fanins first // collect the node fanins first and mark the fanins
Abc_ObjForEachFanin( pObj, pFanin, m ) Abc_ObjForEachFanin( p->pNode, pFanin, m )
{ {
Vec_PtrPush( p->vDivs, pFanin ); Vec_PtrPush( p->vDivs, pFanin );
Abc_NodeSetTravIdCurrent( pFanin ); Abc_NodeSetTravIdCurrent( pFanin );
...@@ -114,6 +116,9 @@ void Res_WinDivisors( Res_Win_t * p, int nLevDivMax ) ...@@ -114,6 +116,9 @@ void Res_WinDivisors( Res_Win_t * p, int nLevDivMax )
Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, p->nLevLeaves, p->nLevDivMax ) Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, p->nLevLeaves, p->nLevDivMax )
if ( !Abc_NodeIsTravIdCurrent(pObj) ) if ( !Abc_NodeIsTravIdCurrent(pObj) )
Vec_PtrPush( p->vDivs, pObj ); Vec_PtrPush( p->vDivs, pObj );
// verify the resulting window
// Res_WinVerify( p );
} }
/**Function************************************************************* /**Function*************************************************************
......
src/opt/res/resFilter.c
...@@ -19,19 +19,21 @@ ...@@ -19,19 +19,21 @@
***********************************************************************/ ***********************************************************************/
#include "abc.h" #include "abc.h"
#include "res.h" #include "resInt.h"
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// DECLARATIONS /// /// DECLARATIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
static unsigned * Res_FilterCollectFaninInfo( Res_Win_t * pWin, Res_Sim_t * pSim, unsigned uMask );
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/**Function************************************************************* /**Function*************************************************************
Synopsis [] Synopsis [Finds sets of feasible candidates.]
Description [] Description []
...@@ -40,26 +42,78 @@ ...@@ -40,26 +42,78 @@
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Vec_Vec_t * Res_FilterCandidates( Res_Win_t * pWin, Res_Sim_t * pSim ) int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs )
{ {
Abc_Obj_t * pFanin, * pFanin2;
unsigned * pInfo; unsigned * pInfo;
Abc_Obj_t * pFanin; int Counter, RetValue, i, k;
int i, RetValue;
// check that the info the node is one // check that the info the node is one
pInfo = Vec_PtrEntry( pSim->vOuts, 1 ); pInfo = Vec_PtrEntry( pSim->vOuts, 1 );
RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut ); RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
if ( RetValue == 0 ) if ( RetValue == 0 )
printf( "Failed 1!" ); printf( "Failed 1!" );
// collect the fanin info // collect the fanin info
pInfo = Vec_PtrEntry( pSim->vOuts, 0 ); pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~0 );
Abc_InfoClear( pInfo, pSim->nWordsOut );
Abc_ObjForEachFanin( pWin->pNode, pFanin, i )
Abc_InfoOr( pInfo, Vec_PtrEntry( pSim->vOuts, 2+i ), pSim->nWordsOut );
// check that the simulation info is constant 1
RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut ); RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
if ( RetValue == 0 ) if ( RetValue == 0 )
printf( "Failed 2!" ); printf( "Failed 2!" );
return NULL;
// try removing fanins
// printf( "Fanins: " );
Counter = 0;
Vec_VecClear( vResubs );
Abc_ObjForEachFanin( pWin->pNode, pFanin, i )
{
pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~(1 << i) );
RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
if ( RetValue )
{
// printf( "Node %4d. Removing fanin %4d.\n", pWin->pNode->Id, Abc_ObjFaninId(pWin->pNode, i) );
// collect the nodes
Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) );
Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) );
Abc_ObjForEachFanin( pWin->pNode, pFanin2, k )
{
if ( k != i )
Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) );
}
Counter++;
}
if ( Counter == Vec_VecSize(vResubs) )
break;
// printf( "%d", RetValue );
}
// printf( "\n\n" );
return Counter;
}
/**Function*************************************************************
Synopsis [Finds sets of feasible candidates.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned * Res_FilterCollectFaninInfo( Res_Win_t * pWin, Res_Sim_t * pSim, unsigned uMask )
{
Abc_Obj_t * pFanin;
unsigned * pInfo;
int i;
pInfo = Vec_PtrEntry( pSim->vOuts, 0 );
Abc_InfoClear( pInfo, pSim->nWordsOut );
Abc_ObjForEachFanin( pWin->pNode, pFanin, i )
{
if ( uMask & (1 << i) )
Abc_InfoOr( pInfo, Vec_PtrEntry(pSim->vOuts, 2+i), pSim->nWordsOut );
}
return pInfo;
} }
......
src/opt/res/resInt.h 0 → 100644
/**CFile****************************************************************
FileName [resInt.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Resynthesis package.]
Synopsis [Internal declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - January 15, 2007.]
Revision [$Id: resInt.h,v 1.00 2007/01/15 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __RES_INT_H__
#define __RES_INT_H__
#ifdef __cplusplus
extern "C" {
#endif
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include "res.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Res_Win_t_ Res_Win_t;
struct Res_Win_t_
{
// the general data
int nWinTfiMax; // the fanin levels
int nWinTfoMax; // the fanout levels
int nLevLeaves; // the level where leaves begin
int nLevDivMax; // the maximum divisor level
int nDivsPlus; // the number of additional divisors
Abc_Obj_t * pNode; // the node in the center
// the window data
Vec_Vec_t * vLevels; // nodes by level
Vec_Ptr_t * vLeaves; // leaves of the window
Vec_Ptr_t * vRoots; // roots of the window
Vec_Ptr_t * vDivs; // the candidate divisors of the node
};
typedef struct Res_Sim_t_ Res_Sim_t;
struct Res_Sim_t_
{
Abc_Ntk_t * pAig; // AIG for simulation
// simulation parameters
int nWords; // the number of simulation words
int nPats; // the number of patterns
int nWordsOut; // the number of simulation words in the output patterns
int nPatsOut; // the number of patterns in the output patterns
// simulation info
Vec_Ptr_t * vPats; // input simulation patterns
Vec_Ptr_t * vPats0; // input simulation patterns
Vec_Ptr_t * vPats1; // input simulation patterns
Vec_Ptr_t * vOuts; // output simulation info
int nPats0; // the number of 0-patterns accumulated
int nPats1; // the number of 1-patterns accumulated
// resub candidates
Vec_Vec_t * vCands; // resubstitution candidates
};
// adds one node to the window
static inline void Res_WinAddNode( Res_Win_t * p, Abc_Obj_t * pObj )
{
assert( !pObj->fMarkA );
pObj->fMarkA = 1;
Vec_VecPush( p->vLevels, pObj->Level, pObj );
}
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== resDivs.c ==========================================================*/
extern void Res_WinDivisors( Res_Win_t * p, int nLevDivMax );
extern int Res_WinVisitMffc( Res_Win_t * p );
/*=== resFilter.c ==========================================================*/
extern int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs );
/*=== resSat.c ==========================================================*/
extern void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins );
/*=== resSim.c ==========================================================*/
extern Res_Sim_t * Res_SimAlloc( int nWords );
extern void Res_SimFree( Res_Sim_t * p );
extern int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig );
/*=== resStrash.c ==========================================================*/
extern Abc_Ntk_t * Res_WndStrash( Res_Win_t * p );
/*=== resWnd.c ==========================================================*/
extern void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc, Vec_Vec_t * vLevels );
/*=== resWnd.c ==========================================================*/
extern Res_Win_t * Res_WinAlloc();
extern void Res_WinFree( Res_Win_t * p );
extern void Res_WinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit, Abc_Obj_t * pNode );
extern int Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t * p );
#ifdef __cplusplus
}
#endif
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/opt/res/resSat.c
...@@ -19,7 +19,7 @@ ...@@ -19,7 +19,7 @@
***********************************************************************/ ***********************************************************************/
#include "abc.h" #include "abc.h"
#include "res.h" #include "resInt.h"
#include "hop.h" #include "hop.h"
#include "satSolver.h" #include "satSolver.h"
...@@ -27,7 +27,7 @@ ...@@ -27,7 +27,7 @@
/// DECLARATIONS /// /// DECLARATIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
extern int Res_SatAddConst1( sat_solver * pSat, int iVar ); extern int Res_SatAddConst1( sat_solver * pSat, int iVar, int fCompl );
extern int Res_SatAddEqual( sat_solver * pSat, int iVar0, int iVar1, int fCompl ); extern int Res_SatAddEqual( sat_solver * pSat, int iVar0, int iVar1, int fCompl );
extern int Res_SatAddAnd( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 ); extern int Res_SatAddAnd( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 );
...@@ -48,70 +48,85 @@ extern int Res_SatAddAnd( sat_solver * pSat, int iVar, int iVar0, int iVar1, int ...@@ -48,70 +48,85 @@ extern int Res_SatAddAnd( sat_solver * pSat, int iVar, int iVar0, int iVar1, int
***********************************************************************/ ***********************************************************************/
void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins ) void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins )
{ {
void * pCnf; void * pCnf = NULL;
sat_solver * pSat; sat_solver * pSat;
Vec_Ptr_t * vNodes; Vec_Ptr_t * vNodes;
Abc_Obj_t * pObj; Abc_Obj_t * pObj;
int i, nNodes, status; int i, nNodes, status;
// make sure the constant node is not involved // make sure fanins contain POs of the AIG
assert( Abc_ObjFanoutNum(Abc_AigConst1(pAig)) == 0 ); pObj = Vec_PtrEntry( vFanins, 0 );
assert( pObj->pNtk == pAig && Abc_ObjIsPo(pObj) );
// collect reachable nodes // collect reachable nodes
vNodes = Abc_NtkDfsNodes( pAig, (Abc_Obj_t **)vFanins->pArray, vFanins->nSize ); vNodes = Abc_NtkDfsNodes( pAig, (Abc_Obj_t **)vFanins->pArray, vFanins->nSize );
// assign unique numbers to each node // assign unique numbers to each node
nNodes = 0; nNodes = 0;
Abc_AigConst1(pAig)->pCopy = (void *)nNodes++;
Abc_NtkForEachPi( pAig, pObj, i ) Abc_NtkForEachPi( pAig, pObj, i )
pObj->pCopy = (void *)nNodes++; pObj->pCopy = (void *)nNodes++;
Vec_PtrForEachEntry( vNodes, pObj, i ) Vec_PtrForEachEntry( vNodes, pObj, i )
pObj->pCopy = (void *)nNodes++; pObj->pCopy = (void *)nNodes++;
Vec_PtrForEachEntry( vFanins, pObj, i ) Vec_PtrForEachEntry( vFanins, pObj, i ) // useful POs
pObj->pCopy = (void *)nNodes++; pObj->pCopy = (void *)nNodes++;
// start the solver // start the solver
pSat = sat_solver_new(); pSat = sat_solver_new();
sat_solver_store_alloc( pSat ); sat_solver_store_alloc( pSat );
// add clause for AND gates // add clause for the constant node
Res_SatAddConst1( pSat, (int)Abc_AigConst1(pAig)->pCopy, 0 );
// add clauses for AND gates
Vec_PtrForEachEntry( vNodes, pObj, i ) Vec_PtrForEachEntry( vNodes, pObj, i )
Res_SatAddAnd( pSat, (int)pObj->pCopy, Res_SatAddAnd( pSat, (int)pObj->pCopy,
(int)Abc_ObjFanin0(pObj)->pCopy, (int)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) ); (int)Abc_ObjFanin0(pObj)->pCopy, (int)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
// add clauses for the POs Vec_PtrFree( vNodes );
// add clauses for POs
Vec_PtrForEachEntry( vFanins, pObj, i ) Vec_PtrForEachEntry( vFanins, pObj, i )
Res_SatAddEqual( pSat, (int)pObj->pCopy, Res_SatAddEqual( pSat, (int)pObj->pCopy,
(int)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) ); (int)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
// add trivial clauses // add trivial clauses
pObj = Vec_PtrEntry(vFanins, 0); pObj = Vec_PtrEntry(vFanins, 0);
Res_SatAddConst1( pSat, (int)pObj->pCopy ); Res_SatAddConst1( pSat, (int)pObj->pCopy, 0 ); // care-set
pObj = Vec_PtrEntry(vFanins, 1); pObj = Vec_PtrEntry(vFanins, 1);
Res_SatAddConst1( pSat, (int)pObj->pCopy ); Res_SatAddConst1( pSat, (int)pObj->pCopy, 0 ); // on-set
// bookmark the clauses of A // bookmark the clauses of A
sat_solver_store_mark_clauses_a( pSat ); sat_solver_store_mark_clauses_a( pSat );
// duplicate the clauses // duplicate the clauses
pObj = Vec_PtrEntry(vFanins, 1); pObj = Vec_PtrEntry(vFanins, 1);
Sat_SolverDoubleClauses( pSat, (int)pObj->pCopy ); Sat_SolverDoubleClauses( pSat, (int)pObj->pCopy );
// add the equality clauses // add the equality constraints
Vec_PtrForEachEntryStart( vFanins, pObj, i, 2 ) Vec_PtrForEachEntryStart( vFanins, pObj, i, 2 )
Res_SatAddEqual( pSat, (int)pObj->pCopy, ((int)pObj->pCopy) + nNodes, 0 ); Res_SatAddEqual( pSat, (int)pObj->pCopy, ((int)pObj->pCopy) + nNodes, 0 );
// bookmark the roots // bookmark the roots
sat_solver_store_mark_roots( pSat ); sat_solver_store_mark_roots( pSat );
Vec_PtrFree( vNodes );
// solve the problem // solve the problem
status = sat_solver_solve( pSat, NULL, NULL, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 ); status = sat_solver_solve( pSat, NULL, NULL, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 );
if ( status == l_False ) if ( status == l_False )
{
pCnf = sat_solver_store_release( pSat ); pCnf = sat_solver_store_release( pSat );
// printf( "unsat\n" );
}
else if ( status == l_True ) else if ( status == l_True )
pCnf = NULL; {
// printf( "sat\n" );
}
else else
pCnf = NULL; {
// printf( "undef\n" );
}
sat_solver_delete( pSat ); sat_solver_delete( pSat );
return pCnf; return pCnf;
} }
/**Function************************************************************* /**Function*************************************************************
Synopsis [Loads two-input AND-gate.] Synopsis [Asserts equality of the variable to a constant.]
Description [] Description []
...@@ -120,9 +135,9 @@ void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins ) ...@@ -120,9 +135,9 @@ void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Res_SatAddConst1( sat_solver * pSat, int iVar ) int Res_SatAddConst1( sat_solver * pSat, int iVar, int fCompl )
{ {
lit Lit = lit_var(iVar); lit Lit = toLitCond( iVar, fCompl );
if ( !sat_solver_addclause( pSat, &Lit, &Lit + 1 ) ) if ( !sat_solver_addclause( pSat, &Lit, &Lit + 1 ) )
return 0; return 0;
return 1; return 1;
...@@ -130,7 +145,7 @@ int Res_SatAddConst1( sat_solver * pSat, int iVar ) ...@@ -130,7 +145,7 @@ int Res_SatAddConst1( sat_solver * pSat, int iVar )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Loads two-input AND-gate.] Synopsis [Asserts equality of two variables.]
Description [] Description []
...@@ -158,7 +173,7 @@ int Res_SatAddEqual( sat_solver * pSat, int iVar0, int iVar1, int fCompl ) ...@@ -158,7 +173,7 @@ int Res_SatAddEqual( sat_solver * pSat, int iVar0, int iVar1, int fCompl )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Loads two-input AND-gate.] Synopsis [Adds constraints for the two-input AND-gate.]
Description [] Description []
......
src/opt/res/resSim.c
...@@ -19,7 +19,7 @@ ...@@ -19,7 +19,7 @@
***********************************************************************/ ***********************************************************************/
#include "abc.h" #include "abc.h"
#include "res.h" #include "resInt.h"
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// DECLARATIONS /// /// DECLARATIONS ///
...@@ -38,7 +38,7 @@ ...@@ -38,7 +38,7 @@
SideEffects [] SideEffects []
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Res_Sim_t * Res_SimAlloc( int nWords ) Res_Sim_t * Res_SimAlloc( int nWords )
{ {
...@@ -57,8 +57,6 @@ Res_Sim_t * Res_SimAlloc( int nWords ) ...@@ -57,8 +57,6 @@ Res_Sim_t * Res_SimAlloc( int nWords )
p->vOuts = Vec_PtrAllocSimInfo( 128, p->nWordsOut ); p->vOuts = Vec_PtrAllocSimInfo( 128, p->nWordsOut );
// resub candidates // resub candidates
p->vCands = Vec_VecStart( 16 ); p->vCands = Vec_VecStart( 16 );
// set siminfo for the constant node
Abc_InfoFill( Vec_PtrEntry(p->vPats,0), p->nWords );
return p; return p;
} }
...@@ -75,6 +73,8 @@ Res_Sim_t * Res_SimAlloc( int nWords ) ...@@ -75,6 +73,8 @@ Res_Sim_t * Res_SimAlloc( int nWords )
***********************************************************************/ ***********************************************************************/
void Res_SimAdjust( Res_Sim_t * p, Abc_Ntk_t * pAig ) void Res_SimAdjust( Res_Sim_t * p, Abc_Ntk_t * pAig )
{ {
srand( 0xABC );
assert( Abc_NtkIsStrash(pAig) ); assert( Abc_NtkIsStrash(pAig) );
p->pAig = pAig; p->pAig = pAig;
if ( Vec_PtrSize(p->vPats) < Abc_NtkObjNumMax(pAig)+1 ) if ( Vec_PtrSize(p->vPats) < Abc_NtkObjNumMax(pAig)+1 )
...@@ -125,44 +125,6 @@ void Res_SimFree( Res_Sim_t * p ) ...@@ -125,44 +125,6 @@ void Res_SimFree( Res_Sim_t * p )
free( p ); free( p );
} }
/**Function*************************************************************
Synopsis [Free simulation engine.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Res_SimReportOne( Res_Sim_t * p )
{
unsigned * pInfoCare, * pInfoNode;
int i, nDcs, nOnes, nZeros;
pInfoCare = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 0)->Id );
pInfoNode = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 1)->Id );
nDcs = nOnes = nZeros = 0;
for ( i = 0; i < p->nPats; i++ )
{
// skip don't-care patterns
if ( !Abc_InfoHasBit(pInfoCare, i) )
{
nDcs++;
continue;
}
// separate offset and onset patterns
if ( !Abc_InfoHasBit(pInfoNode, i) )
nZeros++;
else
nOnes++;
}
printf( "Onset = %3d (%6.2f %%) ", nOnes, 100.0*nOnes/p->nPats );
printf( "Offset = %3d (%6.2f %%) ", nZeros, 100.0*nZeros/p->nPats );
printf( "Dcset = %3d (%6.2f %%) ", nDcs, 100.0*nDcs/p->nPats );
printf( "\n" );
}
/**Function************************************************************* /**Function*************************************************************
...@@ -292,6 +254,7 @@ void Res_SimPerformRound( Res_Sim_t * p ) ...@@ -292,6 +254,7 @@ void Res_SimPerformRound( Res_Sim_t * p )
{ {
Abc_Obj_t * pObj; Abc_Obj_t * pObj;
int i; int i;
Abc_InfoFill( Vec_PtrEntry(p->vPats,0), p->nWords );
Abc_AigForEachAnd( p->pAig, pObj, i ) Abc_AigForEachAnd( p->pAig, pObj, i )
Res_SimPerformOne( pObj, p->vPats, p->nWords ); Res_SimPerformOne( pObj, p->vPats, p->nWords );
Abc_NtkForEachPo( p->pAig, pObj, i ) Abc_NtkForEachPo( p->pAig, pObj, i )
...@@ -313,14 +276,17 @@ void Res_SimProcessPats( Res_Sim_t * p ) ...@@ -313,14 +276,17 @@ void Res_SimProcessPats( Res_Sim_t * p )
{ {
Abc_Obj_t * pObj; Abc_Obj_t * pObj;
unsigned * pInfoCare, * pInfoNode; unsigned * pInfoCare, * pInfoNode;
int i, j; int i, j, nDcs = 0;
pInfoCare = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 0)->Id ); pInfoCare = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 0)->Id );
pInfoNode = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 1)->Id ); pInfoNode = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 1)->Id );
for ( i = 0; i < p->nPats; i++ ) for ( i = 0; i < p->nPats; i++ )
{ {
// skip don't-care patterns // skip don't-care patterns
if ( !Abc_InfoHasBit(pInfoCare, i) ) if ( !Abc_InfoHasBit(pInfoCare, i) )
{
nDcs++;
continue; continue;
}
// separate offset and onset patterns // separate offset and onset patterns
if ( !Abc_InfoHasBit(pInfoNode, i) ) if ( !Abc_InfoHasBit(pInfoNode, i) )
{ {
...@@ -357,14 +323,21 @@ void Res_SimProcessPats( Res_Sim_t * p ) ...@@ -357,14 +323,21 @@ void Res_SimProcessPats( Res_Sim_t * p )
void Res_SimPadSimInfo( Vec_Ptr_t * vPats, int nPats, int nWords ) void Res_SimPadSimInfo( Vec_Ptr_t * vPats, int nPats, int nWords )
{ {
unsigned * pInfo; unsigned * pInfo;
int i, w, iWords, nBits; int i, w, iWords;
assert( nPats > 0 && nPats < nWords * 8 * (int) sizeof(unsigned) );
// pad the first word
if ( nPats < 8 * sizeof(unsigned) )
{
Vec_PtrForEachEntry( vPats, pInfo, i )
if ( pInfo[0] & 1 )
pInfo[0] |= ((~0) << nPats);
nPats = 8 * sizeof(unsigned);
}
// pad the empty words
iWords = nPats / (8 * sizeof(unsigned)); iWords = nPats / (8 * sizeof(unsigned));
nBits = nPats % (8 * sizeof(unsigned));
if ( iWords == nWords )
return;
Vec_PtrForEachEntry( vPats, pInfo, i ) Vec_PtrForEachEntry( vPats, pInfo, i )
{ {
for ( w = iWords; w < nWords; i++ ) for ( w = iWords; w < nWords; w++ )
pInfo[w] = pInfo[0]; pInfo[w] = pInfo[0];
} }
} }
...@@ -424,6 +397,72 @@ void Res_SimDeriveInfoComplement( Res_Sim_t * p ) ...@@ -424,6 +397,72 @@ void Res_SimDeriveInfoComplement( Res_Sim_t * p )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Free simulation engine.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Res_SimReportOne( Res_Sim_t * p )
{
unsigned * pInfoCare, * pInfoNode;
int i, nDcs, nOnes, nZeros;
pInfoCare = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 0)->Id );
pInfoNode = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 1)->Id );
nDcs = nOnes = nZeros = 0;
for ( i = 0; i < p->nPats; i++ )
{
// skip don't-care patterns
if ( !Abc_InfoHasBit(pInfoCare, i) )
{
nDcs++;
continue;
}
// separate offset and onset patterns
if ( !Abc_InfoHasBit(pInfoNode, i) )
nZeros++;
else
nOnes++;
}
printf( "On = %3d (%7.2f %%) ", nOnes, 100.0*nOnes/p->nPats );
printf( "Off = %3d (%7.2f %%) ", nZeros, 100.0*nZeros/p->nPats );
printf( "Dc = %3d (%7.2f %%) ", nDcs, 100.0*nDcs/p->nPats );
printf( "P0 = %3d ", p->nPats0 );
printf( "P1 = %3d ", p->nPats1 );
if ( p->nPats0 < 4 || p->nPats1 < 4 )
printf( "*" );
printf( "\n" );
}
/**Function*************************************************************
Synopsis [Prints output patterns.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Res_SimPrintOutPatterns( Res_Sim_t * p, Abc_Ntk_t * pAig )
{
Abc_Obj_t * pObj;
unsigned * pInfo2;
int i;
Abc_NtkForEachPo( pAig, pObj, i )
{
pInfo2 = Vec_PtrEntry( p->vOuts, i );
Extra_PrintBinary( stdout, pInfo2, p->nPatsOut );
printf( "\n" );
}
}
/**Function*************************************************************
Synopsis [Prepares simulation info for candidate filtering.] Synopsis [Prepares simulation info for candidate filtering.]
Description [] Description []
...@@ -435,19 +474,24 @@ void Res_SimDeriveInfoComplement( Res_Sim_t * p ) ...@@ -435,19 +474,24 @@ void Res_SimDeriveInfoComplement( Res_Sim_t * p )
***********************************************************************/ ***********************************************************************/
int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig ) int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig )
{ {
int Limit = 20; int Limit;
// prepare the manager // prepare the manager
Res_SimAdjust( p, pAig ); Res_SimAdjust( p, pAig );
// collect 0/1 simulation info // collect 0/1 simulation info
while ( p->nPats0 < p->nPats || p->nPats1 < p->nPats || Limit-- == 0 ) for ( Limit = 0; Limit < 100; Limit++ )
{ {
Res_SimSetRandom( p ); Res_SimSetRandom( p );
Res_SimPerformRound( p ); Res_SimPerformRound( p );
Res_SimProcessPats( p ); Res_SimProcessPats( p );
if ( Limit == 19 ) if ( !(p->nPats0 < p->nPats || p->nPats1 < p->nPats) )
Res_SimReportOne( p ); break;
} }
if ( p->nPats0 < 32 || p->nPats1 < 32 ) // printf( "%d ", Limit );
// report the last set of patterns
// Res_SimReportOne( p );
// quit if there is not enough
if ( p->nPats0 < 4 || p->nPats1 < 4 )
return 0; return 0;
// create bit-matrix info // create bit-matrix info
if ( p->nPats0 < p->nPats ) if ( p->nPats0 < p->nPats )
...@@ -462,6 +506,8 @@ int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig ) ...@@ -462,6 +506,8 @@ int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig )
Res_SimSetGiven( p, p->vPats1 ); Res_SimSetGiven( p, p->vPats1 );
Res_SimPerformRound( p ); Res_SimPerformRound( p );
Res_SimDeriveInfoComplement( p ); Res_SimDeriveInfoComplement( p );
// print output patterns
// Res_SimPrintOutPatterns( p, pAig );
return 1; return 1;
} }
......
src/opt/res/resStrash.c
...@@ -19,7 +19,7 @@ ...@@ -19,7 +19,7 @@
***********************************************************************/ ***********************************************************************/
#include "abc.h" #include "abc.h"
#include "res.h" #include "resInt.h"
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// DECLARATIONS /// /// DECLARATIONS ///
...@@ -72,7 +72,7 @@ Abc_Ntk_t * Res_WndStrash( Res_Win_t * p ) ...@@ -72,7 +72,7 @@ Abc_Ntk_t * Res_WndStrash( Res_Win_t * p )
} }
// mark the TFO of the node // mark the TFO of the node
Abc_NtkIncrementTravId( p->pNode->pNtk ); Abc_NtkIncrementTravId( p->pNode->pNtk );
Res_WinVisitNodeTfo( p ); Res_WinSweepLeafTfo_rec( p->pNode, (int)p->pNode->Level + p->nWinTfoMax, NULL );
// redo strashing in the TFO // redo strashing in the TFO
p->pNode->pCopy = Abc_ObjNot( p->pNode->pCopy ); p->pNode->pCopy = Abc_ObjNot( p->pNode->pCopy );
Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, p->pNode->Level + 1, (int)p->pNode->Level + p->nWinTfoMax ) Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, p->pNode->Level + 1, (int)p->pNode->Level + p->nWinTfoMax )
...@@ -92,6 +92,9 @@ Abc_Ntk_t * Res_WndStrash( Res_Win_t * p ) ...@@ -92,6 +92,9 @@ Abc_Ntk_t * Res_WndStrash( Res_Win_t * p )
// add the divisors // add the divisors
Vec_PtrForEachEntry( p->vDivs, pObj, i ) Vec_PtrForEachEntry( p->vDivs, pObj, i )
Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), pObj->pCopy ); Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), pObj->pCopy );
// add the names
Abc_NtkAddDummyPiNames( pAig );
Abc_NtkAddDummyPoNames( pAig );
// check the resulting network // check the resulting network
if ( !Abc_NtkCheck( pAig ) ) if ( !Abc_NtkCheck( pAig ) )
fprintf( stdout, "Res_WndStrash(): Network check has failed.\n" ); fprintf( stdout, "Res_WndStrash(): Network check has failed.\n" );
......
src/opt/res/resUpdate.c
...@@ -19,7 +19,7 @@ ...@@ -19,7 +19,7 @@
***********************************************************************/ ***********************************************************************/
#include "abc.h" #include "abc.h"
#include "res.h" #include "resInt.h"
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// DECLARATIONS /// /// DECLARATIONS ///
......
src/opt/res/resWin.c
...@@ -19,7 +19,7 @@ ...@@ -19,7 +19,7 @@
***********************************************************************/ ***********************************************************************/
#include "abc.h" #include "abc.h"
#include "res.h" #include "resInt.h"
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// DECLARATIONS /// /// DECLARATIONS ///
...@@ -95,7 +95,7 @@ void Res_WinCollectNodeTfi( Res_Win_t * p ) ...@@ -95,7 +95,7 @@ void Res_WinCollectNodeTfi( Res_Win_t * p )
Vec_VecClear( p->vLevels ); Vec_VecClear( p->vLevels );
Res_WinAddNode( p, p->pNode ); Res_WinAddNode( p, p->pNode );
// add one level at a time // add one level at a time
Vec_VecForEachLevelReverseStartStop( p->vLevels, vFront, i, p->pNode->Level, p->nLevLeaves -1 ) Vec_VecForEachLevelReverseStartStop( p->vLevels, vFront, i, p->pNode->Level, p->nLevLeaves + 1 )
{ {
Vec_PtrForEachEntry( vFront, pObj, k ) Vec_PtrForEachEntry( vFront, pObj, k )
Abc_ObjForEachFanin( pObj, pFanin, m ) Abc_ObjForEachFanin( pObj, pFanin, m )
...@@ -190,15 +190,14 @@ void Res_WinCollectRoots_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vRoots ) ...@@ -190,15 +190,14 @@ void Res_WinCollectRoots_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vRoots )
Abc_Obj_t * pFanout; Abc_Obj_t * pFanout;
int i; int i;
assert( Abc_ObjIsNode(pObj) ); assert( Abc_ObjIsNode(pObj) );
assert( Abc_NodeIsTravIdCurrent(pObj) );
// check if the node has all fanouts marked // check if the node has all fanouts marked
Abc_ObjForEachFanout( pObj, pFanout, i ) Abc_ObjForEachFanout( pObj, pFanout, i )
if ( !Abc_NodeIsTravIdCurrent(pObj) ) if ( !Abc_NodeIsTravIdCurrent(pFanout) )
break; break;
// if some of the fanouts are unmarked, add the node to the root // if some of the fanouts are unmarked, add the node to the root
if ( i < Abc_ObjFanoutNum(pObj) ) if ( i < Abc_ObjFanoutNum(pObj) )
{ {
Vec_PtrPush( vRoots, pObj ); Vec_PtrPushUnique( vRoots, pObj );
return; return;
} }
// otherwise, call recursively // otherwise, call recursively
...@@ -220,6 +219,7 @@ void Res_WinCollectRoots_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vRoots ) ...@@ -220,6 +219,7 @@ void Res_WinCollectRoots_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vRoots )
***********************************************************************/ ***********************************************************************/
void Res_WinCollectRoots( Res_Win_t * p ) void Res_WinCollectRoots( Res_Win_t * p )
{ {
assert( !Abc_NodeIsTravIdCurrent(p->pNode) );
Vec_PtrClear( p->vRoots ); Vec_PtrClear( p->vRoots );
Res_WinCollectRoots_rec( p->pNode, p->vRoots ); Res_WinCollectRoots_rec( p->pNode, p->vRoots );
} }
...@@ -241,7 +241,7 @@ void Res_WinAddMissing_rec( Res_Win_t * p, Abc_Obj_t * pObj ) ...@@ -241,7 +241,7 @@ void Res_WinAddMissing_rec( Res_Win_t * p, Abc_Obj_t * pObj )
int i; int i;
if ( pObj->fMarkA ) if ( pObj->fMarkA )
return; return;
if ( !Abc_NodeIsTravIdCurrent(pObj) ) if ( !Abc_NodeIsTravIdCurrent(pObj) || (int)pObj->Level <= p->nLevLeaves )
{ {
Vec_PtrPush( p->vLeaves, pObj ); Vec_PtrPush( p->vLeaves, pObj );
pObj->fMarkA = 1; pObj->fMarkA = 1;
...@@ -250,7 +250,7 @@ void Res_WinAddMissing_rec( Res_Win_t * p, Abc_Obj_t * pObj ) ...@@ -250,7 +250,7 @@ void Res_WinAddMissing_rec( Res_Win_t * p, Abc_Obj_t * pObj )
Res_WinAddNode( p, pObj ); Res_WinAddNode( p, pObj );
// visit the fanins of the node // visit the fanins of the node
Abc_ObjForEachFanin( pObj, pFanin, i ) Abc_ObjForEachFanin( pObj, pFanin, i )
Res_WinAddMissing_rec( p, pObj ); Res_WinAddMissing_rec( p, pFanin );
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -295,7 +295,7 @@ void Res_WinUnmark( Res_Win_t * p ) ...@@ -295,7 +295,7 @@ void Res_WinUnmark( Res_Win_t * p )
/**Function************************************************************* /**Function*************************************************************
Synopsis [Labels the TFO of the node with the current trav ID.] Synopsis [Verifies the window.]
Description [] Description []
...@@ -304,10 +304,30 @@ void Res_WinUnmark( Res_Win_t * p ) ...@@ -304,10 +304,30 @@ void Res_WinUnmark( Res_Win_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Res_WinVisitNodeTfo( Res_Win_t * p ) void Res_WinVerify( Res_Win_t * p )
{ {
// mark the TFO of the node Abc_Obj_t * pObj, * pFanin;
Res_WinSweepLeafTfo_rec( p->pNode, p->nLevDivMax, NULL ); int i, k, f;
// make sure the nodes are not marked
Abc_NtkForEachObj( p->pNode->pNtk, pObj, i )
assert( !pObj->fMarkA );
// mark the leaves
Vec_PtrForEachEntry( p->vLeaves, pObj, i )
pObj->fMarkA = 1;
// make sure all nodes in the topological order have their fanins in the set
Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, p->nLevLeaves + 1, (int)p->pNode->Level + p->nWinTfoMax )
{
assert( (int)pObj->Level == i );
assert( !pObj->fMarkA );
Abc_ObjForEachFanin( pObj, pFanin, f )
assert( pFanin->fMarkA );
pObj->fMarkA = 1;
}
// make sure the roots are marked
Vec_PtrForEachEntry( p->vRoots, pObj, i )
assert( pObj->fMarkA );
// unmark
Res_WinUnmark( p );
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -329,9 +349,7 @@ int Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t ...@@ -329,9 +349,7 @@ int Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t
p->pNode = pNode; p->pNode = pNode;
p->nWinTfiMax = nWinTfiMax; p->nWinTfiMax = nWinTfiMax;
p->nWinTfoMax = nWinTfoMax; p->nWinTfoMax = nWinTfoMax;
p->nLevLeaves = ABC_MAX( 0, p->pNode->Level - p->nWinTfiMax - 1 ); p->nLevLeaves = ABC_MAX( 0, ((int)p->pNode->Level) - p->nWinTfiMax - 1 );
p->nLevDivMax = 0;
Vec_PtrClear( p->vDivs );
// collect the nodes in TFI cone of pNode above the level of leaves (p->nLevLeaves) // collect the nodes in TFI cone of pNode above the level of leaves (p->nLevLeaves)
Res_WinCollectNodeTfi( p ); Res_WinCollectNodeTfi( p );
// find the leaves of the window // find the leaves of the window
...@@ -344,6 +362,12 @@ int Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t ...@@ -344,6 +362,12 @@ int Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t
Res_WinAddMissing( p ); Res_WinAddMissing( p );
// unmark window nodes // unmark window nodes
Res_WinUnmark( p ); Res_WinUnmark( p );
// clear the divisor information
p->nLevDivMax = 0;
p->nDivsPlus = 0;
Vec_PtrClear( p->vDivs );
// verify the resulting window
// Res_WinVerify( p );
return 1; return 1;
} }
......
src/sat/bsat/module.make
SRC += src/sat/bsat/satMem.c \ SRC += src/sat/bsat/satMem.c \
src/sat/bsat/satInter.c \
src/sat/bsat/satSolver.c \ src/sat/bsat/satSolver.c \
src/sat/bsat/satStore.c \
src/sat/bsat/satTrace.c \
src/sat/bsat/satUtil.c src/sat/bsat/satUtil.c
src/sat/bsat/satInter.c
...@@ -71,18 +71,18 @@ struct Int_Man_t_ ...@@ -71,18 +71,18 @@ struct Int_Man_t_
int timeTotal; // the total runtime of interpolation int timeTotal; // the total runtime of interpolation
}; };
// procedure to get hold of the clauses' truth table // procedure to get hold of the clauses' truth table
static inline unsigned * Int_ManTruthRead( Int_Man_t * p, Sto_Cls_t * pCls ) { return p->pInters + pCls->Id * p->nWords; } static inline unsigned * Int_ManTruthRead( Int_Man_t * p, Sto_Cls_t * pCls ) { return p->pInters + pCls->Id * p->nWords; }
static inline void Int_ManTruthClear( unsigned * p, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = 0; } static inline void Int_ManTruthClear( unsigned * p, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = 0; }
static inline void Int_ManTruthFill( unsigned * p, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = ~0; } static inline void Int_ManTruthFill( unsigned * p, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = ~0; }
static inline void Int_ManTruthCopy( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = q[i]; } static inline void Int_ManTruthCopy( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = q[i]; }
static inline void Int_ManTruthAnd( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] &= q[i]; } static inline void Int_ManTruthAnd( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] &= q[i]; }
static inline void Int_ManTruthOr( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] |= q[i]; } static inline void Int_ManTruthOr( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] |= q[i]; }
static inline void Int_ManTruthOrNot( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] |= ~q[i]; } static inline void Int_ManTruthOrNot( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] |= ~q[i]; }
// reading/writing the proof for a clause // reading/writing the proof for a clause
static inline int Int_ManProofRead( Int_Man_t * p, Sto_Cls_t * pCls ) { return p->pProofNums[pCls->Id]; } static inline int Int_ManProofGet( Int_Man_t * p, Sto_Cls_t * pCls ) { return p->pProofNums[pCls->Id]; }
static inline void Int_ManProofWrite( Int_Man_t * p, Sto_Cls_t * pCls, int n ) { p->pProofNums[pCls->Id] = n; } static inline void Int_ManProofSet( Int_Man_t * p, Sto_Cls_t * pCls, int n ) { p->pProofNums[pCls->Id] = n; }
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
...@@ -110,7 +110,7 @@ Int_Man_t * Int_ManAlloc( int nVarsAlloc ) ...@@ -110,7 +110,7 @@ Int_Man_t * Int_ManAlloc( int nVarsAlloc )
p->pResLits = malloc( sizeof(lit) * p->nResLitsAlloc ); p->pResLits = malloc( sizeof(lit) * p->nResLitsAlloc );
// parameters // parameters
p->fProofWrite = 0; p->fProofWrite = 0;
p->fProofVerif = 0; p->fProofVerif = 1;
return p; return p;
} }
...@@ -125,7 +125,7 @@ Int_Man_t * Int_ManAlloc( int nVarsAlloc ) ...@@ -125,7 +125,7 @@ Int_Man_t * Int_ManAlloc( int nVarsAlloc )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Int_ManCommonVars( Int_Man_t * p ) int Int_ManGlobalVars( Int_Man_t * p )
{ {
Sto_Cls_t * pClause; Sto_Cls_t * pClause;
int Var, nVarsAB, v; int Var, nVarsAB, v;
...@@ -161,8 +161,8 @@ int Int_ManCommonVars( Int_Man_t * p ) ...@@ -161,8 +161,8 @@ int Int_ManCommonVars( Int_Man_t * p )
nVarsAB = 0; nVarsAB = 0;
for ( v = 0; v < p->pCnf->nVars; v++ ) for ( v = 0; v < p->pCnf->nVars; v++ )
if ( p->pVarTypes[v] == -1 ) if ( p->pVarTypes[v] == -1 )
p->pVarTypes[v] -= p->nVarsAB++; p->pVarTypes[v] -= nVarsAB++;
printf( "There are %d global variables.\n", nVarsAB ); //printf( "There are %d global variables.\n", nVarsAB );
return nVarsAB; return nVarsAB;
} }
...@@ -182,7 +182,6 @@ void Int_ManResize( Int_Man_t * p ) ...@@ -182,7 +182,6 @@ void Int_ManResize( Int_Man_t * p )
// check if resizing is needed // check if resizing is needed
if ( p->nVarsAlloc < p->pCnf->nVars ) if ( p->nVarsAlloc < p->pCnf->nVars )
{ {
int nVarsAllocOld = p->nVarsAlloc;
// find the new size // find the new size
if ( p->nVarsAlloc == 0 ) if ( p->nVarsAlloc == 0 )
p->nVarsAlloc = 1; p->nVarsAlloc = 1;
...@@ -205,7 +204,7 @@ void Int_ManResize( Int_Man_t * p ) ...@@ -205,7 +204,7 @@ void Int_ManResize( Int_Man_t * p )
memset( p->pWatches , 0, sizeof(Sto_Cls_t *) * p->pCnf->nVars*2 ); memset( p->pWatches , 0, sizeof(Sto_Cls_t *) * p->pCnf->nVars*2 );
// compute the number of common variables // compute the number of common variables
p->nVarsAB = Int_ManCommonVars( p ); p->nVarsAB = Int_ManGlobalVars( p );
// compute the number of words in the truth table // compute the number of words in the truth table
p->nWords = (p->nVarsAB <= 5 ? 1 : (1 << (p->nVarsAB - 5))); p->nWords = (p->nVarsAB <= 5 ? 1 : (1 << (p->nVarsAB - 5)));
...@@ -228,7 +227,7 @@ void Int_ManResize( Int_Man_t * p ) ...@@ -228,7 +227,7 @@ void Int_ManResize( Int_Man_t * p )
p->nIntersAlloc = p->nWords * p->pCnf->nClauses; p->nIntersAlloc = p->nWords * p->pCnf->nClauses;
p->pInters = (unsigned *) realloc( p->pInters, sizeof(unsigned) * p->nIntersAlloc ); p->pInters = (unsigned *) realloc( p->pInters, sizeof(unsigned) * p->nIntersAlloc );
} }
memset( p->pInters, 0, sizeof(unsigned) * p->nIntersAlloc ); // memset( p->pInters, 0, sizeof(unsigned) * p->nWords * p->pCnf->nClauses );
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -244,11 +243,12 @@ void Int_ManResize( Int_Man_t * p ) ...@@ -244,11 +243,12 @@ void Int_ManResize( Int_Man_t * p )
***********************************************************************/ ***********************************************************************/
void Int_ManFree( Int_Man_t * p ) void Int_ManFree( Int_Man_t * p )
{ {
/*
printf( "Runtime stats:\n" ); printf( "Runtime stats:\n" );
PRT( "BCP ", p->timeBcp ); PRT( "BCP ", p->timeBcp );
PRT( "Trace ", p->timeTrace ); PRT( "Trace ", p->timeTrace );
PRT( "TOTAL ", p->timeTotal ); PRT( "TOTAL ", p->timeTotal );
*/
free( p->pInters ); free( p->pInters );
free( p->pProofNums ); free( p->pProofNums );
free( p->pTrail ); free( p->pTrail );
...@@ -278,7 +278,7 @@ PRT( "TOTAL ", p->timeTotal ); ...@@ -278,7 +278,7 @@ PRT( "TOTAL ", p->timeTotal );
void Int_ManPrintClause( Int_Man_t * p, Sto_Cls_t * pClause ) void Int_ManPrintClause( Int_Man_t * p, Sto_Cls_t * pClause )
{ {
int i; int i;
printf( "Clause ID = %d. Proof = %d. {", pClause->Id, Int_ManProofRead(p, pClause) ); printf( "Clause ID = %d. Proof = %d. {", pClause->Id, Int_ManProofGet(p, pClause) );
for ( i = 0; i < (int)pClause->nLits; i++ ) for ( i = 0; i < (int)pClause->nLits; i++ )
printf( " %d", pClause->pLits[i] ); printf( " %d", pClause->pLits[i] );
printf( " }\n" ); printf( " }\n" );
...@@ -534,12 +534,12 @@ p->timeBcp += clock() - clk; ...@@ -534,12 +534,12 @@ p->timeBcp += clock() - clk;
***********************************************************************/ ***********************************************************************/
void Int_ManProofWriteOne( Int_Man_t * p, Sto_Cls_t * pClause ) void Int_ManProofWriteOne( Int_Man_t * p, Sto_Cls_t * pClause )
{ {
Int_ManProofWrite( p, pClause, ++p->Counter ); Int_ManProofSet( p, pClause, ++p->Counter );
if ( p->fProofWrite ) if ( p->fProofWrite )
{ {
int v; int v;
fprintf( p->pFile, "%d", Int_ManProofRead(p, pClause) ); fprintf( p->pFile, "%d", Int_ManProofGet(p, pClause) );
for ( v = 0; v < (int)pClause->nLits; v++ ) for ( v = 0; v < (int)pClause->nLits; v++ )
fprintf( p->pFile, " %d", lit_print(pClause->pLits[v]) ); fprintf( p->pFile, " %d", lit_print(pClause->pLits[v]) );
fprintf( p->pFile, " 0 0\n" ); fprintf( p->pFile, " 0 0\n" );
...@@ -584,7 +584,7 @@ int Int_ManProofTraceOne( Int_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pFin ...@@ -584,7 +584,7 @@ int Int_ManProofTraceOne( Int_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pFin
Int_ManTruthCopy( Int_ManTruthRead(p, pFinal), Int_ManTruthRead(p, pConflict), p->nWords ); Int_ManTruthCopy( Int_ManTruthRead(p, pFinal), Int_ManTruthRead(p, pConflict), p->nWords );
// follow the trail backwards // follow the trail backwards
PrevId = Int_ManProofRead(p, pConflict); PrevId = Int_ManProofGet(p, pConflict);
for ( i = p->nTrailSize - 1; i >= 0; i-- ) for ( i = p->nTrailSize - 1; i >= 0; i-- )
{ {
// skip literals that are not involved // skip literals that are not involved
...@@ -605,10 +605,10 @@ int Int_ManProofTraceOne( Int_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pFin ...@@ -605,10 +605,10 @@ int Int_ManProofTraceOne( Int_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pFin
// record the reason clause // record the reason clause
assert( Int_ManProofRead(p, pReason) > 0 ); assert( Int_ManProofGet(p, pReason) > 0 );
p->Counter++; p->Counter++;
if ( p->fProofWrite ) if ( p->fProofWrite )
fprintf( p->pFile, "%d * %d %d 0\n", p->Counter, PrevId, Int_ManProofRead(p, pReason) ); fprintf( p->pFile, "%d * %d %d 0\n", p->Counter, PrevId, Int_ManProofGet(p, pReason) );
PrevId = p->Counter; PrevId = p->Counter;
if ( p->pCnf->nClausesA ) if ( p->pCnf->nClausesA )
...@@ -700,7 +700,7 @@ p->timeTrace += clock() - clk; ...@@ -700,7 +700,7 @@ p->timeTrace += clock() - clk;
{ {
// Int_ManPrintInterOne( p, pFinal ); // Int_ManPrintInterOne( p, pFinal );
} }
Int_ManProofWrite( p, pFinal, p->Counter ); Int_ManProofSet( p, pFinal, p->Counter );
return p->Counter; return p->Counter;
} }
...@@ -839,7 +839,7 @@ int Int_ManProcessRoots( Int_Man_t * p ) ...@@ -839,7 +839,7 @@ int Int_ManProcessRoots( Int_Man_t * p )
{ {
// detected root level conflict // detected root level conflict
printf( "Int_ManProcessRoots(): Detected a root-level conflict\n" ); printf( "Int_ManProcessRoots(): Detected a root-level conflict\n" );
assert( 0 ); // assert( 0 );
return 0; return 0;
} }
...@@ -873,7 +873,7 @@ void Int_ManPrepareInter( Int_Man_t * p ) ...@@ -873,7 +873,7 @@ void Int_ManPrepareInter( Int_Man_t * p )
{ 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF } { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF }
}; };
Sto_Cls_t * pClause; Sto_Cls_t * pClause;
int Var, v; int Var, VarAB, v;
assert( p->nVarsAB <= 8 ); assert( p->nVarsAB <= 8 );
// set interpolants for root clauses // set interpolants for root clauses
...@@ -892,10 +892,12 @@ void Int_ManPrepareInter( Int_Man_t * p ) ...@@ -892,10 +892,12 @@ void Int_ManPrepareInter( Int_Man_t * p )
Var = lit_var(pClause->pLits[v]); Var = lit_var(pClause->pLits[v]);
if ( p->pVarTypes[Var] < 0 ) // global var if ( p->pVarTypes[Var] < 0 ) // global var
{ {
VarAB = -p->pVarTypes[Var]-1;
assert( VarAB >= 0 && VarAB < p->nVarsAB );
if ( lit_sign(pClause->pLits[v]) ) // negative var if ( lit_sign(pClause->pLits[v]) ) // negative var
Int_ManTruthOrNot( Int_ManTruthRead(p, pClause), uTruths[ -p->pVarTypes[Var]-1 ], p->nWords ); Int_ManTruthOrNot( Int_ManTruthRead(p, pClause), uTruths[VarAB], p->nWords );
else else
Int_ManTruthOr( Int_ManTruthRead(p, pClause), uTruths[ -p->pVarTypes[Var]-1 ], p->nWords ); Int_ManTruthOr( Int_ManTruthRead(p, pClause), uTruths[VarAB], p->nWords );
} }
} }
// Int_ManPrintInterOne( p, pClause ); // Int_ManPrintInterOne( p, pClause );
...@@ -922,12 +924,17 @@ int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned ...@@ -922,12 +924,17 @@ int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned
// check that the CNF makes sense // check that the CNF makes sense
assert( pCnf->nVars > 0 && pCnf->nClauses > 0 ); assert( pCnf->nVars > 0 && pCnf->nClauses > 0 );
p->pCnf = pCnf;
// adjust the manager // adjust the manager
Int_ManResize( p ); Int_ManResize( p );
// propagate root level assignments // propagate root level assignments
Int_ManProcessRoots( p ); if ( !Int_ManProcessRoots( p ) )
{
*ppResult = NULL;
return p->nVarsAB;
}
// prepare the interpolant computation // prepare the interpolant computation
Int_ManPrepareInter( p ); Int_ManPrepareInter( p );
...@@ -969,8 +976,8 @@ int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned ...@@ -969,8 +976,8 @@ int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned
1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) ); 1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) );
p->timeTotal += clock() - clkTotal; p->timeTotal += clock() - clkTotal;
Int_ManFree( p ); *ppResult = Int_ManTruthRead( p, p->pCnf->pTail );
return 1; return p->nVarsAB;
} }
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/sat/bsat/satSolver.c
...@@ -1223,7 +1223,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sin ...@@ -1223,7 +1223,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sin
sat_solver_canceluntil(s,0); sat_solver_canceluntil(s,0);
//////////////////////////////////////////////// ////////////////////////////////////////////////
if ( status == l_Undef && s->pStore ) if ( status == l_False && s->pStore )
{ {
extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd ); extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
int RetValue = Sto_ManAddClause( s->pStore, NULL, NULL ); int RetValue = Sto_ManAddClause( s->pStore, NULL, NULL );
......
src/sat/bsat/satStore.c
...@@ -292,7 +292,7 @@ void Sto_ManDumpClauses( Sto_Man_t * p, char * pFileName ) ...@@ -292,7 +292,7 @@ void Sto_ManDumpClauses( Sto_Man_t * p, char * pFileName )
fprintf( pFile, " %d", lit_print(pClause->pLits[i]) ); fprintf( pFile, " %d", lit_print(pClause->pLits[i]) );
fprintf( pFile, "\n" ); fprintf( pFile, "\n" );
} }
fprintf( pFile, "\n" ); fprintf( pFile, " 0\n" );
fclose( pFile ); fclose( pFile );
} }
......
src/sat/bsat/satStore.h
...@@ -116,6 +116,8 @@ extern int Sto_ManAddClause( Sto_Man_t * p, lit * pBeg, lit * pEnd ); ...@@ -116,6 +116,8 @@ extern int Sto_ManAddClause( Sto_Man_t * p, lit * pBeg, lit * pEnd );
extern int Sto_ManMemoryReport( Sto_Man_t * p ); extern int Sto_ManMemoryReport( Sto_Man_t * p );
extern void Sto_ManMarkRoots( Sto_Man_t * p ); extern void Sto_ManMarkRoots( Sto_Man_t * p );
extern void Sto_ManMarkClausesA( Sto_Man_t * p ); extern void Sto_ManMarkClausesA( Sto_Man_t * p );
extern void Sto_ManDumpClauses( Sto_Man_t * p, char * pFileName );
extern Sto_Man_t * Sto_ManLoadClauses( char * pFileName );
/*=== satInter.c ==========================================================*/ /*=== satInter.c ==========================================================*/
typedef struct Int_Man_t_ Int_Man_t; typedef struct Int_Man_t_ Int_Man_t;
......
src/sat/bsat/satUtil.c
...@@ -190,7 +190,7 @@ int * Sat_SolverGetModel( sat_solver * p, int * pVars, int nVars ) ...@@ -190,7 +190,7 @@ int * Sat_SolverGetModel( sat_solver * p, int * pVars, int nVars )
***********************************************************************/ ***********************************************************************/
void Sat_SolverDoubleClauses( sat_solver * p, int iVar ) void Sat_SolverDoubleClauses( sat_solver * p, int iVar )
{ {
clause ** pClauses; clause * pClause;
lit Lit, * pLits; lit Lit, * pLits;
int RetValue, nClauses, nVarsOld, nLitsOld, nLits, c, v; int RetValue, nClauses, nVarsOld, nLitsOld, nLits, c, v;
// get the number of variables // get the number of variables
...@@ -210,11 +210,11 @@ void Sat_SolverDoubleClauses( sat_solver * p, int iVar ) ...@@ -210,11 +210,11 @@ void Sat_SolverDoubleClauses( sat_solver * p, int iVar )
} }
// duplicate clauses // duplicate clauses
nClauses = vecp_size(&p->clauses); nClauses = vecp_size(&p->clauses);
pClauses = (clause**)vecp_begin(&p->clauses);
for ( c = 0; c < nClauses; c++ ) for ( c = 0; c < nClauses; c++ )
{ {
nLits = clause_size(pClauses[c]); pClause = p->clauses.ptr[c];
pLits = clause_begin(pClauses[c]); nLits = clause_size(pClause);
pLits = clause_begin(pClause);
for ( v = 0; v < nLits; v++ ) for ( v = 0; v < nLits; v++ )
pLits[v] += nLitsOld; pLits[v] += nLitsOld;
RetValue = sat_solver_addclause( p, pLits, pLits + nLits ); RetValue = sat_solver_addclause( p, pLits, pLits + nLits );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment