From 079a309a0d0bbe89eccfb64cdae55d1db73ca03a Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Mon, 8 Nov 2021 21:17:37 -0800
Subject: Bug fix in processing NDR.

---
 src/proof/acec/acecFadds.c | 30 +++++++++++++++++++++++-------
 1 file changed, 23 insertions(+), 7 deletions(-)

(limited to 'src/proof')

diff --git a/src/proof/acec/acecFadds.c b/src/proof/acec/acecFadds.c
index d55eefe2..a2bdcfbe 100644
--- a/src/proof/acec/acecFadds.c
+++ b/src/proof/acec/acecFadds.c
@@ -314,16 +314,21 @@ void Dtc_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_I
         if ( Type == 0 )
             continue;
         vTemp = Type == 1 ? vCutsXor : vCutsMaj;
-        if ( fVerbose )
-            printf( "%d = %s(", iObj, Type == 1 ? "XOR" : "MAJ" );
-        for ( c = 1; c <= pCut[0]; c++ )
+        if ( 0 && Type == 2 )
         {
+            fVerbose = 1;
+            if ( fVerbose )
+                printf( "%d = %s(", iObj, Type == 1 ? "XOR" : "MAJ" );
+            for ( c = 1; c <= pCut[0]; c++ )
+            {
+                if ( fVerbose )
+                    printf( " %d", pCut[c] );
+                Vec_IntPush( vTemp, pCut[c] );
+            }
             if ( fVerbose )
-                printf( " %d", pCut[c] );
-            Vec_IntPush( vTemp, pCut[c] );
+                printf( " )\n" );
+            fVerbose = 0;
         }
-        if ( fVerbose )
-            printf( " )\n" );
         Vec_IntPush( vTemp, iObj );
     }
 }
@@ -450,6 +455,16 @@ Vec_Int_t * Gia_ManDetectFullAdders( Gia_Man_t * p, int fVerbose, Vec_Int_t ** p
     Vec_IntFree( vCutsMaj );
     return vFadds;
 }
+void Gia_ManDetectFullAdders2( Gia_Man_t * p, int fVerbose )
+{
+    Vec_Int_t * vCutsXor2, * vCutsXor, * vCutsMaj;
+    Dtc_ManComputeCuts( p, &vCutsXor2, &vCutsXor, &vCutsMaj, fVerbose );
+    if ( fVerbose )
+        printf( "XOR3 cuts = %d.  MAJ cuts = %d.\n", Vec_IntSize(vCutsXor)/4, Vec_IntSize(vCutsMaj)/4 );
+    Vec_IntFree( vCutsXor2 );
+    Vec_IntFree( vCutsXor );
+    Vec_IntFree( vCutsMaj );
+}
 
 /**Function*************************************************************
 
@@ -1238,6 +1253,7 @@ Gia_Man_t * Gia_ManDupWithArtificialBoxes( Gia_Man_t * p, int DelayC, int nPathM
     return pNew;
 }
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-- 
cgit v1.2.3