libTriton version 1.0 build 1592
Loading...
Searching...
No Matches
bitwuzlaSolver.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_BITWUZLASOLVER_H
9#define TRITON_BITWUZLASOLVER_H
10
11#include <chrono>
12#include <string>
13#include <unordered_map>
14#include <vector>
15
16extern "C" {
17#include <bitwuzla/c/bitwuzla.h>
18}
19
20#include <triton/ast.hpp>
21#include <triton/dllexport.hpp>
27
28
29
31namespace triton {
37 namespace engines {
44 namespace solver {
52
54 private:
56 triton::uint512 fromBvalueToUint512(const char* value) const;
57
59 struct SolverParams {
60 SolverParams(int64_t timeout, size_t memory_limit): timeout(timeout), memory_limit(memory_limit) {
61 }
62
63 std::chrono::time_point<std::chrono::system_clock> start = std::chrono::system_clock::now();
65 int64_t timeout;
66 size_t memory_limit;
67 int64_t last_mem_check = -1;
68 };
69
71 triton::uint32 timeout;
72
74 triton::uint32 memoryLimit;
75
76 public:
78 TRITON_EXPORT BitwuzlaSolver();
79
81
87 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;
88
90
96 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;
97
99 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;
100
102 TRITON_EXPORT triton::uint512 evaluate(const triton::ast::SharedAbstractNode& node) const;
103
105 TRITON_EXPORT std::string getName(void) const;
106
108 TRITON_EXPORT void setTimeout(triton::uint32 ms);
109
111 TRITON_EXPORT void setMemoryLimit(triton::uint32 mem);
112
114 static int32_t terminateCallback(void* state);
115
117 static void abortCallback(const char* msg);
118 };
119
121 };
123 };
125};
126
127#endif /* TRITON_BITWUZLASOLVER_H */
Solver engine using Bitwuzla.
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.
TRITON_EXPORT std::string getName(void) const
Returns the name of this solver.
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...
TRITON_EXPORT BitwuzlaSolver()
Constructor.
TRITON_EXPORT triton::uint512 evaluate(const triton::ast::SharedAbstractNode &node) const
Evaluates a Triton's AST via Bitwuzla and returns a concrete value.
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).
static void abortCallback(const char *msg)
Callback function that implements aborting of Bitwuzla solver with throwing exception.
static int32_t terminateCallback(void *state)
Callback function that implements termination of Bitwuzla solver on timeout and memory limit.
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.
This interface is used to interface with solvers.
std::shared_ptr< triton::ast::AbstractNode > SharedAbstractNode
Shared Abstract Node.
Definition ast.hpp:59
std::uint32_t uint32
unisgned 32-bits
The Triton namespace.