Improvements to command 'twoexact'.

3 files changed, 124 insertions, 19 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 0414687e..eb6f6145 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -8770,7 +8770,7 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
     Bmc_EsPar_t Pars, * pPars = &Pars;
     Bmc_EsParSetDefault( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "INTaogvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "INTadcogvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -8810,6 +8810,12 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'a':
             pPars->fOnlyAnd ^= 1;
             break;
+        case 'd':
+            pPars->fDynConstr ^= 1;
+            break;
+        case 'c':
+            pPars->fDumpCnf ^= 1;
+            break;
         case 'o':
             pPars->fFewerVars ^= 1;
             break;
@@ -8854,12 +8860,14 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: twoexact [-INT <num>] [-aogvh] <hex>\n" );
+    Abc_Print( -2, "usage: twoexact [-INT <num>] [-adcogvh] <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", pPars->nVars );
     Abc_Print( -2, "\t-N <num> : the number of two-input nodes [default = %d]\n", pPars->nNodes );
     Abc_Print( -2, "\t-T <num> : the runtime limit in seconds [default = %d]\n", pPars->RuntimeLim );
     Abc_Print( -2, "\t-a       : toggle using only AND-gates (without XOR-gates) [default = %s]\n", pPars->fOnlyAnd ? "yes" : "no" );
+    Abc_Print( -2, "\t-d       : toggle using dynamic constraint addition [default = %s]\n", pPars->fDynConstr ? "yes" : "no" );
+    Abc_Print( -2, "\t-c       : toggle dumping CNF into a file [default = %s]\n", pPars->fDumpCnf ? "yes" : "no" );
     Abc_Print( -2, "\t-o       : toggle using additional optimizations [default = %s]\n", pPars->fFewerVars ? "yes" : "no" );
     Abc_Print( -2, "\t-g       : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n", pPars->fGlucose ? "yes" : "no" );
     Abc_Print( -2, "\t-v       : toggle verbose printout [default = %s]\n", pPars->fVerbose ? "yes" : "no" );
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 12439faa..4de0bd7d 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -54,6 +54,8 @@ struct Bmc_EsPar_t_
     int        fMajority;
     int        fUseIncr;
     int        fOnlyAnd;
+    int        fDynConstr;
+    int        fDumpCnf;
     int        fGlucose;
     int        fOrderNodes;
     int        fEnumSols;
@@ -73,6 +75,8 @@ static inline void Bmc_EsParSetDefault( Bmc_EsPar_t * pPars )
     pPars->fMajority   = 0; 
     pPars->fUseIncr    = 0;
     pPars->fOnlyAnd    = 0; 
+    pPars->fDynConstr  = 0; 
+    pPars->fDumpCnf    = 0; 
     pPars->fGlucose    = 0; 
     pPars->fOrderNodes = 0; 
     pPars->fEnumSols   = 0; 
diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c
index fc77398a..075288cd 100644
--- a/src/sat/bmc/bmcMaj.c
+++ b/src/sat/bmc/bmcMaj.c
@@ -422,6 +422,8 @@ struct Exa_Man_t_
     int               VarVals[MAJ_NOBJS]; // values of the first nVars variables
     Vec_Wec_t *       vOutLits;  // output vars
     bmcg_sat_solver * pSat;      // SAT solver
+    FILE *            pFile;
+    int               nCnfClauses;
 };
 
 static inline word *  Exa_ManTruth( Exa_Man_t * p, int v ) { return Vec_WrdEntryP( p->vInfo, p->nWords * v ); }
@@ -502,10 +504,26 @@ Exa_Man_t * Exa_ManAlloc( Bmc_EsPar_t * pPars, word * pTruth )
     bmcg_sat_solver_set_nvars( p->pSat, p->iVar );
     if ( pPars->RuntimeLim )
         bmcg_sat_solver_set_runtime_limit( p->pSat, Abc_Clock() + pPars->RuntimeLim * CLOCKS_PER_SEC );
