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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Sat, 5 Mar 2022 19:43:43 +0000 (13:43 -0600)
committer	GitHub <noreply@github.com>
	Sat, 5 Mar 2022 19:43:43 +0000 (19:43 +0000)
commit	3614f1c4b8a439ebf785894fa33640fd015aaefa
tree	c36b4b8e5884665133ddf4adfa48fd80489d70e8	tree
parent	7cf1b94025148115f4523150d169a9b3a6c75da9	commit \| diff

Make seq.unit robust wrt subtyping (#8209)

Fixes cvc5/cvc5-projects#384.
Fixes cvc5/cvc5-projects#426.
Fixes cvc5/cvc5-projects#427.
Fixes cvc5/cvc5-projects#429.

Issue cvc5/cvc5-projects#423 still remains, to be addressed in a followup PR.

Also fixes issues with subtyping in how sequence constants are printed.

Note this solution is required since we are not ready to eliminate arithmetic subtyping in the short term. These changes will be unnecessary when this happens.

32 files changed:

src/CMakeLists.txt		diff \| blob \| history
src/api/cpp/cvc5.cpp		diff \| blob \| history
src/expr/node_manager_template.cpp		diff \| blob \| history
src/expr/node_manager_template.h		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp		diff \| blob \| history
src/theory/rewriter.cpp		diff \| blob \| history
src/theory/sets/singleton_op.cpp		diff \| blob \| history
src/theory/sets/singleton_op.h		diff \| blob \| history
src/theory/sets/theory_sets_type_rules.cpp		diff \| blob \| history
src/theory/strings/array_core_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/eager_solver.cpp		diff \| blob \| history
src/theory/strings/extf_solver.cpp		diff \| blob \| history
src/theory/strings/kinds		diff \| blob \| history
src/theory/strings/seq_unit_op.cpp	[new file with mode: 0644]	blob
src/theory/strings/seq_unit_op.h	[new file with mode: 0644]	blob
src/theory/strings/sequences_rewriter.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.cpp		diff \| blob \| history
src/theory/theory_model.cpp		diff \| blob \| history
test/regress/CMakeLists.txt		diff \| blob \| history
test/regress/regress0/seq/proj-issue384-2-subtypes.smt2	[new file with mode: 0644]	blob
test/regress/regress0/seq/proj-issue384-subtypes.smt2	[new file with mode: 0644]	blob
test/regress/regress0/seq/proj-issue427-subtypes-value.smt2	[new file with mode: 0644]	blob
test/regress/regress0/seq/query0-subtype-skel.smt2	[new file with mode: 0644]	blob
test/regress/regress0/seq/query1-subtype.smt2	[new file with mode: 0644]	blob
test/regress/regress0/seq/query2-subtype.smt2	[new file with mode: 0644]	blob
test/unit/api/cpp/solver_black.cpp		diff \| blob \| history
test/unit/theory/sequences_rewriter_white.cpp		diff \| blob \| history

RSS Atom