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

3 files changed, 90 insertions, 66 deletions

diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c
index 51c2ac6d..18f91cf0 100644
--- a/src/aig/gia/giaAbsGla2.c
+++ b/src/aig/gia/giaAbsGla2.c
@@ -41,8 +41,8 @@ struct Ga2_Man_t_
     Gia_Man_t *    pGia;            // working AIG manager
     Gia_ParVta_t * pPars;           // parameters
     // markings 
-    Vec_Int_t *    vMapping;        // for each object: leaf count, leaves, truth table
     int            nMarked;         // total number of marked nodes and flops
+    Vec_Int_t *    vMapping;        // for each object: leaf count, leaves, truth table
     Vec_Ptr_t *    vDatas;          // for each object: leaves, CNF0, CNF1
     // abstraction
     Vec_Int_t *    vAbs;            // array of abstracted objects
diff --git a/src/sat/bsat/satClause.h b/src/sat/bsat/satClause.h
index 79a43b4e..c40e5f18 100644
--- a/src/sat/bsat/satClause.h
+++ b/src/sat/bsat/satClause.h
@@ -90,6 +90,7 @@ static inline int       Sat_MemHandShift( Sat_Mem_t * p, cla h )     { return h
 
 static inline int       Sat_MemIntSize( int size, int lrn )          { return (size + 2 + lrn) & ~01;               }
 static inline int       Sat_MemClauseSize( clause * p )              { return Sat_MemIntSize(p->size, p->lrn);      }
+static inline int       Sat_MemClauseSize2( clause * p )             { return Sat_MemIntSize(p->size, 1);           }
 
 //static inline clause *  Sat_MemClause( Sat_Mem_t * p, int i, int k ) { assert(i <= p->iPage[i&1] && k <= Sat_MemLimit(p->pPages[i]));  return (clause *)(p->pPages[i] + k ); }
 static inline clause *  Sat_MemClause( Sat_Mem_t * p, int i, int k ) { assert( k ); return (clause *)(p->pPages[i] + k);         }
@@ -112,12 +113,16 @@ static inline double    Sat_MemMemoryAll( Sat_Mem_t * p )            { return 1.
 // i is page number
 // k is page offset
 
-// this macro has to be fixed (Sat_MemClauseSize does not work for problem clauses in proof mode)
-/*
+// print problelm clauses NOT in proof mode
 #define Sat_MemForEachClause( p, c, i, k )      \
     for ( i = 0; i <= p->iPage[0]; i += 2 )     \
         for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize(c) )
-*/
+
+// print problem clauses in proof model
+#define Sat_MemForEachClause2( p, c, i, k )      \
+    for ( i = 0; i <= p->iPage[0]; i += 2 )     \
+        for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize2(c) )
+
 #define Sat_MemForEachLearned( p, c, i, k )     \
     for ( i = 1; i <= p->iPage[1]; i += 2 )     \
         for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize(c) )
diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c
index 05b9403d..8c378569 100644
--- a/src/sat/bsat/satUtil.c
+++ b/src/sat/bsat/satUtil.c
@@ -30,19 +30,6 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-/*
-struct clause_t
-{
-    unsigned   size  :  24;
-    unsigned   lbd   :   6;
-    unsigned   leant :   1;
-    unsigned   mark  :   1;
-    lit lits[0];
-};
-static inline int  clause_size( clause* c )  { return c->size;             }
-static inline lit* clause_begin( clause* c ) { return c->lits;             }
-*/
-
 static void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, int fIncrement );
 
 ////////////////////////////////////////////////////////////////////////
