diff options
author | Hoang M. Le <hle@informatik.uni-bremen.de> | 2017-06-01 12:09:02 +0200 |
---|---|---|
committer | Dan Liew <delcypher@gmail.com> | 2017-06-02 12:52:55 +0100 |
commit | e3b88631ef58ad406ac069bd3a4ba16fb4aa07cc (patch) | |
tree | 008eaafce4f1c077d5d96d2ca2a5a81c57eb44d4 /lib/Solver/MetaSMTSolver.h | |
parent | 3ae967137fc715ff4ae5109895771fd1ca0724e4 (diff) | |
download | klee-e3b88631ef58ad406ac069bd3a4ba16fb4aa07cc.tar.gz |
hide backend solver declarations from public include
Diffstat (limited to 'lib/Solver/MetaSMTSolver.h')
-rw-r--r-- | lib/Solver/MetaSMTSolver.h | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/lib/Solver/MetaSMTSolver.h b/lib/Solver/MetaSMTSolver.h new file mode 100644 index 00000000..60d72383 --- /dev/null +++ b/lib/Solver/MetaSMTSolver.h @@ -0,0 +1,32 @@ +//===-- MetaSMTSolver.h +//---------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_METASMTSOLVER_H +#define KLEE_METASMTSOLVER_H + +#include "klee/Solver.h" + +namespace klee { + +template <typename SolverContext> class MetaSMTSolver : public Solver { +public: + MetaSMTSolver(bool useForked, bool optimizeDivides); + virtual ~MetaSMTSolver(); + + virtual char *getConstraintLog(const Query &); + virtual void setCoreSolverTimeout(double timeout); +}; + +/// createMetaSMTSolver - Create a solver using the metaSMT backend set by +/// the option MetaSMTBackend. +Solver *createMetaSMTSolver(); +} + +#endif /* KLEE_METASMTSOLVER_H */ |