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

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

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 188 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 276 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 103 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 17 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 267 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 55 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 47 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 63 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 87 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 204 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 71 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 249 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 79 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 258 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 222 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 170 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 180 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 151 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 161 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 240 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 196 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 213 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 132 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 142 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 113 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 123 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 231 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 95 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