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

Public Member Functions

 SMTLIBLoggingSolver (Solver *_solver, std::string path, int queryTimeToLog)
 ~SMTLIBLoggingSolver ()
- 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

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

Definition at line 17 of file SMTLIBLoggingSolver.cpp.

Constructor & Destructor Documentation

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

Definition at line 45 of file SMTLIBLoggingSolver.cpp.

References klee::createSMTLIBPrinter().

Here is the call graph for this function:

SMTLIBLoggingSolver::~SMTLIBLoggingSolver ( )

Definition at line 56 of file SMTLIBLoggingSolver.cpp.

Member Function Documentation

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

Implements QueryLoggingSolver.

Definition at line 23 of file SMTLIBLoggingSolver.cpp.

Member Data Documentation

ExprSMTLIBPrinter* SMTLIBLoggingSolver::printer

Definition at line 21 of file SMTLIBLoggingSolver.cpp.

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