Solver engine using z3. More...

#include <z3Solver.hpp>

Inheritance diagram for triton::engines::solver::Z3Solver:

Public Member Functions
TRITON_EXPORT	Z3Solver ()
	Constructor.

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
	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 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 triton::ast::SharedAbstractNode	simplify (const triton::ast::SharedAbstractNode &node) const
	Converts a Triton's AST to a Z3's AST, perform a Z3 simplification and returns a Triton's AST.

TRITON_EXPORT triton::uint512	evaluate (const triton::ast::SharedAbstractNode &node) const
	Evaluates a Triton's AST via Z3 and returns a concrete value.

TRITON_EXPORT std::string	getName (void) const
	Returns the name of this 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).

Public Member Functions inherited from triton::engines::solver::SolverInterface
virtual TRITON_EXPORT	~SolverInterface ()
	Destructor.

Detailed Description

Solver engine using z3.

Definition at line 49 of file z3Solver.hpp.

Constructor & Destructor Documentation

◆ Z3Solver()

triton::engines::solver::Z3Solver::Z3Solver ( )

Constructor.

Definition at line 36 of file z3Solver.cpp.

Member Function Documentation

◆ evaluate()

triton::uint512 triton::engines::solver::Z3Solver::evaluate ( const triton::ast::SharedAbstractNode & node ) const

Evaluates a Triton's AST via Z3 and returns a concrete value.

Definition at line 262 of file z3Solver.cpp.

◆ getModel()

std::unordered_map< triton::usize, SolverModel > triton::engines::solver::Z3Solver::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. 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

Implements triton::engines::solver::SolverInterface.

Definition at line 228 of file z3Solver.cpp.

◆ getModels()

std::vector< std::unordered_map< triton::usize, SolverModel > > triton::engines::solver::Z3Solver::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. 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

Implements triton::engines::solver::SolverInterface.

Definition at line 42 of file z3Solver.cpp.

◆ getName()

std::string triton::engines::solver::Z3Solver::getName ( void ) const

virtual

Returns the name of this solver.

Implements triton::engines::solver::SolverInterface.

Definition at line 316 of file z3Solver.cpp.

◆ isSat()

bool triton::engines::solver::Z3Solver::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 168 of file z3Solver.cpp.

◆ setMemoryLimit()

void triton::engines::solver::Z3Solver::setMemoryLimit ( triton::uint32 mem )

virtual

Defines a solver memory consumption limit (in megabytes).

Implements triton::engines::solver::SolverInterface.

Definition at line 326 of file z3Solver.cpp.

◆ setTimeout()

void triton::engines::solver::Z3Solver::setTimeout ( triton::uint32 ms )

virtual

Defines a solver timeout (in milliseconds).

Implements triton::engines::solver::SolverInterface.

Definition at line 321 of file z3Solver.cpp.

◆ simplify()

triton::ast::SharedAbstractNode triton::engines::solver::Z3Solver::simplify ( const triton::ast::SharedAbstractNode & node ) const

Converts a Triton's AST to a Z3's AST, perform a Z3 simplification and returns a Triton's AST.

Definition at line 240 of file z3Solver.cpp.

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

/Users/jonathan/Works/Tools/Triton/src/libtriton/includes/triton/z3Solver.hpp
/Users/jonathan/Works/Tools/Triton/src/libtriton/engines/solver/z3/z3Solver.cpp

Public Member Functions

Detailed Description

Constructor & Destructor Documentation

◆ Z3Solver()

Member Function Documentation

◆ evaluate()

◆ getModel()

◆ getModels()

◆ getName()

◆ isSat()

◆ setMemoryLimit()

◆ setTimeout()

◆ simplify()