smt_solver.h File Reference

#include <optional>
#include <boost/multi_index/hashed_index.hpp>
#include <boost/multi_index/member.hpp>
#include <boost/multi_index/ordered_index.hpp>
#include <boost/multi_index_container.hpp>
#include <memory>
#include <mutex>
#include <set>
#include <utility>
#include <unordered_map>
#include <unordered_set>
#include <solvers/prop/literal.h>
#include <solvers/prop/pointer_logic.h>
#include <solvers/smt/smt_result.h>
#include <irep2/irep2_utils.h>
#include <util/message/message.h>
#include <util/symtab/namespace.h>
#include <util/base/threeval.h>
#include <solvers/smt/smt_array.h>
#include <solvers/smt/tuple/smt_tuple.h>
#include <solvers/smt/fp/fp_conv.h>

Include dependency graph for smt_solver.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	smt_solver_baset
	The base SMT-conversion class/interface. More...
struct	smt_solver_baset::flat_storet
	One element update an array with denotes, as an index into the array's flattened form and the value stored there. More...
struct	smt_solver_baset::smt_cache_entryt
struct	smt_solver_baset::uf_ackermann_entry
	One recorded uninterpreted-function application in the Ackermannisation fallback: the argument asts, the fresh result ast, and the context level at which it was created (so it can be pruned on the matching pop, since pop_ctx deletes the asts made since the push). More...
struct	smt_solver_baset::ptr_flatten_entry
	One pointer flattened to its machine representation by a bitcast. More...
struct	symtab_entryt

Typedefs
typedef boost::multi_index_container< symtab_entryt, boost::multi_index::indexed_by< boost::multi_index::hashed_unique< BOOST_MULTI_INDEX_MEMBER(symtab_entryt, std::string, val)>, boost::multi_index::ordered_non_unique< BOOST_MULTI_INDEX_MEMBER(symtab_entryt, unsigned int, level), std::greater< unsigned int > > > >	symtabt

Functions
expr2tc	byte_update_bit_offset (const byte_update2t &data)
	The bit a byte update with a symbolic offset writes at, in bit-vector mode: the offset scaled to bits, in the width of the updated value.
bool	lowest_address_high ()
	Whether an object's lowest address sits in the most significant bits of its bit-vector encoding: true on a big-endian target, so the bit-vector reads as the object's bytes in memory order, as byte_extract assumes.
unsigned	flattened_position (unsigned offset, unsigned width, unsigned total)
	Lowest bit of the width bits at bit offset offset of a total bit object's bit-vector encoding.
expr2tc	union_member_bits (const expr2tc &bits, unsigned width)
	The width bits of a union member within the union's bits bits: those at the union's lowest address.
expr2tc	union_bits_with_member (const expr2tc &rest, const expr2tc &member, unsigned bits)
	The bits wide bits of a union whose lowest-addressed bits hold member and whose other bits are those of rest.
expr2tc	union_bits_of_member (const expr2tc &member, unsigned bits)
	A union member's bits member widened to the union's bits, as the bits at the union's lowest address; zero-extension is left to the caller.
type2tc	make_array_domain_type (const array_type2t &arr)
	Given an array type, create a type2tc representing its domain.
unsigned long	array_domain_width_or_word_size (const array_type2t &arr)
	Return the SMT domain bit-width for an array type.

Typedef Documentation

symtabt

typedef boost::multi_index_container< symtab_entryt, boost::multi_index::indexed_by< boost::multi_index::hashed_unique< BOOST_MULTI_INDEX_MEMBER(symtab_entryt, std::string, val)>, boost::multi_index::ordered_non_unique< BOOST_MULTI_INDEX_MEMBER(symtab_entryt, unsigned int, level), std::greater<unsigned int> > > > symtabt

Function Documentation

array_domain_width_or_word_size()

unsigned long array_domain_width_or_word_size

(

const array_type2t &

arr

)

Return the SMT domain bit-width for an array type.

For constant-size arrays this is the minimum bit-width needed to represent every valid index. For VLA, dynamic, or infinite arrays the size is not statically known, so the machine word size is returned as a safe default.

byte_update_bit_offset()

expr2tc byte_update_bit_offset

(

const byte_update2t &

data

)

The bit a byte update with a symbolic offset writes at, in bit-vector mode: the offset scaled to bits, in the width of the updated value.

flattened_position()

unsigned flattened_position	(	unsigned	offset,
		unsigned	width,
		unsigned	total )

Lowest bit of the width bits at bit offset offset of a total bit object's bit-vector encoding.

lowest_address_high()

bool lowest_address_high

(

)

Whether an object's lowest address sits in the most significant bits of its bit-vector encoding: true on a big-endian target, so the bit-vector reads as the object's bytes in memory order, as byte_extract assumes.

make_array_domain_type()

type2tc make_array_domain_type

(

const array_type2t &

arr

)

Given an array type, create a type2tc representing its domain.

union_bits_of_member()

expr2tc union_bits_of_member	(	const expr2tc &	member,
		unsigned	bits )

A union member's bits member widened to the union's bits, as the bits at the union's lowest address; zero-extension is left to the caller.

union_bits_with_member()

expr2tc union_bits_with_member	(	const expr2tc &	rest,
		const expr2tc &	member,
		unsigned	bits )

The bits wide bits of a union whose lowest-addressed bits hold member and whose other bits are those of rest.

union_member_bits()

expr2tc union_member_bits	(	const expr2tc &	bits,
		unsigned	width )

The width bits of a union member within the union's bits bits: those at the union's lowest address.