hal::SMT::Translator Namespace Reference

Functions
Result< std::string >	const2str (const std::vector< BooleanFunction::Value > &number)
Result< std::string >	reduce_to_smt2 (const BooleanFunction::Node &node, std::vector< std::string > &&p, size_t index, const BooleanFunction &function)
Result< std::string >	translate_to_smt2 (const BooleanFunction &function)

Function Documentation

const2str()

Result<std::string> hal::SMT::Translator::const2str

(

const std::vector< BooleanFunction::Value > &

number

)

Helper function to translate arbitrary-long constant values into an decimal string for SMT-LIB v2 translation compatibility.

Parameters

[in]

number

- Boolean function constant node values.

Returns

OK() and constant on success, Err() otherwise.

Definition at line 21 of file translator.cpp.

References ERR, and OK.

Referenced by reduce_to_smt2().

reduce_to_smt2()

Result<std::string> hal::SMT::Translator::reduce_to_smt2	(	const BooleanFunction::Node &	node,
		std::vector< std::string > &&	p,
		size_t	index,
		const BooleanFunction &	function
	)

Helper function to reduce a view into the abstract syntax tree of a node and its parameter leaf nodes to an SMT-LIB string.

Parameters

[in]	node	- Boolean function node.
[in]	p	- Boolean function node parameters.
[in]	index	- Index of node in function.
[in]	function	- Boolean function to be translated to SMT-LIB string.

Returns

OK() and SMT-LIB v2 string representation of node and operands on success, Err() otherwise.

Definition at line 53 of file translator.cpp.

References hal::BooleanFunction::NodeType::Add, hal::BooleanFunction::NodeType::And, hal::BooleanFunction::NodeType::Ashr, hal::BooleanFunction::NodeType::Concat, const2str(), hal::BooleanFunction::Node::constant, hal::BooleanFunction::NodeType::Constant, hal::BooleanFunction::NodeType::Eq, ERR, hal::BooleanFunction::Node::get_arity(), hal::BooleanFunction::Node::index, hal::BooleanFunction::NodeType::Index, hal::BooleanFunction::NodeType::Ite, hal::BooleanFunction::NodeType::Lshr, hal::BooleanFunction::NodeType::Mul, hal::BooleanFunction::NodeType::Not, OK, hal::BooleanFunction::NodeType::Or, hal::BooleanFunction::NodeType::Rol, hal::BooleanFunction::NodeType::Ror, hal::BooleanFunction::NodeType::Sdiv, hal::BooleanFunction::NodeType::Sext, hal::BooleanFunction::NodeType::Shl, hal::BooleanFunction::Node::size, hal::BooleanFunction::NodeType::Sle, hal::BooleanFunction::NodeType::Slice, hal::BooleanFunction::NodeType::Slt, hal::BooleanFunction::NodeType::Srem, control::str, hal::BooleanFunction::NodeType::Sub, hal::BooleanFunction::Node::to_string(), hal::BooleanFunction::Node::type, hal::BooleanFunction::NodeType::Udiv, hal::BooleanFunction::NodeType::Ule, hal::BooleanFunction::NodeType::Ult, hal::BooleanFunction::NodeType::Urem, hal::BooleanFunction::Node::variable, hal::BooleanFunction::NodeType::Variable, hal::BooleanFunction::NodeType::Xor, and hal::BooleanFunction::NodeType::Zext.

Referenced by translate_to_smt2().

translate_to_smt2()

Result< std::string > hal::SMT::Translator::translate_to_smt2

(

const BooleanFunction &

function

)

Translates a Boolean function into a SMT-LIB compatible string.

Parameters

[in]

function

- Boolean function to translate.

Returns

Ok() and SMT-LIB v2 compatible string on success, Err() otherwise.

Definition at line 137 of file translator.cpp.

References ERR, ERR_APPEND, OK, and reduce_to_smt2().