summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abci/abc.c24
-rw-r--r--src/base/abci/abcDar.c8
-rw-r--r--src/base/abci/module.make1
-rw-r--r--src/base/io/ioWriteDot.c11
-rw-r--r--src/base/main/main.c4
-rw-r--r--src/base/main/main.h4
-rw-r--r--src/base/main/mainFrame.c6
7 files changed, 40 insertions, 18 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index aa8d6b30..d1aa2c82 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -297,6 +297,7 @@ void Abc_FrameClearDesign()
void Abc_Init( Abc_Frame_t * pAbc )
{
// Abc_NtkBddImplicationTest();
+// Ply_LutPairTest();
Cmd_CommandAdd( pAbc, "Printing", "print_stats", Abc_CommandPrintStats, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_exdc", Abc_CommandPrintExdc, 0 );
@@ -7072,6 +7073,9 @@ int Abc_CommandEspresso( Abc_Frame_t * pAbc, int argc, char ** argv )
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
+ printf( "This command is currently disabled.\n" );
+ return 0;
+
// set defaults
fVerbose = 0;
Extra_UtilGetoptReset();
@@ -7098,7 +7102,7 @@ int Abc_CommandEspresso( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "SOP minimization is possible for logic networks (run \"renode\").\n" );
return 1;
}
- Abc_NtkEspresso( pNtk, fVerbose );
+// Abc_NtkEspresso( pNtk, fVerbose );
return 0;
usage:
@@ -7764,6 +7768,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
*/
+
+
/*
// pNtkRes = Abc_NtkDar( pNtk );
// pNtkRes = Abc_NtkDarRetime( pNtk, nLevels, 1 );
@@ -7776,8 +7782,10 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+ return 0;
*/
+
// Abc_NtkDarClau( pNtk, nFrames, nLevels, fBmc, fVerbose, fVeryVerbose );
/*
if ( globalUtilOptind != 1 )
@@ -15337,9 +15345,10 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
int nBTLimit;
int fRewrite;
int fTransLoop;
+ int fUsePudlak;
int fVerbose;
- extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fRewrite, int fTransLoop, int fVerbose );
+ extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fRewrite, int fTransLoop, int fUsePudlak, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -15349,9 +15358,10 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
nBTLimit = 20000;
fRewrite = 0;
fTransLoop = 1;
+ fUsePudlak = 0;
fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Crtvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Crtpvh" ) ) != EOF )
{
switch ( c )
{
@@ -15372,6 +15382,9 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
case 't':
fTransLoop ^= 1;
break;
+ case 'p':
+ fUsePudlak ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -15401,15 +15414,16 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( stdout, "Currently only works for single-output miters (run \"orpos\").\n" );
return 0;
}
- Abc_NtkDarBmcInter( pNtk, nBTLimit, fRewrite, fTransLoop, fVerbose );
+ Abc_NtkDarBmcInter( pNtk, nBTLimit, fRewrite, fTransLoop, fUsePudlak, fVerbose );
return 0;
usage:
- fprintf( pErr, "usage: int [-C num] [-rtvh]\n" );
+ fprintf( pErr, "usage: int [-C num] [-rtpvh]\n" );
fprintf( pErr, "\t uses interpolation to prove the property\n" );
fprintf( pErr, "\t-C num : the limit on conflicts for one SAT run [default = %d]\n", nBTLimit );
fprintf( pErr, "\t-r : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" );
fprintf( pErr, "\t-t : toggle adding transition into the init state [default = %s]\n", fTransLoop? "yes": "no" );
+ fprintf( pErr, "\t-p : toggle using original Pudlak's interpolation procedure [default = %s]\n", fUsePudlak? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 2a234b68..a691a205 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1270,7 +1270,7 @@ PRT( "Time", clock() - clk );
SeeAlso []
***********************************************************************/
-int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fRewrite, int fTransLoop, int fVerbose )
+int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fRewrite, int fTransLoop, int fUsePudlak, int fVerbose )
{
Aig_Man_t * pMan;
int RetValue, Depth, clk = clock();
@@ -1282,7 +1282,7 @@ int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fRewrite, int fTra
return -1;
}
assert( pMan->nRegs > 0 );
- RetValue = Saig_Interpolate( pMan, nConfLimit, fRewrite, fTransLoop, fVerbose, &Depth );
+ RetValue = Saig_Interpolate( pMan, nConfLimit, fRewrite, fTransLoop, fUsePudlak, fVerbose, &Depth );
if ( RetValue == 1 )
printf( "Property proved. " );
else if ( RetValue == 0 )
@@ -2148,12 +2148,12 @@ Abc_Ntk_t * Abc_NtkDarCleanupAig( Abc_Ntk_t * pNtk, int fCleanupPis, int fCleanu
***********************************************************************/
void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose )
{
- extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose );
+ extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent );
Aig_Man_t * pMan;
pMan = Abc_NtkToDar( pNtk, 0, 1 );
if ( pMan == NULL )
return;
- Aig_ManVerifyUsingBdds( pMan, nBddMax, nIterMax, fPartition, fReorder, fVerbose );
+ Aig_ManVerifyUsingBdds( pMan, nBddMax, nIterMax, fPartition, fReorder, fVerbose, 0 );
Aig_ManStop( pMan );
}
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 777da95b..e83785fe 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -14,7 +14,6 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcDelay.c \
src/base/abci/abcDress.c \
src/base/abci/abcDsd.c \
- src/base/abci/abcEspresso.c \
src/base/abci/abcExtract.c \
src/base/abci/abcFpga.c \
src/base/abci/abcFpgaFast.c \
diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c
index 88028105..54beb8b6 100644
--- a/src/base/io/ioWriteDot.c
+++ b/src/base/io/ioWriteDot.c
@@ -275,10 +275,16 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
fprintf( pFile, " Level%d;\n", Level );
Vec_PtrForEachEntry( vNodes, pNode, i )
{
+ int SuppSize;
+ Vec_Ptr_t * vSupp;
if ( (int)pNode->Level != Level )
continue;
if ( Abc_ObjFaninNum(pNode) == 0 )
continue;
+ vSupp = Abc_NtkNodeSupport( pNtk, &pNode, 1 );
+ SuppSize = Vec_PtrSize( vSupp );
+ Vec_PtrFree( vSupp );
+
// fprintf( pFile, " Node%d [label = \"%d\"", pNode->Id, pNode->Id );
if ( Abc_NtkIsStrash(pNtk) )
pSopString = "";
@@ -288,7 +294,10 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
pSopString = Abc_NtkPrintSop(Mio_GateReadSop(pNode->pData));
else
pSopString = Abc_NtkPrintSop(pNode->pData);
- fprintf( pFile, " Node%d [label = \"%d\\n%s\"", pNode->Id, pNode->Id, pSopString );
+// fprintf( pFile, " Node%d [label = \"%d\\n%s\"", pNode->Id, pNode->Id, pSopString );
+ fprintf( pFile, " Node%d [label = \"%d\\n%s\"", pNode->Id,
+ SuppSize,
+ pSopString );
fprintf( pFile, ", shape = ellipse" );
if ( pNode->fMarkB )
diff --git a/src/base/main/main.c b/src/base/main/main.c
index 1f1f19ba..6f2e1d11 100644
--- a/src/base/main/main.c
+++ b/src/base/main/main.c
@@ -56,8 +56,10 @@ int main( int argc, char * argv[] )
// added to detect memory leaks:
#ifdef _DEBUG
+#ifdef ABC_CHECK_LEAKS
_CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF );
#endif
+#endif
// Npn_Experiment();
// Npn_Generate();
@@ -255,8 +257,10 @@ void Abc_Start()
Abc_Frame_t * pAbc;
// added to detect memory leaks:
#ifdef _DEBUG
+#ifdef ABC_CHECK_LEAKS
_CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF );
#endif
+#endif
// start the glocal frame
pAbc = Abc_FrameGetGlobalFrame();
// source the resource file
diff --git a/src/base/main/main.h b/src/base/main/main.h
index 852b8f25..62dc394a 100644
--- a/src/base/main/main.h
+++ b/src/base/main/main.h
@@ -40,10 +40,6 @@ typedef struct Abc_Frame_t_ Abc_Frame_t;
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
-// this include should be the first one in the list
-// it is used to catch memory leaks on Windows
-#include "leaks.h"
-
// data structure packages
#include "extra.h"
#include "vec.h"
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index eae8b7a6..462b5a02 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -114,8 +114,8 @@ Abc_Frame_t * Abc_FrameAllocate()
// networks to be used by choice
p->vStore = Vec_PtrAlloc( 16 );
// initialize decomposition manager
- define_cube_size(20);
- set_espresso_flags();
+// define_cube_size(20);
+// set_espresso_flags();
// initialize the trace manager
// Abc_HManStart();
return p;
@@ -139,7 +139,7 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
extern void undefine_cube_size();
// extern void Ivy_TruthManStop();
// Abc_HManStop();
- undefine_cube_size();
+// undefine_cube_size();
Rwt_ManGlobalStop();
// Ivy_TruthManStop();
if ( p->pLibVer ) Abc_LibFree( p->pLibVer, NULL );
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-05 14:29:30 +0000