#include <symbolic_env.h>

Public Member Functions
bool	exists (const IR::StateVariable &var) const
	Checks whether the given variable exists in the symbolic environment.

const IR::Expression *	get (const IR::StateVariable &var) const

const SymbolicMapType &	getInternalMap () const

void	set (const IR::StateVariable &var, const IR::Expression *value)

const IR::Expression *	subst (const IR::Expression *expr) const

Static Public Member Functions
static bool	isSymbolicValue (const IR::Node *)

Detailed Description

A symbolic environment maps variables to their symbolic value. A symbolic value is just an expression on the program's initial state.

Member Function Documentation

◆ get()

const IR::Expression * P4Tools::SymbolicEnv::get ( const IR::StateVariable & var ) const

nodiscard

Returns: the symbolic value for the given variable.

◆ getInternalMap()

const SymbolicMapType & P4Tools::SymbolicEnv::getInternalMap ( ) const

nodiscard

Returns: The immutable map that is internal to this symbolic environment.

◆ isSymbolicValue()

bool P4Tools::SymbolicEnv::isSymbolicValue ( const IR::Node * node )

static

Determines whether the given node represents a symbolic value. Symbolic values may be stored in the symbolic environment.

◆ set()

void P4Tools::SymbolicEnv::set	(	const IR::StateVariable &	var,
		const IR::Expression *	value )

Sets the symbolic value of the given state variable to the given value. Constant folding is done on the given value before updating the symbolic state.

◆ subst()

const IR::Expression * P4Tools::SymbolicEnv::subst ( const IR::Expression * expr ) const

Substitutes state variables in @expr for their symbolic value in this environment. Variables that are unbound by this environment are left untouched.

Traverses the IR to perform substitution.

Public Member Functions