hal::Simplification Namespace Reference

Functions
Result< BooleanFunction >	local_simplification (const BooleanFunction &function)
Result< BooleanFunction >	abc_simplification (const BooleanFunction &function)

Detailed Description

Contains the rewrite rules and helpers used to symbolically simplify a Boolean function.

Function Documentation

abc_simplification()

Result< BooleanFunction > hal::Simplification::abc_simplification

(

const BooleanFunction &

function

)

Implements the interface to simplify a Boolean function using ABC.

Parameters

[in]

function

- Boolean function to simplify.

Returns

Simplified boolean function on success, error otherwise.

Definition at line 970 of file simplification_abc.cpp.

References hal::SMT::ConstantPropagation::And(), ERR_APPEND, hal::z3_utils::get_variable_names(), hal::SMT::ConstantPropagation::Not(), OK, hal::SMT::ConstantPropagation::Or(), hal::status, and hal::SMT::ConstantPropagation::Xor().

local_simplification()

Result< BooleanFunction > hal::Simplification::local_simplification

(

const BooleanFunction &

function

)

Implements the interface to apply local algebraic simplification rules.

Parameters

[in]

function

- Boolean function to simplify.

Returns

Simplified boolean function on success, error otherwise.

Definition at line 6 of file simplification_local.cpp.

References ERR_APPEND, hal::SMT::SymbolicExecution::evaluate(), and OK.

Referenced by hal::BooleanFunction::simplify(), and hal::BooleanFunction::simplify_local().