klee
Z3Solver.h
Go to the documentation of this file.
1//===-- Z3Solver.h
2//---------------------------------------------------===//
3//
4// The KLEE Symbolic Virtual Machine
5//
6// This file is distributed under the University of Illinois Open Source
7// License. See LICENSE.TXT for details.
8//
9//===----------------------------------------------------------------------===//
10
11#ifndef KLEE_Z3SOLVER_H
12#define KLEE_Z3SOLVER_H
13
14#include "klee/Solver/Solver.h"
15
16namespace klee {
18class Z3Solver : public Solver {
19public:
22
25 virtual char *getConstraintLog(const Query &);
26
30 virtual void setCoreSolverTimeout(time::Span timeout);
31};
32}
33
34#endif /* KLEE_Z3SOLVER_H */
Z3Solver - A complete solver based on Z3.
Definition: Z3Solver.h:18
virtual void setCoreSolverTimeout(time::Span timeout)
Z3Solver()
Z3Solver - Construct a new Z3Solver.
virtual char * getConstraintLog(const Query &)
Definition: main.cpp:291