about summary refs log tree commit diff homepage
path: root/lib/Solver
AgeCommit message (Collapse)Author
2020-04-30Removed the Internal directory from include/kleeCristian Cadar
2020-04-08stats: rename QueriesConstructs to QueryConstructsFrank Busse
2020-04-08stats: remove queryConstructTime (unused)Frank Busse
2020-03-27Ensure that temp_builder is used when adding constant array value assertion ↵Daniel Grumberg
constraints
2020-02-19Use `ref<>` for MemoryObject handlingMartin Nowack
This uses the `ref<>`-based memory handling of MemoryObjects. This makes it explicit that references are held in: - ExecutionState::symbolics - ObjectState
2020-02-19Use `ref<>` for UpdateNodeMartin Nowack
Remove additional reference counting as part of UpdateNodeList and UpdateNode. Simplifies code.
2020-02-13Replace old TR1 implementations of unordered_map/set with std::* versionsMartin Nowack
TR1 implementation got replaced by the std::* equivalents with C++11. Start to use the standard versions instead of the old ones.
2020-01-28updatecomet
2019-10-31support compilation against LLVM 9.0Julian Büning
2019-09-03Moved solver-related header files into a separate klee/Solver/ directory.Cristian Cadar
2019-09-03Moved ConstructSolverChain.cpp to the Solver library.Cristian Cadar
2019-09-03Renamed CmdLineOptions.cpp to SolverCmdLine.cpp (in line with the associated ↵Cristian Cadar
header SolverCmdLine.h) and moved it to the Solver library.
2019-07-30Consolidated 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-07-23Refactor ConstraintManager to more modern coding standardsDaniel Schemmel
Eliminates -Wdeprecated-copy warnings Performed clang-format on touched file
2019-07-23Refactor ValueRange to more modern coding standardsDaniel Schemmel
Eliminates -Wdeprecated-copy warnings Performed partia clang-format on touched file
2019-06-04make endif guard naming consistentJulian Büning
2019-06-04make include guard naming consistentJulian Büning
2019-06-04Fixed identifiers used in ifdefs to (1) not use reserved names and (2) use a ↵Cristian Cadar
consistent naming convention
2019-06-04Remove parenthesis around returns, as reported and discussed in #891Cristian Cadar
2019-03-20STPSolver: C++11, add missing free, refactoringFrank Busse
2019-03-13Renamed --use-construct-hash to --use-construct-hash-stp and moved it and ↵Cristian Cadar
use-construct-hash-z3 to the expression building/printing category
2019-03-13Consistently use "default=true" and "default=false" instead of "default=on" ↵Cristian Cadar
and "default=off" in --help
2019-03-13Added options in QueryLoggingSolver.cpp to the constraint solving categoryCristian Cadar
2019-03-13Added options in CexCachingSolver.cpp to the constraint solving category and ↵Cristian Cadar
improved help messages
2019-03-11Replaced "default=off" with "default=false"MartinNowack
Co-Authored-By: ccadar <c.cadar@imperial.ac.uk>
2019-03-11Added options in STPSolver.cpp to the constraint solving categoryCristian Cadar
2019-03-11Added Z3 options to the constraint solving categoryCristian Cadar
2019-01-15make AssignmentLessThan::operator() const-invocableJulian Büning
2018-10-30Base time API upon std::chronoFrank 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)
2018-10-23refactor klee_open_output_file to return std::unique_ptrJulian Büning
and introduce klee_open_compressed_output_file with similar behavior along some other minor improvements
2018-10-23use klee_open_output_file for uncompressed logsJulian Büning
2018-10-16Renamed klee/CommandLine.h to klee/SolverCmdLine.h, since this file is meant ↵Cristian Cadar
to have only solver options.
2018-09-20Silence an uninitialized variable compiler warning (and a tiny formatting ↵Cristian Cadar
change)
2018-07-04Fix compiler warnings if assertions are disabledMartin Nowack
2018-05-21stop using DEBUG macro nameJiri Slaby
This is too generic and llvm 6.0 defines DEBUG as follows: #define DEBUG(X) DEBUG_WITH_TYPE(DEBUG_TYPE, X) This then results in various build failures where once the macro is defined, once it is not. So rename this generic macro to KLEE_ARRAY_DEBUG. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-05-15remove QueryLog.hFrank Busse
2018-05-09Improve handling of constant array in Z3Timotej Kapus
2017-10-17[cmake] detect available metaSMT backends using a pre-defined flag and raise ↵Hoang M. Le
compile flags accordingly
2017-10-17add support for CVC4 and Yices2 via metaSMTHoang M. Le
2017-10-04Remove Autoconf/Makefile build system and adjust the TravisCIDan Liew
configuration, TravisCI scripts and Dockerfile build appropriately. There are a bunch of clean ups this enables but this commit doesn't attempt them. We can do that in future commits.
2017-07-08Corrected comment of Z3Solver classAndrew Santosa
2017-06-02hide backend solver declarations from public includeHoang M. Le
2017-06-02replace 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
2017-06-01[Z3] Remove unused include.Dan Liew
2017-06-01[Z3] Add `-debug-z3-verbosity=<N>` option which behaves like Z3's `-v:<N>` ↵Dan Liew
option. This lets us see what Z3 is doing execution (e.g. which tactic is being applied) which is very useful for debugging.
2017-06-01[Z3] Switch from `Z3_mk_simple_solver()` to `Z3_mk_solver()`.Dan Liew
My discussions [1] with the Z3 team have revealed that `Z3_mk_simple_solver()` is the wrong solver to use. That solver basically runs the `simplify` tactic and then the `smt` tactic. This by-passes Z3's attempt to probe for different logics and apply its own specialized tactic. Using `Z3_mk_solver()` should be closer to the behaviour of the Z3 binary. This partially addresses #653. We still need to try rolling our own custom tactic. [1] https://github.com/Z3Prover/z3/issues/1035
2017-06-01[Z3] In `getConstraintLog()` use a separate builder from that of theDan Liew
solver. This is to avoid tampering with the cache of the builder the solver is using.
2017-06-01[Z3] Implement API logging.Dan Liew
Add `-debug-z3-log-api-interaction` option to allow Z3 API calls to be logged to a file. The files logged by this option can be replayed by the `z3` binary (using its `-log` option). This is incredibly useful because it allows to exactly replay Z3's behaviour outside of KLEE.
2017-06-01[Z3] Add option to manually validate Z3 models.Dan Liew
This can be enabled by passing the command line option `-debug-z3-validate-models`. Although Z3 has a global parameter `model_validate` (off by default) I don't trust it so do the validation manually. This also means we can potentially do validation on a per Z3Solver instance basis rather than globally. When failing to validate a Z3 model the solver state and model are dumped to standard error.
2017-06-01[Z3] Add the `-debug-z3-dump-queries=<path>` command line option. ThisDan Liew
is useful for getting access to the constraints being stored in the Z3 solver in the SMT-LIBv2.5 format.
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-07-17 16:25:55 +0000