about summary refs log tree commit diff homepage
path: root/lib/Solver
AgeCommit message (Collapse)Author
2015-08-03Merge pull request #198 from holycrap872/IndependentSolverGetInitialValuesCristian Cadar
New version of the get initial values functionality which makes use of the independent solver.
2015-07-06Make the super-set check in CexCachingSolver default offEric Rizzi
The super-set check in the CexCachingSolver takes MUCH longer than the sub-set check. Upon closer inspection, the super-set check gets slower and slower as more counterexamples fill the UBTree. Pretty quickly, the cost of the super-set check becomes larger than the time required to simply bypass it and go to the Solver.
2015-04-01Added the function IndependentSolver::createdPointEvaluatesToTrueEric Rizzi
This function should be used solely in assertion statements and is intended as a sanity check to make sure that the solution constructed by IndependentSolver::getInitialValues() produces and answer that in fact satisfies the the query.
2015-04-01Commit of improved IndependentSolver::getIniitalValues().Eric Rizzi
Previous implementation simply passed the entire constraint forward without any factoring of the constraint at all. This is a problem since it is highly likely that there are cached solutions to pieces of the constraint. The new implementation breaks the entire constraint down into its requisite factors and passes each piece forward, one by one, down the solver chain. After an answer is returned, it is integrated into a larger solution. Since, by definition, no factor can affect another, we can safely create a solution to the larger constraint from the answers of its smaller pieces. The reconstruction of the solution is done by analyzing which parts of an array a factor touches. If the factor is the only one to reference a particular array, then all of the values calculated in the solution for that array are included in the final answer. If the factor references a particular element of the array (for example, arr[1]), then only the value in index 1 of array arr will be included in the solution.
2015-04-01Added the ability to solve for all factors in a particular query.Eric Rizzi
This functionality is necessary in order to more effectively handle calls to IndependentSolver::getInitialValues. An incoming query will be broken down into its smaller parts, and each piece will be solved for. At the end, the pieces will be recombined into a larger solution. The IndependentElementSet::getAllFactors() method takes a query and breaks it down into all of it's non-interacting factors. The IndependentElementSet::calculateArrays() method calculates which arrays are involved in a particular factor.
2015-03-20[Solver] Fix leak intermediate expression not freedMartin Nowack
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
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-04-05 12:13:41 +0000