about summary refs log tree commit diff homepage
path: root/lib/Solver
AgeCommit message (Expand)Author
2016-02-23Added missing copyright headers per klee/issue #301Marko Dimjašević
2016-02-14Handle Z3 API change between 4.4.1 and the current master branchDan Liew
2016-02-14Add basic implementation of Z3Builder and Z3Solver and Z3SolverImplDan Liew
2016-02-10Add some of the basic plumbing required to support a Z3 solver in KLEE.Dan Liew
2016-01-14MetaSMT build fixes.Dan Liew
2016-01-14Make it possible to build KLEE without using STP and only MetaSMT.Dan Liew
2016-01-12Refactor setting the core solver (i.e. STP, MetaSMT or DummySolver) by providingDan Liew
2016-01-12Drop unnecessary ``#include``s from Solver.cpp.Dan Liew
2016-01-12Refactor MetaSMTSolver and MetaSMTSolverImpl out of Solver.cpp intoDan Liew
2016-01-12[NFC] Refactor STPSolver and STPSolverImpl out of Solver.cpp into theirDan Liew
2016-01-12[NFC] Refactor DummySolver out of Solver.cpp into its own fileDan Liew
2016-01-12[NFC] Refactor ValidatingSolver out of Solver.cpp into its own fileDan Liew
2016-01-07[NFC] Refactor SolverImpl out of Solver.cpp into its own fileDan Liew
2015-12-23Fix memory leak detected by ASan whenDan Liew
2015-12-23[NFC]Dan Liew
2015-12-18Move lib/Solver/SolverStats.h -> include/klee/SolverStats.hDan Liew
2015-12-17[Solver]Add support to dump STP qeries usingMartin Nowack
2015-12-17Report fatal error in case CexCache Bindings do not matchMartin Nowack
2015-12-17[Solver]Add simple option to dump queriesMartin Nowack
2015-12-17Refactoring: Moving klee_warning/_error functions to ErrorHandling in Support...Martin Nowack
2015-12-04Remove dead ifdef in STPBuilder header file. There is noDan Liew
2015-12-04Remove dead ``tempVars`` and ``getTempVar()`` method in STPBuilderDan Liew
2015-09-22[STPBuilder] Generate SRrem expressions correctlyMartin Nowack
2015-09-21Merge pull request #274 from MartinNowack/fix_sdiv_1Cristian Cadar
2015-09-05Allow to generate initial values with empty constraint setMartin Nowack
2015-08-30Fix signed division by constant 1/ -1Martin Nowack
2015-08-03Merge pull request #198 from holycrap872/IndependentSolverGetInitialValuesCristian Cadar
2015-07-06Make the super-set check in CexCachingSolver default offEric Rizzi
2015-04-01Added the function IndependentSolver::createdPointEvaluatesToTrueEric Rizzi
2015-04-01Commit of improved IndependentSolver::getIniitalValues().Eric Rizzi
2015-04-01Added the ability to solve for all factors in a particular query.Eric Rizzi
2015-03-20[Solver] Fix leak intermediate expression not freedMartin Nowack
2015-03-10Altered DenseSet and IndependentElementSet to record ref<Expr> involvedEric Rizzi
2014-12-09Merge pull request #186 from paulmar/fixshiftCristian Cadar
2014-12-08Fix overshift checkPaul Marinescu
2014-12-03Handling overshift behaviour in MetaSMTBuilderHristina Palikareva
2014-12-02Implement :named and let abbreviation modes in ExprSMTLIBPrinterRaimondas Sasnauskas
2014-09-14Fix compilation error due to change in raw_fd_ostream for LLVM3.5Dan Liew
2014-09-13[Solver] Tune down the shared memory region size on Darwin.Daniel Dunbar
2014-09-13[Solver] Ensure shared memory allocation failures are reported as errors, not...Daniel Dunbar
2014-09-13Add KLEE specific DEBUG macros.Daniel Dunbar
2014-09-12When building against libc++ (vs libstdcxx), use standard unordered_{map,set}...Daniel Dunbar
2014-05-29Use LLVM DEBUG macro instead of #if 0 or #if DEBUGMartin Nowack
2014-05-29Remove #include <iostream> to avoid static constructorsMartin Nowack
2014-05-29Refactoring from std::ostream to llvm::raw_ostreamMartin Nowack
2014-04-24Fixed order of domain and range in array creation in MetaSMTBuilder.Hristina Palikareva
2014-04-24Fixed creation of arrays with variable domains and ranges in STPBuilder and M...Hristina Palikareva
2014-04-24Remove unused pointer to STPSolver in STPSolverImpl to silence clangDan Liew
2014-04-16Removing a few more hard-coded values for domains and ranges of Array objectsHristina Palikareva
2014-04-15Associate a domain and range with each arrayPeter Collingbourne