From 1b18583840f04d84b226cd11fb17a1aa41e5f5a3 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 28 Jul 2012 14:55:55 -0700 Subject: Fixed the problem with 'write_cnf' after recent changes to the SAT solver. --- src/sat/bsat/satUtil.c | 86 ++++++++++++++++++++++++++++---------------------- 1 file changed, 49 insertions(+), 37 deletions(-) (limited to 'src') diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c index 8c378569..abd668c6 100644 --- a/src/sat/bsat/satUtil.c +++ b/src/sat/bsat/satUtil.c @@ -36,6 +36,27 @@ static void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, int fIncreme /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**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.] @@ -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" : ""); } } @@ -141,27 +174,6 @@ void Sat_Solver2WriteDimacs( sat_solver2 * p, char * pFileName, lit* assumptions } -/**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 [Writes the given clause in a file in DIMACS format.] -- cgit v1.2.3