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 ce065a75f0408542039dde7204ee9b1d222e295d..6ee1409d6fa7f393a1fc966a8384bb9ebee2089e 100644 (file)
--- 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 6a7baebb36bd78418bba10ed24fb34db35421cf6..b96598b0bbb6088c8d9acb9aca464fab14c19d19 100644 (file)
--- 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 82cfda017187b818fe8aabb2d22129d0e829c0cd..0f0a824f681c9d394075b73d1e8c9a758aabbd39 100644 (file)
--- 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 0de77e8a6251db447df97f734eec2c72802b0c3e..e0b3f79d18b7eebae5b3f4259929d49b060badcd 100644 (file)
--- 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 9ebea6da04b968fed1ecd68ada49e8469bba3b2c..bb6efb5bcfcac54245d3b0bb0e2c2699383512a8 100644 (file)
--- 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 a8fc50b68970e08cb3bee10f8951aeec9a321279..4d8a979c653769890604f94e041aec0e9406cd77 100644 (file)
--- 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 7e29e484905a26e92e5b2e0692b67a65feb71a2e..23f46cc58c43ea3995095198d8c9c69cbc17c955 100644 (file)
--- 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 2fb83f8986f70e6e05b293e54bf8353206c08374..779a63c29ece4e5db376e6cb1b7aa5164138888e 100644 (file)
--- 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 ebc8f46a18edaa132a688e4760b8927d3cd57792..f6d1da3457e3867a2a73225e62d9517cdd0cfe78 100644 (file)
--- 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 b2a1590b01db499c86df38609f8751ca1cb30dde..e49658c9d88bbb44f67e77d39cbf96084ea18e59 100644 (file)
--- 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 48d81a91f59e7a835283b997937575cd71c9bcbb..813fc45cfb23cfaf0feec27cf594bce7f50c409e 100644 (file)
--- 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 2f9b89d0645d0e6c01c716fac91094bde4ac52f2..e66717f5b77858e2678d41388467e7bc55647711 100644 (file)
--- 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 24a3e409e6293be438a9401b18ead279336e74e2..46e11af205fa26987dabb15800be1057b1cb43e6 100644 (file)
--- 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 cabaf882373748fc060b747937c4f88b9d291cde..4afa15a3bc6b36a15a82351fc87ef91e3b732f79 100644 (file)
--- 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 00598534ff945a0ed22cba0e34b96fe58daab76e..0976442e104473edab226467110fe419e6e893b5 100644 (file)
--- 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 6f2ae9d22c28bd16f9ee472f8ecd05f6c17de019..3c8320d8c98002bcfa24126554cb8c29e6f4d4fe 100644 (file)
--- 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 f65f938b5622cd50c5b0cf49fcaaf8d1bc991f3e..872b23ac4140c945c8bf3720f943403e368e735b 100644 (file)
--- 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"