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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Mon, 13 Jul 2020 05:43:45 +0000 (00:43 -0500)
committer	GitHub <noreply@github.com>
	Mon, 13 Jul 2020 05:43:45 +0000 (22:43 -0700)
commit	c7ec792a2086c5b92c4a96d18f7cedb293712dfd
tree	c88ebf889cb2f6aa6678154e1984bbe60a5b92b9	tree
parent	090d8bc3c31404140856e51d2cc5a5aa1335b3b3	commit \| diff

Add support for string/sequence update (#4725)

This adds basic support for string/sequence updating, which has a semantics that is length preserving.

26 files changed:

src/api/cvc4cpp.cpp		diff \| blob \| history
src/api/cvc4cppkind.h		diff \| blob \| history
src/expr/sequence.cpp		diff \| blob \| history
src/expr/sequence.h		diff \| blob \| history
src/parser/smt2/smt2.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/theory/evaluator.cpp		diff \| blob \| history
src/theory/strings/extf_solver.cpp		diff \| blob \| history
src/theory/strings/kinds		diff \| blob \| history
src/theory/strings/rewrites.cpp		diff \| blob \| history
src/theory/strings/rewrites.h		diff \| blob \| history
src/theory/strings/sequences_rewriter.cpp		diff \| blob \| history
src/theory/strings/sequences_rewriter.h		diff \| blob \| history
src/theory/strings/term_registry.cpp		diff \| blob \| history
src/theory/strings/theory_strings.cpp		diff \| blob \| history
src/theory/strings/theory_strings_preprocess.cpp		diff \| blob \| history
src/theory/strings/theory_strings_type_rules.h		diff \| blob \| history
src/theory/strings/word.cpp		diff \| blob \| history
src/theory/strings/word.h		diff \| blob \| history
src/util/string.cpp		diff \| blob \| history
src/util/string.h		diff \| blob \| history
test/regress/CMakeLists.txt		diff \| blob \| history
test/regress/regress1/strings/update-ex1.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/update-ex2.smt2	[new file with mode: 0644]	blob
test/regress/regress2/strings/update-ex3.smt2	[new file with mode: 0644]	blob
test/regress/regress2/strings/update-ex4-seq.smt2	[new file with mode: 0644]	blob

RSS Atom