@@ -62,16 +49,56 @@ static void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, int fIncreme
 ***********************************************************************/
 void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars )
 {
-/*
+    Sat_Mem_t * pMem = &p->Mem;
     FILE * pFile;
-    void ** pClauses;
-    int nClauses, i;
+    clause * c;
+    int i, k;
+
+    // start the file
+    pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        printf( "Sat_SolverWriteDimacs(): Cannot open the ouput file.\n" );
+        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) );
+
+    // write the original clauses
+    Sat_MemForEachClause( pMem, c, i, k )
+        Sat_SolverClauseWriteDimacs( pFile, c, incrementVars );
+
+    // write the learned clauses
+    Sat_MemForEachLearned( pMem, c, i, k )
+        Sat_SolverClauseWriteDimacs( pFile, c, incrementVars );
 
-    // count the number of clauses
-    nClauses = p->clauses.size + p->learnts.size;
+    // write zero-level assertions
     for ( i = 0; i < p->size; i++ )
         if ( p->levels[i] == 0 && p->assigns[i] != l_Undef )
-            nClauses++;
+            fprintf( pFile, "%s%d%s\n",
+                     (p->assigns[i] == l_False)? "-": "",
+                     i + (int)(incrementVars>0),
+                     (incrementVars) ? " 0" : "");
+
+    // write the assumptions
+    if (assumptionsBegin) {
+        for (; assumptionsBegin != assumptionsEnd; assumptionsBegin++) {
+            fprintf( pFile, "%s%d%s\n",
+                     lit_sign(*assumptionsBegin)? "-": "",
+                     lit_var(*assumptionsBegin) + (int)(incrementVars>0),
+                     (incrementVars) ? " 0" : "");
+        }
+    }
+
+    fprintf( pFile, "\n" );
+    fclose( pFile );
+} 
+void Sat_Solver2WriteDimacs( sat_solver2 * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars )
+{
+    Sat_Mem_t * pMem = &p->Mem;
+    FILE * pFile;
+    clause * c;
+    int i, k;
 
     // start the file
     pFile = fopen( pFileName, "wb" );
@@ -81,19 +108,15 @@ 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, nClauses );
+    fprintf( pFile, "p cnf %d %d\n", p->size, Sat_MemEntryNum(&p->Mem, 0) );
 
     // write the original clauses
-    nClauses = p->clauses.size;
-    pClauses = p->clauses.ptr;
-    for ( i = 0; i < nClauses; i++ )
-        Sat_SolverClauseWriteDimacs( pFile, (clause *)pClauses[i], incrementVars );
+    Sat_MemForEachClause2( pMem, c, i, k )
+        Sat_SolverClauseWriteDimacs( pFile, c, incrementVars );
 
     // write the learned clauses
-    nClauses = p->learnts.size;
-    pClauses = p->learnts.ptr;
-    for ( i = 0; i < nClauses; i++ )
-        Sat_SolverClauseWriteDimacs( pFile, (clause *)pClauses[i], incrementVars );
+    Sat_MemForEachLearned( pMem, c, i, k )
+        Sat_SolverClauseWriteDimacs( pFile, c, incrementVars );
 
     // write zero-level assertions
     for ( i = 0; i < p->size; i++ )
@@ -115,8 +138,8 @@ void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBe
 
     fprintf( pFile, "\n" );
     fclose( pFile );
-*/
 }   
+  
 
 /**Function*************************************************************
 
@@ -131,17 +154,12 @@ void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBe
 ***********************************************************************/
 void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, int fIncrement )
 {
-/*
-    lit * pLits = clause_begin(pC);
-    int nLits = clause_size(pC);
     int i;
-
-    for ( i = 0; i < nLits; i++ )
-        fprintf( pFile, "%s%d ", (lit_sign(pLits[i])? "-": ""),  lit_var(pLits[i]) + (fIncrement>0) );
+    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*************************************************************
@@ -168,32 +186,6 @@ void Sat_SolverPrintStats( FILE * pFile, sat_solver * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the number of bytes used for each variable.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Sat_Solver2GetVarMem( sat_solver2 * s )
-{
-    int Mem = 0;
-    Mem += (sizeof(s->activity[0]) == 4) ? sizeof(unsigned) : sizeof(double);  // activity
-    Mem += 2 * sizeof(veci); // wlists
-    Mem += sizeof(int);      // vi (variable info)
-    Mem += sizeof(int);      // trail
-    Mem += sizeof(int);      // orderpos
-    Mem += sizeof(int);      // reasons
-    Mem += sizeof(int);      // units
-    Mem += sizeof(int);      // order
-    Mem += sizeof(int);      // model
-    return Mem;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Writes the given clause in a file in DIMACS format.]
 
   Description []
@@ -224,6 +216,32 @@ void Sat_Solver2PrintStats( FILE * pFile, sat_solver2 * s )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the number of bytes used for each variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sat_Solver2GetVarMem( sat_solver2 * s )
+{
+    int Mem = 0;
+    Mem += (sizeof(s->activity[0]) == 4) ? sizeof(unsigned) : sizeof(double);  // activity
+    Mem += 2 * sizeof(veci); // wlists
+    Mem += sizeof(int);      // vi (variable info)
+    Mem += sizeof(int);      // trail
+    Mem += sizeof(int);      // orderpos
+    Mem += sizeof(int);      // reasons
+    Mem += sizeof(int);      // units
+    Mem += sizeof(int);      // order
+    Mem += sizeof(int);      // model
+    return Mem;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns a counter-example.]
 
   Description []
@@ -277,6 +295,7 @@ int * Sat_Solver2GetModel( sat_solver2 * p, int * pVars, int nVars )
 ***********************************************************************/
 void Sat_SolverDoubleClauses( sat_solver * p, int iVar )
 {
+    assert( 0 );
 /*
     clause * pClause;
     lit Lit, * pLits;