projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9fae998) | patch
Rename cad to coverings (#8187)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Tue, 1 Mar 2022 00:37:13 +0000 (01:37 +0100)
committerGitHub <noreply@github.com>
Tue, 1 Mar 2022 00:37:13 +0000 (00:37 +0000)
commit8f1ecaaef1ce13533a7dd8b19a3373a64f9edab4
treeb16cc819fea2b47b5c05a50abb98d04f4dad2f31tree
parent9fae9984fdb6e46713839655534e10639ec7f9d0commit | diff
Rename cad to coverings (#8187)

The nonlinear subsolver that implements cylindrical algebraic coverings is still called cad in many places, which really was a misnomer from the beginning. This PR renames it everywhere.
56 files changed:
src/CMakeLists.txt diff | blob | history
src/options/arith_options.toml diff | blob | history
src/proof/lazy_tree_proof_generator.h diff | blob | history
src/proof/proof_rule.cpp diff | blob | history
src/proof/proof_rule.h diff | blob | history
src/smt/set_defaults.cpp diff | blob | history
src/theory/arith/nl/cad/cdcac.cpp [deleted file] blob | history
src/theory/arith/nl/cad/cdcac.h [deleted file] blob | history
src/theory/arith/nl/cad/cdcac_utils.cpp [deleted file] blob | history
src/theory/arith/nl/cad/cdcac_utils.h [deleted file] blob | history
src/theory/arith/nl/cad/constraints.cpp [deleted file] blob | history
src/theory/arith/nl/cad/constraints.h [deleted file] blob | history
src/theory/arith/nl/cad/lazard_evaluation.cpp [deleted file] blob | history
src/theory/arith/nl/cad/lazard_evaluation.h [deleted file] blob | history
src/theory/arith/nl/cad/projections.cpp [deleted file] blob | history
src/theory/arith/nl/cad/projections.h [deleted file] blob | history
src/theory/arith/nl/cad/proof_checker.cpp [deleted file] blob | history
src/theory/arith/nl/cad/proof_checker.h [deleted file] blob | history
src/theory/arith/nl/cad/proof_generator.cpp [deleted file] blob | history
src/theory/arith/nl/cad/proof_generator.h [deleted file] blob | history
src/theory/arith/nl/cad/variable_ordering.cpp [deleted file] blob | history
src/theory/arith/nl/cad/variable_ordering.h [deleted file] blob | history
src/theory/arith/nl/cad_solver.cpp [deleted file] blob | history
src/theory/arith/nl/cad_solver.h [deleted file] blob | history
src/theory/arith/nl/coverings/cdcac.cpp [new file with mode: 0644] blob
src/theory/arith/nl/coverings/cdcac.h [new file with mode: 0644] blob
src/theory/arith/nl/coverings/cdcac_utils.cpp [new file with mode: 0644] blob
src/theory/arith/nl/coverings/cdcac_utils.h [new file with mode: 0644] blob
src/theory/arith/nl/coverings/constraints.cpp [new file with mode: 0644] blob
src/theory/arith/nl/coverings/constraints.h [new file with mode: 0644] blob
src/theory/arith/nl/coverings/lazard_evaluation.cpp [new file with mode: 0644] blob
src/theory/arith/nl/coverings/lazard_evaluation.h [new file with mode: 0644] blob
src/theory/arith/nl/coverings/projections.cpp [new file with mode: 0644] blob
src/theory/arith/nl/coverings/projections.h [new file with mode: 0644] blob
src/theory/arith/nl/coverings/proof_checker.cpp [new file with mode: 0644] blob
src/theory/arith/nl/coverings/proof_checker.h [new file with mode: 0644] blob
src/theory/arith/nl/coverings/proof_generator.cpp [new file with mode: 0644] blob
src/theory/arith/nl/coverings/proof_generator.h [new file with mode: 0644] blob
src/theory/arith/nl/coverings/variable_ordering.cpp [new file with mode: 0644] blob
src/theory/arith/nl/coverings/variable_ordering.h [new file with mode: 0644] blob
src/theory/arith/nl/coverings_solver.cpp [new file with mode: 0644] blob
src/theory/arith/nl/coverings_solver.h [new file with mode: 0644] blob
src/theory/arith/nl/nonlinear_extension.cpp diff | blob | history
src/theory/arith/nl/nonlinear_extension.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/nl/strategy.cpp diff | blob | history
src/theory/arith/nl/strategy.h diff | blob | history
src/theory/inference_id.cpp diff | blob | history
src/theory/inference_id.h diff | blob | history
test/regress/regress0/nl/issue5726-downpolys.smt2 diff | blob | history
test/regress/regress0/nl/issue5726-sqfactor.smt2 diff | blob | history
test/unit/api/cpp/theory_arith_nl_black.cpp diff | blob | history
test/unit/theory/CMakeLists.txt diff | blob | history
test/unit/theory/theory_arith_cad_white.cpp [deleted file] blob | history
test/unit/theory/theory_arith_coverings_white.cpp [new file with mode: 0644] blob