about summary refs log tree commit diff homepage
path: root/lib/Solver
AgeCommit message (Expand)Author
2024-01-30Change `GetConstraintLog` to work with `std::string`s instead of `char*`sDaniel Schemmel
2024-01-30Avoid generating array names in solver builders that could accidently collideMartin Nowack
2023-09-07Remove broken experimental optimisation for validity (--cex-cache-exp)Cristian Cadar
2023-07-21Add code to only keep in the --help menu the KLEE/Kleaver option categoriesCristian Cadar
2023-04-21use unique_ptr all throughout the solver chainDaniel Schemmel
2023-04-21use unique_ptr in SolverDaniel Schemmel
2023-04-21use unique_ptr in QueryLoggingSolverDaniel Schemmel
2023-04-21use unique_ptr in IndependentSolverDaniel Schemmel
2023-04-21use unique_ptr in CexCachingSolverDaniel Schemmel
2023-04-21use unique_ptr in AssignmentValidatingSolverDaniel Schemmel
2023-04-21use unique_ptr in CachingSolverDaniel Schemmel
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 Cry...Frank Busse
2023-03-22Change `llvm_map_components_to_libnames` to `llvm_config` CMake functionMartin Nowack
2023-03-17[cmake] Use LLVM's CMake functionality onlyMartin Nowack
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
2020-04-30Moved header files that were placed directly in include/klee/ into appropriat...Cristian Cadar
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 c...Daniel Grumberg
2020-02-19Use `ref<>` for MemoryObject handlingMartin Nowack
2020-02-19Use `ref<>` for UpdateNodeMartin Nowack
2020-02-13Replace old TR1 implementations of unordered_map/set with std::* versionsMartin Nowack
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
2019-07-30Consolidated Expr-related include files into a single include/klee/Expr direc...Cristian Cadar
2019-07-23Refactor ConstraintManager to more modern coding standardsDaniel Schemmel
2019-07-23Refactor ValueRange to more modern coding standardsDaniel Schemmel
2019-06-04make endif guard naming consistentJulian Büning
2019-06-04make include guard naming consistentJulian Büning
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-05-20 04:58:06 +0000