diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-12-04 16:10:11 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-12-04 16:10:11 -0800 |
| commit | 09d3e1ff77e656976268fa27b6045ff6f284fd3b (patch) | |
| tree | 8fd52c0920fe3a46f7599fdee2b745d24b94320d /src/sat/bsat/satVec.h | |
| parent | a7031bb3f76385b014af0e329e5313b531cf2d72 (diff) | |
| download | abc-09d3e1ff77e656976268fa27b6045ff6f284fd3b.tar.gz abc-09d3e1ff77e656976268fa27b6045ff6f284fd3b.tar.bz2 abc-09d3e1ff77e656976268fa27b6045ff6f284fd3b.zip | |
Proof-logging in the updated solver.
Diffstat (limited to 'src/sat/bsat/satVec.h')
| -rw-r--r-- | src/sat/bsat/satVec.h | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/src/sat/bsat/satVec.h b/src/sat/bsat/satVec.h index aeca3059..1f63ba1e 100644 --- a/src/sat/bsat/satVec.h +++ b/src/sat/bsat/satVec.h @@ -44,7 +44,8 @@ static inline void veci_new (veci* v) { static inline void veci_delete (veci* v) { ABC_FREE(v->ptr); } static inline int* veci_begin (veci* v) { return v->ptr; } static inline int veci_size (veci* v) { return v->size; } -static inline void veci_resize (veci* v, int k) { v->size = k; } // only safe to shrink !! +static inline void veci_resize (veci* v, int k) { assert(k <= v->size); v->size = k; } // only safe to shrink !! +static inline int veci_pop (veci* v) { assert(v->size); return v->ptr[--v->size]; } static inline void veci_push (veci* v, int e) { if (v->size == v->cap) { @@ -82,7 +83,7 @@ static inline void vecp_new (vecp* v) { static inline void vecp_delete (vecp* v) { ABC_FREE(v->ptr); } static inline void** vecp_begin (vecp* v) { return v->ptr; } static inline int vecp_size (vecp* v) { return v->size; } -static inline void vecp_resize (vecp* v, int k) { v->size = k; } // only safe to shrink !! +static inline void vecp_resize (vecp* v, int k) { assert(k <= v->size); v->size = k; } // only safe to shrink !! static inline void vecp_push (vecp* v, void* e) { if (v->size == v->cap) { @@ -143,9 +144,6 @@ struct stats_t }; typedef struct stats_t stats_t; -struct clause_t; -typedef struct clause_t clause; - ABC_NAMESPACE_HEADER_END #endif |