An improvement to 'twoexact' and 'lutexact'.

src/base/abci/abc.c

@@ -8229,6 +8229,16 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Truth table should be given on the command line.\n" );
         return 1;
     }
+    if ( (1 << (nVars-2)) != (int)strlen(pTtStr) )
+    {
+        Abc_Print( -1, "Truth table is expected to have %d hex digits (instead of %d).\n", (1 << (nVars-2)), strlen(pTtStr) );
+        return 1;
+    }
+    if ( nVars > nNodes * (2 - 1) + 1 )
+    {
+        Abc_Print( -1, "Function with %d variales cannot be implemented with %d two-input gates.\n", nVars, nNodes );
+        return 1;
+    }
     if ( nVars > 10 )
     {
         Abc_Print( -1, "Function should not have more than 10 inputs.\n" );
@@ -8250,6 +8260,13 @@ usage:
     Abc_Print( -2, "\t-v       : toggle verbose printout [default = %s]\n", fVerbose ? "yes" : "no" );
     Abc_Print( -2, "\t-h       : print the command usage\n" );
     Abc_Print( -2, "\t<hex>    : truth table in hex notation\n" );
+    Abc_Print( -2, "\t           \n" );
+    Abc_Print( -2, "\t           For example, command line \"twoexact -g -I 5 -N 12 169AE443\"\n" );
+    Abc_Print( -2, "\t           synthesizes the smallest circuit composed of two-input gates\n" );
+    Abc_Print( -2, "\t           for the only NPN class of 5-input functions that requires 12 gates;\n" );
+    Abc_Print( -2, "\t           all other functions can be realized with 11 two-input gates or less\n" );
+    Abc_Print( -2, "\t           (see Section 7.1.2 \"Boolean evaluation\" in the book by Donald Knuth\n" );
+    Abc_Print( -2, "\t           http://www.cs.utsa.edu/~wagner/knuth/fasc0c.pdf)\n" );
     return 1;
 }
 
@@ -8329,6 +8346,16 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Truth table should be given on the command line.\n" );
         return 1;
     }
+    if ( (1 << (nVars-2)) != (int)strlen(pTtStr) )
+    {
+        Abc_Print( -1, "Truth table is expected to have %d hex digits (instead of %d).\n", (1 << (nVars-2)), strlen(pTtStr) );
+        return 1;
+    }
+    if ( nVars > nNodes * (nLutSize - 1) + 1 )
+    {
+        Abc_Print( -1, "Function with %d variales cannot be implemented with %d %d-input LUTs.\n", nVars, nNodes, nLutSize );
+        return 1;
+    }
     if ( nVars > 10 )
     {
         Abc_Print( -1, "Function should not have more than 10 inputs.\n" );

src/sat/bmc/bmc.h

@@ -35,6 +35,8 @@
 
 ABC_NAMESPACE_HEADER_START
 
+//#define USE_NODE_ORDER 1
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////

src/sat/bmc/bmcMaj.c

@@ -628,6 +628,7 @@ int Exa_ManAddCnfStart( Exa_Man_t * p, int fOnlyAnd )
                     return 0;
             }
         }
+#ifdef USE_NODE_ORDER
         // node ordering
         for ( j = p->nVars; j < i; j++ )
         for ( n = 0;   n < p->nObjs; n++ ) if ( p->VarMarks[i][0][n] )
@@ -638,6 +639,7 @@ int Exa_ManAddCnfStart( Exa_Man_t * p, int fOnlyAnd )
             if ( !bmcg_sat_solver_addclause( p->pSat, pLits2, 2 ) )
                 return 0;
         }
+#endif
         // two input functions
         for ( k = 0; k < 3; k++ )
         {
@@ -1017,6 +1019,7 @@ static int Exa3_ManAddCnfStart( Exa3_Man_t * p, int fOnlyAnd )
                     return 0;
             }
         }
+#ifdef USE_NODE_ORDER
         // node ordering
         for ( j = p->nVars; j < i; j++ )
         for ( n = 0;   n < p->nObjs; n++ ) if ( p->VarMarks[i][0][n] )
@@ -1027,6 +1030,7 @@ static int Exa3_ManAddCnfStart( Exa3_Man_t * p, int fOnlyAnd )
             if ( !bmcg_sat_solver_addclause( p->pSat, pLits2, 2 ) )
                 return 0;
         }
+#endif
         if ( p->nLutSize != 2 )
             continue;
         // two-input functions

src/sat/bmc/bmcMaj2.c

@@ -26,7 +26,6 @@
 
 ABC_NAMESPACE_IMPL_START
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -735,6 +734,7 @@ static int Exa_ManAddCnfStart( Exa_Man_t * p, int fOnlyAnd )
                     return 0;
             }
         }
+#ifdef USE_NODE_ORDER
         // node ordering
         for ( j = p->nVars; j < i; j++ )
         for ( n = 0;   n < p->nObjs; n++ ) if ( p->VarMarks[i][0][n] )
@@ -745,6 +745,7 @@ static int Exa_ManAddCnfStart( Exa_Man_t * p, int fOnlyAnd )
             if ( !sat_solver_addclause( p->pSat, pLits2, pLits2+2 ) )
                 return 0;
         }
+#endif
         // two input functions
         for ( k = 0; k < 3; k++ )
         {
@@ -939,7 +940,7 @@ static int Exa3_ManMarkup( Exa3_Man_t * p )
         }
     }
     printf( "The number of parameter variables = %d.\n", p->iVar );
-    //return p->iVar;
+    return p->iVar;
     // printout
 //    for ( i = p->nVars; i < p->nObjs; i++ )
     for ( i = p->nObjs - 1; i >= p->nVars; i-- )
@@ -1018,7 +1019,7 @@ static Exa3_Man_t * Exa3_ManAlloc( int nVars, int nNodes, int nLutSize, word * p
     p->vInfo      = Exa3_ManTruthTables( p );
     p->pSat       = sat_solver_new();
     sat_solver_setnvars( p->pSat, p->iVar );
-    Exa3_ManInitPolarity( p );
+    //Exa3_ManInitPolarity( p );
     return p;
 }
 static void Exa3_ManFree( Exa3_Man_t * p )
@@ -1187,6 +1188,7 @@ static int Exa3_ManAddCnfStart( Exa3_Man_t * p, int fOnlyAnd )
         }
         //printf( "Node %d:\n", i );
         //sat_solver_flip_print_clause( p->pSat );
+#ifdef USE_NODE_ORDER
         // node ordering
         for ( j = p->nVars; j < i; j++ )
         for ( n = 0;   n < p->nObjs; n++ ) if ( p->VarMarks[i][0][n] )
@@ -1197,6 +1199,7 @@ static int Exa3_ManAddCnfStart( Exa3_Man_t * p, int fOnlyAnd )
             if ( !sat_solver_addclause( p->pSat, pLits2, pLits2+2 ) )
                 return 0;
         }
+#endif
         if ( p->nLutSize != 2 )
             continue;
         // two-input functions