klee
 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

ExprSMTLIBPrinterprinter
 

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

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

Definition at line 45 of file SMTLIBLoggingSolver.cpp.

References klee::createSMTLIBPrinter().

Here is the call graph for this function:

SMTLIBLoggingSolver::~SMTLIBLoggingSolver ( )
inline

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

Implements QueryLoggingSolver.

Definition at line 23 of file SMTLIBLoggingSolver.cpp.

Member Data Documentation

ExprSMTLIBPrinter* SMTLIBLoggingSolver::printer
private

Definition at line 21 of file SMTLIBLoggingSolver.cpp.


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