libTriton version 1.0 build 1592
Loading...
Searching...
No Matches
tritonToZ3.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_TRITONTOZ3_H
9#define TRITON_TRITONTOZ3_H
10
11#include <unordered_map>
12#include <z3++.h>
13
14#include <triton/ast.hpp>
15#include <triton/dllexport.hpp>
17
18
19
21namespace triton {
28 namespace ast {
36
37 class TritonToZ3 {
38 private:
40 bool isEval;
41
43 std::string getStringValue(const z3::expr& expr);
44
46 z3::expr do_convert(const triton::ast::SharedAbstractNode& node, std::unordered_map<triton::ast::SharedAbstractNode, z3::expr>* output);
47
48 protected:
50 z3::context context;
51
52 public:
54 std::unordered_map<std::string, triton::ast::SharedAbstractNode> symbols;
55
57 std::unordered_map<std::string, triton::engines::symbolic::SharedSymbolicVariable> variables;
58
60 TRITON_EXPORT TritonToZ3(bool eval=true);
61
63 TRITON_EXPORT ~TritonToZ3();
64
66 TRITON_EXPORT z3::expr convert(const triton::ast::SharedAbstractNode& node);
67 };
68
70 };
72};
73
74#endif /* TRITON_TRITONTOZ3_H */
Converts a Triton's AST to Z3's AST.
std::unordered_map< std::string, triton::engines::symbolic::SharedSymbolicVariable > variables
The set of symbolic variables contained in the expression.
TRITON_EXPORT ~TritonToZ3()
Destructor.
TRITON_EXPORT TritonToZ3(bool eval=true)
Constructor.
std::unordered_map< std::string, triton::ast::SharedAbstractNode > symbols
The map of symbols. E.g: (let (symbols expr1) expr2)
z3::context context
The z3's context.
TRITON_EXPORT z3::expr convert(const triton::ast::SharedAbstractNode &node)
Converts to Z3's AST.
std::shared_ptr< triton::ast::AbstractNode > SharedAbstractNode
Shared Abstract Node.
Definition ast.hpp:59
The Triton namespace.