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

enum triton::engines::solver::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

enum triton::engines::solver::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.