+    if ( pPars->fDumpCnf )
+    {
+        char Buffer[1000];
+        sprintf( Buffer, "%s_%d_%d.cnf", p->pPars->pTtStr, 2, p->nNodes );
+        p->pFile = fopen( Buffer, "wb" );
+        fputs( "p cnf                \n", p->pFile );
+    }
     return p;
 }
 void Exa_ManFree( Exa_Man_t * p )
 {
+    if ( p->pFile ) 
+    {
+        char Buffer[1000];
+        sprintf( Buffer, "%s_%d_%d.cnf", p->pPars->pTtStr, 2, p->nNodes );
+        rewind( p->pFile );
+        fprintf( p->pFile, "p cnf %d %d", bmcg_sat_solver_varnum(p->pSat), p->nCnfClauses );
+        fclose( p->pFile );
+        printf( "CNF was dumped into file \"%s\".\n", Buffer );
+    }
     bmcg_sat_solver_stop( p->pSat );
     Vec_WrdFree( p->vInfo );
     Vec_WecFree( p->vOutLits );
@@ -666,43 +684,115 @@ void Exa_ManPrintSolution( Exa_Man_t * p, int fCompl )
   SeeAlso     []
 
 ***********************************************************************/
-int Exa_ManAddCnfStart( Exa_Man_t * p, int fOnlyAnd )
+static inline int Exa_ManAddClause( Exa_Man_t * p, int * pLits, int nLits )
+{
+    int i;
+    if ( p->pFile )
+    {
+        p->nCnfClauses++;
+        for ( i = 0; i < nLits; i++ )
+            fprintf( p->pFile, "%s%d ", Abc_LitIsCompl(pLits[i]) ? "-" : "", Abc_Lit2Var(pLits[i]) );
+        fprintf( p->pFile, "0\n" );
+    }
+    return bmcg_sat_solver_addclause( p->pSat, pLits, nLits );
+}
+int Exa_ManAddCnfAdd( Exa_Man_t * p, int * pnAdded )
 {
     int pLits[MAJ_NOBJS], pLits2[2], i, j, k, n, m;
-    // input constraints
+    *pnAdded = 0;
     for ( i = p->nVars; i < p->nObjs; i++ )
     {
-        int iVarStart = 1 + 3*(i - p->nVars);
         for ( k = 0; k < 2; k++ )
         {
             int nLits = 0;
             for ( j = 0; j < p->nObjs; j++ )
-                if ( p->VarMarks[i][k][j] )
+                if ( p->VarMarks[i][k][j] && bmcg_sat_solver_read_cex_varvalue(p->pSat, p->VarMarks[i][k][j]) )
                     pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 0 );
             assert( nLits > 0 );
             // input uniqueness
-            if ( !bmcg_sat_solver_addclause( p->pSat, pLits, nLits ) )
-                return 0;
             for ( n = 0;   n < nLits; n++ )
             for ( m = n+1; m < nLits; m++ )
             {
+                (*pnAdded)++;
                 pLits2[0] = Abc_LitNot(pLits[n]);
                 pLits2[1] = Abc_LitNot(pLits[m]);
-                if ( !bmcg_sat_solver_addclause( p->pSat, pLits2, 2 ) )
+                if ( !Exa_ManAddClause( p, pLits2, 2 ) )
                     return 0;
             }
             if ( k == 1 )
                 break;
             // symmetry breaking
-            for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][k][j] )
-            for ( n = j; n < p->nObjs; n++ ) if ( p->VarMarks[i][k+1][n] )
+            for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][k][j]   && bmcg_sat_solver_read_cex_varvalue(p->pSat, p->VarMarks[i][k][j]) )
+            for ( n = j; n < p->nObjs; n++ ) if ( p->VarMarks[i][k+1][n] && bmcg_sat_solver_read_cex_varvalue(p->pSat, p->VarMarks[i][k+1][j]) )
             {
+                (*pnAdded)++;
                 pLits2[0] = Abc_Var2Lit( p->VarMarks[i][k][j], 1 );
                 pLits2[1] = Abc_Var2Lit( p->VarMarks[i][k+1][n], 1 );
-                if ( !bmcg_sat_solver_addclause( p->pSat, pLits2, 2 ) )
+                if ( !Exa_ManAddClause( p, pLits2, 2 ) )
                     return 0;
             }
         }
+    }
+    return 1;
+}
+int Exa_ManSolverSolve( Exa_Man_t * p )
+{
+    int nAdded = 1;
+    while ( nAdded )
+    {
+        int status = bmcg_sat_solver_solve( p->pSat, NULL, 0 );
+        if ( status != GLUCOSE_SAT )
+            return status;
+        status = Exa_ManAddCnfAdd( p, &nAdded );
+        //printf( "Added %d clauses.\n", nAdded );
+        if ( status != GLUCOSE_SAT )
+            return status;
+    }
+    return GLUCOSE_SAT;
+}
+int Exa_ManAddCnfStart( Exa_Man_t * p, int fOnlyAnd )
+{
+    int pLits[MAJ_NOBJS], pLits2[2], i, j, k, n, m;
+    // input constraints
+    for ( i = p->nVars; i < p->nObjs; i++ )
+    {
+        int iVarStart = 1 + 3*(i - p->nVars);
+        for ( k = 0; k < 2; k++ )
+        {
+            int nLits = 0;
+            for ( j = 0; j < p->nObjs; j++ )
+                if ( p->VarMarks[i][k][j] )
+                    pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 0 );
+            assert( nLits > 0 );
+            if ( !Exa_ManAddClause( p, pLits, nLits ) )
+                return 0;
+            // input uniqueness
+            if ( !p->pPars->fDynConstr )
+            {
+                for ( n = 0;   n < nLits; n++ )
+                for ( m = n+1; m < nLits; m++ )
+                {
+                    pLits2[0] = Abc_LitNot(pLits[n]);
+                    pLits2[1] = Abc_LitNot(pLits[m]);
+                    if ( !Exa_ManAddClause( p, pLits2, 2 ) )
+                        return 0;
+                }
+            }
+            if ( k == 1 )
+                break;
+            // symmetry breaking
+            if ( !p->pPars->fDynConstr )
+            {
+                for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][k][j] )
+                for ( n = j; n < p->nObjs; n++ ) if ( p->VarMarks[i][k+1][n] )
+                {
+                    pLits2[0] = Abc_Var2Lit( p->VarMarks[i][k][j], 1 );
+                    pLits2[1] = Abc_Var2Lit( p->VarMarks[i][k+1][n], 1 );
+                    if ( !Exa_ManAddClause( p, pLits2, 2 ) )
+                        return 0;
+                }
+            }
+        }
 #ifdef USE_NODE_ORDER
         // node ordering
         for ( j = p->nVars; j < i; j++ )
