| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-05-16 | Fix error in Windows build | Andres Noetzli | |
| The Windows build was missing the `print_statistics()` function, this commit moves the function out of the `#ifndef __WIN32__` guard. | |||
| 2017-05-15 | Merge pull request #156 from 4tXJ7f/fix_safe_print | Andrew Reynolds | |
| Minor fix in safe_print function | |||
| 2017-05-15 | Minor fix in safe_print function | Andres Noetzli | |
| This commit fixes two issues reported by Coverity: - Fixes the check whether the buffer is full in safe_print_hex - Removes dead code in safe_print for floating-point values Additionally, it fixes an issue reported by Andy where the names of the statistics were printed as "<unsupported>" due to calling the const char* version instead of the std::string version of safe_print. Finally, this fixes an issue where --segv-spin would not print the program name because it was a const char*. The program name is now stored as a string. NOTE: As a side effect, the last part also fixes Coverity issue 1362944, which has been in CVC4 for a long time. | |||
| 2017-05-15 | Cleanup handling of division (possible fix for bugs 803, 804, 805). | ajreynol | |
| 2017-05-15 | Merge pull request #159 from 4tXJ7f/fix_set_types | Andrew Reynolds | |
| Fix type checks for relation operators | |||
| 2017-05-15 | Fix type checks for relation operators | Andres Noetzli | |
| This commit fixes an assertion error when applying transpose or transitive closure to a set instead of a relation. Instead it now prints a parse error. | |||
| 2017-05-15 | Merge pull request #158 from 4tXJ7f/fix_sets_rewriter | Andrew Reynolds | |
| Fix minor bug in sets rewriter | |||
| 2017-05-15 | Fix minor bug in sets rewriter | Andres Noetzli | |
| As reported by Coverity, one of the switches in the sets rewriter had a missing break. This could lead to an assertion failure when rewriting the cardinality of a transpose as in the test case included in this commit. | |||
| 2017-05-15 | Fix bug 806. Minor fixes to remove term formula pass. | ajreynol | |
| 2017-05-15 | Merge pull request #157 from 4tXJ7f/fix_iterator | Andrew Reynolds | |
| Fix condition in upwards closure check for sets | |||
| 2017-05-15 | Fix condition in upwards closure check for sets | Andres Noetzli | |
| Coverity reported this mismatched iterator. | |||
| 2017-05-15 | Fix issue in ceg_instantiator related to types and theoryOf, fixes bug 802. | ajreynol | |
| 2017-05-15 | Make conflict-based instantiation abort if a ground conflict is found in the ↵ | ajreynol | |
| master equality engine during term indexing, fixes bug 801. | |||
| 2017-05-12 | Make signal handlers safer | Andres Notzli | |
| As reported in bug 769, the signal handlers currently use unsafe functions such as dynamic memory allocations and fprintf. This commit fixes the issue by introducing functions for printing statistics in signal handlers (functions with the `safe` prefix). It also avoids copying statistics, which further avoids dynamic memory allocation. The safe printing of statistics has some limitations (it does not support SExprStats or printing CVC4::Result), which should not matter much in practice. Printing statistics in a non-signal handler is not affected by these changes as that uses a separate code path (the functions without the `safe` prefix). Additional changes: - Remove ListStat as it is not used anywhere - Add unit test for safe printing statistics | |||
| 2017-05-10 | Do not split on cardinality for string equivalence classes with non-constant ↵ | ajreynol | |
| lengths if disequalities already imply sufficient lower bound. Fixes bug 799. | |||
| 2017-05-09 | Change str.replace for empty string. | ajreynol | |
| 2017-05-05 | Do not eliminate extended arithmetic symbols when finite model finding is ↵ | ajreynol | |
| on, add regression. | |||
| 2017-05-05 | Fix error message. | ajreynol | |
| 2017-05-04 | skolemization manager may be called also when just unsatCores are on ↵ | guykatzz | |
| (related to bug 717) | |||
| 2017-05-04 | fixing bug 790: track dependencies when the unsatCores() option is on | guykatzz | |
| 2017-04-28 | Partial fix for bug 717.experiment | Clark Barrett | |
| 2017-04-28 | Minor fixes | ajreynol | |
| 2017-04-28 | Fix bug for real division. | ajreynol | |
| 2017-04-28 | Do not eliminate non-standard arithmetic operators in recursive function ↵ | ajreynol | |
| definitions, add regression. | |||
| 2017-04-24 | Fixes and simplifications for fmf mbqi. | ajreynol | |
| 2017-04-24 | Fix parsing selectors for nullary constructors in smtlib 2.6 format. | ajreynol | |
| 2017-04-22 | Updating TheoryArithPrivate::getDeltaValue() to eagerly use the partial ↵ | Tim King | |
| model value if exists. | |||
| 2017-04-21 | Merge pull request #151 from 4tXJ7f/fix_debug | Clark Barrett | |
| Move assertion out of loop for better performance | |||
| 2017-04-21 | Fix for bug 681 (now gives reasonable error message about using constant | Clark Barrett | |
| arrays). | |||
| 2017-04-21 | Move assertion out of loop for better performance | Andres Noetzli | |
| This is related to bug 508. The debug build was taking much longer than the production build to compute the result. The issue was an assertion in a loop in nonClausalSimplify(). By moving the assertion outside of the loop, the debug build is now roughly an order of magnitude slower than the production build (instead of two orders of magnitude), which seems to be roughly in line with the difference for other benchmarks: Debug version before change: - Bug (minified version): 1065.6s - regress3/friedman_n6_i4.smt: 6.9s - regress2/uflia-error0.smt2: 6.3s - regress2/fuzz_2.smt: 2.3s Debug version after change: - Bug (minified version): 131.4s - regress3/friedman_n6_i4.smt: 6.7s - regress2/uflia-error0.smt2: 6.2s - regress2/fuzz_2.smt: 1.9s Production version: - Bug (minified version): 18.8s - regress3/friedman_n6_i4.smt: 0.8s - regress2/uflia-error0.smt2: 0.8s - regress2/fuzz_2.smt: 0.2s | |||
| 2017-04-21 | Handle subtypes in sets. Bug fixes for tuples with subtypes. | ajreynol | |
| 2017-04-20 | Merge pull request #149 from PaulMeng/master | Andrew Reynolds | |
| Support for relational operators identity and join image | |||
| 2017-04-20 | Minor fixes. | ajreynol | |
| 2017-04-20 | Support for relational operators identity and join image | Paul Meng | |
| 2017-04-19 | Fix mktheoryrewriter and mktheorytraits for nullaryoperator. | ajreynol | |
| 2017-04-19 | Fixes for handling set universe: restrict upwards rule for universe to ↵ | ajreynol | |
| memberships into variable sets, do not variable eliminate sets during ppAssert. | |||
| 2017-04-18 | Merge pull request #147 from makaimann/coverage_fix | Clark Barrett | |
| Coverage fix | |||
| 2017-04-18 | Fix for bug 639. | Clark Barrett | |
| 2017-04-18 | Coverage fix | makaimann | |
| Forcing some make variables to be absolute paths lcov does not (officially) support relative paths src/expr and src/options in particular were breaking it | |||
| 2017-04-14 | Actively split for upwards closusure intersection. Minor clean up, add ↵ | ajreynol | |
| regressions. | |||
| 2017-04-14 | Fix bug related to portfolio with nullary operators. | ajreynol | |
| 2017-04-14 | Fix nullary operator printers, minor. | ajreynol | |
| 2017-04-14 | Fix for fmf-fun when the option is set by user command. | ajreynol | |
| 2017-04-13 | Fix for some compilers | Clark Barrett | |
| 2017-04-12 | Add nullary operator metakind. | ajreynol | |
| 2017-04-11 | Bug fix in conjecture generation for --quant-ind. | ajreynol | |
| 2017-04-07 | Change option names for nl. | ajreynol | |
| 2017-04-05 | Merge pull request #143 from FabianWolff/master | Clark Barrett | |
| Fix several spelling errors | |||
| 2017-04-05 | Fix bug 698. | ajreynol | |
| 2017-04-05 | Fixes for nlAlgSolveSubs. | ajreynol | |
 |
index : cvc5.git | |
| CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. | git repository hosting |
| summaryrefslogtreecommitdiff |
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback