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

author	Aina Niemetz <aina.niemetz@gmail.com>
	Sat, 10 Apr 2021 00:22:07 +0000 (17:22 -0700)
committer	GitHub <noreply@github.com>
	Sat, 10 Apr 2021 00:22:07 +0000 (17:22 -0700)
commit	f87f038c5f0821d0fefb01cea00bfdec6004da91
tree	d948178e1c0d2dc459a976f0d187d2d41a5437c0	tree
parent	550c49a7dd2b13ea29743458336f0c0a0fb6099a	commit \| diff

Rename CVC4_ macros to CVC5_. (#6327)

203 files changed:

CMakeLists.txt		diff \| blob \| history
cmake/CVC4Config.cmake.in		diff \| blob \| history
cmake/ConfigCompetition.cmake		diff \| blob \| history
cmake/ConfigDebug.cmake		diff \| blob \| history
cmake/ConfigureCVC4.cmake		diff \| blob \| history
cmake/Toolchain-mingw64.cmake		diff \| blob \| history
cvc4autoconfig.h.in		diff \| blob \| history
examples/CMakeLists.txt		diff \| blob \| history
examples/api/CMakeLists.txt		diff \| blob \| history
examples/api/java/CMakeLists.txt		diff \| blob \| history
examples/api/python/CMakeLists.txt		diff \| blob \| history
examples/nra-translate/CMakeLists.txt		diff \| blob \| history
src/CMakeLists.txt		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/python/CMakeLists.txt		diff \| blob \| history
src/api/python/setup.py.in		diff \| blob \| history
src/base/check.cpp		diff \| blob \| history
src/base/check.h		diff \| blob \| history
src/base/configuration.cpp		diff \| blob \| history
src/base/configuration.h		diff \| blob \| history
src/base/configuration_private.h		diff \| blob \| history
src/base/exception.cpp		diff \| blob \| history
src/base/exception.h		diff \| blob \| history
src/base/output.h		diff \| blob \| history
src/context/cdlist_forward.h		diff \| blob \| history
src/context/context_mm.cpp		diff \| blob \| history
src/context/context_mm.h		diff \| blob \| history
src/decision/justification_heuristic.cpp		diff \| blob \| history
src/expr/attribute.h		diff \| blob \| history
src/expr/attribute_internals.h		diff \| blob \| history
src/expr/metakind_template.cpp		diff \| blob \| history
src/expr/node.cpp		diff \| blob \| history
src/expr/node.h		diff \| blob \| history
src/expr/node_builder.cpp		diff \| blob \| history
src/expr/node_builder.h		diff \| blob \| history
src/expr/node_manager.cpp		diff \| blob \| history
src/expr/node_value.h		diff \| blob \| history
src/expr/type_node.h		diff \| blob \| history
src/include/cvc4_private.h		diff \| blob \| history
src/include/cvc4_private_library.h		diff \| blob \| history
src/include/cvc4_public.h		diff \| blob \| history
src/lib/replacements.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/main.h		diff \| blob \| history
src/main/signal_handlers.cpp		diff \| blob \| history
src/options/mkoptions.py		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/parser/CMakeLists.txt		diff \| blob \| history
src/parser/antlr_input.cpp		diff \| blob \| history
src/parser/antlr_line_buffered_input.cpp		diff \| blob \| history
src/parser/antlr_tracing.h		diff \| blob \| history
src/parser/cvc/Cvc.g		diff \| blob \| history
src/parser/memory_mapped_input_buffer.cpp		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
src/parser/smt2/smt2.cpp		diff \| blob \| history
src/parser/tptp/tptp.cpp		diff \| blob \| history
src/preprocessing/passes/bv_gauss.cpp		diff \| blob \| history
src/preprocessing/passes/bv_to_int.cpp		diff \| blob \| history
src/preprocessing/passes/miplib_trick.cpp		diff \| blob \| history
src/preprocessing/passes/non_clausal_simp.cpp		diff \| blob \| history
src/preprocessing/passes/unconstrained_simplifier.cpp		diff \| blob \| history
src/preprocessing/util/ite_utilities.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/prop/bvminisat/simp/SimpSolver.cc		diff \| blob \| history
src/prop/cadical.cpp		diff \| blob \| history
src/prop/cadical.h		diff \| blob \| history
src/prop/cnf_stream.cpp		diff \| blob \| history
src/prop/cryptominisat.cpp		diff \| blob \| history
src/prop/cryptominisat.h		diff \| blob \| history
src/prop/kissat.cpp		diff \| blob \| history
src/prop/kissat.h		diff \| blob \| history
src/prop/minisat/simp/SimpSolver.cc		diff \| blob \| history
src/prop/proof_cnf_stream.cpp		diff \| blob \| history
src/prop/sat_proof_manager.cpp		diff \| blob \| history
src/prop/sat_solver_factory.cpp		diff \| blob \| history
src/prop/theory_proxy.h		diff \| blob \| history
src/smt/dump.cpp		diff \| blob \| history
src/smt/dump.h		diff \| blob \| history
src/smt/listeners.cpp		diff \| blob \| history
src/smt/managed_ostreams.cpp		diff \| blob \| history
src/smt/set_defaults.cpp		diff \| blob \| history
src/smt/smt_engine_state.cpp		diff \| blob \| history
src/smt_util/boolean_simplification.h		diff \| blob \| history
src/theory/arith/approx_simplex.cpp		diff \| blob \| history
src/theory/arith/arith_static_learner.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/error_set.h		diff \| blob \| history
src/theory/arith/nl/cad/cdcac.cpp		diff \| blob \| history
src/theory/arith/nl/cad/cdcac.h		diff \| blob \| history
src/theory/arith/nl/cad/cdcac_utils.cpp		diff \| blob \| history
src/theory/arith/nl/cad/cdcac_utils.h		diff \| blob \| history
src/theory/arith/nl/cad/constraints.cpp		diff \| blob \| history
src/theory/arith/nl/cad/constraints.h		diff \| blob \| history
src/theory/arith/nl/cad/projections.cpp		diff \| blob \| history
src/theory/arith/nl/cad/projections.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/cad/variable_ordering.cpp		diff \| blob \| history
src/theory/arith/nl/cad/variable_ordering.h		diff \| blob \| history
src/theory/arith/nl/cad_solver.cpp		diff \| blob \| history
src/theory/arith/nl/cad_solver.h		diff \| blob \| history
src/theory/arith/nl/icp/candidate.cpp		diff \| blob \| history
src/theory/arith/nl/icp/candidate.h		diff \| blob \| history
src/theory/arith/nl/icp/icp_solver.cpp		diff \| blob \| history
src/theory/arith/nl/icp/icp_solver.h		diff \| blob \| history
src/theory/arith/nl/icp/intersection.cpp		diff \| blob \| history
src/theory/arith/nl/icp/intersection.h		diff \| blob \| history
src/theory/arith/nl/icp/interval.h		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/partial_model.cpp		diff \| blob \| history
src/theory/arith/theory_arith_private.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays.cpp		diff \| blob \| history
src/theory/booleans/circuit_propagator.h		diff \| blob \| history
src/theory/bv/bitblast/aig_bitblaster.cpp		diff \| blob \| history
src/theory/bv/bitblast/aig_bitblaster.h		diff \| blob \| history
src/theory/bv/bv_eager_solver.cpp		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_simplification.h		diff \| blob \| history
src/theory/fp/fp_converter.cpp		diff \| blob \| history
src/theory/fp/fp_converter.h		diff \| blob \| history
src/theory/fp/theory_fp_rewriter.cpp		diff \| blob \| history
src/theory/fp/theory_fp_type_rules.cpp		diff \| blob \| history
src/theory/model_manager_distributed.cpp		diff \| blob \| history
src/theory/quantifiers/candidate_rewrite_filter.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp		diff \| blob \| history
src/theory/quantifiers/fun_def_evaluator.cpp		diff \| blob \| history
src/theory/quantifiers/instantiate.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif_io.cpp		diff \| blob \| history
src/theory/quantifiers/term_tuple_enumerator.cpp		diff \| blob \| history
src/theory/rewriter.cpp		diff \| blob \| history
src/theory/rewriter.h		diff \| blob \| history
src/theory/strings/arith_entail.cpp		diff \| blob \| history
src/theory/strings/core_solver.cpp		diff \| blob \| history
src/theory/theory.h		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_model.cpp		diff \| blob \| history
src/theory/theory_model_builder.cpp		diff \| blob \| history
src/theory/type_enumerator.h		diff \| blob \| history
src/theory/uf/equality_engine.cpp		diff \| blob \| history
src/theory/uf/symmetry_breaker.cpp		diff \| blob \| history
src/theory/valuation.h		diff \| blob \| history
src/util/CMakeLists.txt		diff \| blob \| history
src/util/floatingpoint.cpp		diff \| blob \| history
src/util/floatingpoint_literal_symfpu.cpp		diff \| blob \| history
src/util/floatingpoint_literal_symfpu.h.in		diff \| blob \| history
src/util/floatingpoint_literal_symfpu_traits.cpp		diff \| blob \| history
src/util/floatingpoint_literal_symfpu_traits.h.in		diff \| blob \| history
src/util/hash.h		diff \| blob \| history
src/util/integer.h.in		diff \| blob \| history
src/util/integer_cln_imp.cpp		diff \| blob \| history
src/util/integer_cln_imp.h		diff \| blob \| history
src/util/integer_gmp_imp.cpp		diff \| blob \| history
src/util/integer_gmp_imp.h		diff \| blob \| history
src/util/poly_util.cpp		diff \| blob \| history
src/util/poly_util.h		diff \| blob \| history
src/util/rational.h.in		diff \| blob \| history
src/util/rational_cln_imp.cpp		diff \| blob \| history
src/util/rational_cln_imp.h		diff \| blob \| history
src/util/rational_gmp_imp.cpp		diff \| blob \| history
src/util/rational_gmp_imp.h		diff \| blob \| history
src/util/real_algebraic_number.h.in		diff \| blob \| history
src/util/real_algebraic_number_poly_imp.cpp		diff \| blob \| history
src/util/roundingmode.h		diff \| blob \| history
src/util/sampler.cpp		diff \| blob \| history
src/util/statistics.cpp		diff \| blob \| history
src/util/statistics_registry.cpp		diff \| blob \| history
src/util/statistics_registry.h		diff \| blob \| history
src/util/stats_base.cpp		diff \| blob \| history
src/util/stats_base.h		diff \| blob \| history
src/util/stats_histogram.h		diff \| blob \| history
src/util/stats_timer.cpp		diff \| blob \| history
src/util/string.cpp		diff \| blob \| history
src/util/utility.cpp		diff \| blob \| history
test/api/CMakeLists.txt		diff \| blob \| history
test/api/issue4889.cpp		diff \| blob \| history
test/regress/run_regression.py		diff \| blob \| history
test/unit/CMakeLists.txt		diff \| blob \| history
test/unit/context/cdlist_black.cpp		diff \| blob \| history
test/unit/context/context_black.cpp		diff \| blob \| history
test/unit/context/context_mm_black.cpp		diff \| blob \| history
test/unit/memory.h		diff \| blob \| history
test/unit/node/kind_map_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_manager_black.cpp		diff \| blob \| history
test/unit/node/node_manager_white.cpp		diff \| blob \| history
test/unit/parser/parser_black.cpp		diff \| blob \| history
test/unit/util/CMakeLists.txt		diff \| blob \| history
test/unit/util/assert_white.cpp		diff \| blob \| history
test/unit/util/binary_heap_black.cpp		diff \| blob \| history
test/unit/util/boolean_simplification_black.cpp		diff \| blob \| history
test/unit/util/check_white.cpp		diff \| blob \| history
test/unit/util/configuration_black.cpp		diff \| blob \| history
test/unit/util/output_black.cpp		diff \| blob \| history
test/unit/util/real_algebraic_number_black.cpp		diff \| blob \| history
test/unit/util/stats_black.cpp		diff \| blob \| history

RSS Atom