about summary refs log tree commit diff homepage
path: root/lib/Solver
AgeCommit message (Expand)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 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
2019-06-04Fixed identifiers used in ifdefs to (1) not use reserved names and (2) use a ...Cristian Cadar
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 use...Cristian Cadar
2019-03-13Consistently use "default=true" and "default=false" instead of "default=on" a...Cristian Cadar
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
2019-03-11Replaced "default=off" with "default=false"MartinNowack
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 13:08:12 +0000