From 9f372f084f5c558e3ff618d02abfdb384a82e066 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 30 Nov 2020 10:56:28 -0600 Subject: [PATCH] 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. --- src/CMakeLists.txt | 1 - src/expr/CMakeLists.txt | 1 - src/expr/array.h | 26 ------------------- src/expr/symbol_table.h | 1 - src/expr/type.h | 3 --- src/expr/type_properties_template.h | 2 +- src/smt/command.cpp | 2 +- src/smt/command.h | 2 -- src/smt/dump_manager.cpp | 1 - src/smt/listeners.cpp | 1 - src/smt/model_blocker.h | 2 +- src/smt/model_core_builder.h | 2 +- src/smt/proof_manager.h | 1 - src/smt_util/boolean_simplification.h | 1 - src/theory/arith/arith_static_learner.cpp | 1 - src/theory/datatypes/type_enumerator.h | 1 - src/theory/fp/fp_converter.h | 2 +- src/theory/quantifiers/expr_miner.h | 3 +-- src/theory/quantifiers/sygus/sygus_abduct.h | 2 +- .../quantifiers/sygus/sygus_grammar_norm.h | 1 - src/theory/quantifiers/sygus/sygus_interpol.h | 2 +- .../quantifiers/sygus/sygus_qe_preproc.h | 2 +- src/theory/smt_engine_subsolver.h | 1 - 23 files changed, 9 insertions(+), 52 deletions(-) delete mode 100644 src/expr/array.h 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 #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 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 #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 #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 -#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 -#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 #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 #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 #include -#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 #include #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 #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 #include #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 #include -#include "expr/expr_manager.h" #include "expr/node.h" #include "smt/smt_engine.h" -- 2.30.2