git.libre-soc.org Git - cvc5.git/commit

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Tue, 6 Mar 2018 02:36:17 +0000 (20:36 -0600)
committer	GitHub <noreply@github.com>
	Tue, 6 Mar 2018 02:36:17 +0000 (20:36 -0600)
commit	e2d714a0839fb80d9a40e9b6fdd8a6fe325a1664
tree	c89479f84c0e912f7b7065ab7e97a57867902016	tree
parent	b8a89b4dbba79ce79f193008a58f7c36deb2a821	commit \| diff

Update semantics for string indexof and replace (#1630)

15 files changed:

src/theory/datatypes/datatypes_sygus.cpp		diff \| blob \| history
src/theory/strings/theory_strings_preprocess.cpp		diff \| blob \| history
src/theory/strings/theory_strings_rewriter.cpp		diff \| blob \| history
src/theory/strings/theory_strings_rewriter.h		diff \| blob \| history
test/regress/regress0/strings/idof-sem.smt2		diff \| blob \| history
test/regress/regress0/strings/repl-rewrites2.smt2		diff \| blob \| history
test/regress/regress1/strings/Makefile.am		diff \| blob \| history
test/regress/regress1/strings/cmu-disagree-0707-dd.smt2	[deleted file]	blob \| history
test/regress/regress1/strings/double-replace.smt2		diff \| blob \| history
test/regress/regress1/strings/repl-empty-sem.smt2		diff \| blob \| history
test/regress/regress1/strings/repl-soundness-sem.smt2		diff \| blob \| history
test/regress/regress1/strings/rew-020618.smt2		diff \| blob \| history
test/regress/regress1/strings/string-unsound-sem.smt2	[new file with mode: 0644]	blob
test/regress/regress2/strings/Makefile.am		diff \| blob \| history
test/regress/regress2/strings/cmu-disagree-0707-dd.smt2	[new file with mode: 0644]	blob