libTriton version 1.0 build 1592
Loading...
Searching...
No Matches
solverEngine.cpp
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#include <triton/config.hpp>
11
12
13
14namespace triton {
15 namespace engines {
16 namespace solver {
17
20 #if defined(TRITON_Z3_INTERFACE)
21 /* By default we initialized the z3 solver */
23 #elif defined(TRITON_BITWUZLA_INTERFACE)
25 #endif
26 }
27
28
32
33
35 if (!this->solver)
36 throw triton::exceptions::SolverEngine("SolverEngine::getSolver(): Solver undefined.");
37 return this->solver.get();
38 }
39
40
42 /* Allocate and init the good solver */
43 switch (kind) {
44 #ifdef TRITON_Z3_INTERFACE
46 /* init the new instance */
47 this->solver.reset(new(std::nothrow) triton::engines::solver::Z3Solver());
48 if (this->solver == nullptr)
49 throw triton::exceptions::SolverEngine("SolverEngine::setSolver(): Not enough memory.");
50 break;
51 #endif
52 #ifdef TRITON_BITWUZLA_INTERFACE
54 /* init the new instance */
55 this->solver.reset(new(std::nothrow) triton::engines::solver::BitwuzlaSolver());
56 if (this->solver == nullptr)
57 throw triton::exceptions::SolverEngine("SolverEngine::setSolver(): Not enough memory.");
58 break;
59 #endif
60
61 default:
62 throw triton::exceptions::SolverEngine("SolverEngine::setSolver(): Solver not supported.");
63 break;
64 }
65
66 /* Setup global variables */
67 this->kind = kind;
68 }
69
70
72 if (customSolver == nullptr)
73 throw triton::exceptions::SolverEngine("SolverEngine::setCustomSolver(): custom solver cannot be null.");
74
75 /* Define the custom solver as current solver */
76 this->solver.reset(customSolver);
77
78 /* Setup global variables */
80 }
81
82
83 bool SolverEngine::isValid(void) const {
85 return false;
86 return true;
87 }
88
89
90 std::unordered_map<triton::usize, SolverModel> SolverEngine::getModel(const triton::ast::SharedAbstractNode& node, triton::engines::solver::status_e* status, triton::uint32 timeout, triton::uint32* solvingTime) const {
91 if (!this->solver)
92 return std::unordered_map<triton::usize, SolverModel>{};
93 return this->solver->getModel(node, status, timeout, solvingTime);
94 }
95
96
97 std::vector<std::unordered_map<triton::usize, SolverModel>> SolverEngine::getModels(const triton::ast::SharedAbstractNode& node, triton::uint32 limit, triton::engines::solver::status_e* status, triton::uint32 timeout, triton::uint32* solvingTime) const {
98 if (!this->solver)
99 return std::vector<std::unordered_map<triton::usize, SolverModel>>{};
100 return this->solver->getModels(node, limit, status, timeout, solvingTime);
101 }
102
103
105 if (!this->solver)
106 return false;
107 return this->solver->isSat(node, status, timeout, solvingTime);
108 }
109
110
111 std::string SolverEngine::getName(void) const {
112 if (!this->solver)
113 return "n/a";
114 return this->solver->getName();
115 }
116
117
119 if (this->solver) {
120 this->solver->setTimeout(ms);
121 }
122 }
123
124
126 if (this->solver) {
127 this->solver->setMemoryLimit(limit);
128 }
129 }
130
131 };
132 };
133};
Solver engine using Bitwuzla.
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.
Solver engine using z3.
Definition z3Solver.hpp:49
The exception class used by the solver engine.
std::shared_ptr< triton::ast::AbstractNode > SharedAbstractNode
Shared Abstract Node.
Definition ast.hpp:59
std::uint32_t uint32
unisgned 32-bits
The Triton namespace.