|
CUDA constexpr | NBitset () |
|
CUDA constexpr | NBitset (const this_type &other) |
|
constexpr | NBitset (this_type &&)=default |
|
CUDA constexpr | NBitset (value_type x) |
|
CUDA constexpr | NBitset (value_type lb, value_type ub) |
|
template<class M > |
CUDA constexpr | NBitset (const this_type2< M > &other) |
|
template<class M > |
CUDA constexpr | NBitset (this_type2< M > &&other) |
|
template<class M > |
CUDA constexpr | NBitset (const battery::bitset< N, M, T > &bits) |
|
template<class M > |
CUDA constexpr this_type & | operator= (const this_type2< M > &other) |
|
CUDA constexpr this_type & | operator= (const this_type &other) |
|
CUDA constexpr local::BInc | is_top () const |
|
CUDA constexpr local::BDec | is_bot () const |
|
CUDA constexpr const bitset_type & | value () const |
|
CUDA constexpr LB | lb () const |
|
CUDA constexpr UB | ub () const |
|
CUDA constexpr local_type | complement () const |
|
CUDA constexpr this_type & | tell_top () |
|
template<class A , class M > |
CUDA constexpr this_type & | tell_lb (const A &lb, BInc< M > &has_changed) |
|
template<class A , class M > |
CUDA constexpr this_type & | tell_ub (const A &ub, BInc< M > &has_changed) |
|
template<class M1 , class M2 > |
CUDA constexpr this_type & | tell (const this_type2< M1 > &other, BInc< M2 > &has_changed) |
|
template<class M > |
CUDA constexpr this_type & | tell (const this_type2< M > &other) |
|
CUDA constexpr this_type & | dtell_bot () |
|
template<class M1 , class M2 > |
CUDA constexpr this_type & | dtell (const this_type2< M1 > &other, BInc< M2 > &has_changed) |
|
template<class M > |
CUDA constexpr this_type & | dtell (const this_type2< M > &other) |
|
template<class M > |
CUDA constexpr bool | extract (this_type2< M > &ua) const |
|
template<class Env > |
CUDA TFormula< typename Env::allocator_type > | deinterpret (AVar x, const Env &env) const |
|
template<class F > |
CUDA NI F | deinterpret () const |
|
CUDA NI void | print () const |
|
CUDA constexpr local_type | width () const |
|
CUDA constexpr local_type | median () const |
|
|
CUDA static constexpr this_type | from_set (const battery::vector< int > &values) |
|
CUDA static constexpr local_type | eq_zero () |
|
CUDA static constexpr local_type | eq_one () |
|
CUDA static constexpr local_type | bot () |
|
CUDA static constexpr local_type | top () |
|
template<bool diagnose = false, class F , class Env , class M > |
CUDA static NI bool | interpret_tell (const F &f, const Env &env, this_type2< M > &tell, IDiagnostics &diagnostics) |
|
template<bool diagnose = false, class F , class Env , class M > |
CUDA static NI bool | interpret_ask (const F &f, const Env &env, this_type2< M > &k, IDiagnostics &diagnostics) |
|
template<IKind kind, bool diagnose = false, class F , class Env , class M > |
CUDA static NI bool | interpret (const F &f, const Env &env, this_type2< M > &k, IDiagnostics &diagnostics) |
|
CUDA NI static constexpr bool | is_supported_fun (Sig sig) |
|
template<class M > |
CUDA static constexpr local_type | neg (const this_type2< M > &x) |
|
template<class M > |
CUDA static constexpr local_type | abs (const this_type2< M > &x) |
|
template<Sig sig, class M > |
CUDA static constexpr local_type | fun (const this_type2< M > &x) |
|
template<class M > |
CUDA static constexpr local_type | additive_inverse (const this_type2< M > &x) |
|
template<Sig sig, class M1 , class M2 > |
CUDA static constexpr local_type | fun (const this_type2< M1 > &x, const this_type2< M2 > &y) |
|
template<size_t N, class Mem, class T = unsigned long long>
class lala::NBitset< N, Mem, T >
This class represents a set of integer values with a fixed-size bitset. In order to have well-defined arithmetic operations preserving bottom and top elements, the first and last bits (written L and R below) of the bitset are reserved. The meaning of L is to include all negative integers and the meaning of R is to include all integers greater than the size of the bitset. Given a bitset \( Lb_0b_1...b_nR \) of size n + 3, the concretization function is given as follows: \( \gamma(Lb_0b_1...b_nR) = \{ i \in \mathbb{Z} \mid 0 \leq i \leq n \land b_i = 1 \} \cup \{ i \in \mathbb{Z} \;|\; i < 0 \land L = 1 \} \cup \{ i \in \mathbb{Z} \;|\; i > n \land R = 1 \} \)
template<size_t N, class Mem , class T = unsigned long long>
template<bool diagnose = false, class F , class Env , class M >
Support the following language where all constants k
are integer or Boolean values:
var x:Z
var x:B
x <op> k
where k
is an integer constant and <op>
in {==, !=, <, <=, >, >=}.
x in S
where S
is a set of integers. It can be over-approximated if the element k
falls out of the bitset.
template<size_t N, class Mem , class T = unsigned long long>
template<bool diagnose = false, class F , class Env , class M >
Support the same language than the "tell language" without existential.