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

author	Aina Niemetz <aina.niemetz@gmail.com>
	Thu, 3 Feb 2022 04:25:14 +0000 (20:25 -0800)
committer	GitHub <noreply@github.com>
	Thu, 3 Feb 2022 04:25:14 +0000 (04:25 +0000)
commit	c335e4d3fa8038bcff96d420b0d487641292c061
tree	3eb9ba6c41a93c79a7f744d7f7ca51e1fad7833b	tree
parent	72f495a4aabe7d129c3614c594b1b8f144e50931	commit \| diff

Rename kind PLUS -> ADD. (#8036)

This renames the arithmetic internal and API kind PLUS to ADD for
consistency with our naming scheme for other operators (e.g.,
BITVECTOR_ADD, FLOATINGPOINT_ADD).

136 files changed:

examples/SimpleVC.java		diff \| blob \| history
examples/api/cpp/combination.cpp		diff \| blob \| history
examples/api/cpp/quickstart.cpp		diff \| blob \| history
examples/api/cpp/sygus-fun.cpp		diff \| blob \| history
examples/api/cpp/sygus-grammar.cpp		diff \| blob \| history
examples/api/cpp/sygus-inv.cpp		diff \| blob \| history
examples/api/java/Combination.java		diff \| blob \| history
examples/api/java/QuickStart.java		diff \| blob \| history
examples/api/java/SygusFun.java		diff \| blob \| history
examples/api/java/SygusGrammar.java		diff \| blob \| history
examples/api/java/SygusInv.java		diff \| blob \| history
examples/api/python/combination.py		diff \| blob \| history
examples/api/python/quickstart.py		diff \| blob \| history
examples/api/python/sygus-fun.py		diff \| blob \| history
examples/api/python/sygus-grammar.py		diff \| blob \| history
examples/api/python/sygus-inv.py		diff \| blob \| history
examples/nra-translate/smt2toisat.cpp		diff \| blob \| history
examples/nra-translate/smt2tomathematica.cpp		diff \| blob \| history
examples/nra-translate/smt2toqepcad.cpp		diff \| blob \| history
examples/nra-translate/smt2toredlog.cpp		diff \| blob \| history
examples/simple_vc_cxx.cpp		diff \| blob \| history
src/api/cpp/cvc5.cpp		diff \| blob \| history
src/api/cpp/cvc5_kind.h		diff \| blob \| history
src/expr/dtype.h		diff \| blob \| history
src/expr/kind_template.cpp		diff \| blob \| history
src/expr/nary_term_util.cpp		diff \| blob \| history
src/expr/node.h		diff \| blob \| history
src/expr/node_algorithm.cpp		diff \| blob \| history
src/expr/node_manager_template.h		diff \| blob \| history
src/expr/subtype_elim_node_converter.cpp		diff \| blob \| history
src/expr/sygus_datatype.h		diff \| blob \| history
src/parser/smt2/smt2.cpp		diff \| blob \| history
src/parser/tptp/Tptp.g		diff \| blob \| history
src/preprocessing/passes/int_to_bv.cpp		diff \| blob \| history
src/preprocessing/passes/miplib_trick.cpp		diff \| blob \| history
src/preprocessing/passes/nl_ext_purify.cpp		diff \| blob \| history
src/preprocessing/passes/pseudo_boolean_processor.cpp		diff \| blob \| history
src/preprocessing/passes/real_to_int.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/proof/lfsc/lfsc_post_processor.cpp		diff \| blob \| history
src/theory/arith/arith_ite_utils.cpp		diff \| blob \| history
src/theory/arith/arith_msum.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_utilities.h		diff \| blob \| history
src/theory/arith/dio_solver.cpp		diff \| blob \| history
src/theory/arith/kinds		diff \| blob \| history
src/theory/arith/nl/ext/factoring_check.cpp		diff \| blob \| history
src/theory/arith/nl/ext/monomial.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_utils.cpp		diff \| blob \| history
src/theory/arith/nl/nl_model.cpp		diff \| blob \| history
src/theory/arith/nl/poly_conversion.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/normal_form.cpp		diff \| blob \| history
src/theory/arith/normal_form.h		diff \| blob \| history
src/theory/arith/operator_elim.cpp		diff \| blob \| history
src/theory/arith/proof_checker.cpp		diff \| blob \| history
src/theory/arith/rewrites.h		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/bags_rewriter.cpp		diff \| blob \| history
src/theory/bags/card_solver.cpp		diff \| blob \| history
src/theory/bags/inference_generator.cpp		diff \| blob \| history
src/theory/builtin/kinds		diff \| blob \| history
src/theory/bv/int_blaster.cpp		diff \| blob \| history
src/theory/bv/theory_bv_utils.cpp		diff \| blob \| history
src/theory/datatypes/datatypes_rewriter.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/bv_inverter.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/ematching/relational_match_generator.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_macros.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.cpp		diff \| blob \| history
src/theory/quantifiers/relevant_domain.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_unif.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_norm.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_norm.h		diff \| blob \| history
src/theory/quantifiers/sygus/type_info.cpp		diff \| blob \| history
src/theory/quantifiers/sygus_sampler.cpp		diff \| blob \| history
src/theory/quantifiers/term_database.h		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/regexp_elim.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/strings_fmf.cpp		diff \| blob \| history
src/theory/strings/term_registry.cpp		diff \| blob \| history
src/theory/strings/theory_strings_preprocess.cpp		diff \| blob \| history
src/theory/theory_model.h		diff \| blob \| history
src/util/statistics_stats.h		diff \| blob \| history
test/unit/api/cpp/op_black.cpp		diff \| blob \| history
test/unit/api/cpp/op_white.cpp		diff \| blob \| history
test/unit/api/cpp/solver_black.cpp		diff \| blob \| history
test/unit/api/cpp/term_black.cpp		diff \| blob \| history
test/unit/api/java/OpTest.java		diff \| blob \| history
test/unit/api/java/SolverTest.java		diff \| blob \| history
test/unit/api/java/TermTest.java		diff \| blob \| history
test/unit/api/python/test_op.py		diff \| blob \| history
test/unit/api/python/test_solver.py		diff \| blob \| history
test/unit/api/python/test_term.py		diff \| blob \| history
test/unit/node/node_algorithm_black.cpp		diff \| blob \| history
test/unit/node/node_algorithms_black.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/node/node_white.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_cad_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_rewriter_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/util/array_store_all_white.cpp		diff \| blob \| history

RSS Atom