libTriton version 1.0 build 1588
Loading...
Searching...
No Matches
tritonToBitwuzla.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_TRITONTOBITWUZLA_H
9#define TRITON_TRITONTOBITWUZLA_H
10
11#include <map>
12#include <unordered_map>
13
14#include <bitwuzla/bitwuzla.h>
15
16#include <triton/ast.hpp>
17#include <triton/dllexport.hpp>
19
20
21
23namespace triton {
30 namespace ast {
38
40 public:
42 TRITON_EXPORT TritonToBitwuzla(bool eval=false);
43
45 TRITON_EXPORT ~TritonToBitwuzla();
46
48 TRITON_EXPORT const BitwuzlaTerm* convert(const SharedAbstractNode& node, Bitwuzla* bzla);
49
51 TRITON_EXPORT const std::unordered_map<const BitwuzlaTerm*, triton::engines::symbolic::SharedSymbolicVariable>& getVariables(void) const;
52
54 TRITON_EXPORT const std::map<size_t, const BitwuzlaSort*>& getBitvectorSorts(void) const;
55
56 private:
58 std::unordered_map<SharedAbstractNode, const BitwuzlaTerm*> translatedNodes;
59
61 std::unordered_map<const BitwuzlaTerm*, triton::engines::symbolic::SharedSymbolicVariable> variables;
62
64 std::unordered_map<std::string, triton::ast::SharedAbstractNode> symbols;
65
67 std::map<size_t, const BitwuzlaSort*> bvSorts;
68
70 bool isEval;
71
73 const BitwuzlaTerm* translate(const SharedAbstractNode& node, Bitwuzla* bzla);
74 };
75
77 };
79};
80
81#endif /* TRITON_TRITONTOBITWUZLA_H */
Converts a Triton's AST to Bitwuzla's AST.
TRITON_EXPORT const BitwuzlaTerm * convert(const SharedAbstractNode &node, Bitwuzla *bzla)
Converts to Bitwuzla's AST.
TRITON_EXPORT ~TritonToBitwuzla()
Destructor.
TRITON_EXPORT const std::map< size_t, const BitwuzlaSort * > & getBitvectorSorts(void) const
Returns bitvector sorts.
TRITON_EXPORT const std::unordered_map< const BitwuzlaTerm *, triton::engines::symbolic::SharedSymbolicVariable > & getVariables(void) const
Returns symbolic variables and its assosiated Bitwuzla terms to process the solver model.
std::shared_ptr< triton::ast::AbstractNode > SharedAbstractNode
Shared Abstract Node.
Definition: ast.hpp:59
The Triton namespace.