smt_tuple.h File Reference

#include <solvers/smt/smt_ast.h>
#include <solvers/smt/tuple/smt_tuple_sort.h>

Include dependency graph for smt_tuple.h:

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

Go to the source code of this file.

Classes
class	tuple_iface

Functions
void	check_tuple_field (unsigned int idx, std::size_t size, const type2tc &tuple_type)
	Reject a tuple field index that the AST cannot hold.

Function Documentation

check_tuple_field()

void check_tuple_field	(	unsigned int	idx,
		std::size_t	size,
		const type2tc &	tuple_type )

Reject a tuple field index that the AST cannot hold.

smt_solver_baset::convert_member and the with_id case of convert_ast take the index from the expression's struct type, while the AST being indexed carries the sort it was built from. Where a frontend leaves the two disagreeing, an unchecked index runs off the end of the flattener's vector – a read in project(), a write in update() – and the process dies far from the cause. Both flatteners route every index through here so the failure names the tuple, the field and the two sizes instead.

Parameters

idx	Field index, as computed from the expression's type.
size	Number of fields the AST actually holds.
tuple_type	The sort's struct/union/complex type, for the message.