#include <smt_bit_vector_theory.h>

Collaboration diagram for smt_bit_vector_theoryt:

Classes
struct	addt

struct	andt

struct	arithmetic_shift_rightt

struct	comparet

struct	concatt

struct	extractt

struct	logical_shift_rightt

struct	multiplyt

struct	nandt

struct	negatet

struct	nort

struct	nott

struct	ort

struct	repeatt

struct	rotate_leftt

struct	rotate_rightt

struct	shift_leftt

struct	sign_extendt

struct	signed_dividet

struct	signed_greater_than_or_equalt

struct	signed_greater_thant

struct	signed_less_than_or_equalt

struct	signed_less_thant

struct	signed_remaindert

struct	subtractt

struct	unsigned_dividet

struct	unsigned_greater_than_or_equalt

struct	unsigned_greater_thant

struct	unsigned_less_than_or_equalt

struct	unsigned_less_thant

struct	unsigned_remaindert

struct	xnort

struct	xort

struct	zero_extendt

Static Public Member Functions
static smt_function_application_termt::factoryt< extractt >	extract (std::size_t i, std::size_t j)
	Makes a factory for extract function applications.

static smt_function_application_termt::factoryt< repeatt >	repeat (std::size_t i)

static smt_function_application_termt::factoryt< zero_extendt >	zero_extend (std::size_t i)

static smt_function_application_termt::factoryt< sign_extendt >	sign_extend (std::size_t i)

static smt_function_application_termt::factoryt< rotate_leftt >	rotate_left (std::size_t i)

static smt_function_application_termt::factoryt< rotate_rightt >	rotate_right (std::size_t i)

Static Public Attributes
static const smt_function_application_termt::factoryt< concatt >	concat {}

static const smt_function_application_termt::factoryt< nott >	make_not {}

static const smt_function_application_termt::factoryt< andt >	make_and {}

static const smt_function_application_termt::factoryt< ort >	make_or {}

static const smt_function_application_termt::factoryt< nandt >	nand {}

static const smt_function_application_termt::factoryt< nort >	nor {}

static const smt_function_application_termt::factoryt< xort >	make_xor {}

static const smt_function_application_termt::factoryt< xnort >	xnor {}

static const smt_function_application_termt::factoryt< comparet >	compare {}

static const smt_function_application_termt::factoryt< unsigned_less_thant >	unsigned_less_than {}

static const smt_function_application_termt::factoryt< unsigned_less_than_or_equalt >	unsigned_less_than_or_equal {}

static const smt_function_application_termt::factoryt< unsigned_greater_thant >	unsigned_greater_than {}

static const smt_function_application_termt::factoryt< unsigned_greater_than_or_equalt >	unsigned_greater_than_or_equal {}

static const smt_function_application_termt::factoryt< signed_less_thant >	signed_less_than {}

static const smt_function_application_termt::factoryt< signed_less_than_or_equalt >	signed_less_than_or_equal {}

static const smt_function_application_termt::factoryt< signed_greater_thant >	signed_greater_than {}

static const smt_function_application_termt::factoryt< signed_greater_than_or_equalt >	signed_greater_than_or_equal {}

static const smt_function_application_termt::factoryt< addt >	add {}

static const smt_function_application_termt::factoryt< subtractt >	subtract {}

static const smt_function_application_termt::factoryt< multiplyt >	multiply {}

static const smt_function_application_termt::factoryt< unsigned_dividet >	unsigned_divide {}

static const smt_function_application_termt::factoryt< signed_dividet >	signed_divide {}

static const smt_function_application_termt::factoryt< unsigned_remaindert >	unsigned_remainder {}

static const smt_function_application_termt::factoryt< signed_remaindert >	signed_remainder {}

static const smt_function_application_termt::factoryt< negatet >	negate {}
	Arithmetic negation in two's complement.

static const smt_function_application_termt::factoryt< shift_leftt >	shift_left {}

static const smt_function_application_termt::factoryt< logical_shift_rightt >	logical_shift_right {}

static const smt_function_application_termt::factoryt< arithmetic_shift_rightt >	arithmetic_shift_right {}

