klee
Public Member Functions | List of all members
klee::Z3Solver Class Reference

Z3Solver - A complete solver based on Z3. More...

#include <Z3Solver.h>

Inheritance diagram for klee::Z3Solver:
Inheritance graph
[legend]
Collaboration diagram for klee::Z3Solver:
Collaboration graph
[legend]

Public Member Functions

 Z3Solver ()
 Z3Solver - Construct a new Z3Solver. More...
 
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

Z3Solver - A complete solver based on Z3.

Definition at line 18 of file Z3Solver.h.

Constructor & Destructor Documentation

◆ Z3Solver()

klee::Z3Solver::Z3Solver ( )

Z3Solver - Construct a new Z3Solver.

Member Function Documentation

◆ getConstraintLog()

virtual char * klee::Z3Solver::getConstraintLog ( const Query &  )
virtual

Get the query in SMT-LIBv2 format.

Returns
A C-style string. The caller is responsible for freeing this.

Reimplemented from klee::Solver.

◆ setCoreSolverTimeout()

virtual void klee::Z3Solver::setCoreSolverTimeout ( time::Span  timeout)
virtual

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

Reimplemented from klee::Solver.

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