diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-03-26 18:42:47 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-03-26 18:42:47 -0700 |
| commit | dfb065fa553e54fe00891fbeefb866be2c6dfa9d (patch) | |
| tree | 4d48259db17b0d627c62021848cfe40172e50e61 /src/sat/bsat/satUtil.c | |
| parent | d010231043bc799ab7598e4ac779161a02001c17 (diff) | |
| download | abc-dfb065fa553e54fe00891fbeefb866be2c6dfa9d.tar.gz abc-dfb065fa553e54fe00891fbeefb866be2c6dfa9d.tar.bz2 abc-dfb065fa553e54fe00891fbeefb866be2c6dfa9d.zip | |
Fixing the dump of SAT solver into a CNF file.
Diffstat (limited to 'src/sat/bsat/satUtil.c')
| -rw-r--r-- | src/sat/bsat/satUtil.c | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c index 59eb047d..dc431440 100644 --- a/src/sat/bsat/satUtil.c +++ b/src/sat/bsat/satUtil.c @@ -78,7 +78,7 @@ void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumpBegin, // 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 ) + if ( p->levels[i] == 0 && p->assigns[i] != 3 ) nUnits++; // start the file @@ -89,21 +89,21 @@ void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumpBegin, 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)+Sat_MemEntryNum(&p->Mem, 1)+nUnits+(int)(assumpEnd-assumpBegin) ); + fprintf( pFile, "p cnf %d %d\n", p->size, Sat_MemEntryNum(&p->Mem, 0)-1+Sat_MemEntryNum(&p->Mem, 1)+nUnits+(int)(assumpEnd-assumpBegin) ); // 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 ); +// Sat_MemForEachLearned( pMem, c, i, k ) +// Sat_SolverClauseWriteDimacs( pFile, c, incrementVars ); // write zero-level assertions for ( i = 0; i < p->size; i++ ) - if ( p->levels[i] == 0 && p->assigns[i] != l_Undef ) + if ( p->levels[i] == 0 && p->assigns[i] != 3 ) // varX fprintf( pFile, "%s%d%s\n", - (p->assigns[i] == l_False)? "-": "", + (p->assigns[i] == 1)? "-": "", // var0 i + (int)(incrementVars>0), (incrementVars) ? " 0" : ""); @@ -130,7 +130,7 @@ void Sat_Solver2WriteDimacs( sat_solver2 * p, char * pFileName, lit* assumpBegin // 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 ) + if ( p->levels[i] == 0 && p->assigns[i] != 3 ) nUnits++; // start the file @@ -141,21 +141,21 @@ void Sat_Solver2WriteDimacs( sat_solver2 * p, char * pFileName, lit* assumpBegin 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)+Sat_MemEntryNum(&p->Mem, 1)+nUnits+(int)(assumpEnd-assumpBegin) ); + fprintf( pFile, "p cnf %d %d\n", p->size, Sat_MemEntryNum(&p->Mem, 0)-1+Sat_MemEntryNum(&p->Mem, 1)+nUnits+(int)(assumpEnd-assumpBegin) ); // write the original clauses Sat_MemForEachClause2( pMem, c, i, k ) Sat_SolverClauseWriteDimacs( pFile, c, incrementVars ); // write the learned clauses - Sat_MemForEachLearned( pMem, c, i, k ) - Sat_SolverClauseWriteDimacs( pFile, c, incrementVars ); +// Sat_MemForEachLearned( pMem, c, i, k ) +// Sat_SolverClauseWriteDimacs( pFile, c, incrementVars ); // write zero-level assertions for ( i = 0; i < p->size; i++ ) - if ( p->levels[i] == 0 && p->assigns[i] != l_Undef ) + if ( p->levels[i] == 0 && p->assigns[i] != 3 ) // varX fprintf( pFile, "%s%d%s\n", - (p->assigns[i] == l_False)? "-": "", + (p->assigns[i] == 1)? "-": "", // var0 i + (int)(incrementVars>0), (incrementVars) ? " 0" : ""); |