From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Wed, 28 Apr 2021 18:32:42 +0000 (+0200)
Subject: Remove exception headers from options.h (#6456)
X-Git-Tag: cvc5-1.0.0~1816
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fc0512b6d13349a91da5ac6617acebc41cbd238c;p=cvc5.git

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.
---

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 <cerrno>
 #include <cstring>
 
+#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 <module>_options.cpp file.
  */
 
-#include "options/options_holder.h"
-#include "base/check.h"
-
 #include <iostream>
 
+#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 <cerrno>
 #include <fstream>
 #include <iostream>
@@ -28,6 +27,7 @@
 #include <utility>
 
 #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 <vector>
 
 #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 <sstream>
 
+#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 <sstream>
 
+#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 <sstream>
 
+#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 <sstream>
 
+#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 <sstream>
 
+#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"