Detailed Description

Definition at line 8 of file smt_bit_vector_theory.h.

Member Function Documentation

◆ extract()

smt_function_application_termt::factoryt< smt_bit_vector_theoryt::extractt > smt_bit_vector_theoryt::extract	(	std::size_t	i,
		std::size_t	j
	)

static

Makes a factory for extract function applications.

Parameters

i	Index of the highest bit to be included in the resulting bit vector.
j	Index of the lowest bit to be included in the resulting bit vector.

Note: Bit vectors are zero indexed. So the lowest bit index is zero and the largest index is the size of the bit vector minus one.

Definition at line 79 of file smt_bit_vector_theory.cpp.

◆ repeat()

smt_function_application_termt::factoryt< smt_bit_vector_theoryt::repeatt > smt_bit_vector_theoryt::repeat ( std::size_t i )

static

Definition at line 729 of file smt_bit_vector_theory.cpp.

◆ rotate_left()

smt_function_application_termt::factoryt< smt_bit_vector_theoryt::rotate_leftt > smt_bit_vector_theoryt::rotate_left ( std::size_t i )

static

Definition at line 815 of file smt_bit_vector_theory.cpp.

◆ rotate_right()

smt_function_application_termt::factoryt< smt_bit_vector_theoryt::rotate_rightt > smt_bit_vector_theoryt::rotate_right ( std::size_t i )

static

Definition at line 842 of file smt_bit_vector_theory.cpp.

◆ sign_extend()

smt_function_application_termt::factoryt< smt_bit_vector_theoryt::sign_extendt > smt_bit_vector_theoryt::sign_extend ( std::size_t i )

static

Definition at line 788 of file smt_bit_vector_theory.cpp.

◆ zero_extend()

smt_function_application_termt::factoryt< smt_bit_vector_theoryt::zero_extendt > smt_bit_vector_theoryt::zero_extend ( std::size_t i )

static

Definition at line 759 of file smt_bit_vector_theory.cpp.

Member Data Documentation

◆ add

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::addt > smt_bit_vector_theoryt::add {}

static

Definition at line 477 of file smt_bit_vector_theory.h.

◆ arithmetic_shift_right

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::arithmetic_shift_rightt > smt_bit_vector_theoryt::arithmetic_shift_right {}

static

Definition at line 702 of file smt_bit_vector_theory.h.

◆ compare

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::comparet > smt_bit_vector_theoryt::compare {}

static

Definition at line 268 of file smt_bit_vector_theory.h.

◆ concat

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::concatt > smt_bit_vector_theoryt::concat {}

static

Definition at line 52 of file smt_bit_vector_theory.h.

◆ logical_shift_right

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::logical_shift_rightt > smt_bit_vector_theoryt::logical_shift_right {}

static

Definition at line 679 of file smt_bit_vector_theory.h.

◆ make_and

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::andt > smt_bit_vector_theoryt::make_and {}

static

Definition at line 136 of file smt_bit_vector_theory.h.

◆ make_not

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::nott > smt_bit_vector_theoryt::make_not {}

static

Definition at line 114 of file smt_bit_vector_theory.h.

◆ make_or

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::ort > smt_bit_vector_theoryt::make_or {}

static

Definition at line 158 of file smt_bit_vector_theory.h.

◆ make_xor

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::xort > smt_bit_vector_theoryt::make_xor {}

static

Definition at line 224 of file smt_bit_vector_theory.h.

◆ multiply

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::multiplyt > smt_bit_vector_theoryt::multiply {}

static

Definition at line 523 of file smt_bit_vector_theory.h.

◆ nand

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::nandt > smt_bit_vector_theoryt::nand {}

static

Definition at line 180 of file smt_bit_vector_theory.h.

◆ negate

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::negatet > smt_bit_vector_theoryt::negate {}

static

Arithmetic negation in two's complement.

Definition at line 633 of file smt_bit_vector_theory.h.

◆ nor

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::nort > smt_bit_vector_theoryt::nor {}

static

Definition at line 202 of file smt_bit_vector_theory.h.

