diff options
210 files changed, 381 insertions, 180 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 0c94320c3..7a191cd8a 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -39,6 +39,8 @@ #include "base/check.h" #include "base/configuration.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" +#include "expr/dtype_selector.h" #include "expr/expr.h" #include "expr/expr_manager.h" #include "expr/expr_manager_scope.h" diff --git a/src/base/exception.cpp b/src/base/exception.cpp index 2a8dc8d10..cddef79fd 100644 --- a/src/base/exception.cpp +++ b/src/base/exception.cpp @@ -28,24 +28,24 @@ using namespace std; namespace CVC4 { -thread_local LastExceptionBuffer* LastExceptionBuffer::s_currentBuffer = NULL; +thread_local LastExceptionBuffer* LastExceptionBuffer::s_currentBuffer = nullptr; -LastExceptionBuffer::LastExceptionBuffer() : d_contents(NULL) {} +LastExceptionBuffer::LastExceptionBuffer() : d_contents(nullptr) {} LastExceptionBuffer::~LastExceptionBuffer() { - if(d_contents != NULL){ + if(d_contents != nullptr){ free(d_contents); - d_contents = NULL; + d_contents = nullptr; } } void LastExceptionBuffer::setContents(const char* string) { - if(d_contents != NULL){ + if(d_contents != nullptr){ free(d_contents); - d_contents = NULL; + d_contents = nullptr; } - if(string != NULL){ + if(string != nullptr){ d_contents = strdup(string); } } @@ -61,7 +61,7 @@ std::string IllegalArgumentException::formatVariadic(const char* format, ...) { va_start(args, format); int n = 512; - char* buf = NULL; + char* buf = nullptr; for (int i = 0; i < 2; ++i){ Assert(n > 0); @@ -80,9 +80,9 @@ std::string IllegalArgumentException::formatVariadic(const char* format, ...) { break; } } - // buf is not NULL is an invariant. + // buf is not nullptr is an invariant. // buf is also 0 terminated. - Assert(buf != NULL); + Assert(buf != nullptr); std::string result(buf); delete [] buf; va_end(args); @@ -107,7 +107,7 @@ void IllegalArgumentException::construct(const char* header, const char* extra, buf = new char[n]; int size; - if(extra == NULL) { + if(extra == nullptr) { size = snprintf(buf, n, "%s\n%s\n%s", header, function, tail); } else { @@ -129,8 +129,8 @@ void IllegalArgumentException::construct(const char* header, const char* extra, #ifdef CVC4_DEBUG LastExceptionBuffer* buffer = LastExceptionBuffer::getCurrent(); - if(buffer != NULL){ - if(buffer->getContents() == NULL) { + if(buffer != nullptr){ + if(buffer->getContents() == nullptr) { buffer->setContents(buf); } } @@ -149,7 +149,7 @@ void IllegalArgumentException::construct(const char* header, const char* extra, buf = new char[n]; int size; - if(extra == NULL) { + if(extra == nullptr) { size = snprintf(buf, n, "%s.\n%s\n", header, function); } else { @@ -170,8 +170,8 @@ void IllegalArgumentException::construct(const char* header, const char* extra, #ifdef CVC4_DEBUG LastExceptionBuffer* buffer = LastExceptionBuffer::getCurrent(); - if(buffer != NULL){ - if(buffer->getContents() == NULL) { + if(buffer != nullptr){ + if(buffer->getContents() == nullptr) { buffer->setContents(buf); } } diff --git a/src/base/exception.h b/src/base/exception.h index 1d49d94cc..8a89c99fc 100644 --- a/src/base/exception.h +++ b/src/base/exception.h @@ -151,7 +151,7 @@ public: static void setCurrent(LastExceptionBuffer* buffer) { s_currentBuffer = buffer; } static const char* currentContents() { - return (getCurrent() == NULL) ? NULL : getCurrent()->getContents(); + return (getCurrent() == nullptr) ? nullptr : getCurrent()->getContents(); } private: diff --git a/src/base/listener.h b/src/base/listener.h index 15256ab01..5c5a58128 100644 --- a/src/base/listener.h +++ b/src/base/listener.h @@ -20,8 +20,6 @@ #ifndef CVC4__LISTENER_H #define CVC4__LISTENER_H -#include <list> - namespace CVC4 { /** diff --git a/src/base/output.h b/src/base/output.h index 96cb9f8ac..9de1d9b09 100644 --- a/src/base/output.h +++ b/src/base/output.h @@ -21,10 +21,8 @@ #include <ios> #include <iostream> -#include <streambuf> #include <string> #include <cstdio> -#include <cstdarg> #include <set> #include <utility> diff --git a/src/context/cdlist.h b/src/context/cdlist.h index cb5e552ac..0515d7126 100644 --- a/src/context/cdlist.h +++ b/src/context/cdlist.h @@ -20,6 +20,7 @@ #ifndef CVC4__CONTEXT__CDLIST_H #define CVC4__CONTEXT__CDLIST_H +#include <cstring> #include <iterator> #include <memory> #include <string> diff --git a/src/context/context.cpp b/src/context/context.cpp index 19be126f8..1313daa9a 100644 --- a/src/context/context.cpp +++ b/src/context/context.cpp @@ -16,6 +16,7 @@ #include <iostream> +#include <string> #include <vector> #include "base/check.h" diff --git a/src/context/context.h b/src/context/context.h index 15b4307b9..afec59747 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -20,10 +20,8 @@ #define CVC4__CONTEXT__CONTEXT_H #include <cstdlib> -#include <cstring> #include <iostream> #include <memory> -#include <new> #include <typeinfo> #include <vector> diff --git a/src/expr/buffered_proof_generator.cpp b/src/expr/buffered_proof_generator.cpp index f6753a601..266cfb18a 100644 --- a/src/expr/buffered_proof_generator.cpp +++ b/src/expr/buffered_proof_generator.cpp @@ -15,6 +15,7 @@ #include "expr/buffered_proof_generator.h" #include "expr/proof.h" +#include "expr/proof_node_manager.h" namespace CVC4 { diff --git a/src/expr/buffered_proof_generator.h b/src/expr/buffered_proof_generator.h index f774e383d..da80891a2 100644 --- a/src/expr/buffered_proof_generator.h +++ b/src/expr/buffered_proof_generator.h @@ -17,17 +17,14 @@ #ifndef CVC4__EXPR__BUFFERED_PROOF_GENERATOR_H #define CVC4__EXPR__BUFFERED_PROOF_GENERATOR_H -#include <map> -#include <vector> - #include "context/cdhashmap.h" -#include "context/cdhashset.h" #include "expr/proof_generator.h" -#include "expr/proof_node_manager.h" #include "expr/proof_step_buffer.h" namespace CVC4 { +class ProofNodeManager; + /** * The proof generator for buffered steps. This class is a context-dependent * mapping from formulas to proof steps. It does not generate ProofNodes until it diff --git a/src/expr/datatype_index.cpp b/src/expr/datatype_index.cpp index 694d75db6..23d6b3ca1 100644 --- a/src/expr/datatype_index.cpp +++ b/src/expr/datatype_index.cpp @@ -15,6 +15,7 @@ #include <sstream> #include <string> +#include "util/hash.h" #include "util/integer.h" using namespace std; diff --git a/src/expr/datatype_index.h b/src/expr/datatype_index.h index c7f170ff6..08640e1d5 100644 --- a/src/expr/datatype_index.h +++ b/src/expr/datatype_index.h @@ -18,7 +18,6 @@ #define CVC4__DATATYPE_INDEX_H #include <iosfwd> -#include "util/hash.h" namespace CVC4 { diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp index 5cb76858a..f94f0063a 100644 --- a/src/expr/dtype.cpp +++ b/src/expr/dtype.cpp @@ -13,6 +13,7 @@ **/ #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "expr/node_algorithm.h" #include "expr/type_matcher.h" diff --git a/src/expr/dtype.h b/src/expr/dtype.h index e4bae29b8..c68a7d44a 100644 --- a/src/expr/dtype.h +++ b/src/expr/dtype.h @@ -20,10 +20,8 @@ #include <map> #include <string> #include <vector> -#include "expr/dtype_cons.h" -#include "expr/dtype_selector.h" +#include "expr/attribute.h" #include "expr/node.h" -#include "expr/node_manager_attributes.h" #include "expr/type_node.h" namespace CVC4 { @@ -76,7 +74,7 @@ struct DTypeUFiniteComputedTag typedef expr::Attribute<DTypeUFiniteComputedTag, bool> DTypeUFiniteComputedAttr; // ----------------------- end datatype attributes -class NodeManager; +class DTypeConstructor; /** * The Node-level representation of an inductive datatype, which currently diff --git a/src/expr/lazy_proof.cpp b/src/expr/lazy_proof.cpp index 0c209f393..8d8d2741f 100644 --- a/src/expr/lazy_proof.cpp +++ b/src/expr/lazy_proof.cpp @@ -15,6 +15,7 @@ #include "expr/lazy_proof.h" #include "expr/proof_ensure_closed.h" +#include "expr/proof_node_manager.h" using namespace CVC4::kind; diff --git a/src/expr/lazy_proof.h b/src/expr/lazy_proof.h index e2bba3015..83dc90e4d 100644 --- a/src/expr/lazy_proof.h +++ b/src/expr/lazy_proof.h @@ -22,10 +22,11 @@ #include "expr/proof.h" #include "expr/proof_generator.h" -#include "expr/proof_node_manager.h" namespace CVC4 { +class ProofNodeManager; + /** * A (context-dependent) lazy proof. This class is an extension of CDProof * that additionally maps facts to proof generators in a context-dependent diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp index 2edad1647..f80ab099c 100644 --- a/src/expr/lazy_proof_chain.cpp +++ b/src/expr/lazy_proof_chain.cpp @@ -17,6 +17,7 @@ #include "expr/proof.h" #include "expr/proof_ensure_closed.h" #include "expr/proof_node_algorithm.h" +#include "expr/proof_node_manager.h" #include "options/proof_options.h" namespace CVC4 { diff --git a/src/expr/lazy_proof_chain.h b/src/expr/lazy_proof_chain.h index 59cab72c9..1604bf182 100644 --- a/src/expr/lazy_proof_chain.h +++ b/src/expr/lazy_proof_chain.h @@ -22,10 +22,11 @@ #include "context/cdhashmap.h" #include "expr/proof_generator.h" -#include "expr/proof_node_manager.h" namespace CVC4 { +class ProofNodeManager; + /** * A (context-dependent) lazy generator for proof chains. This class is an * extension of ProofGenerator that additionally that maps facts to proof diff --git a/src/expr/node.cpp b/src/expr/node.cpp index c45295622..1aca73d2e 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -21,6 +21,7 @@ #include "base/exception.h" #include "base/output.h" #include "expr/attribute.h" +#include "expr/type_checker.h" using namespace std; diff --git a/src/expr/node.h b/src/expr/node.h index 559ce5ddb..06c327018 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -22,8 +22,6 @@ #ifndef CVC4__NODE_H #define CVC4__NODE_H -#include <algorithm> -#include <functional> #include <iostream> #include <string> #include <unordered_map> @@ -32,14 +30,12 @@ #include <vector> #include "base/check.h" -#include "base/configuration.h" #include "base/exception.h" #include "base/output.h" #include "expr/expr.h" #include "expr/expr_iomanip.h" #include "expr/kind.h" #include "expr/metakind.h" -#include "expr/type.h" #include "options/language.h" #include "options/set_language.h" #include "util/hash.h" @@ -980,7 +976,6 @@ std::ostream& operator<<( //#include "expr/attribute.h" #include "expr/node_manager.h" -#include "expr/type_checker.h" namespace CVC4 { diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 883febd6f..4404e3445 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -26,6 +26,7 @@ #include "expr/attribute.h" #include "expr/bound_var_manager.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "expr/node_manager_attributes.h" #include "expr/skolem_manager.h" #include "expr/type_checker.h" diff --git a/src/expr/node_traversal.cpp b/src/expr/node_traversal.cpp index 75a11eac7..0b778ebef 100644 --- a/src/expr/node_traversal.cpp +++ b/src/expr/node_traversal.cpp @@ -14,6 +14,8 @@ #include "node_traversal.h" +#include <functional> + namespace CVC4 { NodeDfsIterator::NodeDfsIterator(TNode n, diff --git a/src/expr/node_traversal.h b/src/expr/node_traversal.h index e7e49db45..124372f79 100644 --- a/src/expr/node_traversal.h +++ b/src/expr/node_traversal.h @@ -17,7 +17,6 @@ #ifndef CVC4__EXPR__NODE_TRAVERSAL_H #define CVC4__EXPR__NODE_TRAVERSAL_H -#include <functional> #include <iterator> #include <unordered_map> #include <vector> diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 0635e983b..1ad498ecd 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -399,7 +399,6 @@ inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv); }/* CVC4 namespace */ #include "expr/node_manager.h" -#include "expr/type_node.h" namespace CVC4 { namespace expr { @@ -501,7 +500,6 @@ inline NodeValue* NodeValue::getChild(int i) const { }/* CVC4 namespace */ #include "expr/node.h" -#include "expr/type_node.h" namespace CVC4 { namespace expr { diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp index 1c21a59e7..b512b5869 100644 --- a/src/expr/proof.cpp +++ b/src/expr/proof.cpp @@ -14,6 +14,8 @@ #include "expr/proof.h" +#include "expr/proof_node_manager.h" + using namespace CVC4::kind; namespace CVC4 { diff --git a/src/expr/proof.h b/src/expr/proof.h index 8350b4954..3a26f0975 100644 --- a/src/expr/proof.h +++ b/src/expr/proof.h @@ -24,11 +24,12 @@ #include "expr/node.h" #include "expr/proof_generator.h" #include "expr/proof_node.h" -#include "expr/proof_node_manager.h" #include "expr/proof_step_buffer.h" namespace CVC4 { +class ProofNodeManager; + /** * A (context-dependent) proof. * diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp index 840cb4c66..ea73b7958 100644 --- a/src/preprocessing/passes/quantifier_macros.cpp +++ b/src/preprocessing/passes/quantifier_macros.cpp @@ -26,6 +26,7 @@ #include "theory/quantifiers/ematching/pattern_term_selector.h" #include "theory/quantifiers/quantifiers_registry.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" #include "theory/rewriter.h" diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp index 707d1314c..7e6371aa9 100644 --- a/src/preprocessing/preprocessing_pass_context.cpp +++ b/src/preprocessing/preprocessing_pass_context.cpp @@ -17,6 +17,7 @@ #include "preprocessing/preprocessing_pass_context.h" #include "expr/node_algorithm.h" +#include "smt/logic_request.h" namespace CVC4 { namespace preprocessing { diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 173e67fd9..82798d074 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -25,6 +25,8 @@ #include <vector> #include "expr/dtype.h" +#include "expr/dtype_cons.h" +#include "expr/dtype_selector.h" #include "expr/node_manager_attributes.h" // for VarNameAttr #include "expr/node_visitor.h" #include "expr/sequence.h" diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index c7962417a..fd9d20e4b 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -17,12 +17,14 @@ #include "printer/smt2/smt2_printer.h" #include <iostream> +#include <list> #include <string> #include <typeinfo> #include <vector> #include "api/cvc4cpp.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "expr/node_manager_attributes.h" #include "expr/node_visitor.h" #include "expr/sequence.h" diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index ac90d0c36..d0c75a924 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -33,6 +33,7 @@ #include "prop/prop_proof_manager.h" #include "prop/sat_solver_types.h" #include "theory/trust_node.h" +#include "theory/theory_inference_manager.h" #include "util/resource_manager.h" #include "util/result.h" #include "util/unsafe_interrupt_exception.h" diff --git a/src/smt/command.cpp b/src/smt/command.cpp index cdaaa0558..f10191c75 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -39,6 +39,7 @@ #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "util/sexpr.h" +#include "util/unsafe_interrupt_exception.h" #include "util/utility.h" using namespace std; diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp index b1fb0589c..aedd946c1 100644 --- a/src/smt/dump.cpp +++ b/src/smt/dump.cpp @@ -16,6 +16,7 @@ #include "smt/dump.h" +#include "base/configuration.h" #include "base/output.h" #include "lib/strtok_r.h" #include "preprocessing/preprocessing_pass_registry.h" diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp index 0347a24ef..f0fad93fe 100644 --- a/src/smt/listeners.cpp +++ b/src/smt/listeners.cpp @@ -14,6 +14,7 @@ #include "smt/listeners.h" +#include "base/configuration.h" #include "expr/attribute.h" #include "expr/node_manager_attributes.h" #include "options/smt_options.h" diff --git a/src/smt/logic_request.h b/src/smt/logic_request.h index 3210de7b1..4e8dcce6c 100644 --- a/src/smt/logic_request.h +++ b/src/smt/logic_request.h @@ -26,7 +26,7 @@ #ifndef CVC4__LOGIC_REQUEST_H #define CVC4__LOGIC_REQUEST_H -#include "expr/kind.h" +#include "theory/theory_id.h" namespace CVC4 { diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 98fbfe1b3..3d306a7a2 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -35,6 +35,7 @@ #include "options/strings_options.h" #include "options/theory_options.h" #include "options/uf_options.h" +#include "smt/logic_exception.h" #include "theory/theory.h" using namespace CVC4::theory; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 941fd111a..ed5e73d5d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -42,7 +42,6 @@ #include "smt/dump_manager.h" #include "smt/interpolation_solver.h" #include "smt/listeners.h" -#include "smt/logic_request.h" #include "smt/model_blocker.h" #include "smt/model_core_builder.h" #include "smt/node_command.h" diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index eb8eb6ca0..53a5b7f2f 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -23,20 +23,15 @@ #include <vector> #include <map> -#include "base/modal_exception.h" #include "context/cdhashmap_forward.h" -#include "context/cdhashset_forward.h" #include "context/cdlist_forward.h" #include "options/options.h" -#include "smt/logic_exception.h" #include "smt/output_manager.h" #include "smt/smt_mode.h" #include "theory/logic_info.h" -#include "util/hash.h" #include "util/result.h" #include "util/sexpr.h" #include "util/statistics.h" -#include "util/unsafe_interrupt_exception.h" // In terms of abstraction, this is below (and provides services to) // ValidityChecker and above (and requires the services of) @@ -51,7 +46,6 @@ class TypeNode; struct NodeHashFunction; class NodeManager; -class DecisionEngine; class TheoryEngine; class ProofManager; class UnsatCore; diff --git a/src/theory/arith/arith_preprocess.cpp b/src/theory/arith/arith_preprocess.cpp index 31eb8bb8f..26f51c8b8 100644 --- a/src/theory/arith/arith_preprocess.cpp +++ b/src/theory/arith/arith_preprocess.cpp @@ -14,6 +14,8 @@ #include "theory/arith/arith_preprocess.h" +#include "theory/arith/inference_manager.h" + namespace CVC4 { namespace theory { namespace arith { diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index 6c858d1eb..396395e1f 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -21,7 +21,6 @@ #define CVC4__THEORY__ARITH__ARITH_REWRITER_H #include "theory/arith/rewrites.h" -#include "theory/theory.h" #include "theory/theory_rewriter.h" namespace CVC4 { diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp index 72f8e49ff..61715df9b 100644 --- a/src/theory/arith/attempt_solution_simplex.cpp +++ b/src/theory/arith/attempt_solution_simplex.cpp @@ -20,6 +20,7 @@ #include "options/arith_options.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" +#include "theory/arith/error_set.h" using namespace std; diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp index 374b17d88..5d4bc9b1e 100644 --- a/src/theory/arith/dual_simplex.cpp +++ b/src/theory/arith/dual_simplex.cpp @@ -20,6 +20,7 @@ #include "options/arith_options.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" +#include "theory/arith/error_set.h" using namespace std; diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp index 85af862fa..8cb249c46 100644 --- a/src/theory/arith/fc_simplex.cpp +++ b/src/theory/arith/fc_simplex.cpp @@ -20,6 +20,7 @@ #include "options/arith_options.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" +#include "theory/arith/error_set.h" #include "util/statistics_registry.h" using namespace std; diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h index 1bd4416e0..e001d98d4 100644 --- a/src/theory/arith/fc_simplex.h +++ b/src/theory/arith/fc_simplex.h @@ -52,6 +52,7 @@ #pragma once +#include "theory/arith/error_set.h" #include "theory/arith/simplex.h" #include "util/dense_map.h" #include "util/statistics_registry.h" diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp index df3ba37f3..04165c289 100644 --- a/src/theory/arith/nl/cad/cdcac.cpp +++ b/src/theory/arith/nl/cad/cdcac.cpp @@ -22,6 +22,7 @@ #include "options/arith_options.h" #include "theory/arith/nl/cad/projections.h" #include "theory/arith/nl/cad/variable_ordering.h" +#include "theory/arith/nl/nl_model.h" namespace std { /** Generic streaming operator for std::vector. */ diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h index 4511d0c55..8736b7a08 100644 --- a/src/theory/arith/nl/cad/cdcac.h +++ b/src/theory/arith/nl/cad/cdcac.h @@ -32,12 +32,14 @@ #include "theory/arith/nl/cad/constraints.h" #include "theory/arith/nl/cad/proof_generator.h" #include "theory/arith/nl/cad/variable_ordering.h" -#include "theory/arith/nl/nl_model.h" namespace CVC4 { namespace theory { namespace arith { namespace nl { + +class NlModel; + namespace cad { /** diff --git a/src/theory/arith/nl/cad_solver.cpp b/src/theory/arith/nl/cad_solver.cpp index 74c0457a8..efc5c465a 100644 --- a/src/theory/arith/nl/cad_solver.cpp +++ b/src/theory/arith/nl/cad_solver.cpp @@ -14,15 +14,11 @@ #include "theory/arith/nl/cad_solver.h" -#ifdef CVC4_POLY_IMP -#include <poly/polyxx.h> -#endif - -#include "options/arith_options.h" #include "theory/inference_id.h" +#include "theory/arith/inference_manager.h" #include "theory/arith/nl/cad/cdcac.h" +#include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/poly_conversion.h" -#include "util/poly_util.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/nl/cad_solver.h b/src/theory/arith/nl/cad_solver.h index 21fbbab2e..b67d78f0d 100644 --- a/src/theory/arith/nl/cad_solver.h +++ b/src/theory/arith/nl/cad_solver.h @@ -17,17 +17,22 @@ #include <vector> +#include "context/context.h" #include "expr/node.h" -#include "theory/arith/inference_manager.h" #include "theory/arith/nl/cad/cdcac.h" #include "theory/arith/nl/cad/proof_checker.h" -#include "theory/arith/nl/nl_model.h" +#include "util/real_algebraic_number.h" namespace CVC4 { namespace theory { namespace arith { + +class InferenceManager; + namespace nl { +class NlModel; + /** * A solver for nonlinear arithmetic that implements the CAD-based method * described in https://arxiv.org/pdf/2003.05633.pdf. diff --git a/src/theory/arith/nl/ext/ext_state.cpp b/src/theory/arith/nl/ext/ext_state.cpp index 5da5319a1..7e77efb16 100644 --- a/src/theory/arith/nl/ext/ext_state.cpp +++ b/src/theory/arith/nl/ext/ext_state.cpp @@ -17,6 +17,7 @@ #include <vector> #include "expr/node.h" +#include "expr/proof.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/ext/monomial.h" #include "theory/arith/nl/nl_model.h" diff --git a/src/theory/arith/nl/ext/ext_state.h b/src/theory/arith/nl/ext/ext_state.h index 863b3f879..285189ccc 100644 --- a/src/theory/arith/nl/ext/ext_state.h +++ b/src/theory/arith/nl/ext/ext_state.h @@ -19,15 +19,21 @@ #include "expr/node.h" #include "expr/proof_set.h" -#include "theory/arith/inference_manager.h" #include "theory/arith/nl/ext/monomial.h" -#include "theory/arith/nl/nl_model.h" namespace CVC4 { + +class CDProof; + namespace theory { namespace arith { + +class InferenceManager; + namespace nl { +class NlModel; + struct ExtState { ExtState(InferenceManager& im, diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp index 7b4d98037..09cfd7410 100644 --- a/src/theory/arith/nl/ext/factoring_check.cpp +++ b/src/theory/arith/nl/ext/factoring_check.cpp @@ -15,10 +15,12 @@ #include "theory/arith/nl/ext/factoring_check.h" #include "expr/node.h" +#include "expr/proof.h" #include "expr/skolem_manager.h" #include "theory/arith/arith_msum.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/nl_model.h" +#include "theory/rewriter.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp index 5ae898bd2..ad6fd36b8 100644 --- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp +++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp @@ -15,11 +15,13 @@ #include "theory/arith/nl/ext/monomial_bounds_check.h" #include "expr/node.h" +#include "expr/proof.h" #include "options/arith_options.h" #include "theory/arith/arith_msum.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/nl_model.h" +#include "theory/rewriter.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp index a3e56358b..d970bd95d 100644 --- a/src/theory/arith/nl/ext/monomial_check.cpp +++ b/src/theory/arith/nl/ext/monomial_check.cpp @@ -15,6 +15,7 @@ #include "theory/arith/nl/ext/monomial_check.h" #include "expr/node.h" +#include "expr/proof.h" #include "theory/arith/arith_msum.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/nl_model.h" diff --git a/src/theory/arith/nl/ext/monomial_check.h b/src/theory/arith/nl/ext/monomial_check.h index 51179826a..05908ecc7 100644 --- a/src/theory/arith/nl/ext/monomial_check.h +++ b/src/theory/arith/nl/ext/monomial_check.h @@ -16,6 +16,7 @@ #define CVC4__THEORY__ARITH__NL__EXT__MONOMIAL_CHECK_H #include "expr/node.h" +#include "theory/theory_inference.h" #include "theory/arith/nl/ext/ext_state.h" namespace CVC4 { diff --git a/src/theory/arith/nl/ext/split_zero_check.cpp b/src/theory/arith/nl/ext/split_zero_check.cpp index 1e9b444e3..5bcdb801d 100644 --- a/src/theory/arith/nl/ext/split_zero_check.cpp +++ b/src/theory/arith/nl/ext/split_zero_check.cpp @@ -15,9 +15,11 @@ #include "theory/arith/nl/ext/split_zero_check.h" #include "expr/node.h" +#include "expr/proof.h" #include "theory/arith/arith_msum.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/nl_model.h" +#include "theory/rewriter.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/nl/ext/split_zero_check.h b/src/theory/arith/nl/ext/split_zero_check.h index e8730e496..0e7ad0999 100644 --- a/src/theory/arith/nl/ext/split_zero_check.h +++ b/src/theory/arith/nl/ext/split_zero_check.h @@ -16,6 +16,7 @@ #define CVC4__THEORY__ARITH__NL__EXT__SPLIT_ZERO_CHECK_H #include "expr/node.h" +#include "context/cdhashset.h" #include "theory/arith/nl/ext/ext_state.h" namespace CVC4 { diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp index 3d646a684..2d04c2b5c 100644 --- a/src/theory/arith/nl/ext/tangent_plane_check.cpp +++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp @@ -15,9 +15,11 @@ #include "theory/arith/nl/ext/tangent_plane_check.h" #include "expr/node.h" +#include "expr/proof.h" #include "theory/arith/arith_msum.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/nl_model.h" +#include "theory/rewriter.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/nl/ext_theory_callback.cpp b/src/theory/arith/nl/ext_theory_callback.cpp index 62e1fa904..ee12d17d6 100644 --- a/src/theory/arith/nl/ext_theory_callback.cpp +++ b/src/theory/arith/nl/ext_theory_callback.cpp @@ -15,6 +15,7 @@ #include "theory/arith/nl/ext_theory_callback.h" #include "theory/arith/arith_utilities.h" +#include "theory/uf/equality_engine.h" using namespace CVC4::kind; diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp index a5b4e87bd..6487b48ec 100644 --- a/src/theory/arith/nl/iand_solver.cpp +++ b/src/theory/arith/nl/iand_solver.cpp @@ -18,7 +18,10 @@ #include "options/smt_options.h" #include "preprocessing/passes/bv_to_int.h" #include "theory/arith/arith_msum.h" +#include "theory/arith/arith_state.h" #include "theory/arith/arith_utilities.h" +#include "theory/arith/inference_manager.h" +#include "theory/arith/nl/nl_model.h" #include "util/iand.h" using namespace CVC4::kind; diff --git a/src/theory/arith/nl/iand_solver.h b/src/theory/arith/nl/iand_solver.h index c854f3ab7..044a37abc 100644 --- a/src/theory/arith/nl/iand_solver.h +++ b/src/theory/arith/nl/iand_solver.h @@ -20,17 +20,20 @@ #include "context/cdhashset.h" #include "expr/node.h" -#include "theory/arith/arith_state.h" -#include "theory/arith/inference_manager.h" #include "theory/arith/nl/iand_utils.h" #include "theory/arith/nl/nl_lemma_utils.h" -#include "theory/arith/nl/nl_model.h" namespace CVC4 { namespace theory { namespace arith { + +class ArithState; +class InferenceManager; + namespace nl { +class NlModel; + /** Integer and solver class * */ diff --git a/src/theory/arith/nl/iand_utils.cpp b/src/theory/arith/nl/iand_utils.cpp index 17eb518a2..652f0eec7 100644 --- a/src/theory/arith/nl/iand_utils.cpp +++ b/src/theory/arith/nl/iand_utils.cpp @@ -19,6 +19,8 @@ #include "cvc4_private.h" #include "theory/arith/nl/nl_model.h" +#include "theory/rewriter.h" + namespace CVC4 { namespace theory { namespace arith { diff --git a/src/theory/arith/nl/iand_utils.h b/src/theory/arith/nl/iand_utils.h index a05defc0a..4c1de0196 100644 --- a/src/theory/arith/nl/iand_utils.h +++ b/src/theory/arith/nl/iand_utils.h @@ -16,7 +16,7 @@ #ifndef CVC4__THEORY__ARITH__IAND_TABLE_H #define CVC4__THEORY__ARITH__IAND_TABLE_H -#include <tuple> +#include <map> #include <vector> #include "expr/node.h" diff --git a/src/theory/arith/nl/icp/icp_solver.cpp b/src/theory/arith/nl/icp/icp_solver.cpp index af86d69fd..7d698a221 100644 --- a/src/theory/arith/nl/icp/icp_solver.cpp +++ b/src/theory/arith/nl/icp/icp_solver.cpp @@ -20,6 +20,7 @@ #include "base/output.h" #include "expr/node_algorithm.h" #include "theory/arith/arith_msum.h" +#include "theory/arith/inference_manager.h" #include "theory/arith/nl/poly_conversion.h" #include "theory/arith/normal_form.h" #include "theory/rewriter.h" diff --git a/src/theory/arith/nl/icp/icp_solver.h b/src/theory/arith/nl/icp/icp_solver.h index 176549d8b..b9ecfc437 100644 --- a/src/theory/arith/nl/icp/icp_solver.h +++ b/src/theory/arith/nl/icp/icp_solver.h @@ -23,7 +23,6 @@ #include "expr/node.h" #include "theory/arith/bound_inference.h" -#include "theory/arith/inference_manager.h" #include "theory/arith/nl/icp/candidate.h" #include "theory/arith/nl/icp/contraction_origins.h" #include "theory/arith/nl/icp/intersection.h" @@ -32,6 +31,9 @@ namespace CVC4 { namespace theory { namespace arith { + +class InferenceManager; + namespace nl { namespace icp { diff --git a/src/theory/arith/nl/icp/intersection.cpp b/src/theory/arith/nl/icp/intersection.cpp index aa8fcf543..b5fedb7eb 100644 --- a/src/theory/arith/nl/icp/intersection.cpp +++ b/src/theory/arith/nl/icp/intersection.cpp @@ -18,6 +18,8 @@ #include <iostream> +#include <poly/polyxx.h> + #include "base/check.h" #include "base/output.h" #include "theory/arith/nl/poly_conversion.h" diff --git a/src/theory/arith/nl/icp/intersection.h b/src/theory/arith/nl/icp/intersection.h index 0df6caf34..cdc166139 100644 --- a/src/theory/arith/nl/icp/intersection.h +++ b/src/theory/arith/nl/icp/intersection.h @@ -18,7 +18,9 @@ #include "util/real_algebraic_number.h" #ifdef CVC4_POLY_IMP -#include <poly/polyxx.h> +namespace poly { + class Interval; +} namespace CVC4 { namespace theory { diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp index 5c4140430..9255d3349 100644 --- a/src/theory/arith/nl/nl_model.cpp +++ b/src/theory/arith/nl/nl_model.cpp @@ -20,6 +20,7 @@ #include "options/theory_options.h" #include "theory/arith/arith_msum.h" #include "theory/arith/arith_utilities.h" +#include "theory/theory_model.h" #include "theory/rewriter.h" using namespace CVC4::kind; diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h index cd2d15563..4d5585545 100644 --- a/src/theory/arith/nl/nl_model.h +++ b/src/theory/arith/nl/nl_model.h @@ -19,15 +19,20 @@ #include <unordered_map> #include <vector> -#include "context/cdo.h" -#include "context/context.h" #include "expr/kind.h" #include "expr/node.h" #include "theory/arith/nl/nl_lemma_utils.h" -#include "theory/theory_model.h" namespace CVC4 { + +namespace context { +class Context; +} + namespace theory { + +class TheoryModel; + namespace arith { namespace nl { diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index c46781e76..f269f1d69 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -18,10 +18,10 @@ #include "theory/arith/nl/nonlinear_extension.h" #include "options/arith_options.h" -#include "options/theory_options.h" #include "theory/arith/arith_state.h" -#include "theory/arith/arith_utilities.h" #include "theory/arith/bound_inference.h" +#include "theory/arith/inference_manager.h" +#include "theory/arith/nl/nl_lemma_utils.h" #include "theory/arith/theory_arith.h" #include "theory/ext_theory.h" #include "theory/theory_model.h" diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index fba9e8e87..6a38021a0 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -21,10 +21,7 @@ #include <map> #include <vector> -#include "context/cdlist.h" -#include "expr/kind.h" #include "expr/node.h" -#include "theory/arith/inference_manager.h" #include "theory/arith/nl/cad_solver.h" #include "theory/arith/nl/ext/factoring_check.h" #include "theory/arith/nl/ext/monomial_bounds_check.h" @@ -35,19 +32,25 @@ #include "theory/arith/nl/ext_theory_callback.h" #include "theory/arith/nl/iand_solver.h" #include "theory/arith/nl/icp/icp_solver.h" -#include "theory/arith/nl/nl_lemma_utils.h" #include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/stats.h" #include "theory/arith/nl/strategy.h" #include "theory/arith/nl/transcendental/transcendental_solver.h" #include "theory/ext_theory.h" -#include "theory/uf/equality_engine.h" namespace CVC4 { namespace theory { +namespace eq { + class EqualityEngine; +} namespace arith { + +class InferenceManager; + namespace nl { +class NlLemma; + /** Non-linear extension class * * This class implements model-based refinement schemes diff --git a/src/theory/arith/nl/poly_conversion.cpp b/src/theory/arith/nl/poly_conversion.cpp index 5b7edb3ef..67cfd5807 100644 --- a/src/theory/arith/nl/poly_conversion.cpp +++ b/src/theory/arith/nl/poly_conversion.cpp @@ -20,9 +20,8 @@ #include "expr/node.h" #include "expr/node_manager_attributes.h" -#include "util/integer.h" +#include "theory/arith/bound_inference.h" #include "util/poly_util.h" -#include "util/rational.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/nl/poly_conversion.h b/src/theory/arith/nl/poly_conversion.h index 37d816179..102d2d6ae 100644 --- a/src/theory/arith/nl/poly_conversion.h +++ b/src/theory/arith/nl/poly_conversion.h @@ -23,15 +23,18 @@ #include <poly/polyxx.h> -#include <iostream> +#include <cstddef> +#include <map> +#include <utility> #include "expr/node.h" -#include "theory/arith/bound_inference.h" -#include "util/real_algebraic_number.h" namespace CVC4 { namespace theory { namespace arith { + +class BoundInference; + namespace nl { /** Bijective mapping between CVC4 variables and poly variables. */ diff --git a/src/theory/arith/nl/stats.h b/src/theory/arith/nl/stats.h index f869d83a4..fab4de35a 100644 --- a/src/theory/arith/nl/stats.h +++ b/src/theory/arith/nl/stats.h @@ -17,8 +17,6 @@ #ifndef CVC4__THEORY__ARITH__NL__STATS_H #define CVC4__THEORY__ARITH__NL__STATS_H -#include "expr/kind.h" -#include "theory/inference_id.h" #include "util/statistics_registry.h" namespace CVC4 { diff --git a/src/theory/arith/nl/strategy.h b/src/theory/arith/nl/strategy.h index 526ae36f1..1f7b85b60 100644 --- a/src/theory/arith/nl/strategy.h +++ b/src/theory/arith/nl/strategy.h @@ -16,7 +16,6 @@ #define CVC4__THEORY__ARITH__NL__STRATEGY_H #include <iosfwd> -#include <map> #include <vector> namespace CVC4 { diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp index 86b17376c..74766926b 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.cpp +++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp @@ -19,9 +19,11 @@ #include "expr/node_algorithm.h" #include "expr/node_builder.h" +#include "expr/proof.h" #include "options/arith_options.h" #include "theory/arith/arith_msum.h" #include "theory/arith/arith_utilities.h" +#include "theory/arith/inference_manager.h" #include "theory/rewriter.h" namespace CVC4 { diff --git a/src/theory/arith/nl/transcendental/exponential_solver.h b/src/theory/arith/nl/transcendental/exponential_solver.h index b874e1a4b..ddef4faf7 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.h +++ b/src/theory/arith/nl/transcendental/exponential_solver.h @@ -21,8 +21,6 @@ #include <vector> #include "expr/node.h" -#include "theory/arith/inference_manager.h" -#include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/transcendental/transcendental_state.h" namespace CVC4 { diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp index f5dc49da8..11852ac3a 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.cpp +++ b/src/theory/arith/nl/transcendental/sine_solver.cpp @@ -19,6 +19,7 @@ #include "expr/node_algorithm.h" #include "expr/node_builder.h" +#include "expr/proof.h" #include "options/arith_options.h" #include "theory/arith/arith_msum.h" #include "theory/arith/arith_utilities.h" diff --git a/src/theory/arith/nl/transcendental/sine_solver.h b/src/theory/arith/nl/transcendental/sine_solver.h index da4b48fd6..a009df09b 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.h +++ b/src/theory/arith/nl/transcendental/sine_solver.h @@ -21,8 +21,6 @@ #include <vector> #include "expr/node.h" -#include "theory/arith/inference_manager.h" -#include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/transcendental/transcendental_state.h" namespace CVC4 { diff --git a/src/theory/arith/nl/transcendental/taylor_generator.cpp b/src/theory/arith/nl/transcendental/taylor_generator.cpp index 375f1757e..f45b906bc 100644 --- a/src/theory/arith/nl/transcendental/taylor_generator.cpp +++ b/src/theory/arith/nl/transcendental/taylor_generator.cpp @@ -15,6 +15,7 @@ #include "theory/arith/nl/transcendental/taylor_generator.h" #include "theory/arith/arith_utilities.h" +#include "theory/arith/nl/nl_model.h" #include "theory/rewriter.h" namespace CVC4 { diff --git a/src/theory/arith/nl/transcendental/taylor_generator.h b/src/theory/arith/nl/transcendental/taylor_generator.h index ccdc80e0f..0e1248f7c 100644 --- a/src/theory/arith/nl/transcendental/taylor_generator.h +++ b/src/theory/arith/nl/transcendental/taylor_generator.h @@ -16,12 +16,14 @@ #define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TAYLOR_GENERATOR_H #include "expr/node.h" -#include "theory/arith/nl/nl_model.h" namespace CVC4 { namespace theory { namespace arith { namespace nl { + +class NlModel; + namespace transcendental { class TaylorGenerator diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp index e58da1aad..d1355c746 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp @@ -22,6 +22,7 @@ #include "options/arith_options.h" #include "theory/arith/arith_msum.h" #include "theory/arith/arith_utilities.h" +#include "theory/arith/inference_manager.h" #include "theory/arith/nl/transcendental/taylor_generator.h" #include "theory/rewriter.h" diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.h b/src/theory/arith/nl/transcendental/transcendental_solver.h index 8135ba1fb..343f303d1 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.h +++ b/src/theory/arith/nl/transcendental/transcendental_solver.h @@ -9,37 +9,15 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -/********************* */ -/*! \file transcendental_solver.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Tim King - ** 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 Solving for handling transcendental functions. **/ #ifndef CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_SOLVER_H #define CVC4__THEORY__ARITH__NL__TRANSCENDENTAL__TRANSCENDENTAL_SOLVER_H -#include <map> -#include <unordered_map> -#include <unordered_set> #include <vector> #include "expr/node.h" -#include "theory/arith/inference_manager.h" -#include "theory/arith/nl/nl_model.h" #include "theory/arith/nl/transcendental/exponential_solver.h" #include "theory/arith/nl/transcendental/sine_solver.h" #include "theory/arith/nl/transcendental/transcendental_state.h" @@ -47,7 +25,13 @@ namespace CVC4 { namespace theory { namespace arith { + +class InferenceManager; + namespace nl { + +class NlModel; + namespace transcendental { /** Transcendental solver class diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp index 76c3d5357..ae8c1eea7 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp @@ -14,8 +14,10 @@ #include "theory/arith/nl/transcendental/transcendental_state.h" +#include "expr/proof.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/nl/transcendental/taylor_generator.h" +#include "theory/rewriter.h" namespace CVC4 { namespace theory { diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h index 93ac4627a..d0678fb9a 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.h +++ b/src/theory/arith/nl/transcendental/transcendental_state.h @@ -23,6 +23,7 @@ #include "theory/arith/nl/transcendental/taylor_generator.h" namespace CVC4 { +class CDProof; namespace theory { namespace arith { namespace nl { diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 5c1b90663..d0a7f7fc4 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -19,6 +19,7 @@ #include "base/output.h" #include "options/arith_options.h" #include "theory/arith/constraint.h" +#include "theory/arith/error_set.h" #include "theory/arith/simplex.h" diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index 6740c8e1c..e34696cb5 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -57,7 +57,6 @@ #include "theory/arith/arithvar.h" #include "theory/arith/delta_rational.h" -#include "theory/arith/error_set.h" #include "theory/arith/linear_equality.h" #include "theory/arith/partial_model.h" #include "theory/arith/tableau.h" @@ -68,6 +67,8 @@ namespace CVC4 { namespace theory { namespace arith { +class ErrorSet; + class SimplexDecisionProcedure { protected: typedef std::vector< std::pair<ArithVar, int> > AVIntPairVec; diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp index 18169474d..796cd9412 100644 --- a/src/theory/arith/soi_simplex.cpp +++ b/src/theory/arith/soi_simplex.cpp @@ -22,6 +22,7 @@ #include "options/arith_options.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" +#include "theory/arith/error_set.h" #include "util/statistics_registry.h" using namespace std; diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index eba84e339..f3344cbda 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -22,13 +22,15 @@ #include "theory/arith/arith_rewriter.h" #include "theory/arith/arith_state.h" #include "theory/arith/inference_manager.h" -#include "theory/arith/nl/nonlinear_extension.h" #include "theory/arith/operator_elim.h" #include "theory/theory.h" namespace CVC4 { namespace theory { namespace arith { +namespace nl { +class NonlinearExtension; +} class TheoryArithPrivate; diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 3b5f0dd82..40bd81795 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -65,6 +65,7 @@ #include "theory/quantifiers/fmf/bounded_integers.h" #include "theory/rewriter.h" #include "theory/theory_model.h" +#include "theory/trust_substitutions.h" #include "theory/valuation.h" #include "util/dense_map.h" #include "util/integer.h" diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 56e8fa4b0..818393cc7 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -43,6 +43,7 @@ #include "theory/arith/delta_rational.h" #include "theory/arith/dio_solver.h" #include "theory/arith/dual_simplex.h" +#include "theory/arith/error_set.h" #include "theory/arith/fc_simplex.h" #include "theory/arith/infer_bounds.h" #include "theory/arith/linear_equality.h" diff --git a/src/theory/arrays/inference_manager.cpp b/src/theory/arrays/inference_manager.cpp index 96f2b02c3..b5bb9be14 100644 --- a/src/theory/arrays/inference_manager.cpp +++ b/src/theory/arrays/inference_manager.cpp @@ -16,6 +16,7 @@ #include "options/smt_options.h" #include "theory/theory.h" +#include "theory/theory_state.h" #include "theory/uf/equality_engine.h" using namespace CVC4::kind; diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 4dd7dcafd..49f530e32 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -28,8 +28,10 @@ #include "smt/smt_statistics_registry.h" #include "theory/arrays/skolem_cache.h" #include "theory/arrays/theory_arrays_rewriter.h" +#include "theory/decision_manager.h" #include "theory/rewriter.h" #include "theory/theory_model.h" +#include "theory/trust_substitutions.h" #include "theory/valuation.h" using namespace std; diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 7e4f0e36c..e02c30296 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -29,7 +29,9 @@ #include "theory/arrays/inference_manager.h" #include "theory/arrays/proof_checker.h" #include "theory/arrays/theory_arrays_rewriter.h" +#include "theory/decision_strategy.h" #include "theory/theory.h" +#include "theory/theory_state.h" #include "theory/uf/equality_engine.h" #include "theory/uf/proof_equality_engine.h" #include "util/statistics_registry.h" diff --git a/src/theory/bags/bag_solver.cpp b/src/theory/bags/bag_solver.cpp index 76c001ba2..c39e0198b 100644 --- a/src/theory/bags/bag_solver.cpp +++ b/src/theory/bags/bag_solver.cpp @@ -17,6 +17,7 @@ #include "theory/bags/bag_solver.h" #include "theory/bags/inference_generator.h" +#include "theory/uf/equality_engine_iterator.h" using namespace std; using namespace CVC4::context; diff --git a/src/theory/bags/bags_rewriter.h b/src/theory/bags/bags_rewriter.h index 48cd9c419..d9f736c4f 100644 --- a/src/theory/bags/bags_rewriter.h +++ b/src/theory/bags/bags_rewriter.h @@ -19,6 +19,7 @@ #include "theory/bags/rewrites.h" #include "theory/rewriter.h" +#include "util/statistics_registry.h" namespace CVC4 { namespace theory { diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp index 726160d83..f00bffb2e 100644 --- a/src/theory/booleans/circuit_propagator.cpp +++ b/src/theory/booleans/circuit_propagator.cpp @@ -21,6 +21,7 @@ #include <vector> #include "expr/node_algorithm.h" +#include "expr/proof_node_manager.h" #include "theory/booleans/proof_circuit_propagator.h" #include "util/utility.h" diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index 90de1d8da..b5ad16b1c 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -25,6 +25,7 @@ #include "theory/booleans/theory_bool_rewriter.h" #include "theory/substitutions.h" #include "theory/theory.h" +#include "theory/trust_substitutions.h" #include "theory/valuation.h" #include "util/hash.h" diff --git a/src/theory/bv/bitblast/simple_bitblaster.cpp b/src/theory/bv/bitblast/simple_bitblaster.cpp index 551c18612..4c7311945 100644 --- a/src/theory/bv/bitblast/simple_bitblaster.cpp +++ b/src/theory/bv/bitblast/simple_bitblaster.cpp @@ -15,6 +15,7 @@ #include "theory/bv/bitblast/simple_bitblaster.h" #include "theory/theory_model.h" +#include "theory/theory_state.h" namespace CVC4 { namespace theory { diff --git a/src/theory/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h index 38e4b3aa6..d9adf06fb 100644 --- a/src/theory/bv/bv_inequality_graph.h +++ b/src/theory/bv/bv_inequality_graph.h @@ -24,6 +24,7 @@ #include <unordered_map> #include <unordered_set> +#include "context/cdhashset.h" #include "context/cdqueue.h" #include "context/context.h" #include "theory/theory.h" diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp index d8d8dbed7..3cadac621 100644 --- a/src/theory/bv/bv_solver_lazy.cpp +++ b/src/theory/bv/bv_solver_lazy.cpp @@ -30,6 +30,7 @@ #include "theory/bv/theory_bv_rewriter.h" #include "theory/bv/theory_bv_utils.h" #include "theory/theory_model.h" +#include "theory/trust_substitutions.h" using namespace CVC4::theory::bv::utils; diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 55a0ff46b..47974fc03 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -21,6 +21,7 @@ #include "theory/bv/bv_solver_lazy.h" #include "theory/bv/bv_solver_simple.h" #include "theory/bv/theory_bv_utils.h" +#include "theory/ee_setup_info.h" namespace CVC4 { namespace theory { diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 2aa722e48..fafde0601 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -24,6 +24,7 @@ #include "theory/bv/theory_bv_rewriter.h" #include "theory/theory.h" #include "theory/theory_eq_notify.h" +#include "theory/theory_state.h" namespace CVC4 { namespace theory { diff --git a/src/theory/care_graph.h b/src/theory/care_graph.h index 40553f01b..6793d6e90 100644 --- a/src/theory/care_graph.h +++ b/src/theory/care_graph.h @@ -21,8 +21,8 @@ #include <set> -#include "expr/kind.h" // For TheoryId. #include "expr/node.h" +#include "theory/theory_id.h" namespace CVC4 { namespace theory { diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index 4dbf26062..5334e76df 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -17,6 +17,7 @@ #include "theory/datatypes/datatypes_rewriter.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "expr/node_algorithm.h" #include "expr/sygus_datatype.h" #include "options/datatypes_options.h" diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp index 14dc9fbf1..ea5928a42 100644 --- a/src/theory/datatypes/infer_proof_cons.cpp +++ b/src/theory/datatypes/infer_proof_cons.cpp @@ -14,6 +14,7 @@ #include "theory/datatypes/infer_proof_cons.h" +#include "expr/proof.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/rewriter.h" diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp index 9702a5584..4c7773e29 100644 --- a/src/theory/datatypes/inference_manager.cpp +++ b/src/theory/datatypes/inference_manager.cpp @@ -17,7 +17,11 @@ #include "expr/dtype.h" #include "options/datatypes_options.h" #include "smt/smt_statistics_registry.h" +#include "theory/eager_proof_generator.h" +#include "theory/rewriter.h" #include "theory/theory.h" +#include "theory/theory_state.h" +#include "theory/trust_substitutions.h" using namespace CVC4::kind; diff --git a/src/theory/datatypes/inference_manager.h b/src/theory/datatypes/inference_manager.h index ba46d2a42..610383ff1 100644 --- a/src/theory/datatypes/inference_manager.h +++ b/src/theory/datatypes/inference_manager.h @@ -25,6 +25,9 @@ namespace CVC4 { namespace theory { + +class EagerProofGenerator; + namespace datatypes { /** diff --git a/src/theory/datatypes/proof_checker.cpp b/src/theory/datatypes/proof_checker.cpp index 6bfa20151..9a9f7cb7b 100644 --- a/src/theory/datatypes/proof_checker.cpp +++ b/src/theory/datatypes/proof_checker.cpp @@ -14,6 +14,7 @@ #include "theory/datatypes/proof_checker.h" +#include "expr/dtype_cons.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/rewriter.h" diff --git a/src/theory/datatypes/sygus_datatype_utils.cpp b/src/theory/datatypes/sygus_datatype_utils.cpp index 60bf36139..6169d3752 100644 --- a/src/theory/datatypes/sygus_datatype_utils.cpp +++ b/src/theory/datatypes/sygus_datatype_utils.cpp @@ -17,6 +17,7 @@ #include "theory/datatypes/sygus_datatype_utils.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "expr/node_algorithm.h" #include "expr/sygus_datatype.h" #include "smt/smt_engine.h" diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp index 7efd2a9ac..8622ec483 100644 --- a/src/theory/datatypes/sygus_extension.cpp +++ b/src/theory/datatypes/sygus_extension.cpp @@ -15,6 +15,7 @@ #include "theory/datatypes/sygus_extension.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "expr/node_manager.h" #include "expr/sygus_datatype.h" #include "options/base_options.h" diff --git a/src/theory/datatypes/sygus_simple_sym.cpp b/src/theory/datatypes/sygus_simple_sym.cpp index b7ab9b4f7..a2530f4ac 100644 --- a/src/theory/datatypes/sygus_simple_sym.cpp +++ b/src/theory/datatypes/sygus_simple_sym.cpp @@ -14,6 +14,7 @@ #include "theory/datatypes/sygus_simple_sym.h" +#include "expr/dtype_cons.h" #include "theory/quantifiers/term_util.h" using namespace std; diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 45787ee04..9105cdfd6 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -19,7 +19,9 @@ #include "base/check.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "expr/kind.h" +#include "expr/proof_node_manager.h" #include "options/datatypes_options.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 2834b86ba..73aef4dd7 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -20,6 +20,7 @@ #define CVC4__THEORY__DATATYPES__THEORY_DATATYPES_TYPE_RULES_H #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "expr/type_matcher.h" #include "theory/datatypes/theory_datatypes_utils.h" diff --git a/src/theory/datatypes/theory_datatypes_utils.cpp b/src/theory/datatypes/theory_datatypes_utils.cpp index c55b4a14f..1247ecca5 100644 --- a/src/theory/datatypes/theory_datatypes_utils.cpp +++ b/src/theory/datatypes/theory_datatypes_utils.cpp @@ -17,6 +17,7 @@ #include "theory/datatypes/theory_datatypes_utils.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" using namespace CVC4; using namespace CVC4::kind; diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp index 079430342..25bdd2f94 100644 --- a/src/theory/datatypes/type_enumerator.cpp +++ b/src/theory/datatypes/type_enumerator.cpp @@ -14,6 +14,7 @@ ** Enumerators for datatypes. **/ +#include "expr/dtype_cons.h" #include "theory/datatypes/type_enumerator.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/datatypes/theory_datatypes_utils.h" diff --git a/src/theory/ext_theory.cpp b/src/theory/ext_theory.cpp index 7b4936a53..030d9a497 100644 --- a/src/theory/ext_theory.cpp +++ b/src/theory/ext_theory.cpp @@ -20,7 +20,9 @@ #include "base/check.h" #include "smt/smt_statistics_registry.h" +#include "theory/output_channel.h" #include "theory/quantifiers_engine.h" +#include "theory/rewriter.h" #include "theory/substitutions.h" using namespace std; diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index 6df991ef9..e9b59fdae 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -22,9 +22,12 @@ #include <unordered_set> #include <vector> +#include "base/configuration.h" #include "options/fp_options.h" +#include "smt/logic_exception.h" #include "theory/fp/fp_converter.h" #include "theory/fp/theory_fp_rewriter.h" +#include "theory/output_channel.h" #include "theory/rewriter.h" #include "theory/theory_model.h" diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index 1a745b3a3..bd6e70ff1 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -23,9 +23,11 @@ #include <string> #include <utility> +#include "context/cdhashset.h" #include "context/cdo.h" #include "theory/fp/theory_fp_rewriter.h" #include "theory/theory.h" +#include "theory/theory_state.h" #include "theory/uf/equality_engine.h" namespace CVC4 { diff --git a/src/theory/inference_manager_buffered.cpp b/src/theory/inference_manager_buffered.cpp index 0c143f265..3e4b921db 100644 --- a/src/theory/inference_manager_buffered.cpp +++ b/src/theory/inference_manager_buffered.cpp @@ -16,6 +16,7 @@ #include "theory/rewriter.h" #include "theory/theory.h" +#include "theory/theory_state.h" using namespace CVC4::kind; diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp index bb2bf937a..24570f9a6 100644 --- a/src/theory/model_manager.cpp +++ b/src/theory/model_manager.cpp @@ -18,6 +18,7 @@ #include "options/theory_options.h" #include "prop/prop_engine.h" #include "theory/quantifiers_engine.h" +#include "theory/quantifiers/fmf/model_builder.h" #include "theory/theory_engine.h" namespace CVC4 { diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp index 16f0f3957..7a584c146 100644 --- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/cegqi/ceg_dt_instantiator.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "expr/node_algorithm.h" #include "theory/datatypes/theory_datatypes_utils.h" diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 0d1a51a30..bda4e31fc 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -18,6 +18,8 @@ #include "theory/quantifiers/cegqi/ceg_bv_instantiator.h" #include "theory/quantifiers/cegqi/ceg_dt_instantiator.h" +#include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "theory/arith/arith_msum.h" diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.cpp b/src/theory/quantifiers/cegqi/vts_term_cache.cpp index e782a1b6f..0c416fdf4 100644 --- a/src/theory/quantifiers/cegqi/vts_term_cache.cpp +++ b/src/theory/quantifiers/cegqi/vts_term_cache.cpp @@ -17,6 +17,7 @@ #include "expr/node_algorithm.h" #include "theory/arith/arith_msum.h" #include "theory/quantifiers/quantifiers_inference_manager.h" +#include "theory/rewriter.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp index eb02eb19e..c553a1239 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.cpp +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -14,11 +14,13 @@ #include "theory/quantifiers/ematching/candidate_generator.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "options/quantifiers_options.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "theory/quantifiers/inst_match.h" #include "theory/quantifiers/instantiate.h" +#include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index 5df350fe5..1875dc631 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -16,7 +16,10 @@ #include "theory/quantifiers/ematching/ho_trigger.h" #include "theory/quantifiers/instantiate.h" +#include "theory/quantifiers/quantifiers_inference_manager.h" +#include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" #include "theory/uf/theory_uf_rewriter.h" #include "util/hash.h" diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index ce535d5e8..07cb74a83 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/ematching/inst_match_generator.h" +#include "expr/dtype_cons.h" #include "options/quantifiers_options.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/ematching/candidate_generator.h" diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp index 5c5dcfef1..dfe2e3ae9 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi.cpp @@ -15,7 +15,9 @@ #include "theory/quantifiers/ematching/inst_match_generator_multi.h" #include "theory/quantifiers/quantifiers_state.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" +#include "theory/uf/equality_engine_iterator.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp index 66433ba78..00a233d6a 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp @@ -14,6 +14,8 @@ #include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h" #include "theory/quantifiers_engine.h" +#include "theory/quantifiers/ematching/trigger_trie.h" +#include "theory/quantifiers/term_util.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp index 6b2f1b7f8..f9692bd76 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator_simple.cpp @@ -14,6 +14,11 @@ #include "theory/quantifiers/ematching/inst_match_generator_simple.h" #include "theory/quantifiers/ematching/trigger_term_info.h" +#include "theory/quantifiers/ematching/trigger_trie.h" +#include "theory/quantifiers/instantiate.h" +#include "theory/quantifiers/quantifiers_state.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index e7635f200..9768e7f2c 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -16,6 +16,8 @@ #include "theory/quantifiers/ematching/pattern_term_selector.h" #include "theory/quantifiers/quant_relevance.h" +#include "theory/quantifiers/quantifiers_inference_manager.h" +#include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers_engine.h" #include "util/random.h" diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp index 14913bdc1..c2b5f78ae 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/ematching/inst_strategy_e_matching_user.h" #include "theory/quantifiers/ematching/pattern_term_selector.h" +#include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers_engine.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/ematching/pattern_term_selector.cpp b/src/theory/quantifiers/ematching/pattern_term_selector.cpp index a64dc4424..6564f407e 100644 --- a/src/theory/quantifiers/ematching/pattern_term_selector.cpp +++ b/src/theory/quantifiers/ematching/pattern_term_selector.cpp @@ -18,6 +18,7 @@ #include "theory/arith/arith_msum.h" #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/term_util.h" +#include "theory/rewriter.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index 79bd5c1dd..9d8b64e25 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -22,10 +22,12 @@ #include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h" #include "theory/quantifiers/ematching/inst_match_generator_simple.h" #include "theory/quantifiers/ematching/pattern_term_selector.h" +#include "theory/quantifiers/ematching/trigger_trie.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_inference_manager.h" #include "theory/quantifiers/quantifiers_state.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/ematching/var_match_generator.cpp b/src/theory/quantifiers/ematching/var_match_generator.cpp index 8448fe810..17baf5000 100644 --- a/src/theory/quantifiers/ematching/var_match_generator.cpp +++ b/src/theory/quantifiers/ematching/var_match_generator.cpp @@ -13,7 +13,9 @@ **/ #include "theory/quantifiers/ematching/var_match_generator.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" +#include "theory/rewriter.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index 759d3e69f..6ce561b2d 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -19,6 +19,7 @@ #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "theory/quantifiers/term_util.h" +#include "theory/rewriter.h" #include "theory/smt_engine_subsolver.h" using namespace std; diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 700ae2c64..fb0505bae 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -16,10 +16,12 @@ #include "theory/quantifiers/fmf/bounded_integers.h" +#include "expr/dtype_cons.h" #include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "theory/arith/arith_msum.h" #include "theory/datatypes/theory_datatypes_utils.h" +#include "theory/decision_manager.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fmf/model_engine.h" #include "theory/quantifiers/term_enumeration.h" diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index 9d4a414e9..3e7466ed2 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -23,6 +23,7 @@ #include "context/cdhashmap.h" #include "context/context.h" #include "expr/attribute.h" +#include "theory/decision_strategy.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index 96e8a40be..c248167cb 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/inst_match.h" #include "theory/quantifiers/instantiate.h" +#include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers_engine.h" diff --git a/src/theory/quantifiers/inst_match_trie.cpp b/src/theory/quantifiers/inst_match_trie.cpp index 993fad90a..ab5dcb166 100644 --- a/src/theory/quantifiers/inst_match_trie.cpp +++ b/src/theory/quantifiers/inst_match_trie.cpp @@ -19,6 +19,7 @@ #include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers_engine.h" +#include "theory/uf/equality_engine_iterator.h" using namespace CVC4::context; diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 2eb99a774..3164ff5ce 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/instantiate.h" #include "expr/node_algorithm.h" +#include "expr/proof_node_manager.h" #include "options/printer_options.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index a0b776819..37cc49f17 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -19,6 +19,8 @@ #include <map> +#include "context/cdhashset.h" +#include "expr/lazy_proof.h" #include "expr/node.h" #include "expr/proof.h" #include "theory/quantifiers/inst_match_trie.h" diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index f89f9f0ea..cf37bc746 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/quant_conflict_find.h" +#include "base/configuration.h" #include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "options/theory_options.h" diff --git a/src/theory/quantifiers/quant_rep_bound_ext.cpp b/src/theory/quantifiers/quant_rep_bound_ext.cpp index 5bb50c926..58716f809 100644 --- a/src/theory/quantifiers/quant_rep_bound_ext.cpp +++ b/src/theory/quantifiers/quant_rep_bound_ext.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/quant_rep_bound_ext.h" #include "theory/quantifiers_engine.h" +#include "theory/quantifiers/first_order_model.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index a0b780836..e3bd2072f 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -13,6 +13,9 @@ **/ #include "theory/quantifiers/quant_split.h" + +#include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers_engine.h" #include "theory/quantifiers/first_order_model.h" diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 2126bf1f0..ec7e7fd2c 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -16,6 +16,7 @@ #include "expr/bound_var_manager.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "theory/arith/arith_msum.h" @@ -27,6 +28,7 @@ #include "theory/quantifiers/skolemize.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" +#include "theory/rewriter.h" #include "theory/strings/theory_strings_utils.h" using namespace std; diff --git a/src/theory/quantifiers/quantifiers_state.cpp b/src/theory/quantifiers/quantifiers_state.cpp index 0bcca266e..55f680897 100644 --- a/src/theory/quantifiers/quantifiers_state.cpp +++ b/src/theory/quantifiers/quantifiers_state.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/quantifiers_state.h" #include "options/quantifiers_options.h" +#include "theory/uf/equality_engine_iterator.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 3cef2884f..b97a8e539 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/relevant_domain.h" #include "theory/arith/arith_msum.h" #include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index a9ac7d0d2..42729ef5b 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/skolemize.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "expr/skolem_manager.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp index b296a4421..77714f87d 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/sygus/ce_guided_single_inv_sol.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "smt/command.h" diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index db2a972d5..a58ce894d 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/sygus/cegis_core_connective.h" +#include "expr/dtype_cons.h" #include "options/base_options.h" #include "printer/printer.h" #include "proof/unsat_core.h" diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index 9db77fd95..5da6f2121 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -19,6 +19,7 @@ #include <map> #include <vector> +#include "theory/decision_strategy.h" #include "theory/quantifiers/sygus/cegis.h" #include "theory/quantifiers/sygus/sygus_unif_rl.h" diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp index 360476399..f6e34e8a1 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/sygus/enum_stream_substitution.h" +#include "expr/dtype_cons.h" #include "options/base_options.h" #include "options/datatypes_options.h" #include "options/quantifiers_options.h" diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp index e0159049b..2fa6009d3 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp @@ -14,6 +14,7 @@ #include "theory/quantifiers/sygus/sygus_enumerator.h" +#include "expr/dtype_cons.h" #include "expr/node_algorithm.h" #include "options/datatypes_options.h" #include "options/quantifiers_options.h" diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp index 882c9ca77..90765284a 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp @@ -14,10 +14,12 @@ #include "theory/quantifiers/sygus/sygus_eval_unfold.h" +#include "expr/dtype_cons.h" #include "expr/sygus_datatype.h" #include "options/quantifiers_options.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/sygus/term_database_sygus.h" +#include "theory/rewriter.h" using namespace std; using namespace CVC4::kind; diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp index 0f9d2ccd1..5965e9430 100644 --- a/src/theory/quantifiers/sygus/sygus_explain.cpp +++ b/src/theory/quantifiers/sygus/sygus_explain.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/sygus/sygus_explain.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/sygus/term_database_sygus.h" diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 538d80e44..98a177f86 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -16,6 +16,7 @@ #include <stack> +#include "expr/dtype_cons.h" #include "options/quantifiers_options.h" #include "theory/bv/theory_bv_utils.h" #include "theory/datatypes/sygus_datatype_utils.h" diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp index 7d757ca98..953eac7b0 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/sygus/sygus_grammar_norm.h" +#include "expr/dtype_cons.h" #include "expr/node_manager_attributes.h" // for VarNameAttr #include "options/quantifiers_options.h" #include "smt/smt_engine.h" diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp index 6e36222b6..cc29e7b0a 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/sygus/sygus_grammar_red.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "expr/sygus_datatype.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/sygus/term_database_sygus.h" diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.cpp b/src/theory/quantifiers/sygus/sygus_process_conj.cpp index 1e67bb8cc..a2675dd96 100644 --- a/src/theory/quantifiers/sygus/sygus_process_conj.cpp +++ b/src/theory/quantifiers/sygus/sygus_process_conj.cpp @@ -19,6 +19,7 @@ #include "options/quantifiers_options.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" +#include "theory/rewriter.h" using namespace CVC4::kind; using namespace std; diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 81120da28..8b741b6d7 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/sygus/sygus_repair_const.h" #include "api/cvc4cpp.h" +#include "expr/dtype_cons.h" #include "expr/node_algorithm.h" #include "options/base_options.h" #include "options/quantifiers_options.h" diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp index f0d3e47b6..1c0cfcc55 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp @@ -15,12 +15,14 @@ #include "theory/quantifiers/sygus/sygus_unif_strat.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/quantifiers/sygus/sygus_eval_unfold.h" #include "theory/quantifiers/sygus/sygus_unif.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" +#include "theory/rewriter.h" using namespace std; using namespace CVC4::kind; diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 0fcba916b..56691c7c1 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -14,6 +14,7 @@ **/ #include "theory/quantifiers/sygus/synth_conjecture.h" +#include "base/configuration.h" #include "options/base_options.h" #include "options/datatypes_options.h" #include "options/quantifiers_options.h" diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index bc5cd1fda..f393601ad 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/sygus/term_database_sygus.h" #include "base/check.h" +#include "expr/dtype_cons.h" #include "expr/sygus_datatype.h" #include "options/base_options.h" #include "options/datatypes_options.h" @@ -23,6 +24,8 @@ #include "theory/arith/arith_msum.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/quantifiers_inference_manager.h" +#include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp index d44d2eda8..8e29ab9d6 100644 --- a/src/theory/quantifiers/sygus/type_info.cpp +++ b/src/theory/quantifiers/sygus/type_info.cpp @@ -16,6 +16,7 @@ #include "base/check.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "expr/sygus_datatype.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/sygus/term_database_sygus.h" diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp index 9fdf0aa7f..a46d4e445 100644 --- a/src/theory/quantifiers/sygus_inst.cpp +++ b/src/theory/quantifiers/sygus_inst.cpp @@ -18,11 +18,14 @@ #include <unordered_set> #include "expr/node_algorithm.h" +#include "options/quantifiers_options.h" #include "theory/bv/theory_bv_utils.h" #include "theory/datatypes/sygus_datatype_utils.h" +#include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/sygus/sygus_enumerator.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" #include "theory/quantifiers/sygus/synth_engine.h" +#include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" namespace CVC4 { diff --git a/src/theory/quantifiers/sygus_inst.h b/src/theory/quantifiers/sygus_inst.h index 3116f35e6..17cb1c9a1 100644 --- a/src/theory/quantifiers/sygus_inst.h +++ b/src/theory/quantifiers/sygus_inst.h @@ -21,6 +21,7 @@ #include <unordered_set> #include "context/cdhashset.h" +#include "theory/decision_strategy.h" #include "theory/quantifiers/quant_module.h" namespace CVC4 { diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index 62eef124a..a72054f6d 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/sygus_sampler.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "expr/node_algorithm.h" #include "options/base_options.h" #include "options/quantifiers_options.h" diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index cb5c7dfec..281d5c844 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -21,6 +21,8 @@ #include "options/uf_options.h" #include "theory/quantifiers/ematching/trigger_term_info.h" #include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/quantifiers_inference_manager.h" +#include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 9a031f99c..b121b2c46 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -20,6 +20,8 @@ #include <map> #include <unordered_set> +#include "context/cdhashmap.h" +#include "context/cdhashset.h" #include "expr/attribute.h" #include "expr/node_trie.h" #include "theory/quantifiers/quant_util.h" diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index 9cbf2cf53..33f74c7c4 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -25,6 +25,7 @@ #include "theory/quantifiers/term_enumeration.h" #include "theory/quantifiers_engine.h" #include "theory/strings/word.h" +#include "theory/rewriter.h" using namespace std; using namespace CVC4::kind; diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index 036b63b27..98bb9bec3 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -18,7 +18,6 @@ #define CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H #include <map> -#include <unordered_set> #include "expr/attribute.h" #include "expr/node.h" @@ -55,8 +54,6 @@ typedef expr::Attribute< QuantIdNumAttributeId, uint64_t > QuantIdNumAttribute; namespace quantifiers { -class TermDatabase; - // TODO : #1216 split this class, most of the functions in this class should be dispersed to where they are used. class TermUtil { diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 7046a8ef0..79422b418 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -20,10 +20,22 @@ #include "options/uf_options.h" #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" +#include "theory/quantifiers/ematching/trigger_trie.h" +#include "theory/quantifiers/equality_query.h" +#include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fmf/first_order_model_fmc.h" #include "theory/quantifiers/fmf/full_model_check.h" +#include "theory/quantifiers/fmf/model_builder.h" +#include "theory/quantifiers/quantifiers_inference_manager.h" #include "theory/quantifiers/quantifiers_modules.h" #include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/quantifiers_state.h" +#include "theory/quantifiers/quant_module.h" +#include "theory/quantifiers/skolemize.h" +#include "theory/quantifiers/sygus/term_database_sygus.h" +#include "theory/quantifiers/term_util.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_enumeration.h" #include "theory/theory_engine.h" #include "theory/uf/equality_engine.h" diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index f464b24d4..d08e32f6e 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -20,23 +20,11 @@ #include <map> #include <unordered_map> +#include "context/cdhashmap.h" #include "context/cdhashset.h" #include "context/cdlist.h" -#include "expr/attribute.h" -#include "theory/quantifiers/ematching/trigger_trie.h" -#include "theory/quantifiers/equality_query.h" -#include "theory/quantifiers/first_order_model.h" -#include "theory/quantifiers/fmf/model_builder.h" -#include "theory/quantifiers/instantiate.h" -#include "theory/quantifiers/quant_module.h" #include "theory/quantifiers/quant_util.h" -#include "theory/quantifiers/quantifiers_inference_manager.h" -#include "theory/quantifiers/quantifiers_state.h" -#include "theory/quantifiers/skolemize.h" -#include "theory/quantifiers/sygus/term_database_sygus.h" -#include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/term_enumeration.h" -#include "theory/quantifiers/term_util.h" +#include "theory/quantifiers/quantifiers_registry.h" #include "util/statistics_registry.h" namespace CVC4 { @@ -46,9 +34,24 @@ class TheoryEngine; namespace theory { class DecisionManager; +class QuantifiersModule; +class RepSetIterator; +namespace inst { +class TriggerTrie; +} namespace quantifiers { +class EqualityQueryQuantifiersEngine; +class FirstOrderModel; +class Instantiate; +class QModelBuilder; +class QuantifiersInferenceManager; class QuantifiersModules; +class QuantifiersState; +class Skolemize; +class TermDb; +class TermDbSygus; +class TermEnumeration; } // TODO: organize this more/review this, github issue #1163 diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index be26510c6..fc98e6198 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -17,6 +17,7 @@ #include "theory/rewriter.h" +#include "expr/term_conversion_proof_generator.h" #include "options/theory_options.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index 572662483..f5c1348ad 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -19,20 +19,21 @@ #pragma once #include "expr/node.h" -#include "expr/term_conversion_proof_generator.h" #include "theory/theory_rewriter.h" -#include "theory/trust_node.h" -#include "util/unsafe_interrupt_exception.h" namespace CVC4 { + +class TConvProofGenerator; +class ProofNodeManager; + namespace theory { +class TrustNode; + namespace builtin { class BuiltinProofRuleChecker; } -class RewriterInitializer; - /** * The rewrite environment holds everything that the individual rewrites have * access to. diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 2a409a304..0a8039ed1 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -24,6 +24,7 @@ #include "options/sep_options.h" #include "options/smt_options.h" #include "smt/logic_exception.h" +#include "theory/decision_manager.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index b2cd6bf45..198273993 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -23,9 +23,11 @@ #include "context/cdhashset.h" #include "context/cdlist.h" #include "context/cdqueue.h" +#include "theory/decision_strategy.h" #include "theory/inference_manager_buffered.h" #include "theory/sep/theory_sep_rewriter.h" #include "theory/theory.h" +#include "theory/theory_state.h" #include "theory/uf/equality_engine.h" #include "util/statistics_registry.h" diff --git a/src/theory/sets/rels_utils.h b/src/theory/sets/rels_utils.h index 13ee672db..0d832b646 100644 --- a/src/theory/sets/rels_utils.h +++ b/src/theory/sets/rels_utils.h @@ -18,6 +18,7 @@ #define SRC_THEORY_SETS_RELS_UTILS_H_ #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "expr/node.h" namespace CVC4 { diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index e06a8cb52..5c6300059 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -20,6 +20,7 @@ #include "theory/sets/theory_sets_private.h" #include "theory/sets/theory_sets_rewriter.h" #include "theory/theory_model.h" +#include "theory/trust_substitutions.h" using namespace CVC4::kind; diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index 1e4473d6f..eb802af4a 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -17,6 +17,7 @@ #include "theory/sets/theory_sets_rewriter.h" #include "expr/attribute.h" +#include "expr/dtype_cons.h" #include "options/sets_options.h" #include "theory/sets/normal_form.h" #include "theory/sets/rels_utils.h" diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index 5446f67be..642a4d4ae 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -16,6 +16,7 @@ #include "theory/strings/core_solver.h" +#include "base/configuration.h" #include "options/strings_options.h" #include "theory/strings/sequences_rewriter.h" #include "theory/strings/strings_entail.h" diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp index 770991286..620cca185 100644 --- a/src/theory/strings/regexp_elim.cpp +++ b/src/theory/strings/regexp_elim.cpp @@ -15,6 +15,7 @@ #include "theory/strings/regexp_elim.h" +#include "expr/proof_node_manager.h" #include "options/strings_options.h" #include "theory/rewriter.h" #include "theory/strings/regexp_entail.h" diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 0157a47f0..bd95933a5 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -19,6 +19,7 @@ #include "options/strings_options.h" #include "options/theory_options.h" #include "smt/logic_exception.h" +#include "theory/decision_manager.h" #include "theory/ext_theory.h" #include "theory/rewriter.h" #include "theory/strings/theory_strings_utils.h" diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp index 82463367e..a725f4d88 100644 --- a/src/theory/term_registration_visitor.cpp +++ b/src/theory/term_registration_visitor.cpp @@ -15,6 +15,7 @@ #include "theory/term_registration_visitor.h" +#include "base/configuration.h" #include "options/quantifiers_options.h" #include "theory/theory_engine.h" diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index fef3fdc67..19fc91312 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -26,10 +26,16 @@ #include "options/smt_options.h" #include "options/theory_options.h" #include "smt/smt_statistics_registry.h" +#include "theory/ee_setup_info.h" #include "theory/ext_theory.h" +#include "theory/output_channel.h" #include "theory/quantifiers_engine.h" #include "theory/substitutions.h" +#include "theory/theory_inference_manager.h" +#include "theory/theory_model.h" #include "theory/theory_rewriter.h" +#include "theory/theory_state.h" +#include "theory/trust_substitutions.h" using namespace std; diff --git a/src/theory/theory.h b/src/theory/theory.h index fa26ab65e..5f4698e56 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -20,49 +20,39 @@ #define CVC4__THEORY__THEORY_H #include <iosfwd> -#include <map> #include <set> #include <string> #include <unordered_set> -#include "context/cdhashset.h" #include "context/cdlist.h" #include "context/cdo.h" #include "context/context.h" #include "expr/node.h" -#include "options/options.h" #include "options/theory_options.h" -#include "smt/logic_request.h" #include "theory/assertion.h" #include "theory/care_graph.h" -#include "theory/decision_manager.h" -#include "theory/ee_setup_info.h" #include "theory/logic_info.h" -#include "theory/output_channel.h" #include "theory/theory_id.h" -#include "theory/theory_inference_manager.h" -#include "theory/theory_rewriter.h" -#include "theory/theory_state.h" #include "theory/trust_node.h" -#include "theory/trust_substitutions.h" #include "theory/valuation.h" #include "util/statistics_registry.h" namespace CVC4 { -class TheoryEngine; class ProofNodeManager; +class TheoryEngine; namespace theory { +class DecisionManager; +struct EeSetupInfo; +class OutputChannel; class QuantifiersEngine; +class TheoryInferenceManager; class TheoryModel; -class SubstitutionMap; class TheoryRewriter; - -namespace rrinst { - class CandidateGenerator; -}/* CVC4::theory::rrinst namespace */ +class TheoryState; +class TrustSubstitutionMap; namespace eq { class EqualityEngine; diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index 53a812653..810f31ce5 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -15,8 +15,11 @@ #include "theory/theory_inference_manager.h" #include "smt/smt_statistics_registry.h" +#include "theory/output_channel.h" #include "theory/theory.h" +#include "theory/theory_state.h" #include "theory/uf/equality_engine.h" +#include "theory/uf/proof_equality_engine.h" using namespace CVC4::kind; diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h index d3a317cbc..61b105dac 100644 --- a/src/theory/theory_inference_manager.h +++ b/src/theory/theory_inference_manager.h @@ -23,9 +23,8 @@ #include "expr/node.h" #include "theory/inference_id.h" #include "theory/output_channel.h" -#include "theory/theory_state.h" #include "theory/trust_node.h" -#include "theory/uf/proof_equality_engine.h" +#include "util/statistics_registry.h" namespace CVC4 { @@ -34,8 +33,10 @@ class ProofNodeManager; namespace theory { class Theory; +class TheoryState; namespace eq { class EqualityEngine; +class ProofEqEngine; } /** diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 9604dc72b..89f53acb8 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -14,6 +14,7 @@ #include "theory/theory_model_builder.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "options/theory_options.h" diff --git a/src/theory/trust_node.h b/src/theory/trust_node.h index a0586bd0c..d4d2a78a5 100644 --- a/src/theory/trust_node.h +++ b/src/theory/trust_node.h @@ -18,11 +18,11 @@ #define CVC4__THEORY__TRUST_NODE_H #include "expr/node.h" -#include "expr/proof_node.h" namespace CVC4 { class ProofGenerator; +class ProofNode; namespace theory { diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp index 7ab43091a..58d5f4924 100644 --- a/src/theory/uf/eq_proof.cpp +++ b/src/theory/uf/eq_proof.cpp @@ -15,6 +15,7 @@ #include "theory/uf/eq_proof.h" +#include "base/configuration.h" #include "expr/proof.h" #include "options/uf_options.h" diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 497e394c7..49e19c15f 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -25,6 +25,7 @@ #include "expr/node_trie.h" #include "theory/theory.h" #include "theory/theory_eq_notify.h" +#include "theory/theory_state.h" #include "theory/uf/equality_engine.h" #include "theory/uf/proof_checker.h" #include "theory/uf/proof_equality_engine.h" diff --git a/src/util/bitvector.cpp b/src/util/bitvector.cpp index 9233bde53..5d017cb0f 100644 --- a/src/util/bitvector.cpp +++ b/src/util/bitvector.cpp @@ -18,6 +18,8 @@ #include "util/bitvector.h" +#include "base/exception.h" + namespace CVC4 { unsigned BitVector::getSize() const { return d_size; } diff --git a/src/util/bitvector.h b/src/util/bitvector.h index 997293639..b1a27929a 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -21,7 +21,6 @@ #include <iosfwd> -#include "base/exception.h" #include "util/integer.h" namespace CVC4 { diff --git a/src/util/cardinality.cpp b/src/util/cardinality.cpp index 585512138..f78b076de 100644 --- a/src/util/cardinality.cpp +++ b/src/util/cardinality.cpp @@ -16,7 +16,10 @@ #include "util/cardinality.h" +#include <ostream> + #include "base/check.h" +#include "base/exception.h" namespace CVC4 { diff --git a/src/util/cardinality.h b/src/util/cardinality.h index 8ad3edbe2..9218095a8 100644 --- a/src/util/cardinality.h +++ b/src/util/cardinality.h @@ -20,10 +20,8 @@ #ifndef CVC4__CARDINALITY_H #define CVC4__CARDINALITY_H -#include <iostream> -#include <utility> +#include <iosfwd> -#include "base/exception.h" #include "util/integer.h" namespace CVC4 { diff --git a/src/util/divisible.h b/src/util/divisible.h index 36bb37db0..b2682b055 100644 --- a/src/util/divisible.h +++ b/src/util/divisible.h @@ -21,8 +21,9 @@ #define CVC4__DIVISIBLE_H #include <iosfwd> +#include <ostream> +#include <stddef.h> -#include "base/exception.h" #include "util/integer.h" namespace CVC4 { diff --git a/src/util/ostream_util.cpp b/src/util/ostream_util.cpp index c97238892..ce8b50bc8 100644 --- a/src/util/ostream_util.cpp +++ b/src/util/ostream_util.cpp @@ -15,6 +15,8 @@ **/ #include "util/ostream_util.h" +#include <ostream> + namespace CVC4 { StreamFormatScope::StreamFormatScope(std::ostream& out) diff --git a/src/util/ostream_util.h b/src/util/ostream_util.h index b27c22819..6e2a291a3 100644 --- a/src/util/ostream_util.h +++ b/src/util/ostream_util.h @@ -20,7 +20,7 @@ #define CVC4__UTIL__OSTREAM_UTIL_H #include <ios> -#include <ostream> +#include <iosfwd> namespace CVC4 { diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp index 17dac50b3..0534be1b7 100644 --- a/src/util/resource_manager.cpp +++ b/src/util/resource_manager.cpp @@ -16,8 +16,13 @@ **/ #include "util/resource_manager.h" +#include <algorithm> +#include <ostream> + #include "base/check.h" +#include "base/listener.h" #include "base/output.h" +#include "options/options.h" #include "options/smt_options.h" #include "util/statistics_registry.h" diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h index 3be99021b..a4a9b7f4e 100644 --- a/src/util/resource_manager.h +++ b/src/util/resource_manager.h @@ -21,18 +21,15 @@ #ifndef CVC4__RESOURCE_MANAGER_H #define CVC4__RESOURCE_MANAGER_H -#include <sys/time.h> - +#include <stdint.h> #include <chrono> #include <memory> - -#include "base/exception.h" -#include "base/listener.h" -#include "options/options.h" -#include "util/unsafe_interrupt_exception.h" +#include <vector> namespace CVC4 { +class Listener; +class Options; class StatisticsRegistry; /** diff --git a/src/util/statistics.cpp b/src/util/statistics.cpp index 73e6afb96..781c73aec 100644 --- a/src/util/statistics.cpp +++ b/src/util/statistics.cpp @@ -17,8 +17,6 @@ #include "util/statistics.h" -#include <typeinfo> - #include "util/safe_print.h" #include "util/statistics_registry.h" // for details about class Stat diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index d2f7244f9..efa1de1c0 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -43,7 +43,6 @@ #include <vector> #include "base/exception.h" -#include "lib/clock_gettime.h" #include "util/safe_print.h" #include "util/statistics.h" diff --git a/src/util/tuple.h b/src/util/tuple.h index 240e41792..109d4640b 100644 --- a/src/util/tuple.h +++ b/src/util/tuple.h @@ -20,7 +20,6 @@ #define CVC4__TUPLE_H #include <iostream> -#include <string> #include <vector> #include <utility> diff --git a/src/util/utility.cpp b/src/util/utility.cpp index 7a50eb7fd..2b848d924 100644 --- a/src/util/utility.cpp +++ b/src/util/utility.cpp @@ -19,7 +19,6 @@ #include <unistd.h> #include <cstdlib> -#include <iostream> #include "base/check.h" diff --git a/src/util/utility.h b/src/util/utility.h index 549b98d66..06155788f 100644 --- a/src/util/utility.h +++ b/src/util/utility.h @@ -21,10 +21,8 @@ #include <algorithm> #include <fstream> -#include <functional> #include <memory> #include <string> -#include <utility> namespace CVC4 { diff --git a/test/unit/expr/node_black.cpp b/test/unit/expr/node_black.cpp index ddbdcde6b..f50d529d5 100644 --- a/test/unit/expr/node_black.cpp +++ b/test/unit/expr/node_black.cpp @@ -21,6 +21,7 @@ #include "api/cvc4cpp.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "expr/expr_manager.h" #include "expr/node.h" #include "expr/node_builder.h" diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h index 7aecdd3b2..cd77f355d 100644 --- a/test/unit/test_smt.h +++ b/test/unit/test_smt.h @@ -15,12 +15,16 @@ #ifndef CVC4__TEST__UNIT__TEST_SMT_H #define CVC4__TEST__UNIT__TEST_SMT_H +#include "expr/dtype_cons.h" #include "expr/node.h" #include "expr/node_manager.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "test.h" +#include "theory/output_channel.h" +#include "theory/rewriter.h" #include "theory/theory.h" +#include "theory/theory_state.h" #include "theory/valuation.h" #include "util/resource_manager.h" #include "util/unsafe_interrupt_exception.h" diff --git a/test/unit/theory/theory_arith_white.cpp b/test/unit/theory/theory_arith_white.cpp index 8bdf82622..5e5b52d3e 100644 --- a/test/unit/theory/theory_arith_white.cpp +++ b/test/unit/theory/theory_arith_white.cpp @@ -12,6 +12,7 @@ ** \brief Whitebox tests for theory Arithmetic. **/ +#include <list> #include <vector> #include "context/context.h" diff --git a/test/unit/util/datatype_black.cpp b/test/unit/util/datatype_black.cpp index 0ef095fd9..0120dda76 100644 --- a/test/unit/util/datatype_black.cpp +++ b/test/unit/util/datatype_black.cpp @@ -18,6 +18,7 @@ #include "api/cvc4cpp.h" #include "expr/dtype.h" +#include "expr/dtype_cons.h" #include "expr/expr.h" #include "expr/type_node.h" #include "test_expr.h" |