libTriton  version 1.0 build 1558
Classes | Public Member Functions | Static Public Member Functions | List of all members
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. More...
 
TRITON_EXPORT std::unordered_map< triton::usize, SolverModelgetModel (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. More...
 
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. More...
 
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. More...
 
TRITON_EXPORT triton::uint512 evaluate (const triton::ast::SharedAbstractNode &node) const
 Evaluates a Triton's AST via Bitwuzla and returns a concrete value. More...
 
TRITON_EXPORT std::string getName (void) const
 Returns the name of this solver. More...
 
TRITON_EXPORT void setTimeout (triton::uint32 ms)
 Defines a solver timeout (in milliseconds). More...
 
TRITON_EXPORT void setMemoryLimit (triton::uint32 mem)
 Defines a solver memory consumption limit (in megabytes). More...
 
- Public Member Functions inherited from triton::engines::solver::SolverInterface
virtual TRITON_EXPORT ~SolverInterface ()
 Destructor. More...
 
virtual TRITON_EXPORT std::unordered_map< triton::usize, SolverModelgetModel (const triton::ast::SharedAbstractNode &node, triton::engines::solver::status_e *status=nullptr, triton::uint32 timeout=0, triton::uint32 *solvingTime=nullptr) const =0
 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. More...
 
virtual 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 =0
 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. More...
 
virtual 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 =0
 Returns true if an expression is satisfiable. More...
 
virtual TRITON_EXPORT std::string getName (void) const =0
 Returns the name of the solver. More...
 
virtual TRITON_EXPORT void setTimeout (triton::uint32 ms)=0
 Defines a solver timeout (in milliseconds). More...
 
virtual TRITON_EXPORT void setMemoryLimit (triton::uint32 mem)=0
 Defines a solver memory consumption limit (in megabytes). More...
 

Static Public Member Functions

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

Detailed Description

Solver engine using Bitwuzla.

Definition at line 51 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 211 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 205 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 235 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 193 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 245 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 240 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: