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/STPSolver.h | |
parent | 3ae967137fc715ff4ae5109895771fd1ca0724e4 (diff) | |
download | klee-e3b88631ef58ad406ac069bd3a4ba16fb4aa07cc.tar.gz |
hide backend solver declarations from public include
Diffstat (limited to 'lib/Solver/STPSolver.h')
-rw-r--r-- | lib/Solver/STPSolver.h | 39 |
1 files changed, 39 insertions, 0 deletions
diff --git a/lib/Solver/STPSolver.h b/lib/Solver/STPSolver.h new file mode 100644 index 00000000..cb68ed91 --- /dev/null +++ b/lib/Solver/STPSolver.h @@ -0,0 +1,39 @@ +//===-- STPSolver.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_STPSOLVER_H +#define KLEE_STPSOLVER_H + +#include "klee/Solver.h" + +namespace klee { +/// STPSolver - A complete solver based on STP. +class STPSolver : public Solver { +public: + /// STPSolver - Construct a new STPSolver. + /// + /// \param useForkedSTP - Whether STP should be run in a separate process + /// (required for using timeouts). + /// \param optimizeDivides - Whether constant division operations should + /// be optimized into add/shift/multiply operations. + STPSolver(bool useForkedSTP, bool optimizeDivides = true); + + /// getConstraintLog - Return the constraint log for the given state in CVC + /// format. + virtual char *getConstraintLog(const Query &); + + /// setCoreSolverTimeout - Set constraint solver timeout delay to the given + /// value; 0 + /// is off. + virtual void setCoreSolverTimeout(double timeout); +}; +} + +#endif /* KLEE_STPSOLVER_H */ |