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

author	mudathirmahgoub <mudathirmahgoub@gmail.com>
	Wed, 13 Apr 2022 18:54:27 +0000 (13:54 -0500)
committer	GitHub <noreply@github.com>
	Wed, 13 Apr 2022 18:54:27 +0000 (13:54 -0500)
commit	12293a35d56ddefe51adba6d07f058f10b1dd20e
tree	090a3fa99d7a51441a5950c9f462d59c81f4e9e8	tree
parent	82f9ba130f855c1a7efb75264728a83cf0fce31a	commit \| diff

Add Relation and Table types to SMTLib parser (#8605)

124 files changed:

docs/theories/sets-and-relations.rst		diff \| blob \| history
examples/api/cpp/relations.cpp		diff \| blob \| history
examples/api/java/Relations.java		diff \| blob \| history
examples/api/java/Statistics.java		diff \| blob \| history
examples/api/python/relations.py		diff \| blob \| history
examples/api/smtlib/relations.smt2		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
src/theory/sets/rels_utils.h		diff \| blob \| history
src/theory/sets/theory_sets_type_rules.h		diff \| blob \| history
test/regress/cli/regress0/fmf/quant_real_univ.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/addr_book_0.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/atom_univ2.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/card_transpose.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/iden_0.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/iden_1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/join-eq-u-sat.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/join-eq-u.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/joinImg_0.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/oneLoc_no_quant-int_0_1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/qgu-fuzz-relations-1-dd.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/qgu-fuzz-relations-1.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_1tup_0.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_complex_0.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_complex_1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_conflict_0.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_join_0.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_join_0_1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_join_1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_join_1_1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_join_2.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_join_2_1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_join_3.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_join_3_1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_join_4.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_join_5.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_join_6.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_join_7.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_product_0.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_product_0_1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_product_1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_product_1_1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_symbolic_1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_symbolic_1_1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_symbolic_2_1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_symbolic_3_1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_tc_11.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_tc_2_1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_tc_3.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_tc_3_1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_tc_7.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_tc_8.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_tp_3_1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_tp_join_0.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_tp_join_1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_tp_join_2.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_tp_join_3.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_tp_join_eq_0.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_tp_join_int_0.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_tp_join_pro_0.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_tp_join_var_0.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_transpose_0.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_transpose_1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_transpose_1_1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_transpose_3.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_transpose_4.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_transpose_5.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_transpose_6.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rel_transpose_7.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/relations-ops.smt2		diff \| blob \| history
test/regress/cli/regress0/rels/rels-sharing-simp.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/sets/complement.cvc.smt2		diff \| blob \| history
test/regress/cli/regress0/sets/complement3.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/bags/card3.smt2		diff \| blob \| history
test/regress/cli/regress1/bags/fuzzy1.smt2		diff \| blob \| history
test/regress/cli/regress1/bags/fuzzy2.smt2		diff \| blob \| history
test/regress/cli/regress1/bags/fuzzy3.smt2		diff \| blob \| history
test/regress/cli/regress1/bags/fuzzy3b.smt2		diff \| blob \| history
test/regress/cli/regress1/bags/fuzzy4.smt2		diff \| blob \| history
test/regress/cli/regress1/bags/fuzzy5.smt2		diff \| blob \| history
test/regress/cli/regress1/bags/fuzzy6.smt2		diff \| blob \| history
test/regress/cli/regress1/bags/product1.smt2		diff \| blob \| history
test/regress/cli/regress1/bags/product2.smt2		diff \| blob \| history
test/regress/cli/regress1/bags/product3.smt2		diff \| blob \| history
test/regress/cli/regress1/fmf/memory_model-R_cpp-dd.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/addr_book_1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/addr_book_1_1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/bv1-unit.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/bv1-unitb.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/bv1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/bv1p-sat.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/bv1p.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/bv2.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/garbage_collect.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/iden_1_1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/join-eq-structure-and.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/join-eq-structure.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/joinImg_0_1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/joinImg_0_2.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/joinImg_1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/joinImg_1_1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/joinImg_2.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/joinImg_2_1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/prod-mod-eq.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/prod-mod-eq2.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/qgu-fuzz-relations-2.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/qgu-fuzz-relations-3-upwards.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/rel_complex_3.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/rel_complex_4.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/rel_complex_5.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/rel_mix_0_1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/rel_pressure_0.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/rel_tc_10_1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/rel_tc_4.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/rel_tc_4_1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/rel_tc_5_1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/rel_tc_6.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/rel_tc_9_1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/rel_tp_2.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/rel_tp_join_2_1.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/set-strat.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/rels/strat.cvc.smt2		diff \| blob \| history
test/regress/cli/regress1/sets/issue4124-need-check.smt2		diff \| blob \| history
test/regress/cli/regress1/sets/proj-issue164.smt2		diff \| blob \| history
test/regress/cli/regress1/sets/sets-tuple-poly.cvc.smt2		diff \| blob \| history

RSS Atom