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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Wed, 29 Sep 2021 15:39:50 +0000 (10:39 -0500)
committer	GitHub <noreply@github.com>
	Wed, 29 Sep 2021 15:39:50 +0000 (15:39 +0000)
commit	a6e09da79c31d9f7cf783f17072239a44e538162
tree	577121352f4ed2a27bfb6297c50055c5ccfca9d2	tree
parent	c9b3f13981ce88bc081e49213b15da6999f4aea5	commit \| diff

Add the strings array solver (#7232)

This adds the arrays subsolver utility. It does not yet connect it down to the core array solver, or up to TheoryStrings.

It adds implementation of its lemma schemas for processing nth/update over concat.

src/CMakeLists.txt		diff \| blob \| history
src/theory/inference_id.cpp		diff \| blob \| history
src/theory/inference_id.h		diff \| blob \| history
src/theory/strings/array_solver.cpp	[new file with mode: 0644]	blob
src/theory/strings/array_solver.h	[new file with mode: 0644]	blob
src/theory/strings/term_registry.cpp		diff \| blob \| history
src/theory/strings/term_registry.h		diff \| blob \| history

RSS Atom