diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-09-16 23:43:47 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-09-16 23:43:47 -0700 |
commit | 5df166fce17e7729b590d799da753f6ab811886b (patch) | |
tree | b6f2bec8adaa3463257bff7fb403dc3125aaedf9 | |
parent | 105648bf7c5ce5825d7b62ffbc05cbbf821c5ced (diff) | |
download | abc-5df166fce17e7729b590d799da753f6ab811886b.tar.gz abc-5df166fce17e7729b590d799da753f6ab811886b.tar.bz2 abc-5df166fce17e7729b590d799da753f6ab811886b.zip |
Changing dynamic CNF loading code to perform loading before propagate() as opposed to when the literal first implied in enqueue().
-rw-r--r-- | src/sat/bsat/satSolver.c | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 022a3221..a13ae040 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -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; |