From 18737f7408a3d0f86c336e4960aef604b84d4168 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 28 Jul 2012 11:03:56 -0700 Subject: Fixed the problem with 'write_cnf' after recent changes to the SAT solver. --- src/sat/bsat/satClause.h | 11 +++- src/sat/bsat/satUtil.c | 143 +++++++++++++++++++++++++++-------------------- 2 files changed, 89 insertions(+), 65 deletions(-) (limited to 'src/sat/bsat') 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************************************************************* @@ -166,32 +184,6 @@ void Sat_SolverPrintStats( FILE * pFile, sat_solver * p ) // printf( "inspects2 : %10d\n", (int)p->stats.inspects2 ); } -/**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.] @@ -222,6 +214,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.] @@ -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; -- cgit v1.2.3