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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Thu, 2 Jun 2022 20:02:55 +0000 (15:02 -0500)
committer	GitHub <noreply@github.com>
	Thu, 2 Jun 2022 20:02:55 +0000 (20:02 +0000)
commit	e83a270a02e236ddc25cf82a3ee0ba073ea8fe77
tree	6de2369034579855e7a7a7f675ace18acc838336	tree
parent	65a77c3d7715af4fe44b81c0e3f9c17c6f154886	commit \| diff

Preparation for SEQ_NTH applied to strings (#8779)

No behavior changes in this commit for current main.

17 files changed:

src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/theory/evaluator.cpp		diff \| blob \| history
src/theory/strings/array_core_solver.cpp		diff \| blob \| history
src/theory/strings/array_solver.cpp		diff \| blob \| history
src/theory/strings/base_solver.cpp		diff \| blob \| history
src/theory/strings/core_solver.cpp		diff \| blob \| history
src/theory/strings/extf_solver.cpp		diff \| blob \| history
src/theory/strings/proof_checker.cpp		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/strings_rewriter.cpp		diff \| blob \| history
src/theory/strings/strings_rewriter.h		diff \| blob \| history
src/theory/strings/term_registry.cpp		diff \| blob \| history
src/theory/strings/term_registry.h		diff \| blob \| history
src/theory/strings/theory_strings_type_rules.cpp		diff \| blob \| history
test/regress/cli/regress0/seq/seq-nth-type-check.smt2		diff \| blob \| history