libTriton  version 1.0 build 1549
z3Solver.hpp
Go to the documentation of this file.
1
2/*
3** Copyright (C) - Triton
4**
5** This program is under the terms of the Apache License 2.0.
6*/
7
8#ifndef TRITON_Z3SOLVER_H
9#define TRITON_Z3SOLVER_H
10
11#include <string>
12#include <unordered_map>
13#include <vector>
14#include <z3++.h>
15#include <z3_api.h>
16
17#include <triton/ast.hpp>
18#include <triton/dllexport.hpp>
23
24
25
27namespace triton {
33 namespace engines {
40 namespace solver {
48
49 class Z3Solver : public SolverInterface {
51 static z3::expr mk_or(z3::expr_vector args);
52
53 private:
55 triton::uint32 timeout;
56
58 triton::uint32 memoryLimit;
59
61 void writeBackStatus(z3::solver& solver, z3::check_result res, triton::engines::solver::status_e* status) const;
62
63 public:
65 TRITON_EXPORT Z3Solver();
66
68
74 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;
75
77
83 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;
84
86 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;
87
90
92 TRITON_EXPORT triton::uint512 evaluate(const triton::ast::SharedAbstractNode& node) const;
93
95 TRITON_EXPORT std::string getName(void) const;
96
98 TRITON_EXPORT void setTimeout(triton::uint32 ms);
99
101 TRITON_EXPORT void setMemoryLimit(triton::uint32 mem);
102 };
103
105 };
107 };
109};
110
111#endif /* TRITON_Z3SOLVER_H */
This interface is used to interface with solvers.
Solver engine using z3.
Definition: z3Solver.hpp:49
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 w...
Definition: z3Solver.cpp:228
TRITON_EXPORT Z3Solver()
Constructor.
Definition: z3Solver.cpp:36
TRITON_EXPORT triton::uint512 evaluate(const triton::ast::SharedAbstractNode &node) const
Evaluates a Triton's AST via Z3 and returns a concrete value.
Definition: z3Solver.cpp:262
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.
Definition: z3Solver.cpp:168
TRITON_EXPORT std::string getName(void) const
Returns the name of this solver.
Definition: z3Solver.cpp:316
TRITON_EXPORT void setTimeout(triton::uint32 ms)
Defines a solver timeout (in milliseconds).
Definition: z3Solver.cpp:321
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.
Definition: z3Solver.cpp:240
TRITON_EXPORT void setMemoryLimit(triton::uint32 mem)
Defines a solver memory consumption limit (in megabytes).
Definition: z3Solver.cpp:326
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 ret...
Definition: z3Solver.cpp:42
std::shared_ptr< triton::ast::AbstractNode > SharedAbstractNode
Shared Abstract Node.
Definition: ast.hpp:59
std::uint32_t uint32
unisgned 32-bits
Definition: tritonTypes.hpp:39
The Triton namespace.