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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Thu, 7 Oct 2021 12:18:08 +0000 (07:18 -0500)
committer	GitHub <noreply@github.com>
	Thu, 7 Oct 2021 12:18:08 +0000 (12:18 +0000)
commit	22ab38c4a3bad18129c740968b36af8c378c4294
tree	250b6a9c2417df52984327b301c0a3aa8ffa15a1	tree
parent	991bef531131336549eccd2446243204f4733c20	commit \| diff

Make the cardinality of the alphabet of strings configurable (#7298)

This adds an option to change the cardinality of the alphabet of strings. The alphabet of strings is always a prefix of the interval of unicode code points in the string standard.

25 files changed:

src/options/strings_options.toml		diff \| blob \| history
src/smt/env.cpp		diff \| blob \| history
src/theory/evaluator.cpp		diff \| blob \| history
src/theory/evaluator.h		diff \| blob \| history
src/theory/strings/base_solver.cpp		diff \| blob \| history
src/theory/strings/base_solver.h		diff \| blob \| history
src/theory/strings/extf_solver.cpp		diff \| blob \| history
src/theory/strings/proof_checker.cpp		diff \| blob \| history
src/theory/strings/proof_checker.h		diff \| blob \| history
src/theory/strings/regexp_operation.cpp		diff \| blob \| history
src/theory/strings/regexp_solver.cpp		diff \| blob \| history
src/theory/strings/regexp_solver.h		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.cpp		diff \| blob \| history
src/theory/strings/theory_strings.h		diff \| blob \| history
src/theory/strings/theory_strings_utils.cpp		diff \| blob \| history
src/theory/strings/theory_strings_utils.h		diff \| blob \| history
src/theory/strings/type_enumerator.cpp		diff \| blob \| history
src/theory/theory_model_builder.cpp		diff \| blob \| history
src/theory/type_enumerator.h		diff \| blob \| history
test/regress/CMakeLists.txt		diff \| blob \| history
test/regress/regress2/strings/strings-alpha-card-129.smt2	[new file with mode: 0644]	blob

RSS Atom