simplification.cpp File Reference

#include "z3_utils/simplification.h"
#include "hal_core/netlist/boolean_function.h"
#include "hal_core/utilities/log.h"
#include "z3_utils/z3_utils.h"
#include <deque>

Include dependency graph for simplification.cpp:

Go to the source code of this file.

Namespaces
	hal
	hal::BV_ConstantPropagation
	hal::z3_utils

Functions
BooleanFunction	hal::BV_ConstantPropagation::And (const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
BooleanFunction	hal::BV_ConstantPropagation::Or (const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
BooleanFunction	hal::BV_ConstantPropagation::Not (const std::vector< BooleanFunction::Value > &p)
BooleanFunction	hal::BV_ConstantPropagation::Xor (const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
BooleanFunction	hal::BV_ConstantPropagation::Add (const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
BooleanFunction	hal::BV_ConstantPropagation::Sub (const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
BooleanFunction	hal::BV_ConstantPropagation::Mul (const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
BooleanFunction	hal::BV_ConstantPropagation::Sle (const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
BooleanFunction	hal::BV_ConstantPropagation::Slt (const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
BooleanFunction	hal::BV_ConstantPropagation::Ule (const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
BooleanFunction	hal::BV_ConstantPropagation::Ult (const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1)
BooleanFunction	hal::BV_ConstantPropagation::Ite (const std::vector< BooleanFunction::Value > &p0, const std::vector< BooleanFunction::Value > &p1, const std::vector< BooleanFunction::Value > &p2)
Result< BooleanFunction >	hal::BV_ConstantPropagation::constant_propagation (const BooleanFunction::Node &node, std::vector< BooleanFunction > &&p)
Result< z3::expr >	hal::z3_utils::simplify_local (const z3::expr &e, std::unordered_map< u32, z3::expr > &cache, const bool check_correctness=false)
	Applies hand-crafted simplification rules iteratively until no further simplifications can be made. More...
Result< z3::expr >	hal::z3_utils::simplify_local (const z3::expr &e, const bool check_correctness=false)
	Applies hand-crafted simplification rules iteratively until no further simplifications can be made. More...