Painless
A framework to ease parallelization of sequential CDCL SAT solvers
Loading...
Searching...
No Matches
Logger.hpp File Reference

Defines logging functions and macros for the SAT solver. More...

#include <atomic>
#include <memory>
#include <vector>
Include dependency graph for Logger.hpp:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Macros

#define BLUE   "\033[34m"
 
#define BOLD   "\033[1m"
 
#define CYAN   "\033[36m"
 
#define GREEN   "\033[32m"
 
#define MAGENTA   "\033[35m"
 
#define RED   "\033[31m"
 
#define RESET   "\033[0m"
 
#define WHITE   "\033[37m"
 
#define YELLOW   "\033[33m"
 
#define FUNC_STYLE   "\033[2m"
 
#define ERROR_STYLE   "\033[1m"
 
#define FUNCTION_NAME   "UnknownFunction"
 
#define LOG(level, ...)
 Log a message with a specified verbosity level.
 
#define LOGERROR(...)
 Log an error message.
 
#define PABORT(EXIT_CODE, ...)
 Log an error message and abort the program with a specified exit code.
 
#define LOGWARN(...)
 Log a warning message.
 
#define LOGSTAT(...)
 Log a statistics message.
 
#define LOG0(...)
 Log a message with verbosity level 0.
 
#define LOG1(...)
 Log a message with verbosity level 1.
 
#define LOG2(...)
 Log a message with verbosity level 2.
 
#define LOG3(...)
 Log a message with verbosity level 3.
 
#define LOG4(...)
 Log a message with verbosity level 4.
 
#define LOGVECTOR(lits, size, ...)
 Log a vector (clause) with cyan color.
 
#define LOGDEBUG1(...)
 Log a debug message with verbosity level 1 and blue color.
 
#define LOGDEBUG2(...)
 Log a debug message with verbosity level 2 and magenta color.
 
#define LOGDEBUG3(...)
 Log a debug message with verbosity level 4 and magenta color.
 
#define LOGCLAUSE1(lits, size, ...)
 Log a clause with verbosity level 2 and cyan color.
 
#define LOGCLAUSE2(lits, size, ...)
 Log a clause with verbosity level 5 and cyan color.
 

Functions

void setVerbosityLevel (int level)
 Set the verbosity level for logging.
 
void log (int verbosityLevel, const char *color, const char *fmt...)
 Log a message with a specified verbosity level and color.
 
void logDebug (int verbosityLevel, const char *color, const char *issuer, const char *fmt...)
 Log a debug message with a specified verbosity level, color, and issuer.
 
void logClause (int verbosityLevel, const char *color, const int *lits, unsigned int size, const char *fmt...)
 Log a clause with a specified verbosity level and color.
 
void logSolution (const char *string)
 Log the solution status of the SAT solver.
 
void lockLogger ()
 Acquire the logger mutex to ensure thread-safe logging.
 
void unlockLogger ()
 Release the logger mutex after logging.
 
void logModel (const std::vector< int > &model)
 Log the model (satisfying assignment) found by the SAT solver.
 

Variables

std::atomic< bool > quiet
 Global flag to enable/disable logging.
 

Detailed Description

Defines logging functions and macros for the SAT solver.

Macro Definition Documentation

◆ LOG

#define LOG ( level,
... )
Value:
do { \
log(level, RESET, __VA_ARGS__); \
} while (0)

Log a message with a specified verbosity level.

◆ LOG0

#define LOG0 ( ...)
Value:
do { \
log(0, RESET, __VA_ARGS__); \
} while (0)

Log a message with verbosity level 0.

◆ LOG1

#define LOG1 ( ...)
Value:
do { \
log(1, RESET, __VA_ARGS__); \
} while (0)

Log a message with verbosity level 1.

◆ LOG2

#define LOG2 ( ...)
Value:
do { \
log(2, RESET, __VA_ARGS__); \
} while (0)

Log a message with verbosity level 2.

◆ LOG3

#define LOG3 ( ...)
Value:
do { \
log(3, RESET, __VA_ARGS__); \
} while (0)

Log a message with verbosity level 3.

◆ LOG4

