triton::engines::solver::SolverInterface Interface Reference

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, SolverModel >	getModel (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.
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.
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.

Constructor & Destructor Documentation

~SolverInterface()

virtual TRITON_EXPORT triton::engines::solver::SolverInterface::~SolverInterface ( )

inlinevirtual

Destructor.

Definition at line 48 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::BitwuzlaSolver, and triton::engines::solver::Z3Solver.

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::BitwuzlaSolver, and triton::engines::solver::Z3Solver.

getName()

virtual TRITON_EXPORT std::string triton::engines::solver::SolverInterface::getName ( void  ) const

pure virtual

Returns the name of the solver.

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

isSat()

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

pure virtual

Returns true if an expression is satisfiable.

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

setMemoryLimit()

virtual TRITON_EXPORT void triton::engines::solver::SolverInterface::setMemoryLimit ( triton::uint32  mem )

pure virtual

Defines a solver memory consumption limit (in megabytes).

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

setTimeout()

virtual TRITON_EXPORT void triton::engines::solver::SolverInterface::setTimeout ( triton::uint32  ms )

pure virtual

Defines a solver timeout (in milliseconds).

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

---

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

• /Users/jonathan/Works/Tools/Triton/src/libtriton/includes/triton/solverInterface.hpp