Skip to content

A
abc
Commit c0ef1f46 by Alan Mishchenko
Options

Version abc60118

parent 9e073ed8
Showing with 869 additions and 179 deletions
abc.dsp
......@@ -42,7 +42,7 @@ RSC=rc.exe
# PROP Ignore_Export_Lib 0
# PROP Target_Dir ""
# 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\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\map\fpga" /I "src\map\pga" /I "src\map\mapper" /I "src\map\mapp" /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" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /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\aig" /I "src\sat\asat" /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\map\fpga" /I "src\map\pga" /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" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR /YX /FD /c
# ADD BASE RSC /l 0x409 /d "NDEBUG"
# ADD RSC /l 0x409 /d "NDEBUG"
BSC32=bscmake.exe
......@@ -66,7 +66,7 @@ LINK32=link.exe
# PROP Ignore_Export_Lib 0
# 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 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\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\map\fpga" /I "src\map\pga" /I "src\map\mapper" /I "src\map\mapp" /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" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /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\aig" /I "src\sat\asat" /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\map\fpga" /I "src\map\pga" /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" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR /YX /FD /GZ /c
# SUBTRACT CPP /X
# ADD BASE RSC /l 0x409 /d "_DEBUG"
# ADD RSC /l 0x409 /d "_DEBUG"
......@@ -210,6 +210,10 @@ SOURCE=.\src\base\abci\abcMiter.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abci\abcNewAig.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abci\abcNtbdd.c
# End Source File
# Begin Source File
......@@ -1098,16 +1102,32 @@ SOURCE=.\src\sat\aig\fraigClass.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\aig\fraigCnf.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\aig\fraigCore.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\aig\fraigEngine.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\aig\fraigProve.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\aig\fraigSim.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\aig\fraigSolver.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\aig\fraigTrav.c
# End Source File
# End Group
# End Group
# Begin Group "opt"
......
abc.opt
No preview for this file type
abc.plg
......@@ -6,13 +6,13 @@
--------------------Configuration: abc - Win32 Debug--------------------
</h3>
<h3>Command Lines</h3>
Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP4FE.tmp" with contents
Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP8E2.tmp" with contents
[
/nologo /MLd /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\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\map\fpga" /I "src\map\pga" /I "src\map\mapper" /I "src\map\mapp" /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" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR"Debug/" /Fp"Debug/abc.pch" /YX /Fo"Debug/" /Fd"Debug/" /FD /GZ /c
"C:\_projects\abc\src\sat\aig\aigReplace.c"
/nologo /MLd /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\aig" /I "src\sat\asat" /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\map\fpga" /I "src\map\pga" /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" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR"Debug/" /Fp"Debug/abc.pch" /YX /Fo"Debug/" /Fd"Debug/" /FD /GZ /c
"C:\_projects\abc\src\sat\aig\fraigSim.c"
]
Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP4FE.tmp"
Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP4FF.tmp" with contents
Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP8E2.tmp"
Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP8E3.tmp" with contents
[
kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib /nologo /subsystem:console /incremental:yes /pdb:"Debug/abc.pdb" /debug /machine:I386 /out:"_TEST/abc.exe" /pdbtype:sept
.\Debug\abcAig.obj
......@@ -210,12 +210,21 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
.\Debug\fraigVec.obj
.\Debug\csat_apis.obj
.\Debug\aigBalance.obj
.\Debug\aigCheck.obj
.\Debug\aigFanout.obj
.\Debug\aigMan.obj
.\Debug\aigMem.obj
.\Debug\aigNode.obj
.\Debug\aigOper.obj
.\Debug\aigReplace.obj
.\Debug\aigTable.obj
.\Debug\aigUtil.obj
.\Debug\fraigClass.obj
.\Debug\fraigCore.obj
.\Debug\fraigProve.obj
.\Debug\fraigSim.obj
.\Debug\fraigSolver.obj
.\Debug\fraigTrav.obj
.\Debug\fxu.obj
.\Debug\fxuCreate.obj
.\Debug\fxuHeapD.obj
......@@ -346,20 +355,16 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
.\Debug\mvcPrint.obj
.\Debug\mvcSort.obj
.\Debug\mvcUtils.obj
.\Debug\aigTable.obj
.\Debug\aigCheck.obj
.\Debug\aigReplace.obj
.\Debug\fraigCore.obj
.\Debug\fraigProve.obj
.\Debug\fraigSim.obj
.\Debug\fraigClass.obj
.\Debug\abcNewAig.obj
.\Debug\fraigCnf.obj
.\Debug\fraigEngine.obj
]
Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP4FF.tmp"
Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP8E3.tmp"
<h3>Output Window</h3>
Compiling...
aigReplace.c
fraigSim.c
Linking...
Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP500.tmp" with contents
Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP8E4.tmp" with contents
[
/nologo /o"Debug/abc.bsc"
.\Debug\abcAig.sbr
......@@ -557,12 +562,21 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP500.tmp" with conte
.\Debug\fraigVec.sbr
.\Debug\csat_apis.sbr
.\Debug\aigBalance.sbr
.\Debug\aigCheck.sbr
.\Debug\aigFanout.sbr
.\Debug\aigMan.sbr
.\Debug\aigMem.sbr
.\Debug\aigNode.sbr
.\Debug\aigOper.sbr
.\Debug\aigReplace.sbr
.\Debug\aigTable.sbr
.\Debug\aigUtil.sbr
.\Debug\fraigClass.sbr
.\Debug\fraigCore.sbr
.\Debug\fraigProve.sbr
.\Debug\fraigSim.sbr
.\Debug\fraigSolver.sbr
.\Debug\fraigTrav.sbr
.\Debug\fxu.sbr
.\Debug\fxuCreate.sbr
.\Debug\fxuHeapD.sbr
......@@ -693,14 +707,10 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP500.tmp" with conte
.\Debug\mvcPrint.sbr
.\Debug\mvcSort.sbr
.\Debug\mvcUtils.sbr
.\Debug\aigTable.sbr
.\Debug\aigCheck.sbr
.\Debug\aigReplace.sbr
.\Debug\fraigCore.sbr
.\Debug\fraigProve.sbr
.\Debug\fraigSim.sbr
.\Debug\fraigClass.sbr]
Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP500.tmp"
.\Debug\abcNewAig.sbr
.\Debug\fraigCnf.sbr
.\Debug\fraigEngine.sbr]
Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP8E4.tmp"
Creating browse info file...
<h3>Output Window</h3>
......
abclib.opt
No preview for this file type
src/base/abci/abc.c
......@@ -3782,8 +3782,9 @@ usage:
int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;//, * pNtkRes;
Abc_Ntk_t * pNtk, * pNtkRes;
int c;
extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk );
pNtk = Abc_FrameReadNet(pAbc);
pOut = Abc_FrameReadOut(pAbc);
......@@ -3807,19 +3808,18 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
if ( !Abc_NtkIsStrash(pNtk) )
if ( Abc_NtkIsSeq(pNtk) )
{
fprintf( pErr, "Only works for strashed networks.\n" );
fprintf( pErr, "Only works for non-sequential networks.\n" );
return 1;
}
// Abc_NtkTestEsop( pNtk );
// Abc_NtkTestSop( pNtk );
// printf( "This command is currently not used.\n" );
/*
// run the command
pNtkRes = Abc_NtkMiterForCofactors( pNtk, 0, 0, -1 );
// pNtkRes = Abc_NtkMiterForCofactors( pNtk, 0, 0, -1 );
pNtkRes = Abc_NtkNewAig( pNtk );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
......@@ -3827,7 +3827,6 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
*/
return 0;
usage:
......
src/base/abci/abcSat.c
......@@ -534,10 +534,10 @@ int Abc_NtkClauseMux( solver * pSat, Abc_Obj_t * pNode, Abc_Obj_t * pNodeC, Abc_
Vec_IntPush( vVars, toLitCond(VarF, 1) );
if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
return 0;
if ( VarT == VarE )
{
assert( fCompT == !fCompE );
// assert( fCompT == !fCompE );
return 1;
}
......@@ -774,7 +774,7 @@ solver * Abc_NtkMiterSatCreate2( Abc_Ntk_t * pNtk )
RetValue = Abc_NtkMiterSatCreate2Int( pSat, pNtk );
Abc_NtkForEachObj( pNtk, pNode, i )
pNode->fMarkA = 0;
Asat_SolverWriteDimacs( pSat, "temp_sat.cnf", NULL, NULL, 1 );
// Asat_SolverWriteDimacs( pSat, "temp_sat.cnf", NULL, NULL, 1 );
if ( RetValue == 0 )
{
solver_delete(pSat);
......
src/bdd/dsd/dsdCheck.c
......@@ -82,7 +82,7 @@ void Dsd_CheckCacheAllocate( int nEntries )
/**Function********************************************************************
Synopsis [Delocates the local cache.]
Synopsis [Deallocates the local cache.]
Description []
......
src/misc/extra/extraBddSymm.c
......@@ -223,7 +223,7 @@ Extra_SymmInfo_t * Extra_SymmPairsAllocate( int nVars )
/**Function********************************************************************
Synopsis [Delocates symmetry information structure.]
Synopsis [Deallocates symmetry information structure.]
Description []
......
src/misc/extra/extraUtilMemory.c
......@@ -257,7 +257,7 @@ void Extra_MmFixedRestart( Extra_MmFixed_t * p )
int i;
char * pTemp;
// delocate all chunks except the first one
// deallocate all chunks except the first one
for ( i = 1; i < p->nChunks; i++ )
free( p->pChunks[i] );
p->nChunks = 1;
......
src/opt/dec/decAbc.c
......@@ -18,6 +18,7 @@
#include "abc.h"
#include "dec.h"
#include "aig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
......@@ -201,6 +202,40 @@ void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpda
assert( nGain <= nNodesOld - nNodesNew );
}
/**Function*************************************************************
Synopsis [Transforms the decomposition graph into the AIG.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Node_t * Dec_GraphToNetworkAig( Aig_Man_t * pMan, Dec_Graph_t * pGraph )
{
Dec_Node_t * pNode;
Aig_Node_t * pAnd0, * pAnd1;
int i;
// check for constant function
if ( Dec_GraphIsConst(pGraph) )
return Aig_NotCond( Aig_ManConst1(pMan), Dec_GraphIsComplement(pGraph) );
// check for a literal
if ( Dec_GraphIsVar(pGraph) )
return Aig_NotCond( Dec_GraphVar(pGraph)->pFunc, Dec_GraphIsComplement(pGraph) );
// build the AIG nodes corresponding to the AND gates of the graph
Dec_GraphForEachNode( pGraph, pNode, i )
{
pAnd0 = Aig_NotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl );
pAnd1 = Aig_NotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl );
pNode->pFunc = Aig_And( pMan, pAnd0, pAnd1 );
}
// complement the result if necessary
return Aig_NotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/opt/fxu/fxu.c
......@@ -159,7 +159,7 @@ int Fxu_FastExtract( Fxu_Data_t * pData )
if ( pData->nNodesNew )
Fxu_CreateCovers( p, pData );
Fxu_MatrixDelete( p );
// printf( "Memory usage after delocation: Total = %d. Peak = %d.\n", s_MemoryTotal, s_MemoryPeak );
// printf( "Memory usage after deallocation: Total = %d. Peak = %d.\n", s_MemoryTotal, s_MemoryPeak );
if ( pData->nNodesNew == pData->nNodesExt )
printf( "Warning: The limit on the number of extracted divisors has been reached.\n" );
return pData->nNodesNew;
......
src/sat/aig/aig.h
......@@ -48,6 +48,7 @@
////////////////////////////////////////////////////////////////////////
#include <stdio.h>
#include "solver.h"
#include "vec.h"
////////////////////////////////////////////////////////////////////////
......@@ -70,6 +71,7 @@ typedef struct Aig_Edge_t_ Aig_Edge_t;
typedef struct Aig_MemFixed_t_ Aig_MemFixed_t;
typedef struct Aig_SimInfo_t_ Aig_SimInfo_t;
typedef struct Aig_Table_t_ Aig_Table_t;
typedef struct Aig_Pattern_t_ Aig_Pattern_t;
// network types
typedef enum {
......@@ -79,12 +81,25 @@ typedef enum {
AIG_AND // 3: internal node
} Aig_NodeType_t;
// proof outcomes
typedef enum {
AIG_PROOF_NONE = 0, // 0: unknown
AIG_PROOF_SAT, // 1: primary input
AIG_PROOF_UNSAT, // 2: primary output
AIG_PROOF_TIMEOUT, // 3: primary output
AIG_PROOF_FAIL // 4: internal node
} Aig_ProofType_t;
// the AIG parameters
struct Aig_Param_t_
{
int nPatsRand; // the number of random patterns
int nBTLimit; // backtrack limit at the intermediate nodes
int nSeconds; // the runtime limit at the final miter
int fVerbose; // verbosity
int fSatVerbose; // verbosity of SAT
};
// the AIG edge
......@@ -127,6 +142,13 @@ struct Aig_Man_t_
Vec_Ptr_t * vPos; // all POs
Aig_Table_t * pTable; // structural hash table
int nLevelMax; // the maximum level
// SAT solver and related structures
solver * pSat;
Vec_Int_t * vVar2Sat; // mapping of nodes into their SAT var numbers (for each node num)
Vec_Int_t * vSat2Var; // mapping of the SAT var numbers into nodes (for each SAT var)
Vec_Int_t * vPiSatNums; // the SAT variable numbers (for each PI)
int * pModel; // the satisfying assignment (for each PI)
int nMuxes; // the number of MUXes
// fanout representation
Vec_Ptr_t * vFanPivots; // fanout pivots
Vec_Ptr_t * vFanFans0; // the next fanout of the first fanin
......@@ -136,6 +158,7 @@ struct Aig_Man_t_
int nTravIds; // the traversal ID
// simulation info
Aig_SimInfo_t * pInfo; // random and systematic sim info for PIs
Aig_SimInfo_t * pInfoPi; // temporary sim info for the PI nodes
Aig_SimInfo_t * pInfoTemp; // temporary sim info for all nodes
// simulation patterns
int nPiWords; // the number of words in the PI info
......@@ -148,6 +171,14 @@ struct Aig_Man_t_
Vec_Ptr_t * vToReplace; // the nodes to replace
};
// the simulation patter
struct Aig_Pattern_t_
{
int nBits;
int nWords;
unsigned * pData;
};
// the AIG simulation info
struct Aig_SimInfo_t_
{
......@@ -166,9 +197,9 @@ struct Aig_SimInfo_t_
for ( i = 0; (i < Aig_ManPiNum(pMan)) && (((pNode) = Aig_ManPi(pMan, i)), 1); i++ )
#define Aig_ManForEachPo( pMan, pNode, i ) \
for ( i = 0; (i < Aig_ManPoNum(pMan)) && (((pNode) = Aig_ManPo(pMan, i)), 1); i++ )
#define Aig_ManForEachAnd( pNtk, pNode, i ) \
#define Aig_ManForEachAnd( pMan, pNode, i ) \
for ( i = 0; (i < Aig_ManNodeNum(pMan)) && (((pNode) = Aig_ManNode(pMan, i)), 1); i++ ) \
if ( Aig_NodeIsAnd(pNode) ) {} else
if ( !Aig_NodeIsAnd(pNode) ) {} else
// maximum/minimum operators
#define AIG_MIN(a,b) (((a) < (b))? (a) : (b))
......@@ -178,8 +209,12 @@ struct Aig_SimInfo_t_
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
static inline int Aig_BitWordNum( int nBits ) { return nBits/32 + ((nBits%32) > 0); }
static inline int Aig_BitWordNum( int nBits ) { return nBits/32 + ((nBits%32) > 0); }
static inline int Aig_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; }
static inline void Aig_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); }
static inline void Aig_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); }
static inline Aig_Node_t * Aig_ManConst1( Aig_Man_t * pMan ) { return pMan->pConst1; }
static inline Aig_Node_t * Aig_ManNode( Aig_Man_t * pMan, int i ) { return Vec_PtrEntry(pMan->vNodes, i); }
static inline Aig_Node_t * Aig_ManPi( Aig_Man_t * pMan, int i ) { return Vec_PtrEntry(pMan->vPis, i); }
static inline Aig_Node_t * Aig_ManPo( Aig_Man_t * pMan, int i ) { return Vec_PtrEntry(pMan->vPos, i); }
......@@ -216,7 +251,8 @@ static inline Aig_Node_t * Aig_NodeChild0( Aig_Node_t * pNode ) { return Aig_N
static inline Aig_Node_t * Aig_NodeChild1( Aig_Node_t * pNode ) { return Aig_NotCond( Aig_NodeFanin1(pNode), Aig_NodeFaninC1(pNode) ); }
static inline Aig_Node_t * Aig_NodeNextH( Aig_Node_t * pNode ) { return pNode->NextH? Aig_ManNode(pNode->pMan, pNode->NextH) : NULL; }
static inline int Aig_NodeWhatFanin( Aig_Node_t * pNode, Aig_Node_t * pFanin ) { if ( Aig_NodeFaninId0(pNode) == pFanin->Id ) return 0; if ( Aig_NodeFaninId1(pNode) == pFanin->Id ) return 1; assert(0); return -1; }
static inline int Aig_NodeGetLevelNew( Aig_Node_t * pNode ) { return 1 + AIG_MAX(Aig_NodeFanin0(pNode)->Level, Aig_NodeFanin1(pNode)->Level); }
static inline int Aig_NodeGetLevelNew( Aig_Node_t * pNode ) { return 1 + AIG_MAX(Aig_NodeFanin0(pNode)->Level, Aig_NodeFanin1(pNode)->Level); }
static inline int Aig_NodeRequiredLevel( Aig_Node_t * pNode ) { return pNode->pMan->nLevelMax + 1 - pNode->LevelR; }
static inline unsigned * Aig_SimInfoForNode( Aig_SimInfo_t * p, Aig_Node_t * pNode ) { assert( p->Type ); return p->pData + p->nWords * pNode->Id; }
static inline unsigned * Aig_SimInfoForPi( Aig_SimInfo_t * p, int Num ) { assert( !p->Type ); return p->pData + p->nWords * Num; }
......@@ -268,6 +304,7 @@ extern void Aig_NodeDisconnectAnd( Aig_Node_t * pNode );
extern void Aig_NodeDeleteAnd_rec( Aig_Man_t * pMan, Aig_Node_t * pRoot );
extern void Aig_NodePrint( Aig_Node_t * pNode );
extern char * Aig_NodeName( Aig_Node_t * pNode );
extern void Aig_PrintNode( Aig_Node_t * pNode );
/*=== aigOper.c ==========================================================*/
extern Aig_Node_t * Aig_And( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 );
extern Aig_Node_t * Aig_Or( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t * p1 );
......@@ -287,18 +324,33 @@ extern void Aig_TableResize( Aig_Man_t * pMan );
extern void Aig_TableRehash( Aig_Man_t * pMan );
/*=== aigUtil.c ==========================================================*/
extern void Aig_ManIncrementTravId( Aig_Man_t * pMan );
extern void Aig_PrintNode( Aig_Node_t * pNode );
extern bool Aig_NodeIsMuxType( Aig_Node_t * pNode );
extern Aig_Node_t * Aig_NodeRecognizeMux( Aig_Node_t * pNode, Aig_Node_t ** ppNodeT, Aig_Node_t ** ppNodeE );
/*=== fraigCore.c ==========================================================*/
extern Aig_ProofType_t Aig_FraigProve( Aig_Man_t * pMan );
/*=== fraigClasses.c ==========================================================*/
extern Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfoAll );
extern void Aig_ManUpdateClasses( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Vec_Vec_t * vClasses );
/*=== fraigCnf.c ==========================================================*/
extern Aig_ProofType_t Aig_ClauseSolverStart( Aig_Man_t * pMan );
/*=== fraigEngine.c ==========================================================*/
extern void Aig_EngineSimulateFirst( Aig_Man_t * p );
extern int Aig_EngineSimulate( Aig_Man_t * p );
extern void Aig_EngineSimulateRandomFirst( Aig_Man_t * p );
/*=== fraigSim.c ==========================================================*/
extern Aig_SimInfo_t * Aig_SimInfoAlloc( int nNodes, int nWords, int Type );
extern void Aig_SimInfoClean( Aig_SimInfo_t * p );
extern void Aig_SimInfoRandom( Aig_SimInfo_t * p );
extern void Aig_SimInfoFromPattern( Aig_SimInfo_t * p, Aig_Pattern_t * pPat );
extern void Aig_SimInfoResize( Aig_SimInfo_t * p );
extern void Aig_SimInfoFree( Aig_SimInfo_t * p );
extern Aig_SimInfo_t * Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi );
extern void Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi, Aig_SimInfo_t * pInfoAll );
extern Aig_Pattern_t * Aig_PatternAlloc( int nBits );
extern void Aig_PatternClean( Aig_Pattern_t * pPat );
extern void Aig_PatternRandom( Aig_Pattern_t * pPat );
extern void Aig_PatternFree( Aig_Pattern_t * pPat );
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
......
src/sat/aig/aigMan.c
......@@ -66,10 +66,11 @@ Aig_Man_t * Aig_ManStart( Aig_Param_t * pParam )
// start the manager
p = ALLOC( Aig_Man_t, 1 );
memset( p, 0, sizeof(Aig_Man_t) );
p->pParam = &p->Param;
p->nTravIds = 1;
p->pParam = &p->Param;
p->nTravIds = 1;
p->nPatsMax = 20;
// set the defaults
*p->pParam = *pParam;
*p->pParam = *pParam;
// start memory managers
p->mmNodes = Aig_MemFixedStart( sizeof(Aig_Node_t) );
// allocate node arrays
......@@ -121,14 +122,22 @@ int Aig_ManCleanup( Aig_Man_t * pMan )
***********************************************************************/
void Aig_ManStop( Aig_Man_t * p )
{
// SAT solver
if ( p->pSat ) solver_delete( p->pSat );
if ( p->vVar2Sat ) Vec_IntFree( p->vVar2Sat );
if ( p->vSat2Var ) Vec_IntFree( p->vSat2Var );
if ( p->vPiSatNums ) Vec_IntFree( p->vPiSatNums );
// fanouts
if ( p->vFanPivots ) Vec_PtrFree( p->vFanPivots );
if ( p->vFanFans0 ) Vec_PtrFree( p->vFanFans0 );
if ( p->vFanFans1 ) Vec_PtrFree( p->vFanFans1 );
if ( p->vClasses ) Vec_VecFree( p->vClasses );
// nodes
Aig_MemFixedStop( p->mmNodes, 0 );
Vec_PtrFree( p->vNodes );
Vec_PtrFree( p->vPis );
Vec_PtrFree( p->vPos );
// temporary
Vec_PtrFree( p->vFanouts );
Vec_PtrFree( p->vToReplace );
Aig_TableFree( p->pTable );
......
src/sat/aig/aigMem.c
......@@ -201,7 +201,7 @@ void Aig_MemFixedRestart( Aig_MemFixed_t * p )
int i;
char * pTemp;
// delocate all chunks except the first one
// deallocate all chunks except the first one
for ( i = 1; i < p->nChunks; i++ )
free( p->pChunks[i] );
p->nChunks = 1;
......
src/sat/aig/aigNode.c
......@@ -46,6 +46,7 @@ static inline Aig_Node_t * Aig_NodeCreate( Aig_Man_t * p )
pNode = (Aig_Node_t *)Aig_MemFixedEntryFetch( p->mmNodes );
memset( pNode, 0, sizeof(Aig_Node_t) );
// assign the number and add to the array of nodes
pNode->pMan = p;
pNode->Id = p->vNodes->nSize;
Vec_PtrPush( p->vNodes, pNode );
return pNode;
......@@ -66,6 +67,7 @@ Aig_Node_t * Aig_NodeCreateConst( Aig_Man_t * p )
{
Aig_Node_t * pNode;
pNode = Aig_NodeCreate( p );
pNode->Type = AIG_NONE;
pNode->fPhase = 1; // sim value for 000... pattern
return pNode;
}
......@@ -86,7 +88,8 @@ Aig_Node_t * Aig_NodeCreatePi( Aig_Man_t * p )
Aig_Node_t * pNode;
pNode = Aig_NodeCreate( p );
Vec_PtrPush( p->vPis, pNode );
pNode->fPhase = 0; // sim value for 000... pattern
pNode->Type = AIG_PI;
pNode->fPhase = 0; // sim value for 000... pattern
return pNode;
}
......@@ -105,6 +108,7 @@ Aig_Node_t * Aig_NodeCreatePo( Aig_Man_t * p, Aig_Node_t * pFanin )
{
Aig_Node_t * pNode;
pNode = Aig_NodeCreate( p );
pNode->Type = AIG_PO;
Vec_PtrPush( p->vPos, pNode );
// connect to the fanin
pNode->Fans[0].fComp = Aig_IsComplement(pFanin);
......@@ -134,6 +138,7 @@ Aig_Node_t * Aig_NodeCreateAnd( Aig_Man_t * p, Aig_Node_t * pFanin0, Aig_Node_t
{
Aig_Node_t * pNode;
pNode = Aig_NodeCreate( p );
pNode->Type = AIG_AND;
Aig_NodeConnectAnd( pFanin0, pFanin1, pNode );
return pNode;
}
......
src/sat/aig/aigTable.c
......@@ -36,7 +36,7 @@ struct Aig_Table_t_
#define Aig_TableBinForEachEntry( pBin, pEnt ) \
for ( pEnt = pBin; \
pEnt; \
pEnt = pEnt->NextH? Aig_ManNode(pEnt->pMan, pEnt->NextH) : NULL )
pEnt = Aig_NodeNextH(pEnt) )
#define Aig_TableBinForEachEntrySafe( pBin, pEnt, pEnt2 ) \
for ( pEnt = pBin, \
pEnt2 = pEnt? Aig_NodeNextH(pEnt) : NULL; \
......@@ -127,9 +127,8 @@ Aig_Node_t * Aig_TableLookupNode( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t
Aig_Node_t * pAnd;
unsigned Key;
assert( Aig_Regular(p0)->Id < Aig_Regular(p1)->Id );
assert( p0->pMan == p1->pMan );
// get the hash key for these two nodes
Key = Abc_HashKey2( p0, p1, pMan->pTable->nBins );
Key = Abc_HashKey2( p0, p1, pMan->pTable->nBins );
// find the matching node in the table
Aig_TableBinForEachEntry( pMan->pTable->pBins[Key], pAnd )
if ( p0 == Aig_NodeChild0(pAnd) && p1 == Aig_NodeChild1(pAnd) )
......@@ -157,8 +156,8 @@ Aig_Node_t * Aig_TableInsertNode( Aig_Man_t * pMan, Aig_Node_t * p0, Aig_Node_t
Aig_TableResize( pMan );
// add the node to the corresponding linked list in the table
Key = Abc_HashKey2( p0, p1, pMan->pTable->nBins );
pAnd->NextH = pMan->pTable->pBins[Key]->Id;
pMan->pTable->pBins[Key]->NextH = pAnd->Id;
pAnd->NextH = pMan->pTable->pBins[Key]? pMan->pTable->pBins[Key]->Id : 0;
pMan->pTable->pBins[Key] = pAnd;
pMan->pTable->nEntries++;
return pAnd;
}
......@@ -195,7 +194,7 @@ void Aig_TableDeleteNode( Aig_Man_t * pMan, Aig_Node_t * pThis )
if ( pPlace == NULL )
pMan->pTable->pBins[Key] = Aig_NodeNextH(pThis);
else
pPlace->NextH = pThis->Id;
pPlace->NextH = pThis->NextH;
break;
}
assert( pThis == pAnd );
......@@ -232,8 +231,8 @@ clk = clock();
Aig_TableBinForEachEntrySafe( pMan->pTable->pBins[i], pEnt, pEnt2 )
{
Key = Abc_HashKey2( Aig_NodeChild0(pEnt), Aig_NodeChild1(pEnt), nBinsNew );
pEnt->NextH = pBinsNew[Key]->Id;
pBinsNew[Key]->NextH = pEnt->Id;
pEnt->NextH = pBinsNew[Key]? pBinsNew[Key]->Id : 0;
pBinsNew[Key] = pEnt;
Counter++;
}
assert( Counter == pMan->pTable->nEntries );
......@@ -282,8 +281,8 @@ void Aig_TableRehash( Aig_Man_t * pMan )
}
// rehash the node
Key = Abc_HashKey2( Aig_NodeChild0(pEnt), Aig_NodeChild1(pEnt), pMan->pTable->nBins );
pEnt->NextH = pBinsNew[Key]->Id;
pBinsNew[Key]->NextH = pEnt->Id;
pEnt->NextH = pBinsNew[Key]? pBinsNew[Key]->Id : 0;
pBinsNew[Key] = pEnt;
Counter++;
}
assert( Counter == pMan->pTable->nEntries );
......
src/sat/aig/aigUtil.c
......@@ -53,6 +53,136 @@ void Aig_ManIncrementTravId( Aig_Man_t * pMan )
}
/**Function*************************************************************
Synopsis [Returns 1 if the node is the root of MUX or EXOR/NEXOR.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
bool Aig_NodeIsMuxType( Aig_Node_t * pNode )
{
Aig_Node_t * pNode0, * pNode1;
// check that the node is regular
assert( !Aig_IsComplement(pNode) );
// if the node is not AND, this is not MUX
if ( !Aig_NodeIsAnd(pNode) )
return 0;
// if the children are not complemented, this is not MUX
if ( !Aig_NodeFaninC0(pNode) || !Aig_NodeFaninC1(pNode) )
return 0;
// get children
pNode0 = Aig_NodeFanin0(pNode);
pNode1 = Aig_NodeFanin1(pNode);
// if the children are not ANDs, this is not MUX
if ( !Aig_NodeIsAnd(pNode0) || !Aig_NodeIsAnd(pNode1) )
return 0;
// otherwise the node is MUX iff it has a pair of equal grandchildren
return (Aig_NodeFaninId0(pNode0) == Aig_NodeFaninId0(pNode1) && (Aig_NodeFaninC0(pNode0) ^ Aig_NodeFaninC0(pNode1))) ||
(Aig_NodeFaninId0(pNode0) == Aig_NodeFaninId1(pNode1) && (Aig_NodeFaninC0(pNode0) ^ Aig_NodeFaninC1(pNode1))) ||
(Aig_NodeFaninId1(pNode0) == Aig_NodeFaninId0(pNode1) && (Aig_NodeFaninC1(pNode0) ^ Aig_NodeFaninC0(pNode1))) ||
(Aig_NodeFaninId1(pNode0) == Aig_NodeFaninId1(pNode1) && (Aig_NodeFaninC1(pNode0) ^ Aig_NodeFaninC1(pNode1)));
}
/**Function*************************************************************
Synopsis [Recognizes what nodes are control and data inputs of a MUX.]
Description [If the node is a MUX, returns the control variable C.
Assigns nodes T and E to be the then and else variables of the MUX.
Node C is never complemented. Nodes T and E can be complemented.
This function also recognizes EXOR/NEXOR gates as MUXes.]
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Node_t * Aig_NodeRecognizeMux( Aig_Node_t * pNode, Aig_Node_t ** ppNodeT, Aig_Node_t ** ppNodeE )
{
Aig_Node_t * pNode0, * pNode1;
assert( !Aig_IsComplement(pNode) );
assert( Aig_NodeIsMuxType(pNode) );
// get children
pNode0 = Aig_NodeFanin0(pNode);
pNode1 = Aig_NodeFanin1(pNode);
// find the control variable
// if ( pNode1->p1 == Fraig_Not(pNode2->p1) )
if ( Aig_NodeFaninId0(pNode0) == Aig_NodeFaninId0(pNode1) && (Aig_NodeFaninC0(pNode0) ^ Aig_NodeFaninC0(pNode1)) )
{
// if ( Fraig_IsComplement(pNode1->p1) )
if ( Aig_NodeFaninC0(pNode0) )
{ // pNode2->p1 is positive phase of C
*ppNodeT = Aig_Not(Aig_NodeChild1(pNode1));//pNode2->p2);
*ppNodeE = Aig_Not(Aig_NodeChild1(pNode0));//pNode1->p2);
return Aig_NodeChild0(pNode1);//pNode2->p1;
}
else
{ // pNode1->p1 is positive phase of C
*ppNodeT = Aig_Not(Aig_NodeChild1(pNode0));//pNode1->p2);
*ppNodeE = Aig_Not(Aig_NodeChild1(pNode1));//pNode2->p2);
return Aig_NodeChild0(pNode0);//pNode1->p1;
}
}
// else if ( pNode1->p1 == Fraig_Not(pNode2->p2) )
else if ( Aig_NodeFaninId0(pNode0) == Aig_NodeFaninId1(pNode1) && (Aig_NodeFaninC0(pNode0) ^ Aig_NodeFaninC1(pNode1)) )
{
// if ( Fraig_IsComplement(pNode1->p1) )
if ( Aig_NodeFaninC0(pNode0) )
{ // pNode2->p2 is positive phase of C
*ppNodeT = Aig_Not(Aig_NodeChild0(pNode1));//pNode2->p1);
*ppNodeE = Aig_Not(Aig_NodeChild1(pNode0));//pNode1->p2);
return Aig_NodeChild1(pNode1);//pNode2->p2;
}
else
{ // pNode1->p1 is positive phase of C
*ppNodeT = Aig_Not(Aig_NodeChild1(pNode0));//pNode1->p2);
*ppNodeE = Aig_Not(Aig_NodeChild0(pNode1));//pNode2->p1);
return Aig_NodeChild0(pNode0);//pNode1->p1;
}
}
// else if ( pNode1->p2 == Fraig_Not(pNode2->p1) )
else if ( Aig_NodeFaninId1(pNode0) == Aig_NodeFaninId0(pNode1) && (Aig_NodeFaninC1(pNode0) ^ Aig_NodeFaninC0(pNode1)) )
{
// if ( Fraig_IsComplement(pNode1->p2) )
if ( Aig_NodeFaninC1(pNode0) )
{ // pNode2->p1 is positive phase of C
*ppNodeT = Aig_Not(Aig_NodeChild1(pNode1));//pNode2->p2);
*ppNodeE = Aig_Not(Aig_NodeChild0(pNode0));//pNode1->p1);
return Aig_NodeChild0(pNode1);//pNode2->p1;
}
else
{ // pNode1->p2 is positive phase of C
*ppNodeT = Aig_Not(Aig_NodeChild0(pNode0));//pNode1->p1);
*ppNodeE = Aig_Not(Aig_NodeChild1(pNode1));//pNode2->p2);
return Aig_NodeChild1(pNode0);//pNode1->p2;
}
}
// else if ( pNode1->p2 == Fraig_Not(pNode2->p2) )
else if ( Aig_NodeFaninId1(pNode0) == Aig_NodeFaninId1(pNode1) && (Aig_NodeFaninC1(pNode0) ^ Aig_NodeFaninC1(pNode1)) )
{
// if ( Fraig_IsComplement(pNode1->p2) )
if ( Aig_NodeFaninC1(pNode0) )
{ // pNode2->p2 is positive phase of C
*ppNodeT = Aig_Not(Aig_NodeChild0(pNode1));//pNode2->p1);
*ppNodeE = Aig_Not(Aig_NodeChild0(pNode0));//pNode1->p1);
return Aig_NodeChild1(pNode1);//pNode2->p2;
}
else
{ // pNode1->p2 is positive phase of C
*ppNodeT = Aig_Not(Aig_NodeChild0(pNode0));//pNode1->p1);
*ppNodeE = Aig_Not(Aig_NodeChild0(pNode1));//pNode2->p1);
return Aig_NodeChild1(pNode0);//pNode1->p2;
}
}
assert( 0 ); // this is not MUX
return NULL;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/sat/aig/fraigClass.c
/**CFile****************************************************************
FileName [aigFraig.c]
FileName [fraigClass.c]
SystemName [ABC: Logic synthesis and verification system.]
......@@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: aigFraig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
Revision [$Id: fraigClass.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
......@@ -25,7 +25,7 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static unsigned Aig_ManHashKey( unsigned * pData, int nWords );
static unsigned Aig_ManHashKey( unsigned * pData, int nWords, bool fPhase );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
......@@ -44,20 +44,24 @@ static unsigned Aig_ManHashKey( unsigned * pData, int nWords );
***********************************************************************/
Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfo )
{
Vec_Vec_t * vClasses; // equivalence classes
Vec_Vec_t * vClasses; // equivalence classes
stmm_table * tSim2Node; // temporary hash table hashing key into the class number
Aig_Node_t * pNode;
unsigned uKey;
int i, * pSpot, ClassNum;
int i, * pSpot, Entry, ClassNum;
assert( pInfo->Type == 1 );
// fill in the hash table
tSim2Node = stmm_init_table( stmm_numcmp, stmm_numhash );
vClasses = Vec_VecAlloc( 100 );
Aig_ManForEachNode( p, pNode, i )
// enumerate the nodes considered in the equivalence classes
// Aig_ManForEachNode( p, pNode, i )
Vec_IntForEachEntry( p->vSat2Var, Entry, i )
{
pNode = Aig_ManNode( p, Entry );
if ( Aig_NodeIsPo(pNode) )
continue;
uKey = Aig_ManHashKey( Aig_SimInfoForNode(pInfo, pNode), pInfo->nWords );
uKey = Aig_ManHashKey( Aig_SimInfoForNode(pInfo, pNode), pInfo->nWords, pNode->fPhase );
if ( !stmm_find_or_add( tSim2Node, (char *)uKey, (char ***)&pSpot ) ) // does not exist
*pSpot = (pNode->Id << 1) | 1; // save the node, and do nothing
else if ( (*pSpot) & 1 ) // this is a node
......@@ -71,11 +75,24 @@ Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfo )
}
else // this is a class
{
ClassNum = (*pSpot) >> 1;
ClassNum = ((*pSpot) >> 1);
Vec_VecPush( vClasses, ClassNum, (void *)pNode->Id );
}
}
stmm_free_table( tSim2Node );
// print the classes
{
Vec_Ptr_t * vVec;
printf( "PI/PO = %4d/%4d. Nodes = %7d. SatVars = %7d. Non-trivial classes = %5d: \n",
Aig_ManPiNum(p), Aig_ManPoNum(p),
Aig_ManNodeNum(p) - Aig_ManPoNum(p),
Vec_IntSize(p->vSat2Var), Vec_VecSize(vClasses) );
Vec_VecForEachLevel( vClasses, vVec, i )
printf( "%d ", Vec_PtrSize(vVec) );
printf( "\n" );
}
return vClasses;
}
......@@ -90,17 +107,38 @@ Vec_Vec_t * Aig_ManDeriveClassesFirst( Aig_Man_t * p, Aig_SimInfo_t * pInfo )
SeeAlso []
***********************************************************************/
unsigned Aig_ManHashKey( unsigned * pData, int nWords )
unsigned Aig_ManHashKey( unsigned * pData, int nWords, bool fPhase )
{
static int Primes[10] = { 1009, 2207, 3779, 4001, 4877, 5381, 6427, 6829, 7213, 7919 };
unsigned uKey;
int i;
uKey = 0;
for ( i = 0; i < nWords; i++ )
uKey ^= pData[i] * Primes[i%10];
if ( fPhase )
for ( i = 0; i < nWords; i++ )
uKey ^= Primes[i%10] * pData[i];
else
for ( i = 0; i < nWords; i++ )
uKey ^= Primes[i%10] * ~pData[i];
return uKey;
}
/**Function*************************************************************
Synopsis [Updates the equivalence classes using the simulation info.]
Description [Records successful simulation patterns into the pattern
storage.]
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManUpdateClasses( Aig_Man_t * p, Aig_SimInfo_t * pInfo, Vec_Vec_t * vClasses )
{
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/sat/aig/fraigCore.c
/**CFile****************************************************************
FileName [aigFraig.c]
FileName [fraigCore.c]
SystemName [ABC: Logic synthesis and verification system.]
......@@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: aigFraig.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
Revision [$Id: fraigCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
......@@ -24,13 +24,56 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static Aig_ProofType_t Aig_FraigProveOutput( Aig_Man_t * pMan );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Synopsis [Top-level equivalence checking procedure.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_ProofType_t Aig_FraigProve( Aig_Man_t * pMan )
{
Aig_ProofType_t RetValue;
int clk, status;
// create the solver
RetValue = Aig_ClauseSolverStart( pMan );
if ( RetValue != AIG_PROOF_NONE )
return RetValue;
// perform solving
// simplify the problem
clk = clock();
status = solver_simplify(pMan->pSat);
if ( status == 0 )
{
// printf( "The problem is UNSATISFIABLE after simplification.\n" );
return AIG_PROOF_UNSAT;
}
// try to prove the output
RetValue = Aig_FraigProveOutput( pMan );
if ( RetValue != AIG_PROOF_TIMEOUT )
return RetValue;
// create equivalence classes
Aig_EngineSimulateRandomFirst( pMan );
return RetValue;
}
/**Function*************************************************************
Synopsis [Top-level equivalence checking procedure.]
Description []
......@@ -39,6 +82,43 @@
SeeAlso []
***********************************************************************/
Aig_ProofType_t Aig_FraigProveOutput( Aig_Man_t * pMan )
{
Aig_ProofType_t RetValue;
int clk, status;
// solve the miter
clk = clock();
pMan->pSat->verbosity = pMan->pParam->fSatVerbose;
status = solver_solve( pMan->pSat, NULL, NULL, pMan->pParam->nSeconds );
if ( status == l_Undef )
{
// printf( "The problem timed out.\n" );
RetValue = AIG_PROOF_TIMEOUT;
}
else if ( status == l_True )
{
// printf( "The problem is SATISFIABLE.\n" );
RetValue = AIG_PROOF_SAT;
}
else if ( status == l_False )
{
// printf( "The problem is UNSATISFIABLE.\n" );
RetValue = AIG_PROOF_UNSAT;
}
else
assert( 0 );
// PRT( "SAT solver time", clock() - clk );
// if the problem is SAT, get the counterexample
if ( status == l_True )
{
if ( pMan->pModel ) free( pMan->pModel );
pMan->pModel = solver_get_model( pMan->pSat, pMan->vPiSatNums->pArray, pMan->vPiSatNums->nSize );
printf( "%d %d %d %d\n", pMan->pModel[0], pMan->pModel[1], pMan->pModel[2], pMan->pModel[3] );
}
return RetValue;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
......
src/sat/aig/fraigEngine.c 0 → 100644
/**CFile****************************************************************
FileName [fraigEngine.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [And-Inverter Graph package.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: fraigEngine.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "aig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Starts the simulation engine for the first time.]
Description [Tries several random patterns and their distance-1
minterms hoping to get simulation started.]
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_EngineSimulateFirst( Aig_Man_t * p )
{
Aig_Pattern_t * pPat;
int i;
assert( Vec_PtrSize(p->vPats) == 0 );
for ( i = 0; i < p->nPatsMax; i++ )
{
pPat = Aig_PatternAlloc( Aig_ManPiNum(p) );
Aig_PatternRandom( pPat );
Vec_PtrPush( p->vPats, pPat );
if ( !Aig_EngineSimulate( p ) )
return;
}
}
/**Function*************************************************************
Synopsis [Implements intelligent simulation engine.]
Description [Assumes that the good simulation patterns have been
assigned (p->vPats). Simulates until all of them are gone. Returns 1
if some classes are left. Returns 0 if there is no more classes.]
SideEffects []
SeeAlso []
***********************************************************************/
int Aig_EngineSimulate( Aig_Man_t * p )
{
Aig_Pattern_t * pPat;
if ( Vec_VecSize(p->vClasses) == 0 )
return 0;
assert( Vec_PtrSize(p->vPats) > 0 );
// process patterns
while ( Vec_PtrSize(p->vPats) > 0 && Vec_VecSize(p->vClasses) > 0 )
{
// get the pattern and create new siminfo
pPat = Vec_PtrPop(p->vPats);
// create the new siminfo
Aig_SimInfoFromPattern( p->pInfoPi, pPat );
// free the patter
Aig_PatternFree( pPat );
// simulate this info
Aig_ManSimulateInfo( p, p->pInfoPi, p->pInfoTemp );
// split the classes and collect the new patterns
Aig_ManUpdateClasses( p, p->pInfoTemp, p->vClasses );
}
return Vec_VecSize(p->vClasses) > 0;
}
/**Function*************************************************************
Synopsis [Simulates all nodes using random simulation for the first time.]
Description [Assigns the original simulation info and the storage for the
future simulation info.]
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_EngineSimulateRandomFirst( Aig_Man_t * p )
{
Aig_SimInfo_t * pInfoPi, * pInfoAll;
assert( !p->pInfo && !p->pInfoTemp );
// create random PI info
pInfoPi = Aig_SimInfoAlloc( p->vPis->nSize, Aig_BitWordNum(p->pParam->nPatsRand), 0 );
Aig_SimInfoRandom( pInfoPi );
// allocate sim info for all nodes
pInfoAll = Aig_SimInfoAlloc( p->vNodes->nSize, pInfoPi->nWords, 1 );
// simulate though the circuit
Aig_ManSimulateInfo( p, pInfoPi, pInfoAll );
// detect classes
p->vClasses = Aig_ManDeriveClassesFirst( p, pInfoAll );
Aig_SimInfoFree( pInfoAll );
// save simulation info
p->pInfo = pInfoPi;
p->pInfoPi = Aig_SimInfoAlloc( p->vPis->nSize, Aig_BitWordNum(p->vPis->nSize), 0 );
p->pInfoTemp = Aig_SimInfoAlloc( p->vNodes->nSize, Aig_BitWordNum(p->vPis->nSize), 1 );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/sat/aig/fraigProve.c
/**CFile****************************************************************
FileName [aigProve.c]
FileName [fraigProve.c]
SystemName [ABC: Logic synthesis and verification system.]
......@@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: aigProve.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
Revision [$Id: fraigProve.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
......
src/sat/aig/fraigSim.c
/**CFile****************************************************************
FileName [aigSim.c]
FileName [fraigSim.c]
SystemName [ABC: Logic synthesis and verification system.]
......@@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: aigSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
Revision [$Id: fraigSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
......@@ -30,59 +30,28 @@
/**Function*************************************************************
Synopsis [Simulates all nodes using random simulation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_ManSimulateRandomFirst( Aig_Man_t * p )
{
Aig_SimInfo_t * pInfoPi, * pInfoAll;
assert( p->pInfo && p->pInfoTemp );
// create random PI info
pInfoPi = Aig_SimInfoAlloc( p->vPis->nSize, Aig_BitWordNum(p->pParam->nPatsRand), 0 );
Aig_SimInfoRandom( pInfoPi );
// simulate it though the circuit
pInfoAll = Aig_ManSimulateInfo( p, pInfoPi );
// detect classes
p->vClasses = Aig_ManDeriveClassesFirst( p, pInfoAll );
Aig_SimInfoFree( pInfoAll );
// save simulation info
p->pInfo = pInfoPi;
p->pInfoTemp = Aig_SimInfoAlloc( p->vNodes->nSize, Aig_BitWordNum(p->vPis->nSize), 1 );
}
/**Function*************************************************************
Synopsis [Simulates all nodes using the given simulation info.]
Description []
Description [Returns the simulation info for all nodes.]
SideEffects []
SeeAlso []
***********************************************************************/
Aig_SimInfo_t * Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi )
void Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi, Aig_SimInfo_t * pInfoAll )
{
Aig_SimInfo_t * pInfoAll;
Aig_Node_t * pNode;
unsigned * pDataPi, * pData0, * pData1, * pDataAnd;
unsigned * pDataPi, * pDataPo, * pData0, * pData1, * pDataAnd;
int i, k, fComp0, fComp1;
assert( !pInfoPi->Type ); // PI siminfo
// allocate sim info for all nodes
pInfoAll = Aig_SimInfoAlloc( p->vNodes->nSize, pInfoPi->nWords, 1 );
// set the constant sim info
pData1 = Aig_SimInfoForNode( pInfoAll, p->pConst1 );
for ( k = 0; k < pInfoPi->nWords; k++ )
pData1[k] = ~((unsigned)0);
// copy the PI siminfo
Vec_PtrForEachEntry( p->vPis, pNode, i )
// set the PI siminfo
Aig_ManForEachPi( p, pNode, i )
{
pDataPi = Aig_SimInfoForPi( pInfoPi, i );
pDataAnd = Aig_SimInfoForNode( pInfoAll, pNode );
......@@ -90,10 +59,8 @@ Aig_SimInfo_t * Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi )
pDataAnd[k] = pDataPi[k];
}
// simulate the nodes
Vec_PtrForEachEntry( p->vNodes, pNode, i )
Aig_ManForEachAnd( p, pNode, i )
{
if ( !Aig_NodeIsAnd(pNode) )
continue;
pData0 = Aig_SimInfoForNode( pInfoAll, Aig_NodeFanin0(pNode) );
pData1 = Aig_SimInfoForNode( pInfoAll, Aig_NodeFanin1(pNode) );
pDataAnd = Aig_SimInfoForNode( pInfoAll, pNode );
......@@ -112,13 +79,25 @@ Aig_SimInfo_t * Aig_ManSimulateInfo( Aig_Man_t * p, Aig_SimInfo_t * pInfoPi )
for ( k = 0; k < pInfoPi->nWords; k++ )
pDataAnd[k] = pData0[k] & pData1[k];
}
return pInfoAll;
// derive the PO siminfo
Aig_ManForEachPi( p, pNode, i )
{
pDataPo = Aig_SimInfoForNode( pInfoAll, pNode );
pDataAnd = Aig_SimInfoForNode( pInfoAll, Aig_NodeFanin0(pNode) );
if ( Aig_NodeFaninC0(pNode) )
for ( k = 0; k < pInfoPi->nWords; k++ )
pDataPo[k] = ~pDataAnd[k];
else
for ( k = 0; k < pInfoPi->nWords; k++ )
pDataPo[k] = pDataAnd[k];
}
}
/**Function*************************************************************
Synopsis []
Synopsis [Allocates the simulation info.]
Description []
......@@ -142,7 +121,7 @@ Aig_SimInfo_t * Aig_SimInfoAlloc( int nNodes, int nWords, int Type )
/**Function*************************************************************
Synopsis []
Synopsis [Sets the simulation info to zero.]
Description []
......@@ -161,7 +140,7 @@ void Aig_SimInfoClean( Aig_SimInfo_t * p )
/**Function*************************************************************
Synopsis []
Synopsis [Sets the random simulation info.]
Description []
......@@ -187,7 +166,40 @@ void Aig_SimInfoRandom( Aig_SimInfo_t * p )
/**Function*************************************************************
Synopsis []
Synopsis [Sets the random simulation info.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_SimInfoFromPattern( Aig_SimInfo_t * p, Aig_Pattern_t * pPat )
{
unsigned * pData;
int i, k;
assert( p->Type == 0 );
assert( p->nNodes == pPat->nBits );
for ( i = 0; i < p->nNodes; i++ )
{
// get the pointer to the bitdata for node i
pData = p->pData + p->nWords * i;
// fill in the bit data according to the pattern
if ( Aig_InfoHasBit(pPat->pData, i) ) // PI has bit set to 1
for ( k = 0; k < p->nWords; k++ )
pData[k] = ~((unsigned)0);
else
for ( k = 0; k < p->nWords; k++ )
pData[k] = 0;
// flip one bit
Aig_InfoXorBit( pData, i );
}
}
/**Function*************************************************************
Synopsis [Resizes the simulation info.]
Description []
......@@ -209,13 +221,15 @@ void Aig_SimInfoResize( Aig_SimInfo_t * p )
for ( k = 0; k < p->nWords; k++ )
pData[2 * p->nWords * i + k + p->nWords] = 0;
}
p->nPatsMax *= 2;
p->nWords *= 2;
p->nPatsMax *= 2;
free( p->pData );
p->pData = pData;
}
/**Function*************************************************************
Synopsis []
Synopsis [Deallocates the simulation info.]
Description []
......@@ -231,6 +245,80 @@ void Aig_SimInfoFree( Aig_SimInfo_t * p )
}
/**Function*************************************************************
Synopsis [Allocates the simulation info.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Pattern_t * Aig_PatternAlloc( int nBits )
{
Aig_Pattern_t * pPat;
pPat = ALLOC( Aig_Pattern_t, 1 );
memset( pPat, 0, sizeof(Aig_Pattern_t) );
pPat->nBits = nBits;
pPat->nWords = Aig_BitWordNum(nBits);
pPat->pData = ALLOC( unsigned, pPat->nWords );
return pPat;
}
/**Function*************************************************************
Synopsis [Cleans the pattern.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_PatternClean( Aig_Pattern_t * pPat )
{
memset( pPat->pData, 0, sizeof(unsigned) * pPat->nWords );
}
/**Function*************************************************************
Synopsis [Sets the random pattern.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_PatternRandom( Aig_Pattern_t * pPat )
{
int i;
for ( i = 0; i < pPat->nWords; i++ )
pPat->pData[i] = ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand()));
}
/**Function*************************************************************
Synopsis [Deallocates the pattern.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Aig_PatternFree( Aig_Pattern_t * pPat )
{
free( pPat->pData );
free( pPat );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/sat/aig/fraigSolver.c 0 → 100644
/**CFile****************************************************************
FileName [fraigSolver.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [And-Inverter Graph package.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: fraigSolver.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "aig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/sat/aig/fraigTrav.c 0 → 100644
/**CFile****************************************************************
FileName [fraigTrav.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [And-Inverter Graph package.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: fraigTrav.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "aig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/sat/csat/csat_apis.h
......@@ -16,8 +16,8 @@
***********************************************************************/
#ifndef __CSAT_APIS_H__
#define __CSAT_APIS_H__
#ifndef __ABC_APIS_H__
#define __ABC_APIS_H__
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
......@@ -32,37 +32,37 @@
////////////////////////////////////////////////////////////////////////
typedef struct CSAT_ManagerStruct_t CSAT_Manager_t;
typedef struct CSAT_ManagerStruct_t * CSAT_Manager;
typedef struct ABC_ManagerStruct_t ABC_Manager_t;
typedef struct ABC_ManagerStruct_t * ABC_Manager;
// GateType defines the gate type that can be added to circuit by
// CSAT_AddGate();
#ifndef _CSAT_GATE_TYPE_
#define _CSAT_GATE_TYPE_
// ABC_AddGate();
#ifndef _ABC_GATE_TYPE_
#define _ABC_GATE_TYPE_
enum GateType
{
CSAT_CONST = 0, // constant gate
CSAT_BPI, // boolean PI
CSAT_BPPI, // bit level PSEUDO PRIMARY INPUT
CSAT_BAND, // bit level AND
CSAT_BNAND, // bit level NAND
CSAT_BOR, // bit level OR
CSAT_BNOR, // bit level NOR
CSAT_BXOR, // bit level XOR
CSAT_BXNOR, // bit level XNOR
CSAT_BINV, // bit level INVERTER
CSAT_BBUF, // bit level BUFFER
CSAT_BPPO, // bit level PSEUDO PRIMARY OUTPUT
CSAT_BPO // boolean PO
ABC_CONST = 0, // constant gate
ABC_BPI, // boolean PI
ABC_BPPI, // bit level PSEUDO PRIMARY INPUT
ABC_BAND, // bit level AND
ABC_BNAND, // bit level NAND
ABC_BOR, // bit level OR
ABC_BNOR, // bit level NOR
ABC_BXOR, // bit level XOR
ABC_BXNOR, // bit level XNOR
ABC_BINV, // bit level INVERTER
ABC_BBUF, // bit level BUFFER
ABC_BPPO, // bit level PSEUDO PRIMARY OUTPUT
ABC_BPO // boolean PO
};
#endif
//CSAT_StatusT defines the return value by CSAT_Solve();
#ifndef _CSAT_STATUS_
#define _CSAT_STATUS_
enum CSAT_StatusT
//ABC_StatusT defines the return value by ABC_Solve();
#ifndef _ABC_STATUS_
#define _ABC_STATUS_
enum ABC_StatusT
{
UNDETERMINED = 0,
UNSATISFIABLE,
......@@ -76,11 +76,11 @@ enum CSAT_StatusT
#endif
// CSAT_OptionT defines the solver option about learning
// which is used by CSAT_SetSolveOption();
#ifndef _CSAT_OPTION_
#define _CSAT_OPTION_
enum CSAT_OptionT
// ABC_OptionT defines the solver option about learning
// which is used by ABC_SetSolveOption();
#ifndef _ABC_OPTION_
#define _ABC_OPTION_
enum ABC_OptionT
{
BASE_LINE = 0,
IMPLICT_LEARNING, //default
......@@ -89,12 +89,12 @@ enum CSAT_OptionT
#endif
#ifndef _CSAT_Target_Result
#define _CSAT_Target_Result
typedef struct _CSAT_Target_ResultT CSAT_Target_ResultT;
struct _CSAT_Target_ResultT
#ifndef _ABC_Target_Result
#define _ABC_Target_Result
typedef struct _ABC_Target_ResultT ABC_Target_ResultT;
struct _ABC_Target_ResultT
{
enum CSAT_StatusT status; // solve status of the target
enum ABC_StatusT status; // solve status of the target
int num_dec; // num of decisions to solve the target
int num_imp; // num of implications to solve the target
int num_cftg; // num of conflict gates learned
......@@ -118,10 +118,10 @@ struct _CSAT_Target_ResultT
////////////////////////////////////////////////////////////////////////
// create a new manager
extern CSAT_Manager CSAT_InitManager(void);
extern ABC_Manager ABC_InitManager(void);
// set solver options for learning
extern void CSAT_SetSolveOption(CSAT_Manager mng, enum CSAT_OptionT option);
extern void ABC_SetSolveOption(ABC_Manager mng, enum ABC_OptionT option);
// add a gate to the circuit
// the meaning of the parameters are:
......@@ -129,7 +129,7 @@ extern void CSAT_SetSolveOption(CSAT_Manager mng, enum CSAT_Opt
// name: the name of the gate to be added, name should be unique in a circuit.
// nofi: number of fanins of the gate to be added;
// fanins: the name array of fanins of the gate to be added
extern int CSAT_AddGate(CSAT_Manager mng,
extern int ABC_AddGate(ABC_Manager mng,
enum GateType type,
char* name,
int nofi,
......@@ -138,38 +138,38 @@ extern int CSAT_AddGate(CSAT_Manager mng,
// check if there are gates that are not used by any primary ouput.
// if no such gates exist, return 1 else return 0;
extern int CSAT_Check_Integrity(CSAT_Manager mng);
extern int ABC_Check_Integrity(ABC_Manager mng);
// set time limit for solving a target.
// runtime: time limit (in second).
extern void CSAT_SetTimeLimit(CSAT_Manager mng, int runtime);
extern void CSAT_SetLearnLimit(CSAT_Manager mng, int num);
extern void CSAT_SetSolveBacktrackLimit(CSAT_Manager mng, int num);
extern void CSAT_SetLearnBacktrackLimit(CSAT_Manager mng, int num);
extern void CSAT_EnableDump(CSAT_Manager mng, char* dump_file);
extern void ABC_SetTimeLimit(ABC_Manager mng, int runtime);
extern void ABC_SetLearnLimit(ABC_Manager mng, int num);
extern void ABC_SetSolveBacktrackLimit(ABC_Manager mng, int num);
extern void ABC_SetLearnBacktrackLimit(ABC_Manager mng, int num);
extern void ABC_EnableDump(ABC_Manager mng, char* dump_file);
// the meaning of the parameters are:
// nog: number of gates that are in the targets
// names: name array of gates
// values: value array of the corresponding gates given in "names" to be
// solved. the relation of them is AND.
extern int CSAT_AddTarget(CSAT_Manager mng, int nog, char**names, int* values);
extern int ABC_AddTarget(ABC_Manager mng, int nog, char**names, int* values);
// initialize the solver internal data structure.
extern void CSAT_SolveInit(CSAT_Manager mng);
extern void CSAT_AnalyzeTargets(CSAT_Manager mng);
extern void ABC_SolveInit(ABC_Manager mng);
extern void ABC_AnalyzeTargets(ABC_Manager mng);
// solve the targets added by CSAT_AddTarget()
extern enum CSAT_StatusT CSAT_Solve(CSAT_Manager mng);
// solve the targets added by ABC_AddTarget()
extern enum ABC_StatusT ABC_Solve(ABC_Manager mng);
// get the solve status of a target
// TargetID: the target id returned by CSAT_AddTarget().
extern CSAT_Target_ResultT * CSAT_Get_Target_Result(CSAT_Manager mng, int TargetID);
extern void CSAT_Dump_Bench_File(CSAT_Manager mng);
// TargetID: the target id returned by ABC_AddTarget().
extern ABC_Target_ResultT * ABC_Get_Target_Result(ABC_Manager mng, int TargetID);
extern void ABC_Dump_Bench_File(ABC_Manager mng);
// ADDED PROCEDURES:
extern void CSAT_QuitManager( CSAT_Manager mng );
extern void CSAT_TargetResFree( CSAT_Target_ResultT * p );
extern void ABC_QuitManager( ABC_Manager mng );
extern void ABC_TargetResFree( ABC_Target_ResultT * p );
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
......
src/sat/fraig/fraigMem.c
......@@ -201,7 +201,7 @@ void Fraig_MemFixedRestart( Fraig_MemFixed_t * p )
int i;
char * pTemp;
// delocate all chunks except the first one
// deallocate all chunks except the first one
for ( i = 1; i < p->nChunks; i++ )
free( p->pChunks[i] );
p->nChunks = 1;
......
src/sat/msat/msatMem.c
......@@ -231,7 +231,7 @@ void Msat_MmFixedRestart( Msat_MmFixed_t * p )
int i;
char * pTemp;
// delocate all chunks except the first one
// deallocate all chunks except the first one
for ( i = 1; i < p->nChunks; i++ )
free( p->pChunks[i] );
p->nChunks = 1;
......
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