klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
klee::STPSolver Class Reference

STPSolver - A complete solver based on STP. More...

#include <Solver.h>

Inheritance diagram for klee::STPSolver:
Collaboration diagram for klee::STPSolver:

Public Member Functions

 STPSolver (bool useForkedSTP, bool optimizeDivides=true)
 
virtual char * getConstraintLog (const Query &)
 
virtual void setCoreSolverTimeout (double timeout)
 
- Public Member Functions inherited from klee::Solver
 Solver (SolverImpl *_impl)
 
virtual ~Solver ()
 
bool evaluate (const Query &, Validity &result)
 
bool mustBeTrue (const Query &, bool &result)
 
bool mustBeFalse (const Query &, bool &result)
 
bool mayBeTrue (const Query &, bool &result)
 
bool mayBeFalse (const Query &, bool &result)
 
bool getValue (const Query &, ref< ConstantExpr > &result)
 
bool getInitialValues (const Query &, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &result)
 
virtual std::pair< ref< Expr >
, ref< Expr > > 
getRange (const Query &)
 

Additional Inherited Members

- Public Types inherited from klee::Solver
enum  Validity { True = 1, False = -1, Unknown = 0 }
 
- Static Public Member Functions inherited from klee::Solver
static const char * validity_to_str (Validity v)
 validity_to_str - Return the name of given Validity enum value. More...
 
- Public Attributes inherited from klee::Solver
SolverImplimpl
 

Detailed Description

STPSolver - A complete solver based on STP.

Definition at line 203 of file Solver.h.

Constructor & Destructor Documentation

STPSolver::STPSolver ( bool  useForkedSTP,
bool  optimizeDivides = true 
)

STPSolver - Construct a new STPSolver.

Parameters
useForkedSTP- Whether STP should be run in a separate process (required for using timeouts).
optimizeDivides- Whether constant division operations should be optimized into add/shift/multiply operations.

Definition at line 565 of file Solver.cpp.

Member Function Documentation

char * STPSolver::getConstraintLog ( const Query query)
virtual

getConstraintLog - Return the constraint log for the given state in CVC format.

Reimplemented from klee::Solver.

Definition at line 570 of file Solver.cpp.

References klee::SolverImpl::getConstraintLog(), and klee::Solver::impl.

Here is the call graph for this function:

void STPSolver::setCoreSolverTimeout ( double  timeout)
virtual

setCoreSolverTimeout - Set constraint solver timeout delay to the given value; 0 is off.

Reimplemented from klee::Solver.

Definition at line 574 of file Solver.cpp.

References klee::Solver::impl, and klee::SolverImpl::setCoreSolverTimeout().

Here is the call graph for this function:


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