solver.cpp File Reference

#include "hal_core/netlist/boolean_function/solver.h"
#include "hal_core/netlist/boolean_function/translator.h"
#include "hal_core/netlist/boolean_function/types.h"
#include "subprocess/process.h"
#include <numeric>
#include <set>

Include dependency graph for solver.cpp:

Go to the source code of this file.

Namespaces
	hal
	hal::SMT
	hal::SMT::Z3
	hal::SMT::Boolector
	hal::SMT::Bitwuzla

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

Variables
bool	hal::SMT::Z3::is_linked = false
bool	hal::SMT::Boolector::is_linked = false
bool	hal::SMT::Bitwuzla::is_linked = false