mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-31 16:33:18 +00:00
Code Activity

static_assert

Browse source
This commit is contained in:
Jakob Rath 2023-07-27 16:54:59 +02:00
parent 8b9d9db77e
commit cd373527ff
1 changed files with 4 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/util/sat_literal.h
View file

@ -39,12 +39,7 @@ namespace sat {
class literal { class literal {
unsigned m_val; unsigned m_val;
public: public:
constexpr literal(): m_val(null_bool_var << 1) { constexpr literal(): m_val(null_bool_var << 1) { }
#ifdef Z3DEBUG
assert(var() == null_bool_var);
assert(!sign());
#endif
}
explicit literal(bool_var v, bool _sign = false): explicit literal(bool_var v, bool _sign = false):
m_val((v << 1) + static_cast<unsigned>(_sign)) { m_val((v << 1) + static_cast<unsigned>(_sign)) {
@ -90,6 +85,9 @@ namespace sat {
}; };
inline constexpr literal null_literal; inline constexpr literal null_literal;
static_assert(null_literal.var() == null_bool_var);
static_assert(!null_literal.sign());
using literal_hash = obj_hash<literal>; using literal_hash = obj_hash<literal>;
inline literal to_literal(unsigned x) { literal l; l.m_val = x; return l; } inline literal to_literal(unsigned x) { literal l; l.m_val = x; return l; }