◆ shift_left

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::shift_leftt > smt_bit_vector_theoryt::shift_left {}

static

Definition at line 656 of file smt_bit_vector_theory.h.

◆ signed_divide

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::signed_dividet > smt_bit_vector_theoryt::signed_divide {}

static

Definition at line 569 of file smt_bit_vector_theory.h.

◆ signed_greater_than

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::signed_greater_thant > smt_bit_vector_theoryt::signed_greater_than {}

static

Definition at line 432 of file smt_bit_vector_theory.h.

◆ signed_greater_than_or_equal

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::signed_greater_than_or_equalt > smt_bit_vector_theoryt::signed_greater_than_or_equal {}

static

Definition at line 455 of file smt_bit_vector_theory.h.

◆ signed_less_than

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::signed_less_thant > smt_bit_vector_theoryt::signed_less_than {}

static

Definition at line 386 of file smt_bit_vector_theory.h.

◆ signed_less_than_or_equal

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::signed_less_than_or_equalt > smt_bit_vector_theoryt::signed_less_than_or_equal {}

static

Definition at line 409 of file smt_bit_vector_theory.h.

◆ signed_remainder

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::signed_remaindert > smt_bit_vector_theoryt::signed_remainder {}

static

Definition at line 615 of file smt_bit_vector_theory.h.

◆ subtract

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::subtractt > smt_bit_vector_theoryt::subtract {}

static

Definition at line 500 of file smt_bit_vector_theory.h.

◆ unsigned_divide

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::unsigned_dividet > smt_bit_vector_theoryt::unsigned_divide {}

static

Definition at line 546 of file smt_bit_vector_theory.h.

◆ unsigned_greater_than

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::unsigned_greater_thant > smt_bit_vector_theoryt::unsigned_greater_than {}

static

Definition at line 339 of file smt_bit_vector_theory.h.

◆ unsigned_greater_than_or_equal

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::unsigned_greater_than_or_equalt > smt_bit_vector_theoryt::unsigned_greater_than_or_equal {}

static

Definition at line 363 of file smt_bit_vector_theory.h.

◆ unsigned_less_than

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::unsigned_less_thant > smt_bit_vector_theoryt::unsigned_less_than {}

static

Definition at line 293 of file smt_bit_vector_theory.h.

◆ unsigned_less_than_or_equal

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::unsigned_less_than_or_equalt > smt_bit_vector_theoryt::unsigned_less_than_or_equal {}

static

Definition at line 316 of file smt_bit_vector_theory.h.

◆ unsigned_remainder

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::unsigned_remaindert > smt_bit_vector_theoryt::unsigned_remainder {}

static

Definition at line 592 of file smt_bit_vector_theory.h.

◆ xnor

const smt_function_application_termt::factoryt< smt_bit_vector_theoryt::xnort > smt_bit_vector_theoryt::xnor {}

static

Definition at line 246 of file smt_bit_vector_theory.h.

The documentation for this class was generated from the following files:

/home/runner/work/cbmc/cbmc/src/solvers/smt2_incremental/theories/smt_bit_vector_theory.h
/home/runner/work/cbmc/cbmc/src/solvers/smt2_incremental/theories/smt_bit_vector_theory.cpp

Classes

Static Public Member Functions

Static Public Attributes

Detailed Description

Member Function Documentation

◆ extract()

◆ repeat()

◆ rotate_left()

◆ rotate_right()

◆ sign_extend()

◆ zero_extend()

Member Data Documentation

◆ add

◆ arithmetic_shift_right

◆ compare

◆ concat

◆ logical_shift_right

◆ make_and

◆ make_not

◆ make_or

◆ make_xor

◆ multiply

◆ nand

◆ negate

◆ nor

◆ shift_left

◆ signed_divide

◆ signed_greater_than

◆ signed_greater_than_or_equal

◆ signed_less_than

◆ signed_less_than_or_equal

◆ signed_remainder

◆ subtract

◆ unsigned_divide

◆ unsigned_greater_than

◆ unsigned_greater_than_or_equal

◆ unsigned_less_than

◆ unsigned_less_than_or_equal

◆ unsigned_remainder

◆ xnor