From 75ee395f916f44fd564deb89b64a2c7e4db081bc Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Mon, 21 Feb 2011 15:09:51 -0800
Subject: Implemented additional filtering of equivalences (&srm -sf).

---
 src/base/abci/abc.c | 21 +++++++++++++--------
 1 file changed, 13 insertions(+), 8 deletions(-)

(limited to 'src/base')

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index eba34d62..1b9d8ab9 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -25941,22 +25941,26 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
     char pFileName[10], pFileName2[10];
     Gia_Man_t * pTemp, * pAux;
     int c, fVerbose = 0;
-    int fSpeculate = 1;
     int fSynthesis = 0;
+    int fSpeculate = 1;
+    int fSkipSome = 0;
     int fDualOut = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "dsrvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "drsfvh" ) ) != EOF )
     {
         switch ( c )
         {
         case 'd':
             fDualOut ^= 1;
             break;
+        case 'r':
+            fSynthesis ^= 1;
+            break;
         case 's':
             fSpeculate ^= 1;
             break;
-        case 'r':
-            fSynthesis ^= 1;
+        case 'f':
+            fSkipSome ^= 1;
             break;
         case 'v':
             fVerbose ^= 1;
@@ -25974,7 +25978,7 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
     } 
     sprintf( pFileName,  "gsrm%s.aig", fSpeculate? "" : "s" );
     sprintf( pFileName2, "gsyn%s.aig", fSpeculate? "" : "s" );
-    pTemp = Gia_ManSpecReduce( pAbc->pGia, fDualOut, fSynthesis, fSpeculate, fVerbose );
+    pTemp = Gia_ManSpecReduce( pAbc->pGia, fDualOut, fSynthesis, fSpeculate, fSkipSome, fVerbose );
     if ( pTemp )
     {
         if ( fSpeculate )
@@ -26004,11 +26008,12 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &srm [-dsrvh]\n" );
+    Abc_Print( -2, "usage: &srm [-drsfvh]\n" );
     Abc_Print( -2, "\t         writes speculatively reduced model into file \"%s\"\n", pFileName );
     Abc_Print( -2, "\t-d     : toggle creating dual output miter [default = %s]\n", fDualOut? "yes": "no" );
-    Abc_Print( -2, "\t-s     : toggle using speculation at the internal nodes [default = %s]\n", fSpeculate? "yes": "no" );
     Abc_Print( -2, "\t-r     : toggle writing reduced network for synthesis [default = %s]\n", fSynthesis? "yes": "no" );
+    Abc_Print( -2, "\t-s     : toggle using speculation at the internal nodes [default = %s]\n", fSpeculate? "yes": "no" );
+    Abc_Print( -2, "\t-f     : toggle filtering to remove redundant equivalences [default = %s]\n", fSkipSome? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
@@ -26127,7 +26132,7 @@ usage:
     Abc_Print( -2, "\t-h          : print the command usage\n");
     Abc_Print( -2, "\t<miter.aig> : file with the external miter to read\n");
     Abc_Print( -2, "\t              \n" );
-    Abc_Print( -2, "\t              The external miter should be generated by &srm -m\n" );
+    Abc_Print( -2, "\t              The external miter should be generated by &srm -s\n" );
     Abc_Print( -2, "\t              and (partially) solved by any verification engine(s).\n" );
     Abc_Print( -2, "\t              The external miter should have as many POs as\n" );
     Abc_Print( -2, "\t              the number of POs in the current AIG plus\n" );
-- 
cgit v1.2.3