From b258db83b8b9becc444baf11732597c000651020 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Wed, 6 Dec 2017 09:53:25 -0800
Subject: An improvement to 'twoexact' and 'lutexact'.

---
 src/sat/bmc/bmcMaj.c  | 23 +++++++++++++++++++----
 src/sat/bmc/bmcMaj2.c | 24 ++++++++++++++++++++----
 2 files changed, 39 insertions(+), 8 deletions(-)

diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c
index 463e9197..0b09e311 100644
--- a/src/sat/bmc/bmcMaj.c
+++ b/src/sat/bmc/bmcMaj.c
@@ -438,7 +438,14 @@ int Exa_ManMarkup( Exa_Man_t * p )
     {
         for ( k = 0; k < 2; k++ )
         {
-            for ( j = 0; j < i - k; j++ )
+            if ( i == p->nObjs - 1 && k == 0 )
+            {
+                j = p->nObjs - 2;
+                Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
+                p->VarMarks[i][k][j] = p->iVar++;
+                continue;
+            }
+            for ( j = 1 - k; j < i - k; j++ )
             {
                 Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
                 p->VarMarks[i][k][j] = p->iVar++;
@@ -789,7 +796,14 @@ static int Exa3_ManMarkup( Exa3_Man_t * p )
     {
         for ( k = 0; k < p->nLutSize; k++ )
         {
-            for ( j = 0; j < i - k; j++ )
+            if ( i == p->nObjs - 1 && k == 0 )
+            {
+                j = p->nObjs - 2;
+                Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
+                p->VarMarks[i][k][j] = p->iVar++;
+                continue;
+            }
+            for ( j = p->nLutSize - 1 - k; j < i - k; j++ )
             {
                 Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
                 p->VarMarks[i][k][j] = p->iVar++;
@@ -799,11 +813,12 @@ static int Exa3_ManMarkup( Exa3_Man_t * p )
     printf( "The number of parameter variables = %d.\n", p->iVar );
     return p->iVar;
     // printout
-    for ( i = p->nVars; i < p->nObjs; i++ )
+    for ( i = p->nObjs - 1; i >= p->nVars; i-- )
     {
-        printf( "Node %d\n", i );
+        printf( "       Node %2d\n", i );
         for ( j = 0; j < p->nObjs; j++ )
         {
+            printf( "Fanin %2d : ", j );
             for ( k = 0; k < p->nLutSize; k++ )
                 printf( "%3d ", p->VarMarks[i][k][j] );
             printf( "\n" );
diff --git a/src/sat/bmc/bmcMaj2.c b/src/sat/bmc/bmcMaj2.c
index 1c61fec1..46f3f1f2 100644
--- a/src/sat/bmc/bmcMaj2.c
+++ b/src/sat/bmc/bmcMaj2.c
@@ -544,7 +544,14 @@ static int Exa_ManMarkup( Exa_Man_t * p )
     {
         for ( k = 0; k < 2; k++ )
         {
-            for ( j = 0; j < i - k; j++ )
+            if ( i == p->nObjs - 1 && k == 0 )
+            {
+                j = p->nObjs - 2;
+                Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
+                p->VarMarks[i][k][j] = p->iVar++;
+                continue;
+            }
+            for ( j = 1 - k; j < i - k; j++ )
             {
                 Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
                 p->VarMarks[i][k][j] = p->iVar++;
@@ -897,7 +904,14 @@ static int Exa3_ManMarkup( Exa3_Man_t * p )
     {
         for ( k = 0; k < p->nLutSize; k++ )
         {
-            for ( j = 0; j < i - k; j++ )
+            if ( i == p->nObjs - 1 && k == 0 )
+            {
+                j = p->nObjs - 2;
+                Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
+                p->VarMarks[i][k][j] = p->iVar++;
+                continue;
+            }
+            for ( j = p->nLutSize - 1 - k; j < i - k; j++ )
             {
                 Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
                 p->VarMarks[i][k][j] = p->iVar++;
@@ -907,11 +921,13 @@ static int Exa3_ManMarkup( Exa3_Man_t * p )
     printf( "The number of parameter variables = %d.\n", p->iVar );
     return p->iVar;
     // printout
-    for ( i = p->nVars; i < p->nObjs; i++ )
+//    for ( i = p->nVars; i < p->nObjs; i++ )
+    for ( i = p->nObjs - 1; i >= p->nVars; i-- )
     {
-        printf( "Node %d\n", i );
+        printf( "       Node %2d\n", i );
         for ( j = 0; j < p->nObjs; j++ )
         {
+            printf( "Fanin %2d : ", j );
             for ( k = 0; k < p->nLutSize; k++ )
                 printf( "%3d ", p->VarMarks[i][k][j] );
             printf( "\n" );
-- 
cgit v1.2.3