libTriton  version 1.0 build 1532
Public Member Functions | List of all members
triton::engines::solver::Z3Solver Class Reference

Solver engine using z3. More...

#include <z3Solver.hpp>

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

Public Member Functions

TRITON_EXPORT Z3Solver ()
 Constructor. More...
 
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. More...
 
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. More...
 
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. More...
 
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. More...
 
TRITON_EXPORT triton::uint512 evaluate (const triton::ast::SharedAbstractNode &node) const
 Evaluates a Triton's AST via Z3 and returns a concrete value. More...
 
TRITON_EXPORT std::string getName (void) const
 Returns the name of this solver. More...
 
TRITON_EXPORT void setTimeout (triton::uint32 ms)
 Defines a solver timeout (in milliseconds). More...
 
TRITON_EXPORT void setMemoryLimit (triton::uint32 mem)
 Defines a solver memory consumption limit (in megabytes). More...
 
- Public Member Functions inherited from triton::engines::solver::SolverInterface
virtual TRITON_EXPORT ~SolverInterface ()
 Destructor. More...
 

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: