Inheritance diagram for SMTLIBLoggingSolver:

Collaboration diagram for SMTLIBLoggingSolver:

[legend]

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

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
ExprSMTLIBPrinter	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

This QueryLoggingSolver will log queries to a file in the SMTLIBv2 format and pass the query down to the underlying solver.

Definition at line 18 of file SMTLIBLoggingSolver.cpp.

Constructor & Destructor Documentation

◆ SMTLIBLoggingSolver()

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

inline

Definition at line 46 of file SMTLIBLoggingSolver.cpp.

References QueryLoggingSolver::logBuffer, printer, and klee::ExprSMTLIBPrinter::setOutput().

Here is the call graph for this function:

Member Function Documentation

◆ printQuery()

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