This class is used to interface with solvers. More...

#include <solverEngine.hpp>

Public Member Functions
TRITON_EXPORT	SolverEngine ()
	Constructor.

TRITON_EXPORT triton::engines::solver::solver_e	getSolver (void) const
	Returns the kind of solver as triton::engines::solver::solver_e.

TRITON_EXPORT const triton::engines::solver::SolverInterface *	getSolverInstance (void) const
	Returns the instance of the initialized solver.

TRITON_EXPORT void	setSolver (triton::engines::solver::solver_e kind)
	Initializes a predefined solver.

TRITON_EXPORT void	setCustomSolver (triton::engines::solver::SolverInterface *customSolver)
	Initializes a custom solver.

TRITON_EXPORT bool	isValid (void) const
	Returns true if the solver is valid.

TRITON_EXPORT std::unordered_map< triton::usize, SolverModel >	getModel (const triton::ast::SharedAbstractNode &node, triton::engines::solver::status_e status=nullptr, triton::uint32 timeout=0, triton::uint32 solvingTime=nullptr) const
	Computes and returns a model from a symbolic constraint. State is returned in the `status` pointer as well as the solving time. A `timeout` can also be defined.

TRITON_EXPORT std::vector< std::unordered_map< triton::usize, SolverModel > >	getModels (const triton::ast::SharedAbstractNode &node, triton::uint32 limit, triton::engines::solver::status_e status=nullptr, triton::uint32 timeout=0, triton::uint32 solvingTime=nullptr) const
	Computes and returns several models from a symbolic constraint. The `limit` is the max number of models returned. State is returned in the `status` pointer as well as the solving time. A `timeout` can also be defined.

TRITON_EXPORT bool	isSat (const triton::ast::SharedAbstractNode &node, triton::engines::solver::status_e status=nullptr, triton::uint32 timeout=0, triton::uint32 solvingTime=nullptr) const
	Returns true if an expression is satisfiable.

TRITON_EXPORT std::string	getName (void) const
	Returns the name of the solver.

TRITON_EXPORT void	setTimeout (triton::uint32 ms)
	Defines a solver timeout (in milliseconds).

TRITON_EXPORT void	setMemoryLimit (triton::uint32 mem)
	Defines a solver memory consumption limit (in megabytes).

Protected Attributes
triton::engines::solver::solver_e	kind
	The kind of the current solver used.

std::unique_ptr< triton::engines::solver::SolverInterface >	solver
	Instance to the real solver class.

Detailed Description

This class is used to interface with solvers.

Definition at line 55 of file solverEngine.hpp.

Constructor & Destructor Documentation

◆ SolverEngine()

triton::engines::solver::SolverEngine::SolverEngine ( )

Constructor.

Definition at line 18 of file solverEngine.cpp.

Member Function Documentation

◆ getModel()

std::unordered_map< triton::usize, SolverModel > triton::engines::solver::SolverEngine::getModel	(	const triton::ast::SharedAbstractNode &	node,
		triton::engines::solver::status_e *	status = nullptr,
		triton::uint32	timeout = 0,
		triton::uint32 *	solvingTime = nullptr ) const

Computes and returns a model from a symbolic constraint. State is returned in the status pointer as well as the solving time. A timeout can also be defined.

map of symbolic variable id -> model

item1: symbolic variable id
item2: model

Definition at line 90 of file solverEngine.cpp.

◆ getModels()

std::vector< std::unordered_map< triton::usize, SolverModel > > triton::engines::solver::SolverEngine::getModels	(	const triton::ast::SharedAbstractNode &	node,
		triton::uint32	limit,
		triton::engines::solver::status_e *	status = nullptr,
		triton::uint32	timeout = 0,
		triton::uint32 *	solvingTime = nullptr ) const

Computes and returns several models from a symbolic constraint. The limit is the max number of models returned. State is returned in the status pointer as well as the solving time. A timeout can also be defined.

vector of map of symbolic variable id -> model

item1: symbolic variable id
item2: model

Definition at line 97 of file solverEngine.cpp.

◆ getName()

std::string triton::engines::solver::SolverEngine::getName ( void ) const

Returns the name of the solver.

Definition at line 111 of file solverEngine.cpp.

◆ getSolver()

triton::engines::solver::solver_e triton::engines::solver::SolverEngine::getSolver ( void ) const

Returns the kind of solver as triton::engines::solver::solver_e.

Definition at line 29 of file solverEngine.cpp.

◆ getSolverInstance()

const triton::engines::solver::SolverInterface * triton::engines::solver::SolverEngine::getSolverInstance ( void ) const

Returns the instance of the initialized solver.

Definition at line 34 of file solverEngine.cpp.

◆ isSat()

bool triton::engines::solver::SolverEngine::isSat	(	const triton::ast::SharedAbstractNode &	node,
		triton::engines::solver::status_e *	status = nullptr,
		triton::uint32	timeout = 0,
		triton::uint32 *	solvingTime = nullptr ) const

Returns true if an expression is satisfiable.

Definition at line 104 of file solverEngine.cpp.

◆ isValid()

bool triton::engines::solver::SolverEngine::isValid ( void ) const

Returns true if the solver is valid.

Definition at line 83 of file solverEngine.cpp.

◆ setCustomSolver()

void triton::engines::solver::SolverEngine::setCustomSolver ( triton::engines::solver::SolverInterface * customSolver )

Initializes a custom solver.

Definition at line 71 of file solverEngine.cpp.

◆ setMemoryLimit()

void triton::engines::solver::SolverEngine::setMemoryLimit ( triton::uint32 mem )

Defines a solver memory consumption limit (in megabytes).

Definition at line 125 of file solverEngine.cpp.

◆ setSolver()

void triton::engines::solver::SolverEngine::setSolver ( triton::engines::solver::solver_e kind )

Initializes a predefined solver.

Definition at line 41 of file solverEngine.cpp.

◆ setTimeout()

void triton::engines::solver::SolverEngine::setTimeout ( triton::uint32 ms )

Defines a solver timeout (in milliseconds).

Definition at line 118 of file solverEngine.cpp.

Member Data Documentation

◆ kind

triton::engines::solver::solver_e triton::engines::solver::SolverEngine::kind

protected

The kind of the current solver used.

Definition at line 58 of file solverEngine.hpp.

◆ solver

std::unique_ptr<triton::engines::solver::SolverInterface> triton::engines::solver::SolverEngine::solver