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 869699ac5657da4d46bc524ab7c1b958d47f4cfa..e56379f0c4e9dd188d62e208a2aa318c0993a7e6 100644 (file)
--- 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 18de83e90246b5380fd9e0bb56ce71784c7a6527..391db4bd46a67a213f55ceb9abdd2ab25f9e20df 100644 (file)
--- 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 (file)
index 620e61e..0000000
--- 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 35bed1dbf4deae1a63e4fbf45f7fea4ff32d7a33..d6a632ac504f49710d0c2f8a3df8d8b394a28bd8 100644 (file)
--- 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 0b923f0274e7d6653712a812ae4a071c9bca62e2..0c70b1667fcdae1acb59cb86146d2dfed667e2d7 100644 (file)
--- 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 264d065d6e46e6522acd1b2e98168661a92566e4..723f805b73069db1fa9c712df48f7806c88dd07a 100644 (file)
--- 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 e6361be9e75863232ae04b6c80b2aad7dd12ce9f..432910cd3c3082066f7658e1934b5f482ef43d29 100644 (file)
--- 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 0b86f35399a085dfcc87626b5947979937d8f5f7..b9c1b7d732a91095a0261017a908c2c52fb27c64 100644 (file)
--- 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 9d3031b4d992844a3270ec273d01487a6396c0e4..51fcf8b5b3693441ab368de5e10cd3b0fb238345 100644 (file)
--- 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 7d34f3373d52c9c64e44dcd6ba91ac2551c0ba12..356cfa8a6e47b8beb34213bce8878553a9c814d1 100644 (file)
--- 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 92d200d408fa180639a5c4d6cbdcaec26d71a972..5c45a6a564c3a76f2b39f2b88d7d3e5e34296157 100644 (file)
--- 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 7a28c47f202b5fdef64162380c6e637a342513f4..327933f1baa089550b602e0fcab5c7a02b6893a9 100644 (file)
--- 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 118b82bec1790a990301cd81dca0fc5ba0e48141..1916f0162c836df0da9690a3848dbce52bc8f9b0 100644 (file)
--- 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 78d7f8c385b22968b42d547b1a4f3384ff745931..d2fbeb413fc020b83a500f5ce2632b8a5de9e197 100644 (file)
--- 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 1e031c3224ed5b7e9c114d15ac5973c387aa1363..f4016d032248fe2d79fa231b5366353709599b97 100644 (file)
--- 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 a0def66c50daa73dd08f2eaee441022745aa9a0a..a090a58fe4b7832e6e602054c66d7c72fe3f0667 100644 (file)
--- 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 59e65c9e1f44b5a157be16126fde5acefeaae7f5..e48d651bd40525df3bdb505a99fd1065027c790b 100644 (file)
--- 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 aa0e6289101747b2a5eb4adf3887a456557e0331..a3938412df35516169ef8669c6090ca76f2a7a6e 100644 (file)
--- 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 9fc8e703c10808269f87f0747ad0e542e13c51ab..d39d2a37790c70ccd2a13ffeffa601268042cee0 100644 (file)
--- 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 acafeec3ca0ce4dc71a1445b4a5525ba0aa6e069..48a5dbe0608653dc6bd3179dce10ef00caa3dc79 100644 (file)
--- 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 916f2d9b596f5930f5fa82a592f66d59021d2c02..4db5f261af9e7eeca96f86b0ef843441863f4738 100644 (file)
--- 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 2214d4beb901379ad0b4a4219bb8197b98df567f..daee1762f8c535d090e724bd7593e938779593eb 100644 (file)
--- 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 f68900ccc0dc6562b569886a054e0cb14691ca03..e2742c8128d34fe8637711042ca014ab08d44c74 100644 (file)
--- 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"