summaryrefslogtreecommitdiffstats
path: root/src/base/abci
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2022-07-30 14:21:47 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2022-07-30 14:21:47 -0700
commitddb22f3bed7cb457576b4b80e55d47eabf3a1308 (patch)
tree7c37fb06dc76ba960f606fb3f738cf31ab0fa347 /src/base/abci
parentc23cd0a7c5f4264b3209f127885b8d5432f2fd5a (diff)
downloadabc-ddb22f3bed7cb457576b4b80e55d47eabf3a1308.tar.gz
abc-ddb22f3bed7cb457576b4b80e55d47eabf3a1308.tar.bz2
abc-ddb22f3bed7cb457576b4b80e55d47eabf3a1308.zip
Various changes.
Diffstat (limited to 'src/base/abci')
-rw-r--r--src/base/abci/abc.c92
1 files changed, 92 insertions, 0 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 33a8315c..2ae994e3 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -561,6 +561,7 @@ static int Abc_CommandAbc9Exorcism ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Mfs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Mfsd ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9DeepSyn ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9SatSyn ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9StochSyn ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9PoPart2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9CexCut ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -1310,6 +1311,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&mfs", Abc_CommandAbc9Mfs, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&mfsd", Abc_CommandAbc9Mfsd, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&deepsyn", Abc_CommandAbc9DeepSyn, 0 );
+ Cmd_CommandAdd( pAbc, "ABC9", "&satsyn", Abc_CommandAbc9SatSyn, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&stochsyn", Abc_CommandAbc9StochSyn, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&popart2", Abc_CommandAbc9PoPart2, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&cexcut", Abc_CommandAbc9CexCut, 0 );
@@ -48310,6 +48312,96 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandAbc9SatSyn( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern Gia_Man_t * Gia_ManSyn( Gia_Man_t * p, int nNodes, int nOuts, int TimeOut, int fUseXor, int fFancy, int fVerbose );
+ Gia_Man_t * pTemp; int c, nNodes = 0, nOuts = 0, TimeOut = 0, fUseXor = 0, fFancy = 0, fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "NTafvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'N':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nNodes = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nNodes < 0 )
+ goto usage;
+ break;
+ case 'O':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nOuts = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nOuts < 0 )
+ goto usage;
+ break;
+ case 'T':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ TimeOut = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( TimeOut < 0 )
+ goto usage;
+ break;
+ case 'a':
+ fUseXor ^= 1;
+ break;
+ case 'f':
+ fFancy ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pAbc->pGia == NULL )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9SatSyn(): There is no AIG.\n" );
+ return 0;
+ }
+ pTemp = Gia_ManSyn( pAbc->pGia, nNodes, nOuts, TimeOut, fUseXor, fFancy, fVerbose );
+ Abc_FrameUpdateGia( pAbc, pTemp );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: &satsyn [-NOT <num>] [-afvh]\n" );
+ Abc_Print( -2, "\t performs synthesis\n" );
+ Abc_Print( -2, "\t-N <num> : the number of window nodes [default = %d]\n", nNodes );
+ Abc_Print( -2, "\t-O <num> : the number of window outputs [default = %d]\n", nOuts );
+ Abc_Print( -2, "\t-T <num> : the timeout in seconds (0 = no timeout) [default = %d]\n", TimeOut );
+ Abc_Print( -2, "\t-a : toggle using xor-nodes [default = %s]\n", fUseXor? "yes": "no" );
+ Abc_Print( -2, "\t-f : toggle using additional feature [default = %s]\n", fFancy? "yes": "no" );
+ Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandAbc9StochSyn( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Gia_ManStochSyn( int nMaxSize, int nIters, int TimeOut, int Seed, int fVerbose, char * pScript );