bv3vlogic.cpp File Reference

Example: Kleene algebra operations. More...

`#include <iostream>`
`#include <vector>`
`#include <cassert>`
`#include "bm.h"`
`#include "bm3vl.h"`
`#include "bmundef.h"`
Include dependency graph for bv3vlogic.cpp:

Go to the source code of this file.

## Functions

static void | PrintKleeneVector (const bm::bvector<> &bv_v, const bm::bvector<> &bv_null)
| Print 3-value vector.
static void | Set3VL_ValueDemo ()
| This demo shows how to use bm::set_value_kleene and bm::get_value_kleene functions to set values into pair of vectors (value vector and knowns vector).
static void | Set3VL_ValueDemo2 ()
| Faster way to initialize Kleene bit-vectors via bulk_insert_iterator.
static void | GenerateDemoVector (bm::bvector<> &bv_v, bm::bvector<> &bv_null)
| Generate Kleene vector (as two bit-vectors).
static void | Set3VL_InvertDemo ()
| Demo for 3-value logic (Kleene) NOT.
static void | Set3VL_AndDemo ()
| Demo for 3-value logic (Kleene) AND.
static void | Set3VL_ORDemo ()
| Demo for 3-value logic (Kleene) OR.
int | main (void)

## Detailed Description

Example: Kleene algebra operations.

BitMagic implements 3-value (Kleene) logic using two separate bit-vectors: bit-vector of values and bit-vector of knowns.

bit-vector of vlaues contains 1s in the positions of true bit-vector of NULLs contains 1s where values in known (or set)

The convention is that unknown elements (0s in the NULL vector) MUST NOT have 1s in the corresponding positions of the value bit-vector so "unknown TRUE" is not a correct situation.

Definition in file bv3vlogic.cpp.

## Function Documentation

## GenerateDemoVector()

void GenerateDemoVector | ( | bm::bvector<> & | bv_v,
|  | bm::bvector<> & | bv_null )

static

Generate Kleene vector (as two bit-vectors).

Examples
  bv3vlogic.cpp.

Definition at line 164 of file bv3vlogic.cpp.

References BM_DECLARE_TEMP_BLOCK, bm::bvector< Alloc >::optimize(), and bm::set_value_kleene().

Referenced by Set3VL_AndDemo(), Set3VL_InvertDemo(), and Set3VL_ORDemo().

## main()

int main | ( | void |  | ) |

Definition at line 284 of file bv3vlogic.cpp.

References Set3VL_AndDemo(), Set3VL_InvertDemo(), Set3VL_ORDemo(), Set3VL_ValueDemo(), and Set3VL_ValueDemo2().

## PrintKleeneVector()

void PrintKleeneVector | ( | const bm::bvector<> & | bv_v,
|  | const bm::bvector<> & | bv_null )

static

Print 3-value vector.

Examples
  bv3vlogic.cpp.

Definition at line 55 of file bv3vlogic.cpp.

References bm::bvector< Alloc >::first(), bm::bvector< Alloc >::test(), and bm::bvector< Alloc >::iterator_base::valid().

Referenced by Set3VL_AndDemo(), Set3VL_InvertDemo(), Set3VL_ORDemo(), Set3VL_ValueDemo(), and Set3VL_ValueDemo2().

## Set3VL_AndDemo()

void Set3VL_AndDemo | ( |  | ) |

static

Demo for 3-value logic (Kleene) AND.

Kleene algebra AND produces known FALSE when known FALSE meets UNKNOWN (false)

Examples
  bv3vlogic.cpp.

Definition at line 209 of file bv3vlogic.cpp.

References bm::and_kleene(), bm::bvector< Alloc >::equal(), GenerateDemoVector(), PrintKleeneVector(), and bm::set_value_kleene().

Referenced by main().

## Set3VL_InvertDemo()

void Set3VL_InvertDemo | ( |  | ) |

static

Demo for 3-value logic (Kleene) NOT.

Examples
  bv3vlogic.cpp.

Definition at line 185 of file bv3vlogic.cpp.

References GenerateDemoVector(), bm::invert_kleene(), and PrintKleeneVector().

Referenced by main().

## Set3VL_ORDemo()

void Set3VL_ORDemo | ( |  | ) |

static

Demo for 3-value logic (Kleene) OR.

Kleene algebra OR produces known TRUE when known TRUE meets UNKNOWN (false)

Examples
  bv3vlogic.cpp.

Definition at line 249 of file bv3vlogic.cpp.

References bm::bvector< Alloc >::equal(), GenerateDemoVector(), bm::or_kleene(), PrintKleeneVector(), and bm::set_value_kleene().

Referenced by main().

## Set3VL_ValueDemo()

void Set3VL_ValueDemo | ( |  | ) |

static

This demo shows how to use bm::set_value_kleene and bm::get_value_kleene functions to set values into pair of vectors (value vector and knowns vector).

Kleene algebra operates on 3 values, which are by convention read as: -1 (known false), 0 (unknown), 1 (known true).

bm::set_value_kleene takes a pair of vectors, position and an int value to set value in a pair of bit-vectors representing value and knowns

Please note that this is the easy but relatively slow method to init the vectors since because it uses random access initialization.

Examples
  bv3vlogic.cpp.

Definition at line 90 of file bv3vlogic.cpp.

References BM_DECLARE_TEMP_BLOCK, bm::get_value_kleene(), bm::bvector< Alloc >::optimize(), PrintKleeneVector(), and bm::set_value_kleene().

Referenced by main().

## Set3VL_ValueDemo2()

void Set3VL_ValueDemo2 | ( |  | ) |

static

Faster way to initialize Kleene bit-vectors via bulk_insert_iterator.

Examples
  bv3vlogic.cpp.

Definition at line 117 of file bv3vlogic.cpp.

References BM_DECLARE_TEMP_BLOCK, bm::bvector< Alloc >::bulk_insert_iterator::flush(), bm::init_kleene(), bm::bvector< Alloc >::inserter(), bm::bvector< Alloc >::optimize(), and PrintKleeneVector().

Referenced by main().