klee
 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

ExprPPrinterprinter
 

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)
 
- Protected Attributes inherited from QueryLoggingSolver
Solversolver
 
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 
)
inline

Definition at line 53 of file PCLoggingSolver.cpp.

virtual PCLoggingSolver::~PCLoggingSolver ( )
inlinevirtual

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 
)
inlineprivatevirtual

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
private

Definition at line 23 of file PCLoggingSolver.cpp.


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