#include "std_expr.h"
#include "arith_tools.h"
#include "config.h"
#include "expr_util.h"
#include "fixedbv.h"
#include "ieee_float.h"
#include "mathematical_types.h"
#include "namespace.h"
#include "pointer_expr.h"
#include "range.h"
#include "rational.h"
#include "rational_tools.h"
#include "substitute_symbols.h"
#include <map>

Include dependency graph for std_expr.cpp:

Functions
bool	operator== (const exprt &lhs, bool rhs)
	Return whether the expression `lhs` is a constant of Boolean type that is representing the Boolean value `rhs`.

bool	operator!= (const exprt &lhs, bool rhs)
	Return whether the expression `lhs` is not a constant of Boolean type or is not representing the Boolean value `rhs`.

bool	operator== (const exprt &lhs, int rhs)
	Return whether the expression `lhs` is a constant representing the numeric value `rhs`; only values 0 and 1 are supported for `rhs`.

bool	operator!= (const exprt &lhs, int rhs)
	Returns the negation of operator==(const exprt &, int).

bool	operator== (const exprt &lhs, std::nullptr_t rhs)
	Return whether the expression `lhs` is a constant representing the NULL pointer.

bool	operator!= (const exprt &lhs, std::nullptr_t rhs)
	Returns the negation of operator==(const exprt &, std::nullptr_t).

exprt	disjunction (const exprt::operandst &op)
	1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) returns false otherwise

exprt	conjunction (exprt a, exprt b)
	Conjunction of two expressions.

exprt	conjunction (const exprt::operandst &op)
	1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) returns true otherwise

template<typename T >
auto	component (T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())

Function Documentation

◆ component()

template<typename T >

auto component	(	T &	struct_expr,
		const irep_idt &	name,
		const namespacet &	ns
	)		-> decltype(struct_expr.op0())

Definition at line 291 of file std_expr.cpp.

◆ conjunction() [1/2]

exprt conjunction ( const exprt::operandst & op )

1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) returns true otherwise

Definition at line 275 of file std_expr.cpp.

◆ conjunction() [2/2]

exprt conjunction	(	exprt	a,
		exprt	b
	)

Conjunction of two expressions.

If the second is already an and_exprt add to its operands instead of creating a new expression. If one is true, return the other expression. If one is false returns false.

Definition at line 252 of file std_expr.cpp.

◆ disjunction()

exprt disjunction ( const exprt::operandst & op )

1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) returns false otherwise

Definition at line 240 of file std_expr.cpp.

◆ operator!=() [1/3]

bool operator!=	(	const exprt &	lhs,
		bool	rhs
	)

Return whether the expression lhs is not a constant of Boolean type or is not representing the Boolean value rhs.

Definition at line 37 of file std_expr.cpp.

◆ operator!=() [2/3]

bool operator!=	(	const exprt &	lhs,
		int	rhs
	)

Returns the negation of operator==(const exprt &, int).

Definition at line 60 of file std_expr.cpp.

◆ operator!=() [3/3]

bool operator!=	(	const exprt &	lhs,
		std::nullptr_t	rhs
	)

Returns the negation of operator==(const exprt &, std::nullptr_t).

Definition at line 192 of file std_expr.cpp.

◆ operator==() [1/3]

bool operator==	(	const exprt &	lhs,
		bool	rhs
	)

Return whether the expression lhs is a constant of Boolean type that is representing the Boolean value rhs.

Definition at line 32 of file std_expr.cpp.

◆ operator==() [2/3]

bool operator==	(	const exprt &	lhs,
		int	rhs
	)

Return whether the expression lhs is a constant representing the numeric value rhs; only values 0 and 1 are supported for rhs.

For value 0 we consider the following types: ID_integer, ID_natural, ID_rational, ID_unsignedbv, ID_signedbv, ID_c_bool, ID_c_bit_field, ID_fixedbv, ID_floatbv, ID_pointer.
For ID_pointer, returns true iff the value is a zero string or a null pointer.
For value 1 we consider the following types: ID_integer, ID_natural, ID_rational, ID_unsignedbv, ID_signedbv, ID_c_bool, ID_c_bit_field, ID_fixedbv, ID_floatbv.
For all other types, return false.

Definition at line 52 of file std_expr.cpp.

◆ operator==() [3/3]

bool operator==	(	const exprt &	lhs,
		std::nullptr_t	rhs
	)

Return whether the expression lhs is a constant representing the NULL pointer.

Definition at line 186 of file std_expr.cpp.

Functions