libTriton version 1.0 build 1590
Loading...
Searching...
No Matches
Public Member Functions | Protected Attributes | List of all members
triton::engines::solver::SolverEngine Interface Reference

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::SolverInterfacegetSolverInstance (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, 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. 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::SolverInterfacesolver
 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
protected

Instance to the real solver class.

Definition at line 61 of file solverEngine.hpp.


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