HAL
Public Member Functions | List of all members
hal::SMT::SymbolicState Class Referencefinal

#include <symbolic_state.h>

Collaboration diagram for hal::SMT::SymbolicState:
Collaboration graph

Public Member Functions

 SymbolicState (const std::vector< BooleanFunction > &variables={})
 
const BooleanFunction & get (const BooleanFunction &key) const
 
void set (const BooleanFunction &key, const BooleanFunction &value)
 

Detailed Description

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

Definition at line 40 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().

◆ 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 24 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: