diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-11-26 18:17:39 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-11-26 18:17:39 -0800 |
| commit | fc4ab6bd39cfd4a83af8069902878c422e1e885e (patch) | |
| tree | f69c22fb4064ab8f87b27cf1b776a386b417b1f8 /src/sat/bsat/satSolver.c | |
| parent | 0cfc97b9400f2d4ff814eb815a584bc6ffbfe1e6 (diff) | |
| download | abc-fc4ab6bd39cfd4a83af8069902878c422e1e885e.tar.gz abc-fc4ab6bd39cfd4a83af8069902878c422e1e885e.tar.bz2 abc-fc4ab6bd39cfd4a83af8069902878c422e1e885e.zip | |
Started experiments with a new solver.
Diffstat (limited to 'src/sat/bsat/satSolver.c')
| -rw-r--r-- | src/sat/bsat/satSolver.c | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 3904f8b0..96541f2d 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -118,15 +118,6 @@ static inline lit clause_read_lit (clause* c) { return (lit)((ABC_PTRUINT_T) static inline int sat_solver_dlevel(sat_solver* s) { return veci_size(&s->trail_lim); } static inline vecp* sat_solver_read_wlist(sat_solver* s, lit l) { return &s->wlists[l]; } -static inline void vecp_remove(vecp* v, void* e) -{ - void** ws = vecp_begin(v); - int j = 0; - for (; ws[j] != e ; j++); - assert(j < vecp_size(v)); - for (; j < vecp_size(v)-1; j++) ws[j] = ws[j+1]; - vecp_resize(v,vecp_size(v)-1); -} //================================================================================================= // Variable order functions: |