libTriton  version 0.6 build 1389
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 (triton::engines::symbolic::SymbolicEngine *symbolicEngine)
 Constructor.
 
TRITON_EXPORT triton::engines::solver::solvers_e getSolver (void) const
 Returns the kind of solver as triton::engines::solver::solvers_e.
 
TRITON_EXPORT const triton::engines::solver::SolverInterfacegetSolverInstance (void) const
 Returns the instance of the initialized solver.
 
TRITON_EXPORT void setSolver (triton::engines::solver::solvers_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::map< triton::uint32, SolverModelgetModel (const triton::ast::SharedAbstractNode &node) const
 Computes and returns a model from a symbolic constraint. More...
 
TRITON_EXPORT std::list< std::map< triton::uint32, SolverModel > > getModels (const triton::ast::SharedAbstractNode &node, triton::uint32 limit) const
 Computes and returns several models from a symbolic constraint. The limit is the max number of models returned. More...
 
TRITON_EXPORT bool isSat (const triton::ast::SharedAbstractNode &node) const
 Returns true if an expression is satisfiable.
 
TRITON_EXPORT std::string getName (void) const
 Returns the name of the solver.
 

Protected Attributes

triton::engines::solver::solvers_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 61 of file solverEngine.hpp.

Member Function Documentation

◆ getModel()

std::map< triton::uint32, SolverModel > triton::engines::solver::SolverEngine::getModel ( const triton::ast::SharedAbstractNode node) const

Computes and returns a model from a symbolic constraint.

map of symbolic variable id -> model

item1: symbolic variable id
item2: model

Definition at line 81 of file solverEngine.cpp.

◆ getModels()

std::list< std::map< triton::uint32, SolverModel > > triton::engines::solver::SolverEngine::getModels ( const triton::ast::SharedAbstractNode node,
triton::uint32  limit 
) const

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

list of map of symbolic variable id -> model

item1: symbolic variable id
item2: model

Definition at line 88 of file solverEngine.cpp.


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