nondet_padding.h File Reference

Expressions for use in incremental SMT2 decision procedure. More...

#include <util/bitvector_types.h>
#include <util/expr.h>
#include <util/invariant.h>

Include dependency graph for nondet_padding.h:

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

Go to the source code of this file.

Classes
class	nondet_padding_exprt
	This expression serves as a placeholder for the bits which have non deterministic value in a larger bit vector. More...

Functions
void	validate_expr (const nondet_padding_exprt &padding)
template<>
bool	can_cast_expr< nondet_padding_exprt > (const exprt &base)

Detailed Description

Expressions for use in incremental SMT2 decision procedure.

Definition in file nondet_padding.h.

Function Documentation

can_cast_expr< nondet_padding_exprt >()

template<>

bool can_cast_expr< nondet_padding_exprt > ( const exprt &  base )

inline

Definition at line 33 of file nondet_padding.h.

validate_expr()

void validate_expr ( const nondet_padding_exprt &  padding )

inline

Definition at line 38 of file nondet_padding.h.