| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-09-18 | Refactor strings extended functions inferences (#2480) | Andrew Reynolds | |
| This refactors the extended function inference step of TheoryStrings. It also generalizes a data member (d_pol) so that we track extended functions that are equal to constants for any type. This is in preparation for working on solving equations and further inferences in this style. | |||
| 2018-09-18 | Decision strategy: incorporate strings fmf. (#2485) | Andrew Reynolds | |
| 2018-09-17 | More aggressive skolem caching for strings, document and clean preprocessor ↵ | Andrew Reynolds | |
| (#2478) | |||
| 2018-09-17 | Make strings model construction robust to lengths that are not propagated ↵ | Andrew Reynolds | |
| equal (#2444) This fixes #2429. This was caused by arithmetic not notifying an equality between shared terms that it assigned to the same value. See explanation in comment. We should investigate a bit more why this is happening. I didnt think arithmetic was allowed to assign the same value to unpropagated shared length terms. I've opened issue https://github.com/CVC4/CVC4/issues/2443 to track this. Regardless, the strings model construction should be robust to handle this case, which this PR does. | |||
| 2018-09-14 | Add Skolem cache for strings, refactor length registration (#2457) | Andrew Reynolds | |
| This PR is in preparation for doing more aggressive caching of skolems (for example, in the strings preprocessor). It refactors sendLengthLemma -> registerLength, which unifies how length lemmas for skolems and other string terms are handled. | |||
| 2018-09-11 | Fix for when strings process loop is disabled. (#2456) | Andrew Reynolds | |
| 2018-08-30 | Add regular expression elimination module (#2400) | Andrew Reynolds | |
| 2018-08-26 | Use uniform length limit for String constants (#2381) | Andres Noetzli | |
| 2018-08-26 | Fix unsigned integer type issues in strings (#2380) | Andrew Reynolds | |
| * Fix unsigned integer types in strings. * Format | |||
| 2018-08-23 | Fixing some coverity warnings (#2357) | Andrew Reynolds | |
| 2018-08-09 | Fix char overflow issues in regular expression solver (#2275) | Andrew Reynolds | |
| 2018-08-06 | Make flat form inferences optional in strings (#2277) | Andrew Reynolds | |
| 2018-08-02 | Make strings robust to regular expression variables. (#2255) | Andrew Reynolds | |
| The theory solver for strings does not support regular expression variables. With this PR, we properly throw an exception if it is given one. However, the rewriter needs to handle regular expression variables (for various reasons: rewriting an expression before its asserted, sygus explanation generalization, etc.). This corrects a few miscellaneous issues in the strings rewriter to make it sound for these cases. It also corrects a seg fault in simpleRegexpConsume when testing memberships `(str.in.re "" R)`, where R is a *non-constant* regular expression (which will now be allowed if variables are allowed). This is in preparation for adding `RegLan` as a token to the smt2/sygus parsers. | |||
| 2018-07-06 | Split ext theory to own file and document (#1809) | Andrew Reynolds | |
| 2018-07-05 | Make string length lemmas more robust to rewriting (#2150) | Andrew Reynolds | |
| 2018-07-02 | Remove some dead code from theory strings (#2125) | Andrew Reynolds | |
| 2018-06-25 | Updated copyright headers. | Aina Niemetz | |
| 2018-05-21 | Infrastructure for strings strategies (#1883) | Andrew Reynolds | |
| 2018-05-08 | Support for str.<= and str.< (#1882) | Andrew Reynolds | |
| 2018-05-07 | Add support for str.code (#1821) | Andrew Reynolds | |
| 2018-04-16 | Make 256 the default cardinality for strings (#1783) | Andrew Reynolds | |
| 2018-04-15 | Make strings fmf apply to all but internally generated Skolems (#1780) | Andrew Reynolds | |
| 2018-04-15 | Fix type error with regexp (#1778) | Andrew Reynolds | |
| 2018-04-13 | Disable split for negative contains. (#1774) | Andrew Reynolds | |
| 2018-03-25 | Cleanup various exit calls (#1692) | Andrew Reynolds | |
| 2018-03-23 | Remove unused code (#1700) | Andrew Reynolds | |
| 2018-03-21 | Fix for string disequality processing (#1679) | Andrew Reynolds | |
| 2018-03-19 | Document inferences for strings (#1642) | Andrew Reynolds | |
| 2018-03-06 | Make statistics output consistent. (#1647) | Mathias Preiner | |
| * Fixes --hide-zero-stats (and really skips the 0 values) * Removes the additional newline after each statistic * Introduces theory::getStatsPrefix(TheoryId) to generate consistent prefixes for statistics based on the theory id (e.g., THEORY_BV -> "theory::bv"). | |||
| 2018-02-23 | Fix cd-simplification for strings (#1624) | Andrew Reynolds | |
| 2018-02-22 | Minor improvements to string rewriter (#1572) | Andrew Reynolds | |
| 2018-01-02 | Improve rewriter for string equality (#1427) | Andrew Reynolds | |
| 2017-12-08 | Make collect model info return a Bool (#1421) | Andrew Reynolds | |
| 2017-11-30 | Fixes for issue 1404 (#1409) | Andrew Reynolds | |
| 2017-09-11 | Adding reasonable breaks in switch statement in ↵ | Tim King | |
| TheoryStrings::normalizeRegexp. Minor code reorganization and applying clang-tidy to the function. (#1079) | |||
| 2017-09-11 | Addressing a coverity scan complaint in theory_strings.cpp. I believe the ↵ | Tim King | |
| root cause is that d_normal_forms_exp[r[0]] could have referred to different vectors (as operator[] is inserting for maps). (#1080) | |||
| 2017-09-05 | Remove support for conversions between uint32/uint16 and string. (#1069) | Andrew Reynolds | |
| * Remove support for conversions between uint32/uint16 and string. * Temporarily disable regression. | |||
| 2017-08-21 | Cleanup: use Assert rather than C assert. (#1052) | Aina Niemetz | |
| 2017-07-29 | Add support for charat in native language, minor cleanup. | ajreynol | |
| 2017-07-28 | Fix cache issues for cyclic string equations. | ajreynol | |
| 2017-07-07 | Update copyright headers. | Mathias Preiner | |
| 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-04-04 | Simplify Theory::collectModelInfo interface to not take deprecated fullModel ↵ | ajreynol | |
| argument. | |||
| 2017-03-27 | Minor cleanups to ExtTheory. | Tim King | |
| 2017-03-27 | Making the ExtTheory object a private member of Theory. | Tim King | |
| 2017-03-22 | Fix more cases of rewritten explanations in strings for bug 784. Minor. | ajreynol | |
| 2017-03-21 | Improve computeCareGraph functions to check shared term equality status once ↵ | ajreynol | |
| per equivalence class pair. | |||
| 2017-03-03 | Fix for collectModelInfo related to finite types + preregistration. ↵ | ajreynol | |
| Generalize previous fix for sets, minor changes to Datatypes. | |||
| 2017-03-02 | Eliminate Boolean term conversion. Generalizes removeITE pass to remove ↵ | ajreynol | |
| Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions. | |||
| 2017-01-30 | Fix regexp cache issue in strings, add regression. | 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