Skip to content

A
abc
Commit da60781c by Alan Mishchenko
Options

SAT solver with dynamic CNF loading.

parent 710fd8e1
Showing with 139 additions and 4 deletions
abclib.dsp
......@@ -1435,6 +1435,10 @@ SOURCE=.\src\sat\bmc\bmcCexTools.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\bmc\bmcLoad.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\bmc\bmcUnroll.c
# End Source File
# End Group
......
src/base/abci/abc.c
......@@ -391,6 +391,7 @@ static int Abc_CommandAbc9Cycle ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Cone ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9PoPart ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9MultiProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Bmc ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9PoPart2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9CexCut ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9CexMerge ( Abc_Frame_t * pAbc, int argc, char ** argv );
......@@ -942,6 +943,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&cone", Abc_CommandAbc9Cone, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&popart", Abc_CommandAbc9PoPart, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&mprove", Abc_CommandAbc9MultiProve, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&bmc", Abc_CommandAbc9Bmc, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&popart2", Abc_CommandAbc9PoPart2, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&cexcut", Abc_CommandAbc9CexCut, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&cexmerge", Abc_CommandAbc9CexMerge, 0 );
......@@ -31547,6 +31549,90 @@ usage:
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9Bmc( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Bmc_PerformBmc( Gia_Man_t * pGia, Bmc_LadPar_t * pPars );
int c;
Bmc_LadPar_t Pars, * pPars = &Pars;
memset( pPars, 0, sizeof(Bmc_LadPar_t) );
pPars->nStart = 0; // starting timeframe
pPars->nFramesMax = 0; // maximum number of timeframes
pPars->nConfLimit = 0; // maximum number of conflicts at a node
pPars->fLoadCnf = 0; // dynamic CNF loading
pPars->fVerbose = 0; // verbose
pPars->fNotVerbose = 0; // skip line-by-line print-out
pPars->iFrame = 0; // explored up to this frame
pPars->nFailOuts = 0; // the number of failed outputs
pPars->nDropOuts = 0; // the number of dropped outputs
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "SFcvh" ) ) != EOF )
{
switch ( c )
{
case 'S':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage;
}
pPars->nStart = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nStart < 0 )
goto usage;
break;
case 'F':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
pPars->nFramesMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nFramesMax < 0 )
goto usage;
break;
case 'c':
pPars->fLoadCnf ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Rpm(): There is no AIG.\n" );
return 0;
}
Bmc_PerformBmc( pAbc->pGia, pPars );
return 0;
usage:
Abc_Print( -2, "usage: &bmc [-SF num] [-cvh]\n" );
Abc_Print( -2, "\t performs bounded model checking\n" );
Abc_Print( -2, "\t-S num : the starting timeframe [default = %d]\n", pPars->nStart );
Abc_Print( -2, "\t-F num : the maximum number of timeframes [default = %d]\n", pPars->nFramesMax );
Abc_Print( -2, "\t-c : toggle dynamic CNF loading [default = %s]\n", pPars->fLoadCnf? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9CexCut( Abc_Frame_t * pAbc, int argc, char ** argv )
{
return -1;
src/sat/bmc/bmc.h
......@@ -68,6 +68,20 @@ struct Saig_ParBmc_t_
int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode
};
typedef struct Bmc_LadPar_t_ Bmc_LadPar_t;
struct Bmc_LadPar_t_
{
int nStart; // starting timeframe
int nFramesMax; // maximum number of timeframes
int nConfLimit; // maximum number of conflicts at a node
int fLoadCnf; // dynamic CNF loading
int fVerbose; // verbose
int fNotVerbose; // skip line-by-line print-out
int iFrame; // explored up to this frame
int nFailOuts; // the number of failed outputs
int nDropOuts; // the number of dropped outputs
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
......
src/sat/bmc/module.make
......@@ -6,4 +6,5 @@ SRC += src/sat/bmc/bmcBmc.c \
src/sat/bmc/bmcCexMin1.c \
src/sat/bmc/bmcCexMin2.c \
src/sat/bmc/bmcCexTools.c \
src/sat/bmc/bmcLoad.c \
src/sat/bmc/bmcUnroll.c
src/sat/bsat/satSolver.c
......@@ -399,7 +399,7 @@ static inline int sat_clause_compute_lbd( sat_solver* s, clause* c )
/* pre: size > 1 && no variable occurs twice
*/
static int clause_create_new(sat_solver* s, lit* begin, lit* end, int learnt)
int sat_solver_clause_new(sat_solver* s, lit* begin, lit* end, int learnt)
{
int fUseBinaryClauses = 1;
int size;
......@@ -478,6 +478,25 @@ static inline int sat_solver_enqueue(sat_solver* s, lit l, int from)
if (var_value(s, v) != varX)
return var_value(s, v) == lit_sign(l);
else{
if ( s->pCnfFunc )
{
if ( lit_sign(l) )
{
if ( (s->loads[v] & 1) == 0 )
{
s->loads[v] ^= 1;
s->pCnfFunc( s->pCnfMan, l );
}
}
else
{
if ( (s->loads[v] & 2) == 0 )
{
s->loads[v] ^= 2;
s->pCnfFunc( s->pCnfMan, l );
}
}
}
// New fact -- store it.
#ifdef VERBOSEDEBUG
printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l));
......@@ -561,7 +580,7 @@ static void sat_solver_record(sat_solver* s, veci* cls)
{
lit* begin = veci_begin(cls);
lit* end = begin + veci_size(cls);
int h = (veci_size(cls) > 1) ? clause_create_new(s,begin,end,1) : 0;
int h = (veci_size(cls) > 1) ? sat_solver_clause_new(s,begin,end,1) : 0;
sat_solver_enqueue(s,*begin,h);
assert(veci_size(cls) > 0);
if ( h == 0 )
......@@ -1026,6 +1045,8 @@ void sat_solver_setnvars(sat_solver* s,int n)
if (s->cap < n){
int old_cap = s->cap;
while (s->cap < n) s->cap = s->cap*2+1;
if ( s->cap < 50000 )
s->cap = 50000;
s->wlists = ABC_REALLOC(veci, s->wlists, s->cap*2);
// s->vi = ABC_REALLOC(varinfo,s->vi, s->cap);
......@@ -1033,6 +1054,7 @@ void sat_solver_setnvars(sat_solver* s,int n)
s->assigns = ABC_REALLOC(char, s->assigns, s->cap);
s->polarity = ABC_REALLOC(char, s->polarity, s->cap);
s->tags = ABC_REALLOC(char, s->tags, s->cap);
s->loads = ABC_REALLOC(char, s->loads, s->cap);
#ifdef USE_FLOAT_ACTIVITY
s->activity = ABC_REALLOC(double, s->activity, s->cap);
#else
......@@ -1070,6 +1092,7 @@ void sat_solver_setnvars(sat_solver* s,int n)
s->assigns [var] = varX;
s->polarity[var] = 0;
s->tags [var] = 0;
s->loads [var] = 0;
s->orderpos[var] = veci_size(&s->order);
s->reasons [var] = 0;
s->model [var] = 0;
......@@ -1113,6 +1136,7 @@ void sat_solver_delete(sat_solver* s)
ABC_FREE(s->assigns );
ABC_FREE(s->polarity );
ABC_FREE(s->tags );
ABC_FREE(s->loads );
ABC_FREE(s->activity );
ABC_FREE(s->activity2);
ABC_FREE(s->pFreqs );
......@@ -1188,6 +1212,7 @@ double sat_solver_memory( sat_solver* s )
Mem += s->cap * sizeof(char); // ABC_FREE(s->assigns );
Mem += s->cap * sizeof(char); // ABC_FREE(s->polarity );
Mem += s->cap * sizeof(char); // ABC_FREE(s->tags );
Mem += s->cap * sizeof(char); // ABC_FREE(s->loads );
#ifdef USE_FLOAT_ACTIVITY
Mem += s->cap * sizeof(double); // ABC_FREE(s->activity );
#else
......@@ -1484,11 +1509,10 @@ int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
return sat_solver_enqueue(s,*begin,0);
// create new clause
clause_create_new(s,begin,j,0);
sat_solver_clause_new(s,begin,j,0);
return true;
}
double luby(double y, int x)
{
int size, seq;
......
src/sat/bsat/satSolver.h
......@@ -45,6 +45,7 @@ extern sat_solver* sat_solver_new(void);
extern void sat_solver_delete(sat_solver* s);
extern int sat_solver_addclause(sat_solver* s, lit* begin, lit* end);
extern int sat_solver_clause_new(sat_solver* s, lit* begin, lit* end, int learnt);
extern int sat_solver_simplify(sat_solver* s);
extern int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal);
extern void sat_solver_restart( sat_solver* s );
......@@ -129,6 +130,7 @@ struct sat_solver_t
char* assigns; // Current values of variables.
char* polarity; //
char* tags; //
char* loads; //
int* orderpos; // Index in variable order.
int* reasons; //
......@@ -183,6 +185,10 @@ struct sat_solver_t
int nRoots;
veci temp_clause; // temporary storage for a CNF clause
// CNF loading
void * pCnfMan; // external CNF manager
int(*pCnfFunc)(void * p, int); // external callback
};
static inline clause * clause_read( sat_solver * s, cla h )
......
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