klee
|
Z3Solver - A complete solver based on Z3. More...
#include <Z3Solver.h>
Public Member Functions | |
Z3Solver () | |
Z3Solver - Construct a new Z3Solver. More... | |
virtual char * | getConstraintLog (const Query &) |
virtual void | setCoreSolverTimeout (time::Span timeout) |
![]() | |
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 | |
![]() | |
enum | Validity { True = 1 , False = -1 , Unknown = 0 } |
![]() | |
static const char * | validity_to_str (Validity v) |
validity_to_str - Return the name of given Validity enum value. More... | |
![]() | |
SolverImpl * | impl |
Z3Solver - A complete solver based on Z3.
Definition at line 18 of file Z3Solver.h.
|
virtual |
Get the query in SMT-LIBv2 format.
Reimplemented from klee::Solver.
|
virtual |
setCoreSolverTimeout - Set constraint solver timeout delay to the given value; 0 is off.
Reimplemented from klee::Solver.