An improvement to 'twoexact' and 'lutexact'.

5 files changed, 63 insertions, 17 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index a8fd4845..e04c651e 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -8241,7 +8241,7 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: twoexact [-IN <num>] [-fcagvh] <hex>\n" );
+    Abc_Print( -2, "usage: twoexact [-IN <num>] [-agvh] <hex>\n" );
     Abc_Print( -2, "\t           exact synthesis of multi-input function using two-input gates\n" );
     Abc_Print( -2, "\t-I <num> : the number of input variables [default = %d]\n", nVars );
     Abc_Print( -2, "\t-N <num> : the number of MAJ3 nodes [default = %d]\n", nNodes );
@@ -8346,7 +8346,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: lutexact [-INK <num>] [-fcagvh] <hex>\n" );
+    Abc_Print( -2, "usage: lutexact [-INK <num>] [-agvh] <hex>\n" );
     Abc_Print( -2, "\t           exact synthesis of multi-input function using two-input gates\n" );
     Abc_Print( -2, "\t-I <num> : the number of input variables [default = %d]\n", nVars );
     Abc_Print( -2, "\t-N <num> : the number of K-input nodes [default = %d]\n", nNodes );
diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c
index 4f5dadef..db56f98b 100644
--- a/src/sat/bmc/bmcMaj.c
+++ b/src/sat/bmc/bmcMaj.c
@@ -628,6 +628,16 @@ int Exa_ManAddCnfStart( Exa_Man_t * p, int fOnlyAnd )
                     return 0;
             }
         }
+        // node ordering
+        for ( j = p->nVars; j < i; j++ )
+        for ( n = 0;   n < p->nObjs; n++ ) if ( p->VarMarks[i][0][n] )
+        for ( m = n+1; m < p->nObjs; m++ ) if ( p->VarMarks[j][0][m] )
+        {
+            pLits2[0] = Abc_Var2Lit( p->VarMarks[i][0][n], 1 );
+            pLits2[1] = Abc_Var2Lit( p->VarMarks[j][0][m], 1 );
+            if ( !bmcg_sat_solver_addclause( p->pSat, pLits2, 2 ) )
+                return 0;
+        }
         // two input functions
         for ( k = 0; k < 3; k++ )
         {
@@ -1007,6 +1017,16 @@ static int Exa3_ManAddCnfStart( Exa3_Man_t * p, int fOnlyAnd )
                     return 0;
             }
         }
+        // node ordering
+        for ( j = p->nVars; j < i; j++ )
+        for ( n = 0;   n < p->nObjs; n++ ) if ( p->VarMarks[i][0][n] )
+        for ( m = n+1; m < p->nObjs; m++ ) if ( p->VarMarks[j][0][m] )
+        {
+            pLits2[0] = Abc_Var2Lit( p->VarMarks[i][0][n], 1 );
+            pLits2[1] = Abc_Var2Lit( p->VarMarks[j][0][m], 1 );
+            if ( !bmcg_sat_solver_addclause( p->pSat, pLits2, 2 ) )
+                return 0;
+        }
         if ( p->nLutSize != 2 )
             continue;
         // two-input functions
diff --git a/src/sat/bmc/bmcMaj2.c b/src/sat/bmc/bmcMaj2.c
index 23b5cf41..aed84474 100644
--- a/src/sat/bmc/bmcMaj2.c
+++ b/src/sat/bmc/bmcMaj2.c
@@ -735,6 +735,16 @@ static int Exa_ManAddCnfStart( Exa_Man_t * p, int fOnlyAnd )
                     return 0;
             }
         }
+        // node ordering
+        for ( j = p->nVars; j < i; j++ )
+        for ( n = 0;   n < p->nObjs; n++ ) if ( p->VarMarks[i][0][n] )
+        for ( m = n+1; m < p->nObjs; m++ ) if ( p->VarMarks[j][0][m] )
+        {
+            pLits2[0] = Abc_Var2Lit( p->VarMarks[i][0][n], 1 );
+            pLits2[1] = Abc_Var2Lit( p->VarMarks[j][0][m], 1 );
+            if ( !sat_solver_addclause( p->pSat, pLits2, pLits2+2 ) )
+                return 0;
+        }
         // two input functions
         for ( k = 0; k < 3; k++ )
         {
@@ -1126,6 +1136,18 @@ static int Exa3_ManAddCnfStart( Exa3_Man_t * p, int fOnlyAnd )
                     return 0;
             }
         }
