hal::SMT::Bitwuzla Namespace Reference

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

Variables
bool	is_linked = false

Function Documentation

query_binary()

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

Queries Bitwuzla 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 Bitwuzla process on success, Err() otherwise

Definition at line 289 of file solver.cpp.

References ERR, ERR_APPEND, query_binary_path(), and UNUSED.

query_binary_path()

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

(

)

Checks whether a Bitwuzla binary is available on the system.

Definition at line 205 of file solver.cpp.

References ERR, and OK.

Referenced by query_binary().

query_library()

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

Queries Bitwuzla 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 Bitwuzla process on success, Err() otherwise

Definition at line 234 of file solver.cpp.

References ERR, hal::SMT::QueryConfig::generate_model, hal::input, OK, hal::output, and control::parser.

Variable Documentation

is_linked

bool hal::SMT::Bitwuzla::is_linked = false

Definition at line 201 of file solver.cpp.