libTriton version 1.0 build 1590
Loading...
Searching...
No Matches
solverInterface.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_SOLVERINTERFACE_HPP
9#define TRITON_SOLVERINTERFACE_HPP
10
11#include <unordered_map>
12#include <vector>
13
14#include <triton/ast.hpp>
15#include <triton/dllexport.hpp>
19
20
21
23namespace triton {
29 namespace engines {
36 namespace solver {
46 public:
48 TRITON_EXPORT virtual ~SolverInterface(){};
49
51
57 TRITON_EXPORT virtual 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 = 0;
58
60
66 TRITON_EXPORT virtual 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 = 0;
67
69 TRITON_EXPORT virtual bool isSat(const triton::ast::SharedAbstractNode& node, triton::engines::solver::status_e* status = nullptr, triton::uint32 timeout = 0, triton::uint32* solvingTime = nullptr) const = 0;
70
72 TRITON_EXPORT virtual std::string getName(void) const = 0;
73
75 TRITON_EXPORT virtual void setTimeout(triton::uint32 ms) = 0;
76
78 TRITON_EXPORT virtual void setMemoryLimit(triton::uint32 mem) = 0;
79 };
80
82 };
84 };
86};
87
88#endif /* TRITON_SOLVERINTERFACE_HPP */
This interface is used to interface with solvers.
virtual 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 =0
Returns true if an expression is satisfiable.
virtual 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 =0
Computes and returns a model from a symbolic constraint. State is returned in the status pointer as w...
virtual TRITON_EXPORT std::string getName(void) const =0
Returns the name of the solver.
virtual TRITON_EXPORT void setTimeout(triton::uint32 ms)=0
Defines a solver timeout (in milliseconds).
virtual TRITON_EXPORT ~SolverInterface()
Destructor.
virtual TRITON_EXPORT void setMemoryLimit(triton::uint32 mem)=0
Defines a solver memory consumption limit (in megabytes).
virtual 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 =0
Computes and returns several models from a symbolic constraint. The limit is the max number of models...
std::shared_ptr< triton::ast::AbstractNode > SharedAbstractNode
Shared Abstract Node.
Definition ast.hpp:59
std::uint32_t uint32
unisgned 32-bits
The Triton namespace.