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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Wed, 29 Sep 2021 18:40:08 +0000 (13:40 -0500)
committer	GitHub <noreply@github.com>
	Wed, 29 Sep 2021 18:40:08 +0000 (13:40 -0500)
commit	e86726da4cf3883888a765aacf81ae76c7611c54
tree	f0565d3bac2bcc04ebe45a948e8032892a25d329	tree
parent	a6e09da79c31d9f7cf783f17072239a44e538162	commit \| diff

Update the syntax for tuples in smt2 (#7265)

This changes mkTuple -> tuple and tupSel -> tuple_select.

This is in line with the most recent syntax for tuples in preparation for the theory of tables in smt2.

107 files changed:

examples/api/smtlib/relations.smt2		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
test/regress/regress0/bug596b.cvc.smt2		diff \| blob \| history
test/regress/regress0/datatypes/4482-unc-simp-one.smt2		diff \| blob \| history
test/regress/regress0/datatypes/Test1-tup-mp.cvc.smt2		diff \| blob \| history
test/regress/regress0/datatypes/boolean-terms-tuple.cvc.smt2		diff \| blob \| history
test/regress/regress0/datatypes/some-boolean-tests.cvc.smt2		diff \| blob \| history
test/regress/regress0/datatypes/tuple-model.cvc.smt2		diff \| blob \| history
test/regress/regress0/datatypes/tuple-no-clash.cvc.smt2		diff \| blob \| history
test/regress/regress0/datatypes/tuple-record-bug.cvc.smt2		diff \| blob \| history
test/regress/regress0/datatypes/tuple.cvc.smt2		diff \| blob \| history
test/regress/regress0/datatypes/tuples-empty.smt2		diff \| blob \| history
test/regress/regress0/datatypes/tuples-multitype.smt2		diff \| blob \| history
test/regress/regress0/fmf/quant_real_univ.cvc.smt2		diff \| blob \| history
test/regress/regress0/printer/tuples_and_records.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/addr_book_0.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/atom_univ2.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/iden_0.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/iden_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/join-eq-u-sat.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/join-eq-u.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/joinImg_0.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/oneLoc_no_quant-int_0_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_1tup_0.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_complex_0.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_complex_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_conflict_0.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_join_0.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_join_0_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_join_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_join_1_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_join_2.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_join_2_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_join_3.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_join_3_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_join_4.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_join_5.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_join_6.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_join_7.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_product_0.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_product_0_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_product_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_product_1_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_symbolic_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_symbolic_1_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_symbolic_2_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_symbolic_3_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_tc_11.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_tc_2_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_tc_3.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_tc_3_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_tc_7.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_tc_8.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_tp_3_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_tp_join_0.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_tp_join_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_tp_join_2.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_tp_join_3.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_tp_join_eq_0.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_tp_join_int_0.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_tp_join_pro_0.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_tp_join_var_0.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_transpose_0.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_transpose_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_transpose_1_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_transpose_3.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_transpose_4.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_transpose_5.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_transpose_6.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/relations-ops.smt2		diff \| blob \| history
test/regress/regress0/rels/rels-sharing-simp.cvc.smt2		diff \| blob \| history
test/regress/regress0/sets/complement3.cvc.smt2		diff \| blob \| history
test/regress/regress1/datatypes/tuple_projection.smt2		diff \| blob \| history
test/regress/regress1/fmf/memory_model-R_cpp-dd.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/addr_book_1.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/addr_book_1_1.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/bv1-unit.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/bv1-unitb.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/bv1.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/bv2.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/garbage_collect.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/iden_1_1.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/join-eq-structure-and.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/join-eq-structure.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/joinImg_0_1.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/joinImg_0_2.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/joinImg_1.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/joinImg_1_1.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/joinImg_2.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/joinImg_2_1.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/prod-mod-eq.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/prod-mod-eq2.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/rel_complex_3.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/rel_complex_4.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/rel_complex_5.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/rel_mix_0_1.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/rel_pressure_0.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/rel_tc_10_1.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/rel_tc_4.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/rel_tc_9_1.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/rel_tp_join_2_1.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/set-strat.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/strat.cvc.smt2		diff \| blob \| history
test/regress/regress1/sets/issue4124-need-check.smt2		diff \| blob \| history
test/regress/regress1/sets/sets-tuple-poly.cvc.smt2		diff \| blob \| history
test/unit/api/solver_black.cpp		diff \| blob \| history

RSS Atom