Small changes for today's experiments.

6 files changed, 43 insertions, 9 deletions

diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 3ffb948e..a2277294 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -2949,7 +2949,7 @@ Gia_Man_t * Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos, int fTrimPis )
 
     // start the new manager
 //    Gia_ManFillValue( p );
-    pNew = Gia_ManStart( Vec_PtrSize(vLeaves) + Vec_PtrSize(vNodes) + Vec_PtrSize(vRoots) + 1);
+    pNew = Gia_ManStart( (fTrimPis ? Vec_PtrSize(vLeaves) : Gia_ManCiNum(p)) + Vec_PtrSize(vNodes) + Vec_PtrSize(vRoots) + 1 );
     pNew->pName = Abc_UtilStrsav( p->pName );
     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     // map the constant node
diff --git a/src/aig/gia/giaHash.c b/src/aig/gia/giaHash.c
index d4a47ac5..c80f9e07 100644
--- a/src/aig/gia/giaHash.c
+++ b/src/aig/gia/giaHash.c
@@ -575,11 +575,6 @@ int Gia_ManHashMuxReal( Gia_Man_t * p, int iLitC, int iLit1, int iLit0 )
 ***********************************************************************/
 int Gia_ManHashAnd( Gia_Man_t * p, int iLit0, int iLit1 )  
 { 
-    if ( p->fGiaSimple )
-    {
-        assert( p->nHTable == 0 );
-        return Gia_ManAppendAnd( p, iLit0, iLit1 );
-    }
     if ( iLit0 < 2 )
         return iLit0 ? iLit1 : 0;
     if ( iLit1 < 2 )
@@ -588,6 +583,11 @@ int Gia_ManHashAnd( Gia_Man_t * p, int iLit0, int iLit1 )
         return iLit1;
     if ( iLit0 == Abc_LitNot(iLit1) )
         return 0;
+    if ( p->fGiaSimple )
+    {
+        assert( p->nHTable == 0 );
+        return Gia_ManAppendAnd( p, iLit0, iLit1 );
+    }
     if ( (p->nObjs & 0xFF) == 0 && 2 * p->nHTable < Gia_ManAndNum(p) )
         Gia_ManHashResize( p );
     if ( p->fAddStrash )
diff --git a/src/aig/gia/giaShow.c b/src/aig/gia/giaShow.c
index 9cf79ccf..039931b2 100644
--- a/src/aig/gia/giaShow.c
+++ b/src/aig/gia/giaShow.c
@@ -362,20 +362,29 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold, int
                 fprintf( pFile, "  Node%d [label = \"%d(%d%s)\"", pNode->Id, pNode->Id, 
                     Gia_Regular(pNode->pEquiv)->Id, Gia_IsComplement(pNode->pEquiv)? "\'":"" );
 */
-            fprintf( pFile, "  Node%d [label = \"%d\"", i, i ); 
             if ( vMarks && Vec_IntEntry(vMarks, i) > 0 )
             {
+                fprintf( pFile, "  Node%d [label = \"%d_%d\"", i, Vec_IntFind(vRemap, i), i ); 
                 if ( Abc_Lit2Att2(Vec_IntEntry(vMarks, i)) == 2 )
                     fprintf( pFile, ", shape = doubleoctagon" );
                 else 
                     fprintf( pFile, ", shape = octagon" );
             }
             else if ( Gia_ObjIsXor(pNode) )
+            {
+                fprintf( pFile, "  Node%d [label = \"%d\"", i, i ); 
                 fprintf( pFile, ", shape = doublecircle" );
+            }
             else if ( Gia_ObjIsMux(pMan, pNode) )
+            {
+                fprintf( pFile, "  Node%d [label = \"%d\"", i, i ); 
                 fprintf( pFile, ", shape = trapezium" );
+            }
             else
+            {
+                fprintf( pFile, "  Node%d [label = \"%d\"", i, i ); 
                 fprintf( pFile, ", shape = ellipse" );
+            }
 
             if ( pNode->fMark0 )
                 fprintf( pFile, ", style = filled" );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 9d21bc72..270101b7 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -6878,6 +6878,12 @@ int Abc_CommandRr( Abc_Frame_t * pAbc, int argc, char ** argv )
         }
     }
 
+    printf( "This command is obsolete." );
+    printf( "To perform pure redudancy removal, try \"mfs -r\".\n" );
+    printf( "To perform something a little stronger try \"mfs2\"\n" );
+    printf( "When working with an AIG, use \"logic\" before and \"strash\" after this command.\n" );
+    return 0;
+
     if ( pNtk == NULL )
     {
         Abc_Print( -1, "Empty network.\n" );
diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index f6cd9310..826dbfa1 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -1344,6 +1344,25 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple
     assert( Vec_PtrSize(pNew->vNamesOut) == Gia_ManCoNum(pNew) );
 */
     pNew->pSpec = Abc_UtilStrsav( p->pSpec ? p->pSpec : p->pName );
+    // dump the miter parts
+    if ( 0 )
+    {
+        char pFileName0[1000], pFileName1[1000];
+        char * pNameGeneric = Extra_FileNameGeneric( p->pSpec );
+        Vec_Int_t * vOrder = Vec_IntStartNatural( Gia_ManPoNum(pNew) );
+        Gia_Man_t * pGia0 = Gia_ManDupCones( pNew, Vec_IntArray(vOrder),                         Vec_IntSize(vOrder)/2, 0 );
+        Gia_Man_t * pGia1 = Gia_ManDupCones( pNew, Vec_IntArray(vOrder) + Vec_IntSize(vOrder)/2, Vec_IntSize(vOrder)/2, 0 );
+        assert( Gia_ManPoNum(pNew) % 2 == 0 );
+        sprintf( pFileName0, "%s_lhs_.aig", pNameGeneric );
+        sprintf( pFileName1, "%s_rhs_.aig", pNameGeneric );
+        Gia_AigerWrite( pGia0, pFileName0, 0, 0 );
+        Gia_AigerWrite( pGia1, pFileName1, 0, 0 );
+        Gia_ManStop( pGia0 );
+        Gia_ManStop( pGia1 );
+        Vec_IntFree( vOrder );
+        ABC_FREE( pNameGeneric );
+        printf( "Dumped two parts of the miter into files \"%s\" and \"%s\".\n", pFileName0, pFileName1 );
+    }
     return pNew;
 }
 
diff --git a/src/proof/acec/acecPolyn.c b/src/proof/acec/acecPolyn.c
index 2f98df73..be601405 100644
--- a/src/proof/acec/acecPolyn.c
+++ b/src/proof/acec/acecPolyn.c
@@ -311,8 +311,8 @@ void Gia_PolynBuildOne( Pln_Man_t * p, int iMono )
         Vec_IntAppendMinus( p->vTempC[0], vConst, 0 );
         Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[2] );   //  C * y 
 
-        //if ( !p->pGia->vXors || Vec_IntFind(p->pGia->vXors, iDriver) > 0 )
-        {
+        //if ( !p->pGia->vXors || Vec_IntFind(p->pGia->vXors, iDriver) == -1 || Vec_IntFind(p->pGia->vXors, iDriver) == 5 )
+        { 
             vConst = Hsh_VecReadEntry( p->pHashC, iConst );
             Vec_IntAppendMinus2x( p->vTempC[0], vConst );
             Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[3] );   // -C * x * y