#define LOG4 ( ...)
Value:
do { \
log(4, RESET, __VA_ARGS__); \
} while (0)

Log a message with verbosity level 4.

◆ LOGCLAUSE1

#define LOGCLAUSE1 ( lits,
size,
... )
Value:
do { \
logClause(2, CYAN, lits, size, __VA_ARGS__); \
} while (0)

Log a clause with verbosity level 2 and cyan color.

◆ LOGCLAUSE2

#define LOGCLAUSE2 ( lits,
size,
... )
Value:
do { \
logClause(5, CYAN, lits, size, __VA_ARGS__); \
} while (0)

Log a clause with verbosity level 5 and cyan color.

◆ LOGDEBUG1

#define LOGDEBUG1 ( ...)
Value:
do { \
logDebug(1, BLUE, FUNCTION_NAME, __VA_ARGS__); \
} while (0)

Log a debug message with verbosity level 1 and blue color.

◆ LOGDEBUG2

#define LOGDEBUG2 ( ...)
Value:
do { \
logDebug(2, MAGENTA, FUNCTION_NAME, __VA_ARGS__); \
} while (0)

Log a debug message with verbosity level 2 and magenta color.

◆ LOGDEBUG3

#define LOGDEBUG3 ( ...)
Value:
do { \
logDebug(4, MAGENTA, FUNCTION_NAME, __VA_ARGS__); \
} while (0)

Log a debug message with verbosity level 4 and magenta color.

◆ LOGERROR

#define LOGERROR ( ...)
Value:
do { \
logDebug(0, RED, FUNCTION_NAME, __VA_ARGS__); \
} while (0)

Log an error message.

◆ LOGSTAT

#define LOGSTAT ( ...)
Value:
do { \
log(0, GREEN, __VA_ARGS__); \
} while (0)

Log a statistics message.

◆ LOGVECTOR

#define LOGVECTOR ( lits,
size,
... )
Value:
do { \
logClause(1, CYAN, lits, size, __VA_ARGS__); \
} while (0)

Log a vector (clause) with cyan color.

◆ LOGWARN

#define LOGWARN ( ...)
Value:
do { \
logDebug(0, YELLOW, FUNCTION_NAME, __VA_ARGS__); \
} while (0)

Log a warning message.

◆ PABORT

#define PABORT ( EXIT_CODE,
... )
Value:
do { \
logDebug(0, RED, FUNCTION_NAME, __VA_ARGS__); \
exit(EXIT_CODE); \
} while (0)

Log an error message and abort the program with a specified exit code.

Function Documentation

◆ log()

void log ( int verbosityLevel,
const char * color,
const char * fmt... )

Log a message with a specified verbosity level and color.

Parameters
verbosityLevelThe verbosity level of the message.
colorThe color to use for the message.
fmtThe format string for the message.
...Additional arguments for the format string.

◆ logClause()

void logClause ( int verbosityLevel,
const char * color,
const int * lits,
unsigned int size,
const char * fmt... )

Log a clause with a specified verbosity level and color.

Parameters
verbosityLevelThe verbosity level of the message.
colorThe color to use for the message.
litsPointer to an array of literals in the clause.
sizeThe number of literals in the clause.
fmtThe format string for the message.
...Additional arguments for the format string.

◆ logDebug()

void logDebug ( int verbosityLevel,
const char * color,
const char * issuer,
const char * fmt... )

Log a debug message with a specified verbosity level, color, and issuer.

Parameters
verbosityLevelThe verbosity level of the message.
colorThe color to use for the message.
issuerThe function or module issuing the log message.
fmtThe format string for the message.
...Additional arguments for the format string.

◆ logModel()

void logModel ( const std::vector< int > & model)

Log the model (satisfying assignment) found by the SAT solver.

Parameters
modelA vector of integers representing the satisfying assignment.

◆ logSolution()

void logSolution ( const char * string)

Log the solution status of the SAT solver.

Parameters
stringThe solution status string to log.

◆ setVerbosityLevel()

void setVerbosityLevel ( int level)

Set the verbosity level for logging.

Parameters
levelThe verbosity level to set.