libTriton  version 1.0 build 1549
solverEngine.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_SOLVERENGINE_HPP
9#define TRITON_SOLVERENGINE_HPP
10
11#include <iostream>
12#include <memory>
13#include <unordered_map>
14#include <vector>
15
16#include <triton/ast.hpp>
17#include <triton/config.hpp>
18#include <triton/dllexport.hpp>
23#ifdef TRITON_Z3_INTERFACE
24 #include <triton/z3Solver.hpp>
25#endif
26#ifdef TRITON_BITWUZLA_INTERFACE
28#endif
29
30
31
33namespace triton {
39 namespace engines {
46 namespace solver {
56 protected:
59
61 std::unique_ptr<triton::engines::solver::SolverInterface> solver;
62
63 public:
65 TRITON_EXPORT SolverEngine();
66
68 TRITON_EXPORT triton::engines::solver::solver_e getSolver(void) const;
69
71 TRITON_EXPORT const triton::engines::solver::SolverInterface* getSolverInstance(void) const;
72
75
77 TRITON_EXPORT void setCustomSolver(triton::engines::solver::SolverInterface* customSolver);
78
80 TRITON_EXPORT bool isValid(void) const;
81
83
89 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;
90
92
98 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;
99
101 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;
102
104 TRITON_EXPORT std::string getName(void) const;
105
107 TRITON_EXPORT void setTimeout(triton::uint32 ms);
108
110 TRITON_EXPORT void setMemoryLimit(triton::uint32 mem);
111 };
112
114 };
116 };
118};
119
120#endif /* TRITON_SOLVERINTERFACE_HPP */
This class is used to interface with solvers.
TRITON_EXPORT std::string getName(void) const
Returns the name of the solver.
TRITON_EXPORT SolverEngine()
Constructor.
TRITON_EXPORT void setSolver(triton::engines::solver::solver_e kind)
Initializes a predefined solver.
TRITON_EXPORT void setCustomSolver(triton::engines::solver::SolverInterface *customSolver)
Initializes a custom solver.
TRITON_EXPORT triton::engines::solver::solver_e getSolver(void) const
Returns the kind of solver as triton::engines::solver::solver_e.
TRITON_EXPORT void setTimeout(triton::uint32 ms)
Defines a solver timeout (in milliseconds).
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...
TRITON_EXPORT const triton::engines::solver::SolverInterface * getSolverInstance(void) const
Returns the instance of the initialized solver.
triton::engines::solver::solver_e kind
The kind of the current solver used.
std::unique_ptr< triton::engines::solver::SolverInterface > solver
Instance to the real solver class.
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 max number of models...
TRITON_EXPORT bool isValid(void) const
Returns true if the solver is valid.
TRITON_EXPORT void setMemoryLimit(triton::uint32 mem)
Defines a solver memory consumption limit (in megabytes).
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.