about summary refs log tree commit diff homepage
path: root/lib/Solver
AgeCommit message (Collapse)Author
2023-04-21use unique_ptr in StagedSolverImplDaniel Schemmel
2023-04-21use unique_ptr in Z3SolverImplDaniel Schemmel
2023-04-21use unique_ptr in ValidatingSolverDaniel Schemmel
2023-04-21use unique_ptr in STPSolverImplDaniel Schemmel
2023-04-01remove include/klee/Support/IntEvaluation.hDaniel Schemmel
2023-03-23stats: rename numQueries/Queries -> SolverQueries, add QueriesFrank Busse
2023-03-22STP: add option to switch SAT solver: --stp-sat-solver and set default to ↵Frank Busse
CryptoMinisat
2023-03-22Change `llvm_map_components_to_libnames` to `llvm_config` CMake functionMartin Nowack
With recent LLVM versions, this should allow to link against dynamic LLVM libraries.
2023-03-17[cmake] Use LLVM's CMake functionality onlyMartin Nowack
LLVM became more complex, use LLVM's CMake functionality directly instead of replicating this behaviour in KLEE's build system. Use the correct build flags provided by LLVM itself. This is influenced by the way LLVM is built in the first place. Remove older CMake support (< 3.0).
2023-03-16The KDAlloc slot allocator is useful for small sized allocationsDaniel Schemmel
2022-08-26Use true instead of Z3_TRUE (removed in z3 4.11.0)Jerry James
2022-07-04Fix memory leak in crosscheck core solver mechanismDaniel Schemmel
2022-06-30remove LLVM < 9Frank Busse
2022-06-28Implement getArrayForUpdate iterativelyDaniel Schemmel
2022-06-15Spelling Fixesm-davis
2022-03-17remove obsolete KLEE_LLVM legacy definesJulian Büning
2021-03-04[Z3] Handle the case when interruption caught by Z3Pavel Yatcheniy
2020-11-12Ref: implement operator bool()Julian Büning
2020-07-01Separate constraint set and constraint managerMartin Nowack
2020-05-01[Solver:STP] Fix handling of array namesMartin Nowack
Array names used for STP queries used to be restricted to 32 characters, with the last characters replaced by a unique number. Similarly, an array is made unique by `klee_make_symbolic`. Unfortunately, both combined can lead to the generation of the same STP array name for different arrays. This leads to wrong queries with invalid results. This is more likely be triggered with longer names for `klee_make_symbolic` Fixes #1257
2020-04-30Moved header files that were placed directly in include/klee/ into ↵Cristian Cadar
appropriate existing directories and a new directory Statistics; a few missing renames.
2020-04-30Removed include/klee/util and moved header files to appropriate placesCristian Cadar
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
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-28 15:52:16 +0000