luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Fixing the dump of SAT solver into a CNF file.

This commit is contained in:
Alan Mishchenko 2013-03-26 18:42:47 -07:00
parent d010231043
commit dfb065fa55
4 changed files with 30 additions and 19 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
src/opt/mfs/mfsInter.c
View File

@ -329,7 +329,8 @@ int Abc_NtkMfsInterplateEval( Mfs_Man_t * p, int * pCands, int nCands )
Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands )
{
extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
int fDumpFile = 0;
char FileName[32];
sat_solver * pSat;
Sto_Man_t * pCnf = NULL;
unsigned * puTruth;
@ -338,14 +339,23 @@ Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands )
int nFanins, status;
int c, i, * pGloVars;
// clock_t clk = clock();
// p->nDcMints += Abc_NtkMfsInterplateEval( p, pCands, nCands );
// derive the SAT solver for interpolation
pSat = Abc_MfsCreateSolverResub( p, pCands, nCands, 0 );
// dump CNF file (remember to uncomment two-lit clases in clause_create_new() in 'satSolver.c')
if ( fDumpFile )
{
static int Counter = 0;
sprintf( FileName, "cnf\\pj1_if6_mfs%03d.cnf", Counter++ );
Sat_SolverWriteDimacs( pSat, FileName, NULL, NULL, 1 );
}
// solve the problem
status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( fDumpFile )
printf( "File %s has UNSAT problem with %d conflicts.\n", FileName, (int)pSat->stats.conflicts );
if ( status != l_False )
{
p->nTimeOuts++;

8
src/sat/bsat/satClause.h
View File

@ -113,15 +113,15 @@ static inline double Sat_MemMemoryAll( Sat_Mem_t * p ) { return 1.
// i is page number
// k is page offset
// print problelm clauses NOT in proof mode
// print problem 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) )
for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize(c) ) if ( i == 0 && k == 2 ) {} else
// print problem clauses in proof model
// print problem clauses in proof mode
#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) )
for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize2(c) ) if ( i == 0 && k == 2 ) {} else
#define Sat_MemForEachLearned( p, c, i, k ) \
for ( i = 1; i <= p->iPage[1]; i += 2 ) \

3
src/sat/bsat/satSolver.c
View File

@ -401,6 +401,7 @@ static inline int sat_clause_compute_lbd( sat_solver* s, clause* c )
*/
static int clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt)
{
int fUseBinaryClauses = 1;
int size;
clause* c;
int h;
@ -410,7 +411,7 @@ static int clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt)
size = end - begin;
// do not allocate memory for the two-literal problem clause
if ( size == 2 && !learnt )
if ( fUseBinaryClauses && size == 2 && !learnt )
{
veci_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(clause_from_lit(begin[1])));
veci_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(clause_from_lit(begin[0])));

24
src/sat/bsat/satUtil.c
View File

@ -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" : "");