Skip to content

A
abc
Commit 18737f74 by Alan Mishchenko
Options

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

parent 46772882
Showing with 90 additions and 66 deletions
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
......
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) )
......
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,9 +138,9 @@ void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBe
fprintf( pFile, "\n" );
fclose( pFile );
*/
}
/**Function*************************************************************
Synopsis [Writes the given clause in a file in DIMACS format.]
......@@ -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;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment