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. More...

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) More...

static void	Set3VL_ValueDemo2 ()
	Faster way to initialize Kleene bit-vectors via bulk_insert_iterator. More...

static void	GenerateDemoVector (bm::bvector<> &bv_v, bm::bvector<> &bv_null)
	Generate Kleene vector (as two bit-vectors) More...

static void	Set3VL_InvertDemo ()
	Demo for 3-value logic (Kleene) NOT. More...

static void	Set3VL_AndDemo ()
	Demo for 3-value logic (Kleene) AND. More...

static void	Set3VL_ORDemo ()
	Demo for 3-value logic (Kleene) OR. More...

int	main (void)
	More...

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()

static 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 )

Examples: bv3vlogic.cpp.

Definition at line 284 of file bv3vlogic.cpp.

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

◆ PrintKleeneVector()

static 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()

static 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()

static 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()

static 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()

static 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.