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
16
namespace
klee
{
18
class
Z3Solver
:
public
Solver
{
19
public
:
21
Z3Solver
();
22
25
virtual
char
*
getConstraintLog
(
const
Query
&);
26
30
virtual
void
setCoreSolverTimeout
(
time::Span
timeout);
31
};
32
}
33
34
#endif
/* KLEE_Z3SOLVER_H */
Solver.h
klee::Solver
Definition:
Solver.h:60
klee::Z3Solver
Z3Solver - A complete solver based on Z3.
Definition:
Z3Solver.h:18
klee::Z3Solver::setCoreSolverTimeout
virtual void setCoreSolverTimeout(time::Span timeout)
klee::Z3Solver::Z3Solver
Z3Solver()
Z3Solver - Construct a new Z3Solver.
klee::Z3Solver::getConstraintLog
virtual char * getConstraintLog(const Query &)
klee
Definition:
main.cpp:291
klee::Query
Definition:
Solver.h:32
klee::time::Span
Definition:
Time.h:67
lib
Solver
Z3Solver.h
Generated by
1.9.3