hal::SMT::SymbolicExecution Class Reference

#include <symbolic_execution.h>

Collaboration diagram for hal::SMT::SymbolicExecution:

Public Member Functions
	SymbolicExecution (const std::vector< BooleanFunction > &variables={})
Result< BooleanFunction >	evaluate (const BooleanFunction &function) const
Result< std::monostate >	evaluate (const Constraint &constraint)

Public Attributes
SymbolicState	state
	The current symbolic state. More...

Detailed Description

Represents the symbolic execution engine that handles the evaluation and simplification of Boolean function abstract syntax trees.

Definition at line 42 of file symbolic_execution.h.

Constructor & Destructor Documentation

SymbolicExecution()

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

explicit

Creates a symbolic execution engine and initializes the variables.

Parameters

[in]

variables

- The (optional) list of variables.

Definition at line 414 of file symbolic_execution.cpp.

References hal::state.

Member Function Documentation

evaluate() [1/2]

Result< BooleanFunction > hal::SMT::SymbolicExecution::evaluate

(

const BooleanFunction &

function

)

const

Evaluates a Boolean function within the symbolic state of the symbolic execution.

Parameters

[in]

function

- The Boolean function to evaluate.

Returns

Ok() and the evaluated Boolean function on success, Err() otherwise.

Definition at line 418 of file symbolic_execution.cpp.

References ERR, ERR_APPEND, and OK.

Referenced by evaluate(), hal::Simplification::local_simplification(), and hal::smt_init().

evaluate() [2/2]

Result< std::monostate > hal::SMT::SymbolicExecution::evaluate

(

const Constraint &

constraint

)

Evaluates an equality constraint and applies it to the symbolic state of the symbolic execution.

Parameters

[in]

constraint

- The equality constraint to evaluate.

Returns

Ok() on success, Err() otherwise.

Definition at line 446 of file symbolic_execution.cpp.

References ERR_APPEND, evaluate(), hal::SMT::Constraint::get_assignment(), hal::SMT::Constraint::is_assignment(), and OK.

Member Data Documentation

state

SymbolicState hal::SMT::SymbolicExecution::state

The current symbolic state.

Definition at line 50 of file symbolic_execution.h.

Referenced by hal::smt_init().

---

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

• /home/runner/work/hal/hal/include/hal_core/netlist/boolean_function/symbolic_execution.h
• /home/runner/work/hal/hal/src/netlist/boolean_function/symbolic_execution.cpp