about summary refs log tree commit diff homepage
path: root/lib/Solver
AgeCommit message (Collapse)Author
2015-03-10Altered DenseSet and IndependentElementSet to record ref<Expr> involvedEric Rizzi
This is important for future changes to IndependentSolver:: getInitialValues() so that an incoming constraint can be broken down into its smallest possible parts. Each of these individual parts may then be solved for and then the solutions to each piece combined to create a final answer. Finally, several fields which had previously been private are now public to facilitate the smaller solutions being combined into a larger solution.
2014-12-09Merge pull request #186 from paulmar/fixshiftCristian Cadar
Fix overshift check
2014-12-08Fix overshift checkPaul Marinescu
Shifting by bitwidth-1 is valid
2014-12-03Handling overshift behaviour in MetaSMTBuilderHristina Palikareva
2014-12-02Implement :named and let abbreviation modes in ExprSMTLIBPrinterRaimondas Sasnauskas
* Set the default abbreviation mode to let (ExprSMTLIBPrinter::ABBR_LET) * Remove the now defunct ExprSMTLIBLetPrinter * Improve performance of ExprSMTLIBPrinter::scan() by keeping track of visited Expr to avoid visiting them again * Rename ExprSMTLIBPrinter::printQuery() to ExprSMTLIBPrinter::printQueryExpr()
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
- See comment, this is a gross workaround for Darwin's very small default limit on shared memory size. I'm not sure how big of a counterexample users can actually expect STP to solve in practice -- if there is a practical use for larger ones it would probably be good for us to write a fallback strategy.
2014-09-13[Solver] Ensure shared memory allocation failures are reported as errors, ↵Daniel Dunbar
not asserts.
2014-09-13Add KLEE specific DEBUG macros.Daniel Dunbar
- This allows us to build in +Asserts mode even when LLVM isn't (by disabling the checks in that mode). - Eventually it would be nice to just move off of LLVM's DEBUG infrastructure entirely and just have our own copy, but this works for now. - Fixes #150.
2014-09-12When building against libc++ (vs libstdcxx), use standard ↵Daniel Dunbar
unordered_{map,set} includes. - I'm not sure what the status of libstdcxx's c++11 support is. It may be we can just move over to <unordered_map> everywhere, but I don't have a Linux test machine handy at the moment.
2014-05-29Use LLVM DEBUG macro instead of #if 0 or #if DEBUGMartin Nowack
2014-05-29Remove #include <iostream> to avoid static constructorsMartin Nowack
iostream injects static constructor function into every compilation unit. Remove this to avoid it.
2014-05-29Refactoring from std::ostream to llvm::raw_ostreamMartin Nowack
According to LLVM: lightweight and simpler implementation of streams.
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 ↵Hristina Palikareva
MetaSMTBuilder.
2014-04-24Remove unused pointer to STPSolver in STPSolverImpl to silence clangDan Liew
warning.
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
2014-02-14Explicitly get the width of the "shift" expression rather than assumingDan Liew
that is the samw width of the "expr" expression. It probably is the same width (it defintely is in SMT-LIB but I'm not sure about STP) but it is probably better to be explicit.
2014-02-14Remove STPBuilder::getShiftBits() which is no longer used.Dan Liew
2014-02-14Fixed overshift of arithmetic right shift by constant so that itDan Liew
overshifts to zero. Test case is included.
2014-02-14Fixed overshift of arithmetic right shift by symbolic so that it overshiftsDan Liew
to zero. Test case is included.
2014-02-14Fixed overshift of logical right shift by constant so that itDan Liew
overshifts to zero. Test case is included.
2014-02-14Fixed overshift of logical right shift by symbolic so that it overshiftsDan Liew
to zero. Test case is included.
2014-02-14Fixed overshifting an expression by a constant so that we overshift toDan Liew
zero. A test case was added for this. In addition the use to vc_bvExtract() was removed for shifting left by an expression because we don't want/need bitmasked behaviour anymore.
2014-02-14Added a test case for testing overshift behaviour of Shl and fixedDan Liew
a bug in the previous commit where 32-bit width was assumed.
2014-02-14Translate shl overshifts into 0Paul Marinescu
The other shift operators still need to be changed
2013-12-21Do not install KLEE's internal libraries.Dan Liew
2013-10-11getConstraintLog() of MetaSMTSolver explicitly states that this feature is ↵Hristina Palikareva
not supported; a test case modified to not fail because of this.
2013-10-11Bug fix in MetaSMTBuilderHristina Palikareva
2013-10-11MetaSMT builder, solver and command-line options.Hristina Palikareva
2013-09-17Merge pull request #21 from delcypher/fix_query_loggingCristian Cadar
Fix queries not being logged correctly if an assertion failure is hit.
2013-08-28Fix constness warnings issued by gcc 4.7Martin Nowack
2013-08-23In QueryLoggingSolver call flush() on std::ofstream so that queriesDan Liew
get correctly logged if an assertion failure is hit later on.
2013-08-06Methods getConstraintLog() and setTimeout() made virtual and moved from ↵Hristina Palikareva
STPSolver to base Solver and SolverImpl classes, and consequently redefined in derived classes to call the corresponding methods down the solver chain. Method setTimeout() renamed to setCoreSolverTimeout().
2013-08-06Renaming solver-related command-line options in order to decouple them from ↵Hristina Palikareva
STP. More specifically, command-line options max-stp-time, use-forked-stp and stp-optimize-divides renamed to max-solver-time, use-forked-solver and solver-optimize-divides, respectively. Option of running the SMT solver in a separate process (i.e. forked) set to true by default. Options of running SMT solver forked and with optimized divides made available to Kleaver as well.
2013-07-11Fixed and improved the stats on (cex)cache hits and misses.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@186097 91177308-0d34-0410-b5e6-96231b3b80d8
2013-01-22Added a new option --ignore-solver-failures, disabled by default, toCristian Cadar
cause KLEE to terminate on fatal solver errors. Better documented the ulimit issue when STP seg faults. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@173187 91177308-0d34-0410-b5e6-96231b3b80d8
2013-01-02Forgot to add QueryLoggingSolver in patch 171387 from Tomasz Kuchta.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@171392 91177308-0d34-0410-b5e6-96231b3b80d8
2013-01-02Patch by Tomasz Kuchta adding more detailed information on query failures.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@171391 91177308-0d34-0410-b5e6-96231b3b80d8
2013-01-02Patch by Tomasz Kuchta that refactors the logging code, by introducing a new ↵Cristian Cadar
logging class hierarchy. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@171387 91177308-0d34-0410-b5e6-96231b3b80d8
2013-01-02Patch by Tomasz Kuchta adding a new option (min-query-time-to-log) that ↵Cristian Cadar
enables KLEE to log only the queries exceeding a certain duration, or only those that time out. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@171385 91177308-0d34-0410-b5e6-96231b3b80d8
2012-10-24Patch by Dan Liew: "Added SMTLIBLoggingSolver for logging queries in ↵Cristian Cadar
SMT-LIBv2 format." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166564 91177308-0d34-0410-b5e6-96231b3b80d8
2012-10-18Nice patch by Hristina Palikareva that removes the dependency on STPCristian Cadar
arrays from the Array and UpdateNode classes. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166214 91177308-0d34-0410-b5e6-96231b3b80d8
2012-07-31Patch by Dan Liew that removes our internal copy of STP, and makes the ↵Cristian Cadar
--with-stp option mandatory: "1. At configure time the --with-stp= option is now mandatory. 2. The HAVE_EXT_STP macro has been removed. 3. The ENABLE_EXT_STP autoconf replacement variable has been removed and consequently the Makefile variable of the same name has been removed." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@161055 91177308-0d34-0410-b5e6-96231b3b80d8
2012-06-01Patch by Oscar Dustmann fixing a buffer overflow when long names areCristian Cadar
used: "patch for STPBuilder.cpp that allows for arbitrary length symbol names while still limiting the unique string to 32 bytes." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@157820 91177308-0d34-0410-b5e6-96231b3b80d8
2012-03-26STPBuilder: fix getShiftBits properly.Peter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@153475 91177308-0d34-0410-b5e6-96231b3b80d8
2012-03-26STPBuilder: fix bv{Zero,One,MinusOne} for the case where width>64Peter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@153474 91177308-0d34-0410-b5e6-96231b3b80d8
2012-03-26STPBuilder: fix ConstantExpr builder for the case where width>64 butPeter Collingbourne
is not a multiple of 64. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@153473 91177308-0d34-0410-b5e6-96231b3b80d8
2011-12-13Fix STPBuilder::getShiftBits for non-power-of-2 bitwidths up to 64.Peter Collingbourne
(Yes, we should really be handling more bitwidths here.) git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@146510 91177308-0d34-0410-b5e6-96231b3b80d8
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-07-17 15:44:56 +0000