libTriton version 1.0 build 1590
Loading...
Searching...
No Matches
Classes | Enumerations | Functions
Solver
Collaboration diagram for Solver:

Classes

class  triton::engines::solver::BitwuzlaSolver
 Solver engine using Bitwuzla. More...
 
interface  triton::engines::solver::SolverEngine
 This class is used to interface with solvers. More...
 
interface  triton::engines::solver::SolverInterface
 This interface is used to interface with solvers. More...
 
class  triton::engines::solver::SolverModel
 This class is used to represent a constraint model solved. More...
 
class  triton::engines::solver::Z3Solver
 Solver engine using z3. More...
 

Enumerations

enum  triton::engines::solver::solver_e { triton::engines::solver::SOLVER_INVALID = 0 , triton::engines::solver::SOLVER_CUSTOM , triton::engines::solver::SOLVER_Z3 , triton::engines::solver::SOLVER_BITWUZLA }
 
enum  triton::engines::solver::status_e {
  triton::engines::solver::UNSAT = 0 , triton::engines::solver::SAT = 1 , triton::engines::solver::TIMEOUT , triton::engines::solver::OUTOFMEM ,
  triton::engines::solver::UNKNOWN
}
 

Functions

std::ostream & triton::engines::solver::operator<< (std::ostream &stream, const SolverModel &model)
 Display a solver model.
 
std::ostream & triton::engines::solver::operator<< (std::ostream &stream, const SolverModel *model)
 Display a solver model.
 

Detailed Description

Enumeration Type Documentation

◆ solver_e

The different kind of solvers

Enumerator
SOLVER_INVALID 

invalid solver.

SOLVER_CUSTOM 

custom solver.

SOLVER_Z3 

z3 solver.

SOLVER_BITWUZLA 

bitwuzla solver.

Definition at line 39 of file solverEnums.hpp.

◆ status_e

The different kind of status

Enumerator
UNSAT 

UNSAT

SAT 

SAT

TIMEOUT 

TIMEOUT

OUTOFMEM 

MEMORY LIMIT REACHED

UNKNOWN 

UNKNOWN

Definition at line 51 of file solverEnums.hpp.

Function Documentation

◆ operator<<() [1/2]

TRITON_EXPORT std::ostream & triton::engines::solver::operator<< ( std::ostream &  stream,
const SolverModel model 
)

Display a solver model.

Definition at line 72 of file solverModel.cpp.

◆ operator<<() [2/2]

TRITON_EXPORT std::ostream & triton::engines::solver::operator<< ( std::ostream &  stream,
const SolverModel model 
)

Display a solver model.

Definition at line 78 of file solverModel.cpp.