Age | Commit message (Collapse) | Author | |
---|---|---|---|
2023-04-21 | use unique_ptr all throughout the solver chain | Daniel Schemmel | |
2023-03-23 | stats: rename numQueries/Queries -> SolverQueries, add Queries | Frank Busse | |
2020-07-01 | Separate constraint set and constraint manager | Martin Nowack | |
2020-04-30 | Removed the Internal directory from include/klee | Cristian Cadar | |
2019-09-03 | Moved solver-related header files into a separate klee/Solver/ directory. | Cristian Cadar | |
2019-07-30 | Consolidated Expr-related include files into a single include/klee/Expr ↵ | Cristian Cadar | |
directory. This improves the organization of the code, and also makes it easier to reuse Expr outside KLEE. | |||
2019-06-04 | Remove parenthesis around returns, as reported and discussed in #891 | Cristian Cadar | |
2018-10-30 | Base time API upon std::chrono | Frank Busse | |
This should not change the behaviour of KLEE and mimics the old API. - functions moved from util into time namespace - uses time points and time spans instead of double - CLI arguments now have the form "3h5min8us" Changed command line parameters: - batch-time (double to string) - istats-write-interval (double to string) - max-instruction-time (double to string) - max-solver-time (double to string) - max-time (double to string) - min-query-time-to-log (double to string) - seed-time (double to string) - stats-write-interval (double to string) - uncovered-update-interval (double to string) - added: log-timed-out-queries (replaces negative max-solver-time) | |||
2017-10-17 | [cmake] detect available metaSMT backends using a pre-defined flag and raise ↵ | Hoang M. Le | |
compile flags accordingly | |||
2017-10-17 | add support for CVC4 and Yices2 via metaSMT | Hoang M. Le | |
2017-06-02 | hide backend solver declarations from public include | Hoang M. Le | |
2017-06-02 | replace handleMetaSMT() with klee::createMetaSMTSolver() and move it into ↵ | Hoang M. Le | |
MetaSMTSolver.cpp so that the backend headers only need to be included once there | |||
2016-10-27 | apply clang-format | Hoang M. Le | |
2016-10-27 | update comments | Hoang M. Le | |
2016-10-27 | upgrade to boolector-2.2.0 & remove the no longer needed aux array vector | Hoang M. Le | |
2016-10-26 | move the query creation part into runAndGetCex() (to be consistent with ↵ | Hoang M. Le | |
runAndGetCexForked()) | |||
2016-10-26 | change signature of runAndGetCex() to match runAndGetCexForked() | Hoang M. Le | |
2016-10-26 | remove outdated FIXME (metaSMT-Z3 implements assumption via push/pop) | Hoang M. Le | |
2016-09-26 | Modified logging information to steer the usage of klee_message, ↵ | Andrea Mattavelli | |
klee_warning, and klee_error | |||
2016-08-03 | fprintf: convert to klee_warning | Jiri Slaby | |
In some Solver sources, some error outputs were missing \n. Instead of adding a new line to all of them, convert the fprintf's to klee_warning which adds \n automatically. ErrorHandling.h had to be included in MetaSMTSolver.cpp to have klee_warning declared there. Signed-off-by: Jiri Slaby <jslaby@suse.cz> | |||
2016-06-10 | clean up metaSMT includes | Hoang M. Le | |
2016-01-14 | MetaSMT build fixes. | Dan Liew | |
2016-01-14 | Make it possible to build KLEE without using STP and only MetaSMT. | Dan Liew | |
The default core solver is STP if KLEE is built with STP otherwise it is MetaSMT. Whilst I'm here rename SUPPORT_METASMT macro to ENABLE_METASMT for consistency. | |||
2016-01-12 | Refactor MetaSMTSolver and MetaSMTSolverImpl out of Solver.cpp into | Dan Liew | |
their own file ``MetaSMTSolver.cpp``. Whilst I'm here also clang-format the modified code. This might not be a NFC (non functional change) as there's a good chance this has broken the MetaSMT build of KLEE. I don't have a build of MetaSMT to hand and there is no TravisCI build. At this point because there is no maintainer for this code I think we should consider removing it as it is going bitrot. |