smt_solver.cpp File Reference

#include "irep2/irep2_expr.h"
#include <cfloat>
#include <iomanip>
#include <solvers/prop/literal.h>
#include <solvers/smt/smt_solver.h>
#include <solvers/smt/fp/ir_ieee_conv.h>
#include <solvers/smt/smt_fp_rounding_utils.h>
#include <sstream>
#include <util/arith/arith_tools.h>
#include <util/expr/base_type.h>
#include <util/lang/c_types.h>
#include <util/expr/expr_util.h>
#include <util/message/message.h>
#include <util/message/format.h>
#include <util/expr/type_byte_size.h>
#include <cmath>
#include <limits>

Include dependency graph for smt_solver.cpp:

Functions
static std::string	extract_magnitude (const std::string &v, unsigned width)
static std::string	extract_fraction (const std::string &v, unsigned width)
static std::string	double2string (double d)
static std::string	itos (int64_t i)
static void	replace_name_in_body (const expr2tc &lhs, const expr2tc &replacement, expr2tc &body)
	Replace all occurrences of the named symbol lhs with replacement throughout body (in-place).
static void	expand_quantifier_defs_in (expr2tc &e, const std::unordered_map< irep_idt, expr2tc, irep_id_hash > &defs)
	Recursively expand any symbol in e that is a key in defs, replacing it with (a clone of) its associated forall/exists expression.
static expr2tc	shift_count (const expr2tc &value, const expr2tc &count)
static bool	walks_operands (const expr2tc &expr)
static smt_astt	with_dividend_sign (smt_solver_baset &s, smt_astt a, smt_astt of_abs_a)
	SMT-LIB integer div/mod are Euclidean (0 <= mod < |b|); C11 6.5.5p6 truncates toward zero.
static smt_astt	abs_int (smt_solver_baset &s, smt_astt a)
static std::string	fixed_point (const std::string &v, unsigned width)
static expr2tc	nest_row_major (const type2tc &type, const std::vector< expr2tc > &elems, std::size_t &next)
template<typename Object, typename Method>
static smt_astt	make_n_ary (const Object o, const Method m, const smt_solver_baset::ast_vec &v)
	Make an n-ary function application.
static unsigned long	size_to_bit_width (unsigned long sz)
	Convert the size of an array to its bit width.
unsigned long	array_domain_width_or_word_size (const array_type2t &arr)
	Return the SMT domain bit-width for an array type.
type2tc	make_array_domain_type (const array_type2t &arr)
	Given an array type, create a type2tc representing its domain.
static expr2tc	gen_additions (const type2tc &type, std::vector< expr2tc > &exprs)
static BigInt	padded_extent (const BigInt &n)
static expr2tc	size_constant (const BigInt &v)
static expr2tc	row_stride (const type2tc &row)
static const expr2tc &	with_chain_base (const expr2tc &e)
static const expr2tc &	select_chain_root (const expr2tc &e)
static bool	is_flattened_row (const expr2tc &e)
static expr2tc	push_row_read (const type2tc &t, const expr2tc &row, const expr2tc &i)
static expr2tc	lower_flattened_row_select (const index2t &index)
static expr2tc	materialize_flattened_row (const expr2tc &row)
static bool	selects_flattened_dimension (const index2t &index)
static expr2tc	constant_index_into_array (const expr2tc &array, uint64_t idx)

Function Documentation

abs_int()

smt_astt abs_int ( smt_solver_baset & s, smt_astt a )

static

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.

constant_index_into_array()

expr2tc constant_index_into_array ( const expr2tc & array, uint64_t idx )

static

double2string()

std::string double2string ( double d )

static

expand_quantifier_defs_in()

void expand_quantifier_defs_in ( expr2tc & e, const std::unordered_map< irep_idt, expr2tc, irep_id_hash > & defs )

static

Recursively expand any symbol in e that is a key in defs, replacing it with (a clone of) its associated forall/exists expression.

This inlines nested quantifier bodies so that replace_name_in_body can substitute the outer bound variable into their predicates.

extract_fraction()

std::string extract_fraction ( const std::string & v, unsigned width )

static

extract_magnitude()

std::string extract_magnitude ( const std::string & v, unsigned width )

static

fixed_point()

std::string fixed_point ( const std::string & v, unsigned width )

static

gen_additions()

expr2tc gen_additions ( const type2tc & type, std::vector< expr2tc > & exprs )

static

is_flattened_row()

bool is_flattened_row ( const expr2tc & e )

static

itos()

std::string itos ( int64_t i )

static

lower_flattened_row_select()

expr2tc lower_flattened_row_select ( const index2t & index )

static

make_array_domain_type()

type2tc make_array_domain_type

(

const array_type2t &

arr

)

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

make_n_ary()

template<typename Object, typename Method>

smt_astt make_n_ary ( const Object o, const Method m, const smt_solver_baset::ast_vec & v )

static

Make an n-ary function application.

Takes a vector of smt_ast's, and creates a single function app over all the smt_ast's.

materialize_flattened_row()

expr2tc materialize_flattened_row ( const expr2tc & row )

static

nest_row_major()

expr2tc nest_row_major ( const type2tc & type, const std::vector< expr2tc > & elems, std::size_t & next )

static

padded_extent()

BigInt padded_extent ( const BigInt & n )

static

push_row_read()

expr2tc push_row_read ( const type2tc & t, const expr2tc & row, const expr2tc & i )

static

replace_name_in_body()

void replace_name_in_body ( const expr2tc & lhs, const expr2tc & replacement, expr2tc & body )

static

Replace all occurrences of the named symbol lhs with replacement throughout body (in-place).

row_stride()

expr2tc row_stride ( const type2tc & row )

static

select_chain_root()

const expr2tc & select_chain_root ( const expr2tc & e )

static

selects_flattened_dimension()

bool selects_flattened_dimension ( const index2t & index )

static

shift_count()

expr2tc shift_count ( const expr2tc & value, const expr2tc & count )

static

size_constant()

expr2tc size_constant ( const BigInt & v )

static

size_to_bit_width()

unsigned long size_to_bit_width ( unsigned long sz )

static

Convert the size of an array to its bit width.

Essential log2 with some rounding.

walks_operands()

bool walks_operands ( const expr2tc & expr )

static

with_chain_base()

const expr2tc & with_chain_base ( const expr2tc & e )

static

with_dividend_sign()

smt_astt with_dividend_sign ( smt_solver_baset & s, smt_astt a, smt_astt of_abs_a )

static

SMT-LIB integer div/mod are Euclidean (0 <= mod < |b|); C11 6.5.5p6 truncates toward zero.

The two agree on a non-negative dividend whatever b's sign, so apply them to |a| and give the result a's sign: one div or mod per operation, as before (#8662). Unsigned operations stay Euclidean: integer-mode byte extraction (smt_byteops.cpp) relies on that.