| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-07-30 | Minor improvement for rewriter for str.replace (#3124) | Andrew Reynolds | |
| 2019-07-18 | Basic rewrites for tolower/toupper (#3095) | Andrew Reynolds | |
| 2019-07-16 | Add support for str.tolower and str.toupper (#3092) | Andrew Reynolds | |
| 2019-06-12 | Refactor parser to define fewer tokens for symbols (#2936) | Andres Noetzli | |
| 2019-05-06 | Add support for re.all (#2980) | Andres Noetzli | |
| 2019-04-30 | Remove stoi solve rewrite (#2985) | Andrew Reynolds | |
| 2019-04-17 | Fix extended function decomposition (#2960) | Andrew Reynolds | |
| Fixes #2958. The issue was: we had substr(x,0,2) in R, and the "derivable substitution" modifed this to substr(substr(x,0,2),0,2) in R, since substr(x,0,2) was the representative of x (which is a bad choice, but regardless is legal). Then decomposition inference asked "can i reduce substr(substr(x,0,2),0,2) in R"? It determines substr(substr(x,0,2),0,2) in R rewrites to substr(x,0,2) in R, which is already true. However, substr(x,0,2) in R was what we started with. The fix makes things much more conservative: we never mark extended functions reduced based on decomposition, since there isnt a strong argument based on an ordering. | |||
| 2019-01-15 | Fix constant contains ITOS rewrite (#2799) | Andrew Reynolds | |
| 2018-11-21 | Support string replace all (#2704) | Andrew Reynolds | |
| 2018-11-07 | Fix collectEmptyEqs in string rewriter (#2692) | Andres Noetzli | |
| 2018-10-18 | Non-contributing find replace rewrite (#2652) | Andrew Reynolds | |
| 2018-09-30 | Add rewrite for solving stoi (#2532) | Andrew Reynolds | |
| 2018-09-26 | Fix homogeneous string constant rewrite (#2545) | Andrew Reynolds | |
| 2018-09-22 | cmake: Added regression tests and target make regress. | Aina Niemetz | |
| 2018-09-22 | cmake: Added initial build infrastructure. | Aina Niemetz | |
| 2018-09-05 | Extended rewriter for string equalities (#2427) | Andrew Reynolds | |
| 2018-08-30 | Add regular expression elimination module (#2400) | Andrew Reynolds | |
| 2018-06-12 | Fix strip constant endpoint for ITOS in strings rewriter (#2067) | Andrew Reynolds | |
| 2018-05-08 | Support for str.<= and str.< (#1882) | Andrew Reynolds | |
| 2018-05-02 | Initial support for string standard in smt lib 2.6 (#1848) | Andrew Reynolds | |
| 2018-03-21 | Move regression tests to single Makefile.am (#1658) | Andres Noetzli | |
| Until now, regression tests were split across tens of different Makefile.am, which required a lot of code duplication and does not really seem to be in the spirit of automake. If we want to change the LOG_COMPILER/LOG_DRIVER for example, we have to change every single Makefile.am, which is cumbersome (I was able to get something semi-working by exporting those variables but it didn't seem very clean). Additionally, it made the output of the regression tests fairly verbose and split the output across multiple log files. Finally it also limited parallelism when running the regression tests (this fix lowers the time it takes to run regression level 1 from 3m to 1m45s on my machine with 16 threads). This commit moves all the regression tests into test/regress/Makefile.tests and changes test/regress/Makefile.am to deal with this new structure. Finally, it changes how the test summary in test/Makefile.am is produced: instead of relying on the log files for the subdirectories, it greps for the test results in the log files of the individual tests. Not the most elegant solution but we should probably anyway delegate that task to a Python script at some point. | |||
| 2018-03-05 | Update semantics for string indexof and replace (#1630) | Andrew Reynolds | |
| 2018-02-27 | Improve rewriter for string indexof (#1592) | Andrew Reynolds | |
| 2018-02-15 | Refactor regressions (#1581) | Andrew Reynolds | |
| 2018-02-06 | Fix rewrite for string replace (#1537) | Andrew Reynolds | |
| 2017-12-04 | Fix strings rewriter for strip constant endpoint reverse direction (#1424) | Andrew Reynolds | |
| 2017-11-28 | Improve rewrite for string substr (#1337) | Andrew Reynolds | |
| 2017-11-15 | Reenable some regressions, minor. (#1369) | Andrew Reynolds | |
| 2017-11-05 | Improve rewriting for string contains part 2 (#1300) | Andrew Reynolds | |
| * Generalize component contains, some infrastructure. * Length entailment, substr for component contains, int.to.str for constant can contain concat. * Disable rewrite. * Fix, reenable length entailment for contains. * Clang format, minor. * Comment * Minor fixes and improvements for comments. * Improvements * Clang format * Fixes * Clang format * Fix, improve. * Format * Fix assertion | |||
| 2017-10-27 | Improve strings rewriter for contains (#1207) | Andrew Reynolds | |
| * Work on rewriter for string contains. * Add rewrites that mix str.to.int and str.contains. Documentation, add regression. * Minor * Minor * Address review, add a few TODOs. Improve some non-digit -> not is number. * Fix * Simplify. * Clang format, minor fixing of comments. | |||
| 2017-09-18 | Fix issue #1105 involving string to int (#1112) | Andrew Reynolds | |
| This was introduced by changing the implementation of "isNumber" in this commit: a94318b This fixes issue #1105. | |||
| 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-04 | Set default language to smt lib 2.6 (including as a base language for ↵ | ajreynol | |
| sygus), update regressions. | |||
| 2017-07-29 | Add support for charat in native language, minor cleanup. | ajreynol | |
| 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-01-30 | Fix regexp cache issue in strings, add regression. | ajreynol | |
| 2016-12-07 | Fix nf exp tracking for non-linear string equalities, fixes bug 768. | ajreynol | |
| 2016-12-01 | Improvement and bug fix for str.indexof reduction, add regression. Other ↵ | ajreynol | |
| minor changes. | |||
| 2016-11-17 | Fix Makefiles in test | Andres Notzli | |
| With the recent changes to the regress tests, some of the Makefiles were not in sync anymore. This commit fixes that. | |||
| 2016-10-21 | Move slow regress0 benchmarks to regress1, increment regress1 through regress3. | ajreynol | |
| 2016-08-12 | Add a few more regressions. | ajreynol | |
| 2016-08-10 | Improvements to strings: work on propagations for reverse normal form ↵ | ajreynol | |
| processing. Better handling of disequalities, constant splitting and neg contain approximation. Introduce proxy vars for replace. Refactoring. | |||
| 2016-07-21 | Fixes for strings, explanations for constant split propagations, substr ↵ | ajreynol | |
| under concat rewrite. Avoid duplicate re.range length lemmas. | |||
| 2016-07-20 | Infer conflicts in strings based on abstracting equality as contains. Minor ↵ | ajreynol | |
| cleanup. | |||
| 2016-07-08 | Minor fix to last commit. | ajreynol | |
| 2016-07-07 | Simplifications for strings normal forms, fix case for concat reps in normal ↵ | ajreynol | |
| forms. | |||
| 2016-07-07 | Refactoring of strings preprocess module. When enabled, apply eager ↵ | ajreynol | |
| preprocess during ppRewrite instead of during processAssertions. Simplify reduction for contains. Fix bug in explanations for F_EndpointEq. Minor cleanup for sep. | |||
| 2016-05-21 | Minor fix for strings. | ajreynol | |
| 2016-05-20 | Minor fix to strings, cleanup in datatypes. | 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