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

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Tue, 3 May 2022 02:36:33 +0000 (21:36 -0500)
committer	GitHub <noreply@github.com>
	Tue, 3 May 2022 02:36:33 +0000 (21:36 -0500)
commit	2b364e03e54e06ca00b47812b7abbcedb6165409
tree	78d2222680dcf78fc391daea976ecf2209c69c44	tree
parent	9a7f4cfbc05782b53cbff450e863247f183bba6c	commit \| diff

Final preparation for CONST_INTEGER (#8700)

With this PR, CI passes when using CONST_INTEGER instead of (all) integral CONST_RATIONAL.

This does not make this change yet, so CONST_RATIONAL is still used throughout.

36 files changed:

src/api/cpp/cvc5.cpp		diff \| blob \| history
src/expr/node_manager_template.cpp		diff \| blob \| history
src/theory/arith/arith_poly_norm.cpp		diff \| blob \| history
src/theory/arith/arith_rewriter.cpp		diff \| blob \| history
src/theory/arith/arith_rewriter.h		diff \| blob \| history
src/theory/arith/arith_utilities.h		diff \| blob \| history
src/theory/arith/linear/normal_form.cpp		diff \| blob \| history
src/theory/arith/linear/theory_arith_private.cpp		diff \| blob \| history
src/theory/arith/rewriter/node_utils.cpp		diff \| blob \| history
src/theory/arith/rewriter/node_utils.h		diff \| blob \| history
test/unit/node/node_algorithm_black.cpp		diff \| blob \| history
test/unit/node/node_black.cpp		diff \| blob \| history
test/unit/node/node_manager_black.cpp		diff \| blob \| history
test/unit/node/node_manager_white.cpp		diff \| blob \| history
test/unit/node/node_white.cpp		diff \| blob \| history
test/unit/node/type_node_white.cpp		diff \| blob \| history
test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp		diff \| blob \| history
test/unit/theory/arith_poly_white.cpp		diff \| blob \| history
test/unit/theory/evaluator_white.cpp		diff \| blob \| history
test/unit/theory/sequences_rewriter_white.cpp		diff \| blob \| history
test/unit/theory/theory_arith_coverings_white.cpp		diff \| blob \| history
test/unit/theory/theory_arith_pow2_white.cpp		diff \| blob \| history
test/unit/theory/theory_arith_rewriter_black.cpp		diff \| blob \| history
test/unit/theory/theory_arith_white.cpp		diff \| blob \| history
test/unit/theory/theory_bags_normal_form_white.cpp		diff \| blob \| history
test/unit/theory/theory_bags_rewriter_white.cpp		diff \| blob \| history
test/unit/theory/theory_bags_type_rules_white.cpp		diff \| blob \| history
test/unit/theory/theory_black.cpp		diff \| blob \| history
test/unit/theory/theory_bv_int_blaster_white.cpp		diff \| blob \| history
test/unit/theory/theory_engine_white.cpp		diff \| blob \| history
test/unit/theory/theory_int_opt_white.cpp		diff \| blob \| history
test/unit/theory/theory_sets_rewriter_white.cpp		diff \| blob \| history
test/unit/theory/theory_strings_skolem_cache_black.cpp		diff \| blob \| history
test/unit/theory/type_enumerator_white.cpp		diff \| blob \| history
test/unit/util/array_store_all_white.cpp		diff \| blob \| history
test/unit/util/datatype_black.cpp		diff \| blob \| history

RSS Atom