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

author	Mathias Preiner <mathias.preiner@gmail.com>
	Wed, 21 Apr 2021 17:21:34 +0000 (10:21 -0700)
committer	GitHub <noreply@github.com>
	Wed, 21 Apr 2021 17:21:34 +0000 (10:21 -0700)
commit	ae5ee4b07dc3d3c792e7fe7f382ff490dd28aca4
tree	a7c2ab8013f46dbea75fcd6e7da3fb83e2012b2f	tree
parent	86aa9bc35ba9dc9a57913a2ffc71619c7657cc35	commit \| diff

Goodbye CVC4, hello cvc5! (#6371)

This commits changes the build system to cvc5 and removes the remaining
occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.

221 files changed:

.github/workflows/ci.yml		diff \| blob \| history
AUTHORS		diff \| blob \| history
CMakeLists.txt		diff \| blob \| history
CONTRIBUTING.md		diff \| blob \| history
COPYING		diff \| blob \| history
INSTALL.md		diff \| blob \| history
README.md		diff \| blob \| history
cmake/CVC4Config.cmake.in	[deleted file]	blob \| history
cmake/ConfigCompetition.cmake		diff \| blob \| history
cmake/ConfigDebug.cmake		diff \| blob \| history
cmake/ConfigProduction.cmake		diff \| blob \| history
cmake/ConfigTesting.cmake		diff \| blob \| history
cmake/ConfigureCVC4.cmake	[deleted file]	blob \| history
cmake/ConfigureCvc5.cmake	[new file with mode: 0644]	blob
cmake/Helpers.cmake		diff \| blob \| history
cmake/cvc5Config.cmake.in	[new file with mode: 0644]	blob
contrib/README		diff \| blob \| history
contrib/alttheoryskel/README.WHATS-NEXT	[deleted file]	blob \| history
contrib/alttheoryskel/kinds	[deleted file]	blob \| history
contrib/alttheoryskel/options	[deleted file]	blob \| history
contrib/alttheoryskel/options_handlers.h	[deleted file]	blob \| history
contrib/alttheoryskel/theory_DIR.cpp	[deleted file]	blob \| history
contrib/alttheoryskel/theory_DIR.h	[deleted file]	blob \| history
contrib/competitions/smt-comp/run-script-smtcomp-current		diff \| blob \| history
contrib/competitions/smt-comp/run-script-smtcomp-current-incremental		diff \| blob \| history
contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation		diff \| blob \| history
contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores		diff \| blob \| history
contrib/cut-release	[deleted file]	blob \| history
contrib/cvc4_strict_smtlib	[deleted file]	blob \| history
contrib/cvc5_strict_smtlib	[new file with mode: 0644]	blob
contrib/debug-keys	[deleted file]	blob \| history
contrib/depgraph	[deleted file]	blob \| history
contrib/dimacs_to_smt.pl	[deleted file]	blob \| history
contrib/get-abc		diff \| blob \| history
contrib/get-authors		diff \| blob \| history
contrib/get-drat2er		diff \| blob \| history
contrib/get-glpk-cut-log		diff \| blob \| history
contrib/get-lfsc-checker		diff \| blob \| history
contrib/get-script-header.sh		diff \| blob \| history
contrib/learn_resource_weights.py		diff \| blob \| history
contrib/luby.c	[deleted file]	blob \| history
contrib/mk_starexec	[deleted file]	blob \| history
contrib/new-theory	[deleted file]	blob \| history
contrib/new-theory.awk	[deleted file]	blob \| history
contrib/optionsskel/DIR_options.toml	[deleted file]	blob \| history
contrib/spellcheck	[deleted file]	blob \| history
contrib/sygus-v1-to-v2.sh	[deleted file]	blob \| history
contrib/test_install_headers.sh	[deleted file]	blob \| history
contrib/theoryskel/README.WHATS-NEXT	[deleted file]	blob \| history
contrib/theoryskel/kinds	[deleted file]	blob \| history
contrib/theoryskel/theory_DIR.cpp	[deleted file]	blob \| history
contrib/theoryskel/theory_DIR.h	[deleted file]	blob \| history
contrib/theoryskel/theory_DIR_rewriter.h	[deleted file]	blob \| history
contrib/theoryskel/theory_DIR_type_rules.h	[deleted file]	blob \| history
contrib/update-copyright.pl		diff \| blob \| history
cvc4autoconfig.h.in	[deleted file]	blob \| history
doc/CMakeLists.txt		diff \| blob \| history
doc/cvc4.1_template.in	[deleted file]	blob \| history
doc/cvc4.5.in	[deleted file]	blob \| history
doc/cvc5.1_template.in	[new file with mode: 0644]	blob
doc/cvc5.5.in	[new file with mode: 0644]	blob
doc/libcvc4.3.in	[deleted file]	blob \| history
doc/libcvc4parser.3.in	[deleted file]	blob \| history
doc/libcvc5.3.in	[new file with mode: 0644]	blob
doc/libcvc5parser.3.in	[new file with mode: 0644]	blob
doc/mainpage.md	[deleted file]	blob \| history
docs/cpp.rst	[new file with mode: 0644]	blob
docs/cpp/Doxyfile.in		diff \| blob \| history
docs/cpp/exceptions.rst		diff \| blob \| history
examples/CMakeLists.txt		diff \| blob \| history
examples/README.md		diff \| blob \| history
examples/SimpleVC.py	[deleted file]	blob \| history
examples/api/CMakeLists.txt		diff \| blob \| history
examples/api/java/CMakeLists.txt		diff \| blob \| history
examples/api/python/bitvectors.py		diff \| blob \| history
examples/api/python/bitvectors_and_arrays.py		diff \| blob \| history
examples/api/python/combination.py		diff \| blob \| history
examples/api/python/datatypes.py		diff \| blob \| history
examples/api/python/exceptions.py		diff \| blob \| history
examples/api/python/extract.py		diff \| blob \| history
examples/api/python/floating_point.py		diff \| blob \| history
examples/api/python/helloworld.py		diff \| blob \| history
examples/api/python/linear_arith.py		diff \| blob \| history
examples/api/python/sequences.py		diff \| blob \| history
examples/api/python/sets.py		diff \| blob \| history
examples/api/python/strings.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/CMakeLists.txt		diff \| blob \| history
examples/sets-translate/CMakeLists.txt		diff \| blob \| history
examples/simple_vc_quant_cxx.cpp		diff \| blob \| history
src/CMakeLists.txt		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/parsekinds.py		diff \| blob \| history
src/api/python/CMakeLists.txt		diff \| blob \| history
src/api/python/cvc4.pxd	[deleted file]	blob \| history
src/api/python/cvc4.pxi	[deleted file]	blob \| history
src/api/python/cvc5.pxd	[new file with mode: 0644]	blob
src/api/python/cvc5.pxi	[new file with mode: 0644]	blob
src/api/python/genkinds.py.in		diff \| blob \| history
src/api/python/pycvc4.pyx	[deleted file]	blob \| history
src/api/python/pycvc5.pyx	[new file with mode: 0644]	blob
src/api/python/setup.py.in		diff \| blob \| history
src/base/CMakeLists.txt		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/cvc5config.h.in	[new file with mode: 0644]	blob
src/base/exception.h		diff \| blob \| history
src/base/output.cpp		diff \| blob \| history
src/base/output.h		diff \| blob \| history
src/context/CMakeLists.txt		diff \| blob \| history
src/expr/CMakeLists.txt		diff \| blob \| history
src/expr/node.h		diff \| blob \| history
src/expr/node_manager.cpp		diff \| blob \| history
src/expr/node_manager.h		diff \| blob \| history
src/expr/node_value.h		diff \| blob \| history
src/expr/symbol_manager.h		diff \| blob \| history
src/expr/symbol_table.h		diff \| blob \| history
src/expr/type_node.h		diff \| blob \| history
src/fix-install-headers.sh		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/lib/ffs.h		diff \| blob \| history
src/lib/replacements.h		diff \| blob \| history
src/main/CMakeLists.txt		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/main/time_limit.cpp		diff \| blob \| history
src/options/CMakeLists.txt		diff \| blob \| history
src/options/datatypes_options.toml		diff \| blob \| history
src/options/language.h		diff \| blob \| history
src/options/mkoptions.py		diff \| blob \| history
src/options/open_ostream.cpp		diff \| blob \| history
src/options/open_ostream.h		diff \| blob \| history
src/options/option_exception.h		diff \| blob \| history
src/options/options.h		diff \| blob \| history
src/options/options_handler.cpp		diff \| blob \| history
src/options/options_template.cpp		diff \| blob \| history
src/options/set_language.h		diff \| blob \| history
src/parser/CMakeLists.txt		diff \| blob \| history
src/parser/antlr_tracing.h		diff \| blob \| history
src/parser/input.h		diff \| blob \| history
src/parser/parser.h		diff \| blob \| history
src/parser/parser_builder.h		diff \| blob \| history
src/parser/parser_exception.h		diff \| blob \| history
src/prop/bvminisat/bvminisat.cpp		diff \| blob \| history
src/prop/bvminisat/bvminisat.h		diff \| blob \| history
src/prop/bvminisat/core/Solver.h		diff \| blob \| history
src/prop/cryptominisat.cpp		diff \| blob \| history
src/prop/cryptominisat.h		diff \| blob \| history
src/smt/command.h		diff \| blob \| history
src/smt/smt_engine.h		diff \| blob \| history
src/theory/CMakeLists.txt		diff \| blob \| history
src/theory/arith/approx_simplex.cpp		diff \| blob \| history
src/theory/arith/cut_log.cpp		diff \| blob \| history
src/theory/arith/cut_log.h		diff \| blob \| history
src/theory/bv/bv_subtheory_algebraic.cpp		diff \| blob \| history
src/theory/logic_info.h		diff \| blob \| history
src/theory/quantifiers/term_tuple_enumerator.cpp		diff \| blob \| history
src/theory/sets/cardinality_extension.cpp		diff \| blob \| history
src/util/CMakeLists.txt		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/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/safe_print.h		diff \| blob \| history
src/util/unsafe_interrupt_exception.h		diff \| blob \| history
test/CMakeLists.txt		diff \| blob \| history
test/api/CMakeLists.txt		diff \| blob \| history
test/api/boilerplate.cpp		diff \| blob \| history
test/api/interactive_shell.py		diff \| blob \| history
test/api/python/CMakeLists.txt		diff \| blob \| history
test/api/python/test_datatype_api.py		diff \| blob \| history
test/api/python/test_grammar.py		diff \| blob \| history
test/api/python/test_term.py		diff \| blob \| history
test/api/python/test_to_python_obj.py		diff \| blob \| history
test/api/sep_log_api.cpp		diff \| blob \| history
test/java/BitVectors.java	[deleted file]	blob \| history
test/java/BitVectorsAndArrays.java	[deleted file]	blob \| history
test/java/CMakeLists.txt	[deleted file]	blob \| history
test/java/Combination.java	[deleted file]	blob \| history
test/java/HelloWorld.java	[deleted file]	blob \| history
test/java/Issue2846.java	[deleted file]	blob \| history
test/java/LinearArith.java	[deleted file]	blob \| history
test/python/CMakeLists.txt		diff \| blob \| history
test/python/unit/api/test_solver.py		diff \| blob \| history
test/python/unit/api/test_sort.py		diff \| blob \| history
test/regress/CMakeLists.txt		diff \| blob \| history
test/unit/CMakeLists.txt		diff \| blob \| history
test/unit/api/CMakeLists.txt		diff \| blob \| history
test/unit/api/solver_black.cpp		diff \| blob \| history
test/unit/base/CMakeLists.txt		diff \| blob \| history
test/unit/context/CMakeLists.txt		diff \| blob \| history
test/unit/main/CMakeLists.txt		diff \| blob \| history
test/unit/memory.h		diff \| blob \| history
test/unit/node/CMakeLists.txt		diff \| blob \| history
test/unit/parser/CMakeLists.txt		diff \| blob \| history
test/unit/preprocessing/CMakeLists.txt		diff \| blob \| history
test/unit/printer/CMakeLists.txt		diff \| blob \| history
test/unit/prop/CMakeLists.txt		diff \| blob \| history
test/unit/theory/CMakeLists.txt		diff \| blob \| history
test/unit/util/CMakeLists.txt		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

RSS Atom