summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/CMakeLists.txt1
-rw-r--r--src/expr/CMakeLists.txt1
-rw-r--r--src/expr/array.h26
-rw-r--r--src/expr/symbol_table.h1
-rw-r--r--src/expr/type.h3
-rw-r--r--src/expr/type_properties_template.h2
-rw-r--r--src/smt/command.cpp2
-rw-r--r--src/smt/command.h2
-rw-r--r--src/smt/dump_manager.cpp1
-rw-r--r--src/smt/listeners.cpp1
-rw-r--r--src/smt/model_blocker.h2
-rw-r--r--src/smt/model_core_builder.h2
-rw-r--r--src/smt/proof_manager.h1
-rw-r--r--src/smt_util/boolean_simplification.h1
-rw-r--r--src/theory/arith/arith_static_learner.cpp1
-rw-r--r--src/theory/datatypes/type_enumerator.h1
-rw-r--r--src/theory/fp/fp_converter.h2
-rw-r--r--src/theory/quantifiers/expr_miner.h3
-rw-r--r--src/theory/quantifiers/sygus/sygus_abduct.h2
-rw-r--r--src/theory/quantifiers/sygus/sygus_grammar_norm.h1
-rw-r--r--src/theory/quantifiers/sygus/sygus_interpol.h2
-rw-r--r--src/theory/quantifiers/sygus/sygus_qe_preproc.h2
-rw-r--r--src/theory/smt_engine_subsolver.h1
23 files changed, 9 insertions, 52 deletions
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"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback