smt_tuple_node.cpp File Reference

#include <solvers/smt/smt_solver.h>
#include <solvers/smt/tuple/smt_tuple.h>
#include <solvers/smt/tuple/smt_tuple_node_ast.h>
#include <solvers/smt/tuple/smt_tuple_node.h>
#include <sstream>
#include <util/expr/base_type.h>
#include <util/lang/c_types.h>

Include dependency graph for smt_tuple_node.cpp:

Functions
static bool	read_through_member_arrays (smt_tuple_node_flattener &flat, smt_solver_baset *ctx, array_convt &array_conv, smt_astt array, smt_astt *vals, unsigned int sz, smt_sortt subtype)
	Reads an unbounded constant array of structs whose members are all bit-vectors through one native solver array per member, each a chain of stores over that member's values, so a read is one select per member.

Function Documentation

read_through_member_arrays()

bool read_through_member_arrays ( smt_tuple_node_flattener & flat, smt_solver_baset * ctx, array_convt & array_conv, smt_astt array, smt_astt * vals, unsigned int sz, smt_sortt subtype )

static

Reads an unbounded constant array of structs whose members are all bit-vectors through one native solver array per member, each a chain of stores over that member's values, so a read is one select per member.

Returns false, and does nothing, when the solver has no native arrays or a member is not a bit-vector.