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

author	Aina Niemetz <aina.niemetz@gmail.com>
	Thu, 15 Apr 2021 20:04:55 +0000 (13:04 -0700)
committer	GitHub <noreply@github.com>
	Thu, 15 Apr 2021 20:04:55 +0000 (20:04 +0000)
commit	77bca094a140b35341257f125a55212ff0108250
tree	1d3369b9be5fc4c3e8cb279ae5ea662e59cbcb3e	tree
parent	63647b1d79df6f287ea6599958b16fce44b8271d	commit \| diff

Rename occurrences of CVC4 to CVC5. (#6351)

This renames everything but GitHub links and build system related
macros. Switching the build system to cvc5 will be the last step in the
renaming process.

149 files changed:

docs/cpp/exceptions.rst		diff \| blob \| history
src/api/cpp/cvc5.cpp		diff \| blob \| history
src/api/cpp/cvc5.h		diff \| blob \| history
src/api/cpp/cvc5_checks.h		diff \| blob \| history
src/api/cpp/cvc5_kind.h		diff \| blob \| history
src/api/java/genkinds.py.in		diff \| blob \| history
src/api/parsekinds.py		diff \| blob \| history
src/api/python/cvc4.pxd		diff \| blob \| history
src/api/python/genkinds.py.in		diff \| blob \| history
src/api/python/setup.py.in		diff \| blob \| history
src/base/configuration.cpp		diff \| blob \| history
src/base/configuration.h		diff \| blob \| history
src/base/modal_exception.h		diff \| blob \| history
src/base/output.cpp		diff \| blob \| history
src/base/output.h		diff \| blob \| history
src/expr/attribute.cpp		diff \| blob \| history
src/expr/attribute.h		diff \| blob \| history
src/expr/dtype.cpp		diff \| blob \| history
src/expr/dtype.h		diff \| blob \| history
src/expr/dtype_cons.cpp		diff \| blob \| history
src/expr/dtype_selector.cpp		diff \| blob \| history
src/expr/kind_template.h		diff \| blob \| history
src/expr/metakind_template.h		diff \| blob \| history
src/expr/mkexpr		diff \| blob \| history
src/expr/mkkind		diff \| blob \| history
src/expr/mkmetakind		diff \| blob \| history
src/expr/node.h		diff \| blob \| history
src/expr/node_manager.h		diff \| blob \| history
src/expr/node_value.h		diff \| blob \| history
src/expr/proof_node.h		diff \| blob \| history
src/expr/sequence.h		diff \| blob \| history
src/expr/type_node.h		diff \| blob \| history
src/include/cvc5_private.h		diff \| blob \| history
src/include/cvc5_private_library.h		diff \| blob \| history
src/include/cvc5parser_private.h		diff \| blob \| history
src/include/cvc5parser_public.h		diff \| blob \| history
src/main/driver_unified.cpp		diff \| blob \| history
src/main/interactive_shell.cpp		diff \| blob \| history
src/main/main.cpp		diff \| blob \| history
src/main/signal_handlers.cpp		diff \| blob \| history
src/options/base_options.toml		diff \| blob \| history
src/options/didyoumean.cpp		diff \| blob \| history
src/options/didyoumean.h		diff \| blob \| history
src/options/didyoumean_test.cpp		diff \| blob \| history
src/options/language.cpp		diff \| blob \| history
src/options/language.h		diff \| blob \| history
src/options/main_options.toml		diff \| blob \| history
src/options/options_handler.cpp		diff \| blob \| history
src/options/options_handler.h		diff \| blob \| history
src/options/options_template.cpp		diff \| blob \| history
src/options/parser_options.toml		diff \| blob \| history
src/options/quantifiers_options.toml		diff \| blob \| history
src/parser/antlr_input.cpp		diff \| blob \| history
src/parser/antlr_input_imports.cpp		diff \| blob \| history
src/parser/antlr_line_buffered_input.h		diff \| blob \| history
src/parser/antlr_tracing.h		diff \| blob \| history
src/parser/cvc/Cvc.g		diff \| blob \| history
src/parser/cvc/README		diff \| blob \| history
src/parser/parser.h		diff \| blob \| history
src/parser/parser_builder.h		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
src/parser/smt2/smt2.cpp		diff \| blob \| history
src/parser/tptp/Tptp.g		diff \| blob \| history
src/preprocessing/passes/unconstrained_simplifier.cpp		diff \| blob \| history
src/printer/cvc/cvc_printer.cpp		diff \| blob \| history
src/printer/printer.cpp		diff \| blob \| history
src/prop/README.minisat		diff \| blob \| history
src/prop/bvminisat/utils/System.cc		diff \| blob \| history
src/prop/cadical.cpp		diff \| blob \| history
src/prop/cadical.h		diff \| blob \| history
src/prop/minisat/CVC4-README		diff \| blob \| history
src/prop/minisat/core/Solver.cc		diff \| blob \| history
src/prop/minisat/core/Solver.h		diff \| blob \| history
src/prop/minisat/minisat.cpp		diff \| blob \| history
src/prop/sat_solver_factory.cpp		diff \| blob \| history
src/smt/command.cpp		diff \| blob \| history
src/smt/dump.cpp		diff \| blob \| history
src/smt/dump.h		diff \| blob \| history
src/smt/logic_exception.h		diff \| blob \| history
src/smt/managed_ostreams.cpp		diff \| blob \| history
src/smt/model.h		diff \| blob \| history
src/smt/options_manager.cpp		diff \| blob \| history
src/smt/smt_engine.cpp		diff \| blob \| history
src/smt/smt_engine.h		diff \| blob \| history
src/smt/update_ostream.h		diff \| blob \| history
src/theory/arith/approx_simplex.cpp		diff \| blob \| history
src/theory/arith/attempt_solution_simplex.cpp		diff \| blob \| history
src/theory/arith/constraint.cpp		diff \| blob \| history
src/theory/arith/dio_solver.cpp		diff \| blob \| history
src/theory/arith/dual_simplex.cpp		diff \| blob \| history
src/theory/arith/fc_simplex.cpp		diff \| blob \| history
src/theory/arith/kinds		diff \| blob \| history
src/theory/arith/linear_equality.cpp		diff \| blob \| history
src/theory/arith/nl/cad/constraints.h		diff \| blob \| history
src/theory/arith/nl/cad/proof_generator.cpp		diff \| blob \| history
src/theory/arith/nl/cad/proof_generator.h		diff \| blob \| history
src/theory/arith/nl/icp/icp_solver.cpp		diff \| blob \| history
src/theory/arith/nl/poly_conversion.cpp		diff \| blob \| history
src/theory/arith/nl/poly_conversion.h		diff \| blob \| history
src/theory/arith/soi_simplex.cpp		diff \| blob \| history
src/theory/arith/theory_arith_private.cpp		diff \| blob \| history
src/theory/builtin/kinds		diff \| blob \| history
src/theory/datatypes/datatypes_rewriter.h		diff \| blob \| history
src/theory/fp/fp_converter.cpp		diff \| blob \| history
src/theory/fp/fp_converter.h		diff \| blob \| history
src/theory/incomplete_id.h		diff \| blob \| history
src/theory/interrupted.h		diff \| blob \| history
src/theory/logic_info.h		diff \| blob \| history
src/theory/mkrewriter		diff \| blob \| history
src/theory/mktheorytraits		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator.h		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h		diff \| blob \| history
src/theory/quantifiers/ematching/trigger.h		diff \| blob \| history
src/theory/quantifiers/fmf/full_model_check.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/model_engine.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_attributes.cpp		diff \| blob \| history
src/theory/quantifiers/query_generator.cpp		diff \| blob \| history
src/theory/quantifiers/term_tuple_enumerator.cpp		diff \| blob \| history
src/theory/sets/kinds		diff \| blob \| history
src/theory/sets/theory_sets_rels.h		diff \| blob \| history
src/theory/substitutions.cpp		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/theory/uf/cardinality_extension.cpp		diff \| blob \| history
src/util/cardinality.h		diff \| blob \| history
src/util/floatingpoint_literal_symfpu_traits.h.in		diff \| blob \| history
src/util/sexpr.cpp		diff \| blob \| history
src/util/string.h		diff \| blob \| history
src/util/utility.cpp		diff \| blob \| history
src/util/utility.h		diff \| blob \| history
test/api/interactive_shell.py		diff \| blob \| history
test/api/ouroborous.cpp		diff \| blob \| history
test/api/sep_log_api.cpp		diff \| blob \| history
test/regress/README.md		diff \| blob \| history
test/regress/regress0/sygus/no-logic.sy		diff \| blob \| history
test/regress/run_regression.py		diff \| blob \| history
test/unit/api/datatype_api_black.cpp		diff \| blob \| history
test/unit/api/grammar_black.cpp		diff \| blob \| history
test/unit/api/op_black.cpp		diff \| blob \| history
test/unit/api/op_white.cpp		diff \| blob \| history
test/unit/api/solver_black.cpp		diff \| blob \| history
test/unit/api/sort_black.cpp		diff \| blob \| history
test/unit/api/term_black.cpp		diff \| blob \| history
test/unit/main/interactive_shell_black.cpp		diff \| blob \| history
test/unit/node/node_black.cpp		diff \| blob \| history
test/unit/parser/parser_black.cpp		diff \| blob \| history
test/unit/parser/parser_builder_black.cpp		diff \| blob \| history
test/unit/theory/theory_sets_type_rules_white.cpp		diff \| blob \| history
test/unit/util/boolean_simplification_black.cpp		diff \| blob \| history
test/unit/util/output_black.cpp		diff \| blob \| history

RSS Atom