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

author	Aina Niemetz <aina.niemetz@gmail.com>
	Wed, 2 Feb 2022 22:27:14 +0000 (14:27 -0800)
committer	GitHub <noreply@github.com>
	Wed, 2 Feb 2022 22:27:14 +0000 (22:27 +0000)
commit	eab7bf6702c174c2c58373035cf9b8a099a209ae
tree	45b7cdda411e5f823395d081030271bc0770b7f8	tree
parent	d1545ff42c2c609e567c85f5daa5e518cd87d289	commit \| diff

Rename kinds MINUS -> SUB and UMINUS -> NEG. (#8035)

This renames the internal arithmetic kinds MINUS and UMINUS for
consistency with our naming scheme for other operators (e.g.,
BITVECTOR_SUB, FLOATINGPOINT_SUB).

60 files changed:

src/api/cpp/cvc5.cpp		diff \| blob \| history
src/preprocessing/passes/int_to_bv.cpp		diff \| blob \| history
src/preprocessing/passes/nl_ext_purify.cpp		diff \| blob \| history
src/preprocessing/passes/unconstrained_simplifier.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/proof/alethe/alethe_post_processor.cpp		diff \| blob \| history
src/proof/lfsc/lfsc_node_converter.cpp		diff \| blob \| history
src/theory/arith/arith_poly_norm.cpp		diff \| blob \| history
src/theory/arith/arith_poly_norm.h		diff \| blob \| history
src/theory/arith/arith_rewriter.cpp		diff \| blob \| history
src/theory/arith/arith_rewriter.h		diff \| blob \| history
src/theory/arith/kinds		diff \| blob \| history
src/theory/arith/nl/ext/monomial_check.cpp		diff \| blob \| history
src/theory/arith/nl/ext/proof_checker.cpp		diff \| blob \| history
src/theory/arith/nl/ext/tangent_plane_check.cpp		diff \| blob \| history
src/theory/arith/nl/iand_solver.cpp		diff \| blob \| history
src/theory/arith/nl/iand_utils.cpp		diff \| blob \| history
src/theory/arith/nl/nl_model.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/exponential_solver.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/proof_checker.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/sine_solver.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/taylor_generator.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/transcendental_state.cpp		diff \| blob \| history
src/theory/arith/operator_elim.cpp		diff \| blob \| history
src/theory/arith/theory_arith.cpp		diff \| blob \| history
src/theory/arith/theory_arith_private.cpp		diff \| blob \| history
src/theory/bags/bag_reduction.cpp		diff \| blob \| history
src/theory/bags/inference_generator.cpp		diff \| blob \| history
src/theory/bv/int_blaster.cpp		diff \| blob \| history
src/theory/datatypes/sygus_extension.cpp		diff \| blob \| history
src/theory/datatypes/sygus_simple_sym.cpp		diff \| blob \| history
src/theory/evaluator.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/pattern_term_selector.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/bounded_integers.cpp		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.cpp		diff \| blob \| history
src/theory/quantifiers/skolemize.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp		diff \| blob \| history
src/theory/quantifiers/sygus_sampler.cpp		diff \| blob \| history
src/theory/quantifiers/term_util.cpp		diff \| blob \| history
src/theory/sets/theory_sets_rewriter.cpp		diff \| blob \| history
src/theory/strings/arith_entail.cpp		diff \| blob \| history
src/theory/strings/array_core_solver.cpp		diff \| blob \| history
src/theory/strings/array_solver.cpp		diff \| blob \| history
src/theory/strings/core_solver.cpp		diff \| blob \| history
src/theory/strings/regexp_elim.cpp		diff \| blob \| history
src/theory/strings/regexp_operation.cpp		diff \| blob \| history
src/theory/strings/sequences_rewriter.cpp		diff \| blob \| history
src/theory/strings/skolem_cache.cpp		diff \| blob \| history
src/theory/strings/strings_entail.cpp		diff \| blob \| history
src/theory/strings/theory_strings_preprocess.cpp		diff \| blob \| history
src/theory/strings/theory_strings_utils.cpp		diff \| blob \| history
test/unit/node/node_black.cpp		diff \| blob \| history
test/unit/node/node_builder_black.cpp		diff \| blob \| history
test/unit/theory/arith_poly_white.cpp		diff \| blob \| history
test/unit/theory/sequences_rewriter_white.cpp		diff \| blob \| history
test/unit/theory/theory_arith_rewriter_black.cpp		diff \| blob \| history

RSS Atom