hal::SMT::Z3 Namespace Reference

Functions
Result< std::string >	query_binary_path ()
	Checks whether a Z3 binary is available on the system. More...
Result< std::tuple< bool, std::string > >	query_binary (const std::string &input, const QueryConfig &config)
Result< std::tuple< bool, std::string > >	query_library (const std::string &input, const QueryConfig &config)

Variables
bool	is_linked = false

Function Documentation

query_binary()

Result<std::tuple<bool, std::string> > hal::SMT::Z3::query_binary	(	const std::string &	input,
		const QueryConfig &	config
	)

Queries Z3 with an SMT-LIB input and a query configuration.

Parameters

[in]	input	- SMT-LIB input.
[in]	config	- SMT query configuration.

Returns

Ok() and status with (0) was_killed (true in case process was killed), and (1) stdout Stdout of Z3 process on success, Err() otherwise

Definition at line 53 of file solver.cpp.

References ERR_APPEND, hal::input, OK, hal::output, query_binary_path(), and hal::SMT::QueryConfig::timeout_in_seconds.

query_binary_path()

Result<std::string> hal::SMT::Z3::query_binary_path

(

)

Checks whether a Z3 binary is available on the system.

Definition at line 24 of file solver.cpp.

References ERR, and OK.

Referenced by query_binary().

query_library()

Result<std::tuple<bool, std::string> > hal::SMT::Z3::query_library	(	const std::string &	input,
		const QueryConfig &	config
	)

Queries Z3 with an SMT-LIB input and a query configuration.

Parameters

[in]	input	- SMT-LIB input.
[in]	config	- SMT query configuration.

Returns

Ok() and status with (0) was_killed (true in case process was killed), and (1) stdout Stdout of Z3 process on success, Err() otherwise

Definition at line 98 of file solver.cpp.

References ERR, hal::input, and UNUSED.

Variable Documentation

is_linked

bool hal::SMT::Z3::is_linked = false

Definition at line 21 of file solver.cpp.