4 files changed, 41 insertions, 8 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 3fdbf4b5..84c22f03 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -826,7 +826,7 @@ extern Gia_Man_t *         Gia_ManDupDfsCone( Gia_Man_t * p, Gia_Obj_t * pObj );
 extern Gia_Man_t *         Gia_ManDupDfsLitArray( Gia_Man_t * p, Vec_Int_t * vLits );
 extern Gia_Man_t *         Gia_ManDupNormalize( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupUnnomalize( Gia_Man_t * p );
-extern Gia_Man_t *         Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos, int fDualOut );
+extern Gia_Man_t *         Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos, int fDualOut, int OutValue );
 extern Gia_Man_t *         Gia_ManDupOntop( Gia_Man_t * p, Gia_Man_t * p2 );
 extern Gia_Man_t *         Gia_ManDupWithNewPo( Gia_Man_t * p1, Gia_Man_t * p2 );
 extern Gia_Man_t *         Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index b5fcae45..0df414ab 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -1175,7 +1175,27 @@ Vec_Int_t * Gia_ManDupTrimmedNonZero( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos, int fDualOut )
+int Gia_ManPoIsToRemove( Gia_Man_t * p, Gia_Obj_t * pObj, int Value )
+{
+    assert( Gia_ObjIsCo(pObj) );
+    if ( Value == -1 )
+        return Gia_ObjIsConst0(Gia_ObjFanin0(pObj));
+    assert( Value == 0 || Value == 1 );
+    return Value == Gia_ObjFaninC0(pObj);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates AIG in the DFS order while putting CIs first.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos, int fDualOut, int OutValue )
 {
     Vec_Int_t * vNonZero = NULL;
     Gia_Man_t * pNew, * pTemp;
@@ -1231,12 +1251,12 @@ Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int fTrimCos, int fD
     {
         // check if there are POs to be added
         Gia_ManForEachPo( p, pObj, i )
-            if ( !fTrimCos || !Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
+            if ( !fTrimCos || !Gia_ManPoIsToRemove(p, pObj, OutValue) )
                 break;
         if ( i == Gia_ManPoNum(p) ) // there is no POs - add dummy PO
             Gia_ManAppendCo( pNew, 0 );
         Gia_ManForEachCo( p, pObj, i )
-            if ( !fTrimCos || !Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) || Gia_ObjIsRi(p, pObj) )
+            if ( !fTrimCos || !Gia_ManPoIsToRemove(p, pObj, OutValue) || Gia_ObjIsRi(p, pObj) )
                 Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
         Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
     }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 56aaed9e..25a7638c 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -24324,15 +24324,27 @@ int Abc_CommandAbc9Trim( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_Man_t * pTemp, * pTemp2;
     int c;
+    int OutValue = -1;
     int fTrimCis = 1;
     int fTrimCos = 1;
     int fDualOut = 0;
     int fPoFedByPi = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "iocdh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Viocdh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'V':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-V\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            OutValue = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( OutValue < 0 )
+                goto usage;
+            break;
         case 'i':
             fTrimCis ^= 1;
             break;
@@ -24356,7 +24368,7 @@ int Abc_CommandAbc9Trim( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Trim(): There is no AIG.\n" );
         return 1;
     }
-    pTemp = Gia_ManDupTrimmed( pAbc->pGia, fTrimCis, fTrimCos, fDualOut );
+    pTemp = Gia_ManDupTrimmed( pAbc->pGia, fTrimCis, fTrimCos, fDualOut, OutValue );
     if ( fPoFedByPi )
     {
         extern Gia_Man_t * Gia_ManDupTrimmed2( Gia_Man_t * p );
@@ -24367,8 +24379,9 @@ int Abc_CommandAbc9Trim( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &trim [-iocdh]\n" );
+    Abc_Print( -2, "usage: &trim [-V num] [-iocdh]\n" );
     Abc_Print( -2, "\t         removes PIs without fanout and PO driven by constants\n" );
+    Abc_Print( -2, "\t-V num : the value (0 or 1) of POs to remove [default = both]\n" );
     Abc_Print( -2, "\t-i     : toggle removing PIs [default = %s]\n", fTrimCis? "yes": "no" );
     Abc_Print( -2, "\t-o     : toggle removing POs [default = %s]\n", fTrimCos? "yes": "no" );
     Abc_Print( -2, "\t-c     : toggle additionally removing POs fed by PIs [default = %s]\n", fPoFedByPi? "yes": "no" );
diff --git a/src/proof/abs/absRpmOld.c b/src/proof/abs/absRpmOld.c
index fd90ae01..acf664a8 100644
--- a/src/proof/abs/absRpmOld.c
+++ b/src/proof/abs/absRpmOld.c
@@ -151,7 +151,7 @@ Gia_Man_t * Abs_RpmPerformOld( Gia_Man_t * p, int fVerbose )
     }
 
     // perform input trimming
-    pNew = Gia_ManDupTrimmed( p, 1, 0, 0 );
+    pNew = Gia_ManDupTrimmed( p, 1, 0, 0, -1 );
     if ( fVerbose )
     {
         printf( "After PI trimming:\n" );