libTriton version 1.0 build 1588
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
16#include <bitwuzla/bitwuzla.h>
17
18#include <triton/ast.hpp>
19#include <triton/dllexport.hpp>
25
26
27
29namespace triton {
35 namespace engines {
42 namespace solver {
50
52 private:
54 triton::uint512 fromBvalueToUint512(const char* value) const;
55
57 struct SolverParams {
58 SolverParams(int64_t timeout, size_t memory_limit): timeout(timeout), memory_limit(memory_limit) {
59 }
60
61 std::chrono::time_point<std::chrono::system_clock> start = std::chrono::system_clock::now();
63 int64_t timeout;
64 size_t memory_limit;
65 int64_t last_mem_check = -1;
66 };
67
69 triton::uint32 timeout;
70
72 triton::uint32 memoryLimit;
73
74 public:
76 TRITON_EXPORT BitwuzlaSolver();
77
79
85 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;
86
88
94 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;
95
97 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;
98
100 TRITON_EXPORT triton::uint512 evaluate(const triton::ast::SharedAbstractNode& node) const;
101
103 TRITON_EXPORT std::string getName(void) const;
104
106 TRITON_EXPORT void setTimeout(triton::uint32 ms);
107
109 TRITON_EXPORT void setMemoryLimit(triton::uint32 mem);
110
112 static int32_t terminateCallback(void* state);
113
115 static void abortCallback(const char* msg);
116 };
117
119 };
121 };
123};
124
125#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
Definition: tritonTypes.hpp:39
The Triton namespace.