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

Changing dynamic CNF loading code to perform loading before propagate() as opposed to when the literal first implied in enqueue().

This commit is contained in:
Alan Mishchenko 2013-09-16 23:43:47 -07:00
parent 105648bf7c
commit 5df166fce1
1 changed files with 31 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -478,6 +478,7 @@ 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) )
@ -497,6 +498,7 @@ static inline int sat_solver_enqueue(sat_solver* s, lit l, int from)
}
}
}
*/
// New fact -- store it.
#ifdef VERBOSEDEBUG
printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l));
@ -876,6 +878,7 @@ static void sat_solver_analyze(sat_solver* s, int h, veci* learnt)
#endif
}
//#define TEST_CNF_LOAD
int sat_solver_propagate(sat_solver* s)
{
@ -886,6 +889,31 @@ int sat_solver_propagate(sat_solver* s)
//printf("sat_solver_propagate\n");
while (hConfl == 0 && s->qtail - s->qhead > 0){
lit p = s->trail[s->qhead++];
int v = lit_var(p);
#ifdef TEST_CNF_LOAD
if ( s->pCnfFunc )
{
if ( lit_sign(p) )
{
if ( (s->loads[v] & 1) == 0 )
{
s->loads[v] ^= 1;
s->pCnfFunc( s->pCnfMan, p );
}
}
else
{
if ( (s->loads[v] & 2) == 0 )
{
s->loads[v] ^= 2;
s->pCnfFunc( s->pCnfMan, p );
}
}
}
{
#endif
veci* ws = sat_solver_read_wlist(s,p);
int* begin = veci_begin(ws);
int* end = begin + veci_size(ws);
@ -959,6 +987,9 @@ int sat_solver_propagate(sat_solver* s)
s->stats.inspects += j - veci_begin(ws);
veci_resize(ws,j - veci_begin(ws));
#ifdef TEST_CNF_LOAD
}
#endif
}
return hConfl;