From fc0512b6d13349a91da5ac6617acebc41cbd238c Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 28 Apr 2021 20:32:42 +0200 Subject: [PATCH] Remove exception headers from options.h (#6456) This PR removes two headers for exceptions from options.h, and instead pushes the includes to a couple of source files. --- src/api/cpp/cvc5.cpp | 2 ++ src/main/main.cpp | 1 + src/main/time_limit.cpp | 1 + src/options/module_template.cpp | 8 ++++---- src/options/open_ostream.cpp | 2 +- src/options/options.h | 2 -- src/smt/abduction_solver.cpp | 1 + src/smt/assertions.cpp | 1 + src/smt/check_models.cpp | 1 + src/smt/command.cpp | 1 + src/smt/interpolation_solver.cpp | 1 + src/smt/quant_elim_solver.cpp | 1 + src/smt/smt_engine.cpp | 1 + src/smt/smt_engine_state.cpp | 2 ++ src/smt/sygus_solver.cpp | 2 ++ src/theory/quantifiers/sygus/sygus_interpol.cpp | 1 + src/util/resource_manager.cpp | 1 + 17 files changed, 22 insertions(+), 7 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index ce065a75f..6ee1409d6 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -38,6 +38,7 @@ #include "api/cpp/cvc5_checks.h" #include "base/check.h" #include "base/configuration.h" +#include "base/modal_exception.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/dtype_selector.h" @@ -50,6 +51,7 @@ #include "expr/sequence.h" #include "expr/type_node.h" #include "options/main_options.h" +#include "options/option_exception.h" #include "options/options.h" #include "options/smt_options.h" #include "proof/unsat_core.h" diff --git a/src/main/main.cpp b/src/main/main.cpp index 6a7baebb3..b96598b0b 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -26,6 +26,7 @@ #include "main/command_executor.h" #include "main/interactive_shell.h" #include "options/language.h" +#include "options/option_exception.h" #include "options/options.h" #include "parser/parser.h" #include "parser/parser_builder.h" diff --git a/src/main/time_limit.cpp b/src/main/time_limit.cpp index 82cfda017..0f0a824f6 100644 --- a/src/main/time_limit.cpp +++ b/src/main/time_limit.cpp @@ -55,6 +55,7 @@ #include #include +#include "base/exception.h" #include "signal_handlers.h" namespace cvc5 { diff --git a/src/options/module_template.cpp b/src/options/module_template.cpp index 0de77e8a6..e0b3f79d1 100644 --- a/src/options/module_template.cpp +++ b/src/options/module_template.cpp @@ -16,17 +16,17 @@ * expands this template and generates a _options.cpp file. */ -#include "options/options_holder.h" -#include "base/check.h" - #include +#include "base/check.h" +#include "options/option_exception.h" +#include "options/options_holder.h" + // clang-format off namespace cvc5 { ${accs}$ - namespace options { ${defs}$ diff --git a/src/options/open_ostream.cpp b/src/options/open_ostream.cpp index 9ebea6da0..bb6efb5bc 100644 --- a/src/options/open_ostream.cpp +++ b/src/options/open_ostream.cpp @@ -18,7 +18,6 @@ #include "options/open_ostream.h" - #include #include #include @@ -28,6 +27,7 @@ #include #include "lib/strtok_r.h" +#include "options/option_exception.h" #include "options/parser_options.h" namespace cvc5 { diff --git a/src/options/options.h b/src/options/options.h index a8fc50b68..4d8a979c6 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -24,10 +24,8 @@ #include #include "base/listener.h" -#include "base/modal_exception.h" #include "cvc5_export.h" #include "options/language.h" -#include "options/option_exception.h" #include "options/printer_modes.h" namespace cvc5 { diff --git a/src/smt/abduction_solver.cpp b/src/smt/abduction_solver.cpp index 7e29e4849..23f46cc58 100644 --- a/src/smt/abduction_solver.cpp +++ b/src/smt/abduction_solver.cpp @@ -17,6 +17,7 @@ #include +#include "base/modal_exception.h" #include "options/smt_options.h" #include "smt/smt_engine.h" #include "theory/quantifiers/quantifiers_attributes.h" diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp index 2fb83f898..779a63c29 100644 --- a/src/smt/assertions.cpp +++ b/src/smt/assertions.cpp @@ -17,6 +17,7 @@ #include +#include "base/modal_exception.h" #include "expr/node_algorithm.h" #include "options/base_options.h" #include "options/expr_options.h" diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp index ebc8f46a1..f6d1da345 100644 --- a/src/smt/check_models.cpp +++ b/src/smt/check_models.cpp @@ -15,6 +15,7 @@ #include "smt/check_models.h" +#include "base/modal_exception.h" #include "options/smt_options.h" #include "smt/model.h" #include "smt/node_command.h" diff --git a/src/smt/command.cpp b/src/smt/command.cpp index b2a1590b0..e49658c9d 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -24,6 +24,7 @@ #include "api/cpp/cvc5.h" #include "base/check.h" +#include "base/modal_exception.h" #include "base/output.h" #include "expr/expr_iomanip.h" #include "expr/node.h" diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp index 48d81a91f..813fc45cf 100644 --- a/src/smt/interpolation_solver.cpp +++ b/src/smt/interpolation_solver.cpp @@ -17,6 +17,7 @@ #include +#include "base/modal_exception.h" #include "options/smt_options.h" #include "smt/smt_engine.h" #include "theory/quantifiers/quantifiers_attributes.h" diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp index 2f9b89d06..e66717f5b 100644 --- a/src/smt/quant_elim_solver.cpp +++ b/src/smt/quant_elim_solver.cpp @@ -15,6 +15,7 @@ #include "smt/quant_elim_solver.h" +#include "base/modal_exception.h" #include "expr/skolem_manager.h" #include "expr/subs.h" #include "smt/smt_solver.h" diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 24a3e409e..46e11af20 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -26,6 +26,7 @@ #include "options/expr_options.h" #include "options/language.h" #include "options/main_options.h" +#include "options/option_exception.h" #include "options/printer_options.h" #include "options/proof_options.h" #include "options/smt_options.h" diff --git a/src/smt/smt_engine_state.cpp b/src/smt/smt_engine_state.cpp index cabaf8823..4afa15a3b 100644 --- a/src/smt/smt_engine_state.cpp +++ b/src/smt/smt_engine_state.cpp @@ -15,6 +15,8 @@ #include "smt/smt_engine_state.h" +#include "base/modal_exception.h" +#include "options/option_exception.h" #include "options/smt_options.h" #include "smt/smt_engine.h" diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp index 00598534f..0976442e1 100644 --- a/src/smt/sygus_solver.cpp +++ b/src/smt/sygus_solver.cpp @@ -17,8 +17,10 @@ #include +#include "base/modal_exception.h" #include "expr/dtype.h" #include "expr/skolem_manager.h" +#include "options/option_exception.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "printer/printer.h" diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp index 6f2ae9d22..3c8320d8c 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.cpp +++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp @@ -18,6 +18,7 @@ #include +#include "base/modal_exception.h" #include "expr/dtype.h" #include "expr/node_algorithm.h" #include "options/smt_options.h" diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp index f65f938b5..872b23ac4 100644 --- a/src/util/resource_manager.cpp +++ b/src/util/resource_manager.cpp @@ -22,6 +22,7 @@ #include "base/check.h" #include "base/listener.h" #include "base/output.h" +#include "options/option_exception.h" #include "options/options.h" #include "options/smt_options.h" #include "util/statistics_registry.h" -- 2.30.2