libTriton  version 1.0 build 1530
Public Member Functions | List of all members
triton::engines::solver::SolverInterface Interface Referenceabstract

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

#include <solverInterface.hpp>

Inheritance diagram for triton::engines::solver::SolverInterface:

Public Member Functions

virtual TRITON_EXPORT ~SolverInterface ()
 Destructor.
 
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.
 
virtual TRITON_EXPORT std::string getName (void) const =0
 Returns the name of the solver.
 
virtual TRITON_EXPORT void setTimeout (triton::uint32 ms)=0
 Defines a solver timeout (in milliseconds).
 
virtual TRITON_EXPORT void setMemoryLimit (triton::uint32 mem)=0
 Defines a solver memory consumption limit (in megabytes).
 

Detailed Description

This interface is used to interface with solvers.

Definition at line 45 of file solverInterface.hpp.

Member Function Documentation

◆ getModel()

virtual TRITON_EXPORT std::unordered_map<triton::usize, SolverModel> triton::engines::solver::SolverInterface::getModel ( const triton::ast::SharedAbstractNode node,
triton::engines::solver::status_e status = nullptr,
triton::uint32  timeout = 0,
triton::uint32 solvingTime = nullptr 
) const
pure virtual

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

Implemented in triton::engines::solver::Z3Solver, and triton::engines::solver::BitwuzlaSolver.

◆ getModels()

virtual TRITON_EXPORT std::vector<std::unordered_map<triton::usize, SolverModel> > triton::engines::solver::SolverInterface::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
pure virtual

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

Implemented in triton::engines::solver::Z3Solver, and triton::engines::solver::BitwuzlaSolver.


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