klee::MetaSMTSolver< SolverContext > Class Template Reference
#include <MetaSMTSolver.h>
Inheritance diagram for klee::MetaSMTSolver< SolverContext >:
Collaboration diagram for klee::MetaSMTSolver< SolverContext >:
Public Member Functions | |
| MetaSMTSolver (bool useForked, bool optimizeDivides) | |
| virtual | ~MetaSMTSolver () |
| virtual char * | getConstraintLog (const Query &) |
| virtual void | setCoreSolverTimeout (time::Span 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 &) |
| virtual char * | getConstraintLog (const Query &query) |
| virtual void | setCoreSolverTimeout (time::Span timeout) |
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 | |
| SolverImpl * | impl |
Detailed Description
template<typename SolverContext>
class klee::MetaSMTSolver< SolverContext >
class klee::MetaSMTSolver< SolverContext >
Definition at line 18 of file MetaSMTSolver.h.
Constructor & Destructor Documentation
◆ MetaSMTSolver()
template<typename SolverContext >
| klee::MetaSMTSolver< SolverContext >::MetaSMTSolver | ( | bool | useForked, |
| bool | optimizeDivides | ||
| ) |
◆ ~MetaSMTSolver()
template<typename SolverContext >
|
virtual |
Member Function Documentation
◆ getConstraintLog()
template<typename SolverContext >
|
virtual |
Reimplemented from klee::Solver.
◆ setCoreSolverTimeout()
template<typename SolverContext >
|
virtual |
Reimplemented from klee::Solver.
The documentation for this class was generated from the following file:
- /Users/cristic/klee/lib/Solver/MetaSMTSolver.h
