diff options
Diffstat (limited to 'src/sat/bsat/satVec.h')
| -rw-r--r-- | src/sat/bsat/satVec.h | 38 |
1 files changed, 38 insertions, 0 deletions
diff --git a/src/sat/bsat/satVec.h b/src/sat/bsat/satVec.h index 6e604d36..4eedbdd0 100644 --- a/src/sat/bsat/satVec.h +++ b/src/sat/bsat/satVec.h @@ -86,6 +86,44 @@ static inline void vecp_push (vecp* v, void* e) +//================================================================================================= +// Simple types: + +#ifndef __cplusplus +#ifndef false +# define false 0 +#endif +#ifndef true +# define true 1 +#endif +#endif + +typedef int lit; +typedef char lbool; + +static const int var_Undef = -1; +static const lit lit_Undef = -2; + +static const lbool l_Undef = 0; +static const lbool l_True = 1; +static const lbool l_False = -1; + +static inline lit toLit (int v) { return v + v; } +static inline lit toLitCond(int v, int c) { return v + v + (c != 0); } +static inline lit lit_neg (lit l) { return l ^ 1; } +static inline int lit_var (lit l) { return l >> 1; } +static inline int lit_sign (lit l) { return l & 1; } +static inline int lit_print(lit l) { return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; } +static inline lit lit_read (int s) { return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); } +static inline int lit_check(lit l, int n) { return l >= 0 && lit_var(l) < n; } + +struct stats_t +{ + ABC_INT64_T starts, decisions, propagations, inspects, conflicts; + ABC_INT64_T clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals; +}; +typedef struct stats_t stats_t; + ABC_NAMESPACE_HEADER_END |