hal::SMT::SymbolicState Class Reference

#include <hal_core/netlist/boolean_function/symbolic_state.h>

Collaboration diagram for hal::SMT::SymbolicState:

Public Member Functions
	SymbolicState (const std::vector< BooleanFunction > &variables={})
const BooleanFunction &	get (const BooleanFunction &key) const
void	set (const BooleanFunction &key, const BooleanFunction &value)
std::unordered_map< std::string, const BooleanFunction * >	get_bindings () const

Detailed Description

Represents the data structure that keeps track of symbolic variable values (e.g., required for symbolic simplification).

Definition at line 41 of file symbolic_state.h.

Constructor & Destructor Documentation

SymbolicState()

hal::SMT::SymbolicState::SymbolicState ( const std::vector< BooleanFunction > &  variables = {} )

explicit

Constructs a symbolic state and initializes the variables.

Parameters

[in]

variables

- The list of variables.

Definition at line 7 of file symbolic_state.cpp.

Member Function Documentation

get()

const BooleanFunction & hal::SMT::SymbolicState::get

(

const BooleanFunction &

key

)

const

Looks up a Boolean function in the symbolic state.

Parameters

[in]

key

- The Boolean function to look up.

Returns

The Boolean function from the symbolic state or the key itself if it is not contained in the symbolic state.

Definition at line 18 of file symbolic_state.cpp.

Referenced by hal::smt_init().

get_bindings()

std::unordered_map< std::string, const BooleanFunction * > hal::SMT::SymbolicState::get_bindings

(

)

const

Collects the variables bound within the symbolic state, indexed by their name.

Looking a variable up through get() builds a Boolean function to use as the key and compares it against the keys of the state node by node. Callers that resolve many variables of the same state, such as the evaluation of a Boolean function, are better served by this index.

Returns

A map from variable name to the Boolean function bound to it.

Definition at line 24 of file symbolic_state.cpp.

set()

void hal::SMT::SymbolicState::set	(	const BooleanFunction &	key,
		const BooleanFunction &	value
	)

Sets a Boolean function equivalent in the symbolic state.

Parameters

[in]	key	- The Boolean function.
[in]	value	- The equivalent Boolean function.

Definition at line 38 of file symbolic_state.cpp.

References hal::BooleanFunction::is_variable().

Referenced by hal::smt_init().

---

The documentation for this class was generated from the following files:

• include/hal_core/netlist/boolean_function/symbolic_state.h
• src/netlist/boolean_function/symbolic_state.cpp