+        //printf( "Node %d:\n", i );
+        //sat_solver_flip_print_clause( p->pSat );
+        // node ordering
+        for ( j = p->nVars; j < i; j++ )
+        for ( n = 0;   n < p->nObjs; n++ ) if ( p->VarMarks[i][0][n] )
+        for ( m = n+1; m < p->nObjs; m++ ) if ( p->VarMarks[j][0][m] )
+        {
+            pLits2[0] = Abc_Var2Lit( p->VarMarks[i][0][n], 1 );
+            pLits2[1] = Abc_Var2Lit( p->VarMarks[j][0][m], 1 );
+            if ( !sat_solver_addclause( p->pSat, pLits2, pLits2+2 ) )
+                return 0;
+        }
         if ( p->nLutSize != 2 )
             continue;
         // two-input functions
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 96b03e62..31ae8dae 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -1716,12 +1716,11 @@ void sat_solver_rollback( sat_solver* s )
 
 int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
 {
-    int fVerbose = 0;
     lit *i,*j;
     int maxvar;
     lit last;
     assert( begin < end );
-    if ( fVerbose )
+    if ( s->fPrintClause )
     {
         for ( i = begin; i < end; i++ )
             printf( "%s%d ", (*i)&1 ? "!":"", (*i)>>1 );
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index e82f17a4..f4126567 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -158,6 +158,7 @@ struct sat_solver_t
     double      progress_estimate;
     int         verbosity;     // Verbosity level. 0=silent, 1=some progress report, 2=everything
     int         fVerbose;
+    int         fPrintClause;
 
     stats_t     stats;
     int         nLearntMax;    // max number of learned clauses
@@ -212,17 +213,21 @@ static inline clause * clause_read( sat_solver * s, cla h )
     return Sat_MemClauseHand( &s->Mem, h );      
 }
 
-static int sat_solver_var_value( sat_solver* s, int v )
+static inline int sat_solver_var_value( sat_solver* s, int v )
 {
     assert( v >= 0 && v < s->size );
     return (int)(s->model[v] == l_True);
 }
-static int sat_solver_var_literal( sat_solver* s, int v )
+static inline int sat_solver_var_literal( sat_solver* s, int v )
 {
     assert( v >= 0 && v < s->size );
     return toLitCond( v, s->model[v] != l_True );
 }
-static void sat_solver_act_var_clear(sat_solver* s) 
+static inline void sat_solver_flip_print_clause( sat_solver* s )
+{
+    s->fPrintClause ^= 1;
+}
+static inline void sat_solver_act_var_clear(sat_solver* s) 
 {
     int i;
     if ( s->VarActType == 0 )
@@ -245,7 +250,7 @@ static void sat_solver_act_var_clear(sat_solver* s)
     }
     else assert(0);
 }
-static void sat_solver_compress(sat_solver* s) 
+static inline void sat_solver_compress(sat_solver* s) 
 {
     if ( s->qtail != s->qhead )
     {
@@ -254,19 +259,19 @@ static void sat_solver_compress(sat_solver* s)
         (void) RetValue;
     }
 }
-static void sat_solver_delete_p( sat_solver ** ps )
+static inline void sat_solver_delete_p( sat_solver ** ps )
 {
     if ( *ps )
         sat_solver_delete( *ps );
     *ps = NULL;
 }
-static void sat_solver_clean_polarity(sat_solver* s, int * pVars, int nVars )
+static inline void sat_solver_clean_polarity(sat_solver* s, int * pVars, int nVars )
 {
     int i;
     for ( i = 0; i < nVars; i++ )
         s->polarity[pVars[i]] = 0;
 }
-static void sat_solver_set_polarity(sat_solver* s, int * pVars, int nVars )
+static inline void sat_solver_set_polarity(sat_solver* s, int * pVars, int nVars )
 {
     int i;
     for ( i = 0; i < s->size; i++ )
@@ -274,27 +279,27 @@ static void sat_solver_set_polarity(sat_solver* s, int * pVars, int nVars )
     for ( i = 0; i < nVars; i++ )
         s->polarity[pVars[i]] = 1;
 }
-static void sat_solver_set_literal_polarity(sat_solver* s, int * pLits, int nLits )
+static inline void sat_solver_set_literal_polarity(sat_solver* s, int * pLits, int nLits )
 {
     int i;
     for ( i = 0; i < nLits; i++ )
         s->polarity[Abc_Lit2Var(pLits[i])] = !Abc_LitIsCompl(pLits[i]);
 }
 
-static int sat_solver_final(sat_solver* s, int ** ppArray)
+static inline int sat_solver_final(sat_solver* s, int ** ppArray)
 {
     *ppArray = s->conf_final.ptr;
     return s->conf_final.size;
 }
 
-static abctime sat_solver_set_runtime_limit(sat_solver* s, abctime Limit)
+static inline abctime sat_solver_set_runtime_limit(sat_solver* s, abctime Limit)
 {
     abctime nRuntimeLimit = s->nRuntimeLimit;
     s->nRuntimeLimit = Limit;
     return nRuntimeLimit;
 }
 
-static int sat_solver_set_random(sat_solver* s, int fNotUseRandom)
+static inline int sat_solver_set_random(sat_solver* s, int fNotUseRandom)
 {
     int fNotUseRandomOld = s->fNotUseRandom;
     s->fNotUseRandom = fNotUseRandom;
@@ -330,11 +335,11 @@ static inline int sat_solver_count_usedvars(sat_solver* s)
         }
     return nVars;
 }
-static void sat_solver_set_runid( sat_solver *s, int id )               
+static inline void sat_solver_set_runid( sat_solver *s, int id )               
 { 
     s->RunId      = id;  
 }
-static void sat_solver_set_stop_func( sat_solver *s, int (*fnct)(int) ) 
+static inline void sat_solver_set_stop_func( sat_solver *s, int (*fnct)(int) ) 
 { 
     s->pFuncStop = fnct; 
 }