@@ -711,7 +801,7 @@ int Exa_ManAddCnfStart( Exa_Man_t * p, int fOnlyAnd )
         {
             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 ) )
+            if ( !Exa_ManAddClause( p, pLits2, 2 ) )
                 return 0;
         }
 #endif
@@ -721,7 +811,7 @@ int Exa_ManAddCnfStart( Exa_Man_t * p, int fOnlyAnd )
             pLits[0] = Abc_Var2Lit( iVarStart,   k==1 );
             pLits[1] = Abc_Var2Lit( iVarStart+1, k==2 );
             pLits[2] = Abc_Var2Lit( iVarStart+2, k!=0 );
-            if ( !bmcg_sat_solver_addclause( p->pSat, pLits, 3 ) )
+            if ( !Exa_ManAddClause( p, pLits, 3 ) )
                 return 0;
         }
         if ( fOnlyAnd )
@@ -729,7 +819,7 @@ int Exa_ManAddCnfStart( Exa_Man_t * p, int fOnlyAnd )
             pLits[0] = Abc_Var2Lit( iVarStart,   1 );
             pLits[1] = Abc_Var2Lit( iVarStart+1, 1 );
             pLits[2] = Abc_Var2Lit( iVarStart+2, 0 );
-            if ( !bmcg_sat_solver_addclause( p->pSat, pLits, 3 ) )
+            if ( !Exa_ManAddClause( p, pLits, 3 ) )
                 return 0;
         }
     }
@@ -738,7 +828,7 @@ int Exa_ManAddCnfStart( Exa_Man_t * p, int fOnlyAnd )
     {
         Vec_Int_t * vArray = Vec_WecEntry(p->vOutLits, i);
         assert( Vec_IntSize(vArray) > 0 );
-        if ( !bmcg_sat_solver_addclause( p->pSat, Vec_IntArray(vArray), Vec_IntSize(vArray) ) )
+        if ( !Exa_ManAddClause( p, Vec_IntArray(vArray), Vec_IntSize(vArray) ) )
             return 0;
     }
     return 1;
@@ -770,7 +860,7 @@ int Exa_ManAddCnf( Exa_Man_t * p, int iMint )
                         pLits[nLits++] = Abc_Var2Lit( iBaseSatVarJ + 2, !n );
                     else if ( p->VarVals[j] == n )
                         continue;
-                    if ( !bmcg_sat_solver_addclause( p->pSat, pLits, nLits ) )
+                    if ( !Exa_ManAddClause( p, pLits, nLits ) )
                         return 0;
                 }
             }
@@ -790,7 +880,7 @@ int Exa_ManAddCnf( Exa_Man_t * p, int iMint )
                 if ( i != p->nObjs - 1 ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 2, !n );
                 if ( k > 0 )             pLits[nLits++] = Abc_Var2Lit( iVarStart +  k-1,  n );
                 assert( nLits <= 4 );
-                if ( !bmcg_sat_solver_addclause( p->pSat, pLits, nLits ) )
+                if ( !Exa_ManAddClause( p, pLits, nLits ) )
                     return 0;
             }
         }
@@ -815,7 +905,10 @@ void Exa_ManExactSynthesis( Bmc_EsPar_t * pPars )
         abctime clk = Abc_Clock();
         if ( !Exa_ManAddCnf( p, iMint ) )
             break;
-        status = bmcg_sat_solver_solve( p->pSat, NULL, 0 );
+        if ( pPars->fDynConstr )
+            status = Exa_ManSolverSolve( p );
+        else
+            status = bmcg_sat_solver_solve( p->pSat, NULL, 0 );
         if ( pPars->fVerbose )
         {
             printf( "Iter %3d : ", i );