Inheritance diagram for KQueryLoggingSolver:

Collaboration diagram for KQueryLoggingSolver:

[legend]

Public Member Functions
	KQueryLoggingSolver (Solver *_solver, std::string path, time::Span queryTimeToLog, bool logTimedOut)

virtual	~KQueryLoggingSolver ()

Public Member Functions inherited from QueryLoggingSolver
	QueryLoggingSolver (Solver *_solver, std::string path, const std::string &commentSign, time::Span queryTimeToLog, bool logTimedOut)

virtual	~QueryLoggingSolver ()

bool	computeTruth (const Query &query, bool &isValid)
	implementation of the SolverImpl interface More...

bool	computeValidity (const Query &query, Solver::Validity &result)

bool	computeValue (const Query &query, ref< Expr > &result)

bool	computeInitialValues (const Query &query, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &values, bool &hasSolution)

SolverRunStatus	getOperationStatusCode ()
	getOperationStatusCode - get the status of the last solver operation More...

char *	getConstraintLog (const Query &)

void	setCoreSolverTimeout (time::Span timeout)

Public Member Functions inherited from klee::SolverImpl
	SolverImpl ()

virtual	~SolverImpl ()

virtual bool	computeValidity (const Query &query, Solver::Validity &result)

virtual bool	computeTruth (const Query &query, bool &isValid)=0

virtual bool	computeValue (const Query &query, ref< Expr > &result)=0

virtual bool	computeInitialValues (const Query &query, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &values, bool &hasSolution)=0

virtual SolverRunStatus	getOperationStatusCode ()=0
	getOperationStatusCode - get the status of the last solver operation More...

virtual char *	getConstraintLog (const Query &query)

virtual void	setCoreSolverTimeout (time::Span timeout)

Private Member Functions
virtual void	printQuery (const Query &query, const Query falseQuery=0, const std::vector< const Array > *objects=0)

Private Attributes
ExprPPrinter *	printer

Additional Inherited Members
Public Types inherited from klee::SolverImpl
enum	SolverRunStatus { SOLVER_RUN_STATUS_SUCCESS_SOLVABLE , SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE , SOLVER_RUN_STATUS_FAILURE , SOLVER_RUN_STATUS_TIMEOUT , SOLVER_RUN_STATUS_FORK_FAILED , SOLVER_RUN_STATUS_INTERRUPTED , SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE , SOLVER_RUN_STATUS_WAITPID_FAILED }

Static Public Member Functions inherited from klee::SolverImpl
static const char *	getOperationStatusString (SolverRunStatus statusCode)

Protected Member Functions inherited from QueryLoggingSolver
virtual void	startQuery (const Query &query, const char typeName, const Query falseQuery=0, const std::vector< const Array * > *objects=0)

virtual void	finishQuery (bool success)

void	flushBuffer (void)

virtual void	printQuery (const Query &query, const Query falseQuery=0, const std::vector< const Array > *objects=0)=0

void	flushBufferConditionally (bool writeToFile)

Protected Attributes inherited from QueryLoggingSolver
Solver *	solver

std::unique_ptr< llvm::raw_ostream >	os

std::string	BufferString

llvm::raw_string_ostream	logBuffer

unsigned	queryCount

time::Span	minQueryTimeToLog

bool	logTimedOutQueries = false

time::Point	startTime

time::Span	lastQueryDuration

const std::string	queryCommentSign

Detailed Description

Definition at line 18 of file KQueryLoggingSolver.cpp.

Constructor & Destructor Documentation

◆ KQueryLoggingSolver()

KQueryLoggingSolver::KQueryLoggingSolver	(	Solver *	_solver,
		std::string	path,
		time::Span	queryTimeToLog,
		bool	logTimedOut
	)

inline

Definition at line 51 of file KQueryLoggingSolver.cpp.

◆ ~KQueryLoggingSolver()

virtual KQueryLoggingSolver::~KQueryLoggingSolver ( )

inlinevirtual

Definition at line 56 of file KQueryLoggingSolver.cpp.

References printer.

Member Function Documentation

◆ printQuery()

virtual void KQueryLoggingSolver::printQuery	(	const Query &	query,
		const Query *	falseQuery = `0`,
		const std::vector< const Array * > *	objects = `0`
	)