All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
PCLoggingSolver Class Reference
Inheritance diagram for PCLoggingSolver:
Collaboration diagram for PCLoggingSolver:

Public Member Functions

 PCLoggingSolver (Solver *_solver, std::string path, int queryTimeToLog)
virtual ~PCLoggingSolver ()
- Public Member Functions inherited from QueryLoggingSolver
 QueryLoggingSolver (Solver *_solver, std::string path, const std::string &commentSign, int queryTimeToLog)
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 (double timeout)
- Public Member Functions inherited from klee::SolverImpl
 SolverImpl ()
virtual ~SolverImpl ()

Private Member Functions

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

Private Attributes


Additional Inherited Members

- Public Types inherited from klee::SolverImpl
enum  SolverRunStatus {
- 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)
- Protected Attributes inherited from QueryLoggingSolver
std::string ErrorInfo
llvm::raw_fd_ostream os
std::string BufferString
llvm::raw_string_ostream logBuffer
unsigned queryCount
int minQueryTimeToLog
double startTime
double lastQueryTime
const std::string queryCommentSign

Detailed Description

Definition at line 20 of file PCLoggingSolver.cpp.

Constructor & Destructor Documentation

PCLoggingSolver::PCLoggingSolver ( Solver _solver,
std::string  path,
int  queryTimeToLog 

Definition at line 53 of file PCLoggingSolver.cpp.

virtual PCLoggingSolver::~PCLoggingSolver ( )

Definition at line 58 of file PCLoggingSolver.cpp.

Member Function Documentation

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

Implements QueryLoggingSolver.

Definition at line 25 of file PCLoggingSolver.cpp.

References klee::Query::constraints, klee::Query::expr, and klee::Array::size.

Member Data Documentation

ExprPPrinter* PCLoggingSolver::printer

Definition at line 23 of file PCLoggingSolver.cpp.

The documentation for this class was generated from the following file: