cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Age	Commit message (Collapse)	Author
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-26	Better normalization of string concatenation (#1719)	Andres Noetzli

2018-03-26	Add reasoning for inequalities in str rewriter (#1713)	Andres Noetzli

2018-03-26	Rewrites for substr of strings of length one (#1712)	Andres Noetzli
	This commit adds a rewrite for substrings of strings of length one to the empty string if it can be shown that it is not possible that the start position and the length are both greater than zero: ``` (str.substr "A" x y) --> "" if x = 0 \|= 0 >= y ``` The commit introduces a set of functions to check such entailments with assumptions.
2018-03-25	Cleanup various exit calls (#1692)	Andrew Reynolds

2018-03-23	Remove abstract regular expression constant (#1698)	Andrew Reynolds

2018-03-23	Remove unused code (#1700)	Andrew Reynolds

2018-03-21	More rewrites for indexof (#1648)	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-03-05	Update semantics for string indexof and replace (#1630)	Andrew Reynolds

2018-03-05	Enable -Wsuggest-override by default. (#1643)	Mathias Preiner
	Adds missing override keywords.
2018-02-27	Improve rewriter for string indexof (#1592)	Andrew Reynolds

2018-02-23	Fix cd-simplification for strings (#1624)	Andrew Reynolds

2018-02-22	Minor improvements to string rewriter (#1572)	Andrew Reynolds

2018-02-06	Resolving warnings from -Winconsistent-missing-override on clang. (#1563)	Tim King

2018-02-06	Fix rewrite for string replace (#1537)	Andrew Reynolds

2018-01-10	Removing throw specifiers for TypeRules. (#1501)	Tim King

2018-01-10	Removing throw specifiers from type enumerators. (#1502)	Tim King

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-12-06	Remove CDChunkList (#1414)	Andres Noetzli

2017-12-04	Fix strings rewriter for strip constant endpoint reverse direction (#1424)	Andrew Reynolds

2017-12-01	Improve rewriter for string replace (#1416)	Andrew Reynolds

2017-11-30	Fixes for issue 1404 (#1409)	Andrew Reynolds

2017-11-28	Improve rewrite for string substr (#1337)	Andrew Reynolds

2017-11-13	Initializes RegExpOpr::d_char_start and d_char_end. (#1359)	Tim King

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-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-24	Merge pull request #191 from timothy-king/cleanup-regexp	Andrew Reynolds
	Cleaning up the CVC4::String class.
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-13	Cleaning up the CVC4::String class.	Tim King

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-05-09	Change str.replace for empty string.	ajreynol

2017-04-05	Fix several spelling errors	Fabian Wolff

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	Merge pull request #137 from 4tXJ7f/throw_quals	Clark Barrett
	Remove throw qualifiers in type enumerators
2017-03-27	Making the ExtTheory object a private member of Theory.	Tim King

2017-03-27	Remove throw qualifiers in type enumerators	Andres Notzli
	This addresses Coverity issues: - 1172154 - 1172156 - 1172157 - 1172158 - 1172159 - 1379612 - 1379612 - 1421430 - 1172166 - 1172144 - 1362709 - 1362696 - 1172145 - 1172147 - 1172148 - 1379610 - 1362772 - 1362676 - 1362704 - 1362749 - 1362876 - 1362843 - 1362837 - 1362881 - 1172223 - 1172155