BitMagic-C++
bm3vl.h
Go to the documentation of this file.
1#ifndef BM3VL__H__INCLUDED__
2#define BM3VL__H__INCLUDED__
3/*
4Copyright(c) 2021 Anatoliy Kuznetsov(anatoliy_kuznetsov at yahoo.com)
5
6Licensed under the Apache License, Version 2.0 (the "License");
7you may not use this file except in compliance with the License.
8You may obtain a copy of the License at
9
10 http://www.apache.org/licenses/LICENSE-2.0
11
12Unless required by applicable law or agreed to in writing, software
13distributed under the License is distributed on an "AS IS" BASIS,
14WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
15See the License for the specific language governing permissions and
16limitations under the License.
17
18For more information please visit: http://bitmagic.io
19*/
20
21/*! \file bm3vl.h
22 \brief Three-valued logic (3VL) operations
23*/
24
25#include "bm.h"
26
27namespace bm
28{
29
30/** @defgroup bm3VL three-valued logic
31 Functions for three-valued logic (Kleene)
32 https://en.wikipedia.org/wiki/Three-valued_logic
33 @ingroup bvector
34 */
35
36
37/**
38 @brief Initialized the value bit-vector so that it always returns 0 (false)
39 for the unknown.
40
41 3-value logics in BitMagic is built on two bit-vectors:
42 value-bit-vector and NULL bit-vector. Value vector contains '1s' for the
43 true known elements. bm::init_3vl makes sure this is true by running
44 bv_value = bv_value AND bv_null logical operation.
45 NULL bit-vector represents NOT NULL (known) values as 1s
46
47 @param bv_value - [in, out] values bit-vector
48 @param bv_null - [in] not NULL (known) bit-vector
49
50 @ingroup bm3VL
51
52 */
53template<class BV>
54void init_kleene(BV& bv_value, const BV& bv_null)
55{
56 bv_value.bit_and(bv_null);
57}
58
59/**
60 @brief Return Kleene logic value based on value and known vectors
61
62 @param bv_value - [in] values bit-vector
63 @param bv_null - [in] knowns bit-vector
64 @param idx - [in] index of value to extract and return
65
66 @return (−1: false; 0: unknown; +1: true)
67 @ingroup bm3VL
68*/
69template<class BV>
70int get_value_kleene(const BV& bv_value, const BV& bv_null,
71 typename BV::size_type idx) BMNOEXCEPT
72{
73 bool b_notnull = bv_null.test(idx);
74 if (b_notnull)
75 {
76 // TODO: optimization may be needed to test 2 bvs in the same coord
77 bool b_val = bv_value.test(idx);
78 if (b_val)
79 return 1;
80 return -1;
81 }
82 return 0; // unknown
83}
84
85/**
86 @brief Set Kleene logic value based on value and known vectors
87
88 @param bv_value - [out] values bit-vector
89 @param bv_null - [out] knowns bit-vector
90 @param idx - [in] index of value to extract and return
91 @param val - [in] value which can be: (−1: false; 0: unknown; +1: true)
92
93 @ingroup bm3VL
94*/
95template<class BV>
96void set_value_kleene(BV& bv_value, BV& bv_null,
97 typename BV::size_type idx, int val)
98{
99 bool is_set;
100 switch (val)
101 {
102 case -1:
103 bv_value.clear_bit(idx);
104 bv_null.set(idx);
105 break;
106 case 0:
107 is_set = bv_null.set_bit_and(idx, false);
108 if (is_set)
109 bv_value.clear_bit(idx);
110 break;
111 case 1:
112 // TODO: optimization may be needed to set 2 bvs in the same coords
113 bv_value.set(idx);
114 bv_null.set(idx);
115 break;
116 default:
117 BM_ASSERT(0); // unknown 3-value logic constant
118 } // switch
119}
120
121
122/**
123 @brief Kleene NEG operation
124
125 True becomes false and vice verse, but unknowns remain unknown false
126 if we look directly into bv_value vector. This oprtaion does NOT produce
127 unknown true values.
128
129 @param bv_value - [in, out] values bit-vector
130 @param bv_null - [in] not NULL (known) bit-vector
131
132 @ingroup bm3VL
133 */
134template<class BV>
135void invert_kleene(BV& bv_value, const BV& bv_null)
136{
137 bv_value.bit_xor(bv_null);
138}
139
140/**
141 @brief Kleene OR(vect1, vect2) (vect1 |= vect2)
142 1 OR Unk = 1 (known)
143 @param bv_value1 - [in, out] values bit-vector
144 @param bv_null1 - [in, out] not NULL (known) bit-vector
145 @param bv_value2 - [in] values bit-vector
146 @param bv_null2 - [in] not NULL (known) bit-vector
147
148 @ingroup bm3VL
149 */
150template<class BV>
151void or_kleene(BV& bv_value1, BV& bv_null1,
152 const BV& bv_value2, const BV& bv_null2)
153{
154 BV bv_known_false1, bv_known_false2; // known but false
155 bv_known_false1.bit_xor(bv_value1, bv_null1, BV::opt_none);
156 bv_known_false2.bit_xor(bv_value2, bv_null2, BV::opt_none);
157
158 bv_known_false1.bit_sub(bv_null2); // known false but unknown in 2
159 bv_known_false2.bit_sub(bv_null1); // known false but unknown in 1
160
161 bv_value1.bit_or(bv_value2);
162 bv_null1.bit_or(bv_null2);
163
164 bv_null1.bit_sub(bv_known_false1); // exclude FALSE-unknown combinations
165 bv_null1.bit_sub(bv_known_false2);
166}
167
168/**
169 @brief 3-way Kleene OR: target := OR(vect1, vect2) (target := vect1 | vect2)
170 1 OR Unk = 1 (known)
171 @param bv_value_target - [out] target values bit-vector
172 @param bv_null_target - [out] target not NULL (known) bit-vector
173 @param bv_value1 - [in] values bit-vector
174 @param bv_null1 - [in] not NULL (known) bit-vector
175 @param bv_value2 - [in] values bit-vector
176 @param bv_null2 - [in] not NULL (known) bit-vector
177
178 @ingroup bm3VL
179 */
180template<class BV>
181void or_kleene(BV& bv_value_target, BV& bv_null_target,
182 const BV& bv_value1, const BV& bv_null1,
183 const BV& bv_value2, const BV& bv_null2)
184{
185 BV bv_known_false1, bv_known_false2; // known but false
186 bv_known_false1.bit_xor(bv_value1, bv_null1, BV::opt_none);
187 bv_known_false2.bit_xor(bv_value2, bv_null2, BV::opt_none);
188
189 bv_known_false1.bit_sub(bv_null2); // known false but unknown in 2
190 bv_known_false2.bit_sub(bv_null1); // known false but unknown in 1
191
192 bv_value_target.bit_or(bv_value1, bv_value2, BV::opt_none);
193 bv_null_target.bit_or(bv_null1, bv_null2, BV::opt_none);
194
195 // exclude FALSE-unknown combinations
196 bv_null_target.bit_sub(bv_known_false1);
197 bv_null_target.bit_sub(bv_known_false2);
198}
199
200
201
202/**
203 @brief Kleene AND(vect1, vect2) (vect1 &= vect2)
204 0 AND Unk = 0 (known)
205 @param bv_value1 - [in, out] values bit-vector
206 @param bv_null1 - [in, out] not NULL (known) bit-vector
207 @param bv_value2 - [in] values bit-vector
208 @param bv_null2 - [in] not NULL (known) bit-vector
209
210 @ingroup bm3VL
211 */
212template<class BV>
213void and_kleene(BV& bv_value1, BV& bv_null1,
214 const BV& bv_value2, const BV& bv_null2)
215{
216 BV bv_ambig_null1; // unknowns on just one of the two args
217 bv_ambig_null1.bit_xor(bv_null1, bv_null2, BV::opt_none);
218
219 BV bv_ambig_null2(bv_ambig_null1); // just a copy
220
221 bv_ambig_null1.bit_and(bv_value1); // "unknowns 1"
222 bv_ambig_null2.bit_and(bv_value2); // "unknowns 2"
223
224 bv_value1.bit_and(bv_value2);
225
226 bv_null1.bit_or(bv_null2); // merge all null2 knowns
227 // minus all single-end TRUE unk
228 bv_null1.bit_sub(bv_ambig_null1);
229 bv_null1.bit_sub(bv_ambig_null2);
230}
231
232/**
233 @brief 3-way Kleene target:=AND(vect1, vect2) (target:= vect1 & vect2)
234 0 AND Unk = 0 (known)
235 @param bv_value_target - [out] values bit-vector
236 @param bv_null_target - [out] not NULL (known) bit-vector
237 @param bv_value1 - [in] values bit-vector
238 @param bv_null1 - [in] not NULL (known) bit-vector
239 @param bv_value2 - [in] values bit-vector
240 @param bv_null2 - [in] not NULL (known) bit-vector
241
242 @ingroup bm3VL
243 */
244template<class BV>
245void and_kleene(BV& bv_value_target, BV& bv_null_target,
246 const BV& bv_value1, const BV& bv_null1,
247 const BV& bv_value2, const BV& bv_null2)
248{
249 BV bv_ambig_null1; // unknowns on just one of the two args
250 bv_ambig_null1.bit_xor(bv_null1, bv_null2, BV::opt_none);
251
252 BV bv_ambig_null2(bv_ambig_null1); // just a copy
253
254 bv_ambig_null1.bit_and(bv_value1); // "unknowns 1"
255 bv_ambig_null2.bit_and(bv_value2); // "unknowns 2"
256
257 bv_value_target.bit_and(bv_value1, bv_value2, BV::opt_none);
258 bv_null_target.bit_or(bv_null1, bv_null2, BV::opt_none);
259
260 bv_null_target.bit_sub(bv_ambig_null1);
261 bv_null_target.bit_sub(bv_ambig_null2);
262}
263
264
265/**
266 Reference function for Kleene logic AND (for verification and testing)
267 @ingroup bm3VL
268 @internal
269 */
270inline
272{
273 switch (a)
274 {
275 case -1:
276 return -1; // always false
277 case 0:
278 switch (b)
279 {
280 case -1: return -1;
281 case 0: return 0;
282 case 1: return 0;
283 default:
284 BM_ASSERT(0);
285 }
286 break;
287 case 1:
288 switch (b)
289 {
290 case -1: return -1;
291 case 0: return 0;
292 case 1: return 1;
293 default:
294 BM_ASSERT(0);
295 }
296 break;
297 default:
298 BM_ASSERT(0);
299 }
300 BM_ASSERT(0);
301 return 0;
302}
303
304
305/**
306 Reference function for Kleene logic OR (for verification and testing)
307 @ingroup bm3VL
308 @internal
309 */
310inline
312{
313 switch (a)
314 {
315 case -1:
316 switch (b)
317 {
318 case -1: return -1;
319 case 0: return 0;
320 case 1: return 1;
321 default:
322 BM_ASSERT(0);
323 }
324 break;
325 case 0:
326 switch (b)
327 {
328 case -1: return 0;
329 case 0: return 0;
330 case 1: return 1;
331 default:
332 BM_ASSERT(0);
333 }
334 break;
335 case 1:
336 return 1;
337 default:
338 BM_ASSERT(0);
339 }
340 BM_ASSERT(0);
341 return 0;
342}
343
344
345} // namespace bm
346
347#endif
Compressed bit-vector bvector<> container, set algebraic methods, traversal iterators.
#define BMNOEXCEPT
Definition: bmdef.h:82
#define BM_ASSERT
Definition: bmdef.h:139
void invert_kleene(BV &bv_value, const BV &bv_null)
Kleene NEG operation.
Definition: bm3vl.h:135
int or_values_kleene(int a, int b) BMNOEXCEPT
Reference function for Kleene logic OR (for verification and testing)
Definition: bm3vl.h:311
void init_kleene(BV &bv_value, const BV &bv_null)
Initialized the value bit-vector so that it always returns 0 (false) for the unknown.
Definition: bm3vl.h:54
void and_kleene(BV &bv_value1, BV &bv_null1, const BV &bv_value2, const BV &bv_null2)
Kleene AND(vect1, vect2) (vect1 &= vect2) 0 AND Unk = 0 (known)
Definition: bm3vl.h:213
void set_value_kleene(BV &bv_value, BV &bv_null, typename BV::size_type idx, int val)
Set Kleene logic value based on value and known vectors.
Definition: bm3vl.h:96
int and_values_kleene(int a, int b) BMNOEXCEPT
Reference function for Kleene logic AND (for verification and testing)
Definition: bm3vl.h:271
int get_value_kleene(const BV &bv_value, const BV &bv_null, typename BV::size_type idx) BMNOEXCEPT
Return Kleene logic value based on value and known vectors.
Definition: bm3vl.h:70
void or_kleene(BV &bv_value1, BV &bv_null1, const BV &bv_value2, const BV &bv_null2)
Kleene OR(vect1, vect2) (vect1 |= vect2) 1 OR Unk = 1 (known)
Definition: bm3vl.h:151
Definition: bm.h:78