triton::engines::solver::BitwuzlaSolver Class Reference

Solver engine using Bitwuzla. More...

#include <bitwuzlaSolver.hpp>

Inheritance diagram for triton::engines::solver::BitwuzlaSolver:

Public Member Functions
TRITON_EXPORT	BitwuzlaSolver ()
	Constructor.
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.
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 number of models returned.
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 triton::uint512	evaluate (const triton::ast::SharedAbstractNode &node) const
	Evaluates a Triton's AST via Bitwuzla and returns a concrete value.
TRITON_EXPORT std::string	getName (void) const
	Returns the name of this 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).
Public Member Functions inherited from triton::engines::solver::SolverInterface
virtual TRITON_EXPORT	~SolverInterface ()
	Destructor.

Static Public Member Functions
static int32_t	terminateCallback (void *state)
	Callback function that implements termination of Bitwuzla solver on timeout and memory limit.
static void	abortCallback (const char *msg)
	Callback function that implements aborting of Bitwuzla solver with throwing exception.

Detailed Description

Solver engine using Bitwuzla.

Definition at line 53 of file bitwuzlaSolver.hpp.

Constructor & Destructor Documentation

BitwuzlaSolver()

triton::engines::solver::BitwuzlaSolver::BitwuzlaSolver

(

)

Constructor.

Definition at line 26 of file bitwuzlaSolver.cpp.

Member Function Documentation

abortCallback()

void triton::engines::solver::BitwuzlaSolver::abortCallback ( const char * msg )

static

Callback function that implements aborting of Bitwuzla solver with throwing exception.

Definition at line 85 of file bitwuzlaSolver.cpp.

evaluate()

triton::uint512 triton::engines::solver::BitwuzlaSolver::evaluate

(

const triton::ast::SharedAbstractNode &

node

)

const

Evaluates a Triton's AST via Bitwuzla and returns a concrete value.

Definition at line 214 of file bitwuzlaSolver.cpp.

getModel()

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

virtual

Computes and returns a model from a symbolic constraint.

map of symbolic variable id -> model

item1: symbolic variable id
item2: model

Implements triton::engines::solver::SolverInterface.

Definition at line 208 of file bitwuzlaSolver.cpp.

getModels()

std::vector< std::unordered_map< triton::usize, SolverModel > > triton::engines::solver::BitwuzlaSolver::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

virtual

Computes and returns several models from a symbolic constraint. The limit is the number of models returned.

vector of map of symbolic variable id -> model

item1: symbolic variable id
item2: model

Implements triton::engines::solver::SolverInterface.

Definition at line 90 of file bitwuzlaSolver.cpp.

getName()

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

virtual

Returns the name of this solver.

Implements triton::engines::solver::SolverInterface.

Definition at line 250 of file bitwuzlaSolver.cpp.

isSat()

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

virtual

Returns true if an expression is satisfiable.

Implements triton::engines::solver::SolverInterface.

Definition at line 196 of file bitwuzlaSolver.cpp.

setMemoryLimit()

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

virtual

Defines a solver memory consumption limit (in megabytes).

Implements triton::engines::solver::SolverInterface.

Definition at line 260 of file bitwuzlaSolver.cpp.

setTimeout()

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

virtual

Defines a solver timeout (in milliseconds).

Implements triton::engines::solver::SolverInterface.

Definition at line 255 of file bitwuzlaSolver.cpp.

terminateCallback()

int32_t triton::engines::solver::BitwuzlaSolver::terminateCallback ( void * state )

static

Callback function that implements termination of Bitwuzla solver on timeout and memory limit.

Definition at line 35 of file bitwuzlaSolver.cpp.

---

The documentation for this class was generated from the following files:

• /Users/jonathan/Works/Tools/Triton/src/libtriton/includes/triton/bitwuzlaSolver.hpp
• /Users/jonathan/Works/Tools/Triton/src/libtriton/engines/solver/bitwuzla/bitwuzlaSolver.cpp