Fixed the problem with 'write_cnf' after recent changes to the SAT solver.

src/sat/bsat/satUtil.c

@@ -38,6 +38,27 @@ static void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, int fIncreme
 
 /**Function*************************************************************
 
+  Synopsis    [Writes the given clause in a file in DIMACS format.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, int fIncrement )
+{
+    int i;
+    for ( i = 0; i < (int)pC->size; i++ )
+        fprintf( pFile, "%s%d ", (lit_sign(pC->lits[i])? "-": ""),  lit_var(pC->lits[i]) + (fIncrement>0) );
+    if ( fIncrement )
+        fprintf( pFile, "0" );
+    fprintf( pFile, "\n" );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Write the clauses in the solver into a file in DIMACS format.]
 
   Description []
@@ -47,12 +68,18 @@ static void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, int fIncreme
   SeeAlso     []
 
 ***********************************************************************/
-void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars )
+void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumpBegin, lit* assumpEnd, int incrementVars )
 {
     Sat_Mem_t * pMem = &p->Mem;
     FILE * pFile;
     clause * c;
-    int i, k;
+    int i, k, nUnits;
+
+    // count the number of unit clauses
+    nUnits = 0;
+    for ( i = 0; i < p->size; i++ )
+        if ( p->levels[i] == 0 && p->assigns[i] != l_Undef )
+            nUnits++;
 
     // start the file
     pFile = fopen( pFileName, "wb" );
@@ -62,7 +89,7 @@ void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBe
         return;
     }
 //    fprintf( pFile, "c CNF generated by ABC on %s\n", Extra_TimeStamp() );
-    fprintf( pFile, "p cnf %d %d\n", p->size, Sat_MemEntryNum(&p->Mem, 0) );
+    fprintf( pFile, "p cnf %d %d\n", p->size, Sat_MemEntryNum(&p->Mem, 0)+Sat_MemEntryNum(&p->Mem, 1)+nUnits+(assumpEnd-assumpBegin) );
 
     // write the original clauses
     Sat_MemForEachClause( pMem, c, i, k )
@@ -80,12 +107,12 @@ void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBe
                      i + (int)(incrementVars>0),
                      (incrementVars) ? " 0" : "");
 
-    // write the assumptions
-    if (assumptionsBegin) {
-        for (; assumptionsBegin != assumptionsEnd; assumptionsBegin++) {
+    // write the assump
+    if (assumpBegin) {
+        for (; assumpBegin != assumpEnd; assumpBegin++) {
             fprintf( pFile, "%s%d%s\n",
-                     lit_sign(*assumptionsBegin)? "-": "",
-                     lit_var(*assumptionsBegin) + (int)(incrementVars>0),
+                     lit_sign(*assumpBegin)? "-": "",
+                     lit_var(*assumpBegin) + (int)(incrementVars>0),
                      (incrementVars) ? " 0" : "");
         }
     }
@@ -93,12 +120,18 @@ void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBe
     fprintf( pFile, "\n" );
     fclose( pFile );
 } 
-void Sat_Solver2WriteDimacs( sat_solver2 * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars )
+void Sat_Solver2WriteDimacs( sat_solver2 * p, char * pFileName, lit* assumpBegin, lit* assumpEnd, int incrementVars )
 {
     Sat_Mem_t * pMem = &p->Mem;
     FILE * pFile;
     clause * c;
-    int i, k;
+    int i, k, nUnits;
+
+    // count the number of unit clauses
+    nUnits = 0;
+    for ( i = 0; i < p->size; i++ )
+        if ( p->levels[i] == 0 && p->assigns[i] != l_Undef )
+            nUnits++;
 
     // start the file
     pFile = fopen( pFileName, "wb" );
@@ -108,7 +141,7 @@ void Sat_Solver2WriteDimacs( sat_solver2 * p, char * pFileName, lit* assumptions
         return;
     }
 //    fprintf( pFile, "c CNF generated by ABC on %s\n", Extra_TimeStamp() );
-    fprintf( pFile, "p cnf %d %d\n", p->size, Sat_MemEntryNum(&p->Mem, 0) );
+    fprintf( pFile, "p cnf %d %d\n", p->size, Sat_MemEntryNum(&p->Mem, 0)+Sat_MemEntryNum(&p->Mem, 1)+nUnits+(assumpEnd-assumpBegin) );
 
     // write the original clauses
     Sat_MemForEachClause2( pMem, c, i, k )
@@ -126,12 +159,12 @@ void Sat_Solver2WriteDimacs( sat_solver2 * p, char * pFileName, lit* assumptions
                      i + (int)(incrementVars>0),
                      (incrementVars) ? " 0" : "");
 
-    // write the assumptions
-    if (assumptionsBegin) {
-        for (; assumptionsBegin != assumptionsEnd; assumptionsBegin++) {
+    // write the assump
+    if (assumpBegin) {
+        for (; assumpBegin != assumpEnd; assumpBegin++) {
             fprintf( pFile, "%s%d%s\n",
-                     lit_sign(*assumptionsBegin)? "-": "",
-                     lit_var(*assumptionsBegin) + (int)(incrementVars>0),
+                     lit_sign(*assumpBegin)? "-": "",
+                     lit_var(*assumpBegin) + (int)(incrementVars>0),
                      (incrementVars) ? " 0" : "");
         }
     }
@@ -152,27 +185,6 @@ void Sat_Solver2WriteDimacs( sat_solver2 * p, char * pFileName, lit* assumptions
   SeeAlso     []
 
 ***********************************************************************/
-void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, int fIncrement )
-{
-    int i;
-    for ( i = 0; i < (int)pC->size; i++ )
-        fprintf( pFile, "%s%d ", (lit_sign(pC->lits[i])? "-": ""),  lit_var(pC->lits[i]) + (fIncrement>0) );
-    if ( fIncrement )
-        fprintf( pFile, "0" );
-    fprintf( pFile, "\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Writes the given clause in a file in DIMACS format.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 void Sat_SolverPrintStats( FILE * pFile, sat_solver * p )
 {
 //    printf( "calls         : %10d (%d)\n", (int)p->nCalls, (int)p->nCalls2 );