From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 30 Nov 2020 16:56:28 +0000 (-0600)
Subject: Remove includes for old API from internal code (#5536)
X-Git-Tag: cvc5-1.0.0~2543
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9f372f084f5c558e3ff618d02abfdb384a82e066;p=cvc5.git

Remove includes for old API from internal code (#5536)

The only code including the old API now are in parser/ and main/ which will require further untangling.
---

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 869699ac5..e56379f0c 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -1137,7 +1137,6 @@ install(FILES
         DESTINATION
           ${CMAKE_INSTALL_INCLUDEDIR}/cvc4)
 install(FILES
-          expr/array.h
           expr/array_store_all.h
           expr/ascription_type.h
           expr/emptyset.h
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 18de83e90..391db4bd4 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -9,7 +9,6 @@
 ## directory for licensing information.
 ##
 libcvc4_add_sources(
-  array.h
   array_store_all.cpp
   array_store_all.h
   ascription_type.cpp
diff --git a/src/expr/array.h b/src/expr/array.h
deleted file mode 100644
index 620e61ea0..000000000
--- a/src/expr/array.h
+++ /dev/null
@@ -1,26 +0,0 @@
-/*********************                                                        */
-/*! \file array.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Mathias Preiner, Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Array types.
- **
- ** Array types.
- **/
-
-#include "cvc4_public.h"
-
-#ifndef CVC4__ARRAY_H
-#define CVC4__ARRAY_H
-
-// we get ArrayType right now by #including type.h.
-// array.h is still useful for the auto-generated kinds #includes.
-#include "expr/type.h"
-
-#endif /* CVC4__ARRAY_H */
diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h
index 35bed1dbf..d6a632ac5 100644
--- a/src/expr/symbol_table.h
+++ b/src/expr/symbol_table.h
@@ -24,7 +24,6 @@
 #include <vector>
 
 #include "base/exception.h"
-#include "expr/expr.h"
 #include "expr/type.h"
 
 namespace CVC4 {
diff --git a/src/expr/type.h b/src/expr/type.h
index 0b923f027..0c70b1667 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -35,9 +35,6 @@ struct CVC4_PUBLIC ExprManagerMapCollection;
 
 class SmtEngine;
 
-class CVC4_PUBLIC Datatype;
-class Record;
-
 template <bool ref_count>
 class NodeTemplate;
 
diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h
index 264d065d6..723f805b7 100644
--- a/src/expr/type_properties_template.h
+++ b/src/expr/type_properties_template.h
@@ -22,8 +22,8 @@
 #include <sstream>
 
 #include "base/check.h"
-#include "expr/expr.h"
 #include "expr/kind.h"
+#include "expr/node.h"
 #include "expr/type_node.h"
 #include "options/language.h"
 
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index e6361be9e..432910cd3 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -29,7 +29,7 @@
 #include "expr/expr_iomanip.h"
 #include "expr/node.h"
 #include "expr/symbol_manager.h"
-#include "expr/type.h"
+#include "expr/type_node.h"
 #include "options/options.h"
 #include "options/smt_options.h"
 #include "printer/printer.h"
diff --git a/src/smt/command.h b/src/smt/command.h
index 0b86f3539..b9c1b7d73 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -29,8 +29,6 @@
 #include <vector>
 
 #include "api/cvc4cpp.h"
-#include "expr/expr.h"
-#include "expr/type.h"
 #include "util/result.h"
 #include "util/sexpr.h"
 
diff --git a/src/smt/dump_manager.cpp b/src/smt/dump_manager.cpp
index 9d3031b4d..51fcf8b5b 100644
--- a/src/smt/dump_manager.cpp
+++ b/src/smt/dump_manager.cpp
@@ -14,7 +14,6 @@
 
 #include "smt/dump_manager.h"
 
-#include "expr/expr_manager.h"
 #include "options/smt_options.h"
 #include "smt/dump.h"
 #include "smt/node_command.h"
diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp
index 7d34f3373..356cfa8a6 100644
--- a/src/smt/listeners.cpp
+++ b/src/smt/listeners.cpp
@@ -15,7 +15,6 @@
 #include "smt/listeners.h"
 
 #include "expr/attribute.h"
-#include "expr/expr.h"
 #include "expr/node_manager_attributes.h"
 #include "options/smt_options.h"
 #include "printer/printer.h"
diff --git a/src/smt/model_blocker.h b/src/smt/model_blocker.h
index 92d200d40..5c45a6a56 100644
--- a/src/smt/model_blocker.h
+++ b/src/smt/model_blocker.h
@@ -19,7 +19,7 @@
 
 #include <vector>
 
-#include "expr/expr.h"
+#include "expr/node.h"
 #include "options/smt_options.h"
 #include "theory/theory_model.h"
 
diff --git a/src/smt/model_core_builder.h b/src/smt/model_core_builder.h
index 7a28c47f2..327933f1b 100644
--- a/src/smt/model_core_builder.h
+++ b/src/smt/model_core_builder.h
@@ -19,7 +19,7 @@
 
 #include <vector>
 
-#include "expr/expr.h"
+#include "expr/node.h"
 #include "options/smt_options.h"
 #include "theory/theory_model.h"
 
diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h
index 118b82bec..1916f0162 100644
--- a/src/smt/proof_manager.h
+++ b/src/smt/proof_manager.h
@@ -18,7 +18,6 @@
 #define CVC4__SMT__PROOF_MANAGER_H
 
 #include "context/cdlist.h"
-#include "expr/expr.h"
 #include "expr/node.h"
 #include "expr/proof_checker.h"
 #include "expr/proof_node.h"
diff --git a/src/smt_util/boolean_simplification.h b/src/smt_util/boolean_simplification.h
index 78d7f8c38..d2fbeb413 100644
--- a/src/smt_util/boolean_simplification.h
+++ b/src/smt_util/boolean_simplification.h
@@ -23,7 +23,6 @@
 #include <algorithm>
 
 #include "base/check.h"
-#include "expr/expr_manager_scope.h"
 #include "expr/node.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index 1e031c322..f4016d032 100644
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -18,7 +18,6 @@
 #include <vector>
 
 #include "base/output.h"
-#include "expr/expr.h"
 #include "expr/node_algorithm.h"
 #include "options/arith_options.h"
 #include "smt/smt_statistics_registry.h"
diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index a0def66c5..a090a58fe 100644
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -21,7 +21,6 @@
 
 #include "expr/dtype.h"
 #include "expr/kind.h"
-#include "expr/type.h"
 #include "expr/type_node.h"
 #include "options/quantifiers_options.h"
 #include "theory/type_enumerator.h"
diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h
index 59e65c9e1..e48d651bd 100644
--- a/src/theory/fp/fp_converter.h
+++ b/src/theory/fp/fp_converter.h
@@ -26,7 +26,7 @@
 #include "context/cdlist.h"
 #include "expr/node.h"
 #include "expr/node_builder.h"
-#include "expr/type.h"
+#include "expr/type_node.h"
 #include "theory/valuation.h"
 #include "util/bitvector.h"
 #include "util/floatingpoint_size.h"
diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h
index aa0e62891..a3938412d 100644
--- a/src/theory/quantifiers/expr_miner.h
+++ b/src/theory/quantifiers/expr_miner.h
@@ -21,8 +21,7 @@
 #include <memory>
 #include <vector>
 
-#include "expr/expr.h"
-#include "expr/expr_manager.h"
+#include "expr/node.h"
 #include "smt/smt_engine.h"
 #include "theory/quantifiers/sygus_sampler.h"
 
diff --git a/src/theory/quantifiers/sygus/sygus_abduct.h b/src/theory/quantifiers/sygus/sygus_abduct.h
index 9fc8e703c..d39d2a377 100644
--- a/src/theory/quantifiers/sygus/sygus_abduct.h
+++ b/src/theory/quantifiers/sygus/sygus_abduct.h
@@ -19,7 +19,7 @@
 #include <string>
 #include <vector>
 #include "expr/node.h"
-#include "expr/type.h"
+#include "expr/type_node.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
index acafeec3c..48a5dbe06 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
@@ -24,7 +24,6 @@
 
 #include "expr/node.h"
 #include "expr/sygus_datatype.h"
-#include "expr/type.h"
 #include "expr/type_node.h"
 #include "theory/quantifiers/term_util.h"
 
diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h
index 916f2d9b5..4db5f261a 100644
--- a/src/theory/quantifiers/sygus/sygus_interpol.h
+++ b/src/theory/quantifiers/sygus/sygus_interpol.h
@@ -20,7 +20,7 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "expr/type.h"
+#include "expr/type_node.h"
 #include "smt/smt_engine.h"
 
 namespace CVC4 {
diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.h b/src/theory/quantifiers/sygus/sygus_qe_preproc.h
index 2214d4beb..daee1762f 100644
--- a/src/theory/quantifiers/sygus/sygus_qe_preproc.h
+++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.h
@@ -18,7 +18,7 @@
 #include <string>
 #include <vector>
 #include "expr/node.h"
-#include "expr/type.h"
+#include "expr/type_node.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/smt_engine_subsolver.h b/src/theory/smt_engine_subsolver.h
index f68900ccc..e2742c812 100644
--- a/src/theory/smt_engine_subsolver.h
+++ b/src/theory/smt_engine_subsolver.h
@@ -22,7 +22,6 @@
 #include <memory>
 #include <vector>
 
-#include "expr/expr_manager.h"
 #include "expr/node.h"
 #include "smt/smt_engine.h"