diff options
Diffstat (limited to 'src/expr')
42 files changed, 82 insertions, 28 deletions
diff --git a/src/expr/buffered_proof_generator.h b/src/expr/buffered_proof_generator.h index da80891a2..15ae6ea83 100644 --- a/src/expr/buffered_proof_generator.h +++ b/src/expr/buffered_proof_generator.h @@ -19,11 +19,11 @@ #include "context/cdhashmap.h" #include "expr/proof_generator.h" -#include "expr/proof_step_buffer.h" namespace CVC4 { class ProofNodeManager; +class ProofStep; /** * The proof generator for buffered steps. This class is a context-dependent diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp index f94f0063a..5451edc02 100644 --- a/src/expr/dtype.cpp +++ b/src/expr/dtype.cpp @@ -13,6 +13,8 @@ **/ #include "expr/dtype.h" +#include <sstream> + #include "expr/dtype_cons.h" #include "expr/node_algorithm.h" #include "expr/type_matcher.h" diff --git a/src/expr/kind_template.cpp b/src/expr/kind_template.cpp index 0bda68b7b..e82e614b3 100644 --- a/src/expr/kind_template.cpp +++ b/src/expr/kind_template.cpp @@ -15,6 +15,8 @@ ** \todo document this file **/ +#include <sstream> + #include "expr/kind.h" namespace CVC4 { diff --git a/src/expr/lazy_proof.cpp b/src/expr/lazy_proof.cpp index 8d8d2741f..9c6d0e290 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.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 83dc90e4d..7c39164fe 100644 --- a/src/expr/lazy_proof.h +++ b/src/expr/lazy_proof.h @@ -17,14 +17,11 @@ #ifndef CVC4__EXPR__LAZY_PROOF_H #define CVC4__EXPR__LAZY_PROOF_H -#include <unordered_map> -#include <vector> - #include "expr/proof.h" -#include "expr/proof_generator.h" namespace CVC4 { +class ProofGenerator; class ProofNodeManager; /** diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp index f80ab099c..0e5e8c376 100644 --- a/src/expr/lazy_proof_chain.cpp +++ b/src/expr/lazy_proof_chain.cpp @@ -16,6 +16,7 @@ #include "expr/proof.h" #include "expr/proof_ensure_closed.h" +#include "expr/proof_node.h" #include "expr/proof_node_algorithm.h" #include "expr/proof_node_manager.h" #include "options/proof_options.h" diff --git a/src/expr/lazy_proof_chain.h b/src/expr/lazy_proof_chain.h index 1604bf182..e1b0f3cd0 100644 --- a/src/expr/lazy_proof_chain.h +++ b/src/expr/lazy_proof_chain.h @@ -17,7 +17,6 @@ #ifndef CVC4__EXPR__LAZY_PROOF_CHAIN_H #define CVC4__EXPR__LAZY_PROOF_CHAIN_H -#include <unordered_map> #include <vector> #include "context/cdhashmap.h" diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 1aca73d2e..eee8d0136 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -15,8 +15,9 @@ **/ #include "expr/node.h" -#include <iostream> #include <cstring> +#include <iostream> +#include <sstream> #include "base/exception.h" #include "base/output.h" diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp index b512b5869..6596f6c5f 100644 --- a/src/expr/proof.cpp +++ b/src/expr/proof.cpp @@ -14,6 +14,8 @@ #include "expr/proof.h" +#include "expr/proof_checker.h" +#include "expr/proof_node.h" #include "expr/proof_node_manager.h" using namespace CVC4::kind; diff --git a/src/expr/proof.h b/src/expr/proof.h index 3a26f0975..abb0b9b37 100644 --- a/src/expr/proof.h +++ b/src/expr/proof.h @@ -17,17 +17,16 @@ #ifndef CVC4__EXPR__PROOF_H #define CVC4__EXPR__PROOF_H -#include <map> #include <vector> #include "context/cdhashmap.h" #include "expr/node.h" #include "expr/proof_generator.h" -#include "expr/proof_node.h" #include "expr/proof_step_buffer.h" namespace CVC4 { +class ProofNode; class ProofNodeManager; /** diff --git a/src/expr/proof_checker.cpp b/src/expr/proof_checker.cpp index dc87d1795..a5655c9db 100644 --- a/src/expr/proof_checker.cpp +++ b/src/expr/proof_checker.cpp @@ -14,6 +14,7 @@ #include "expr/proof_checker.h" +#include "expr/proof_node.h" #include "expr/skolem_manager.h" #include "options/proof_options.h" #include "smt/smt_statistics_registry.h" diff --git a/src/expr/proof_checker.h b/src/expr/proof_checker.h index ab9c24434..200a1839d 100644 --- a/src/expr/proof_checker.h +++ b/src/expr/proof_checker.h @@ -20,12 +20,13 @@ #include <map> #include "expr/node.h" -#include "expr/proof_node.h" +#include "expr/proof_rule.h" #include "util/statistics_registry.h" namespace CVC4 { class ProofChecker; +class ProofNode; /** A virtual base class for checking a proof rule */ class ProofRuleChecker diff --git a/src/expr/proof_ensure_closed.cpp b/src/expr/proof_ensure_closed.cpp index 6eebcd3ec..183ff0d5b 100644 --- a/src/expr/proof_ensure_closed.cpp +++ b/src/expr/proof_ensure_closed.cpp @@ -14,6 +14,10 @@ #include "expr/proof_ensure_closed.h" +#include <sstream> + +#include "expr/proof_generator.h" +#include "expr/proof_node.h" #include "expr/proof_node_algorithm.h" #include "options/proof_options.h" #include "options/smt_options.h" diff --git a/src/expr/proof_ensure_closed.h b/src/expr/proof_ensure_closed.h index 7b970a71a..c54a5dfd5 100644 --- a/src/expr/proof_ensure_closed.h +++ b/src/expr/proof_ensure_closed.h @@ -18,11 +18,12 @@ #define CVC4__EXPR__PROOF_ENSURE_CLOSED_H #include "expr/node.h" -#include "expr/proof_generator.h" -#include "expr/proof_node.h" namespace CVC4 { +class ProofGenerator; +class ProofNode; + /** * Debug check closed on Trace c. Context ctx is string for debugging. * This method throws an assertion failure if pg cannot provide a closed diff --git a/src/expr/proof_generator.cpp b/src/expr/proof_generator.cpp index d2206a570..31af09b7f 100644 --- a/src/expr/proof_generator.cpp +++ b/src/expr/proof_generator.cpp @@ -14,7 +14,10 @@ #include "expr/proof_generator.h" +#include <sstream> + #include "expr/proof.h" +#include "expr/proof_node.h" #include "expr/proof_node_algorithm.h" #include "options/smt_options.h" diff --git a/src/expr/proof_generator.h b/src/expr/proof_generator.h index 869f226b8..3b376d77c 100644 --- a/src/expr/proof_generator.h +++ b/src/expr/proof_generator.h @@ -18,11 +18,11 @@ #define CVC4__EXPR__PROOF_GENERATOR_H #include "expr/node.h" -#include "expr/proof_node.h" namespace CVC4 { class CDProof; +class ProofNode; /** An overwrite policy for CDProof */ enum class CDPOverwrite : uint32_t diff --git a/src/expr/proof_node_algorithm.cpp b/src/expr/proof_node_algorithm.cpp index 2af296813..751dcc39e 100644 --- a/src/expr/proof_node_algorithm.cpp +++ b/src/expr/proof_node_algorithm.cpp @@ -14,6 +14,8 @@ #include "expr/proof_node_algorithm.h" +#include "expr/proof_node.h" + namespace CVC4 { namespace expr { diff --git a/src/expr/proof_node_algorithm.h b/src/expr/proof_node_algorithm.h index 43d06ea91..af8de066d 100644 --- a/src/expr/proof_node_algorithm.h +++ b/src/expr/proof_node_algorithm.h @@ -20,9 +20,11 @@ #include <vector> #include "expr/node.h" -#include "expr/proof_node.h" namespace CVC4 { + +class ProofNode; + namespace expr { /** diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp index f5e15f6d6..91858f239 100644 --- a/src/expr/proof_node_manager.cpp +++ b/src/expr/proof_node_manager.cpp @@ -15,6 +15,8 @@ #include "expr/proof_node_manager.h" #include "expr/proof.h" +#include "expr/proof_checker.h" +#include "expr/proof_node.h" #include "expr/proof_node_algorithm.h" #include "options/proof_options.h" #include "theory/rewriter.h" diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h index 3ad56c92d..e7be50065 100644 --- a/src/expr/proof_node_manager.h +++ b/src/expr/proof_node_manager.h @@ -19,11 +19,14 @@ #include <vector> -#include "expr/proof_checker.h" -#include "expr/proof_node.h" +#include "expr/node.h" +#include "expr/proof_rule.h" namespace CVC4 { +class ProofChecker; +class ProofNode; + /** * A manager for proof node objects. This is a trusted interface for creating * and updating ProofNode objects. diff --git a/src/expr/proof_node_to_sexpr.cpp b/src/expr/proof_node_to_sexpr.cpp index fbfc3e3d4..6830326ba 100644 --- a/src/expr/proof_node_to_sexpr.cpp +++ b/src/expr/proof_node_to_sexpr.cpp @@ -15,7 +15,9 @@ #include "expr/proof_node_to_sexpr.h" #include <iostream> +#include <sstream> +#include "expr/proof_node.h" #include "options/proof_options.h" using namespace CVC4::kind; diff --git a/src/expr/proof_node_to_sexpr.h b/src/expr/proof_node_to_sexpr.h index 3e0d42a7d..e6c003d10 100644 --- a/src/expr/proof_node_to_sexpr.h +++ b/src/expr/proof_node_to_sexpr.h @@ -20,10 +20,12 @@ #include <map> #include "expr/node.h" -#include "expr/proof_node.h" +#include "expr/proof_rule.h" namespace CVC4 { +class ProofNode; + /** A class to convert ProofNode objects to s-expressions */ class ProofNodeToSExpr { diff --git a/src/expr/proof_node_updater.cpp b/src/expr/proof_node_updater.cpp index e0f096075..f421ff4f3 100644 --- a/src/expr/proof_node_updater.cpp +++ b/src/expr/proof_node_updater.cpp @@ -17,6 +17,7 @@ #include "expr/lazy_proof.h" #include "expr/proof_ensure_closed.h" #include "expr/proof_node_algorithm.h" +#include "expr/proof_node_manager.h" namespace CVC4 { diff --git a/src/expr/proof_node_updater.h b/src/expr/proof_node_updater.h index 9814c8166..2df668384 100644 --- a/src/expr/proof_node_updater.h +++ b/src/expr/proof_node_updater.h @@ -18,14 +18,17 @@ #define CVC4__EXPR__PROOF_NODE_UPDATER_H #include <map> -#include <unordered_set> +#include <memory> -#include "expr/proof.h" +#include "expr/node.h" #include "expr/proof_node.h" -#include "expr/proof_node_manager.h" namespace CVC4 { +class CDProof; +class ProofNode; +class ProofNodeManager; + /** * A virtual callback class for updating ProofNode. An example use case of this * class is to eliminate a proof rule by expansion. diff --git a/src/expr/proof_step_buffer.cpp b/src/expr/proof_step_buffer.cpp index bb02aeb20..4c99855df 100644 --- a/src/expr/proof_step_buffer.cpp +++ b/src/expr/proof_step_buffer.cpp @@ -14,6 +14,8 @@ #include "expr/proof_step_buffer.h" +#include "expr/proof_checker.h" + using namespace CVC4::kind; namespace CVC4 { diff --git a/src/expr/proof_step_buffer.h b/src/expr/proof_step_buffer.h index 4e463a7b3..1b09a8f96 100644 --- a/src/expr/proof_step_buffer.h +++ b/src/expr/proof_step_buffer.h @@ -20,11 +20,12 @@ #include <vector> #include "expr/node.h" -#include "expr/proof_checker.h" #include "expr/proof_rule.h" namespace CVC4 { +class ProofChecker; + /** * Information for constructing a step in a CDProof. Notice that the conclusion * of the proof step is intentionally not included in this data structure. diff --git a/src/expr/record.h b/src/expr/record.h index 4e1ff6772..1ab84c30c 100644 --- a/src/expr/record.h +++ b/src/expr/record.h @@ -19,7 +19,6 @@ #ifndef CVC4__RECORD_H #define CVC4__RECORD_H -#include <functional> #include <iostream> #include <string> #include <vector> diff --git a/src/expr/sequence.cpp b/src/expr/sequence.cpp index f65558184..68c4985bb 100644 --- a/src/expr/sequence.cpp +++ b/src/expr/sequence.cpp @@ -14,6 +14,7 @@ #include "expr/sequence.h" +#include <sstream> #include <vector> #include "expr/node.h" diff --git a/src/expr/subs.cpp b/src/expr/subs.cpp index 541db1ac5..3ca75050a 100644 --- a/src/expr/subs.cpp +++ b/src/expr/subs.cpp @@ -14,6 +14,8 @@ #include "expr/subs.h" +#include <sstream> + #include "theory/rewriter.h" namespace CVC4 { diff --git a/src/expr/sygus_datatype.cpp b/src/expr/sygus_datatype.cpp index 3401e55f7..e67a1befe 100644 --- a/src/expr/sygus_datatype.cpp +++ b/src/expr/sygus_datatype.cpp @@ -14,6 +14,8 @@ #include "expr/sygus_datatype.h" +#include <sstream> + using namespace CVC4::kind; namespace CVC4 { diff --git a/src/expr/symbol_manager.h b/src/expr/symbol_manager.h index fa5732854..73018d7ca 100644 --- a/src/expr/symbol_manager.h +++ b/src/expr/symbol_manager.h @@ -19,7 +19,6 @@ #include <map> #include <memory> -#include <set> #include <string> #include "api/cvc4cpp.h" diff --git a/src/expr/tconv_seq_proof_generator.cpp b/src/expr/tconv_seq_proof_generator.cpp index 8bd850488..105c811d4 100644 --- a/src/expr/tconv_seq_proof_generator.cpp +++ b/src/expr/tconv_seq_proof_generator.cpp @@ -14,6 +14,10 @@ #include "expr/tconv_seq_proof_generator.h" +#include <sstream> + +#include "expr/proof_node_manager.h" + namespace CVC4 { TConvSeqProofGenerator::TConvSeqProofGenerator( diff --git a/src/expr/tconv_seq_proof_generator.h b/src/expr/tconv_seq_proof_generator.h index 95499d6b8..9197028d6 100644 --- a/src/expr/tconv_seq_proof_generator.h +++ b/src/expr/tconv_seq_proof_generator.h @@ -20,11 +20,12 @@ #include "context/cdhashmap.h" #include "expr/node.h" #include "expr/proof_generator.h" -#include "expr/proof_node_manager.h" #include "theory/trust_node.h" namespace CVC4 { +class ProofNodeManager; + /** * The term conversion sequence proof generator. This is used for maintaining * a fixed sequence of proof generators that provide proofs for rewrites diff --git a/src/expr/term_canonize.cpp b/src/expr/term_canonize.cpp index e5ebd0209..91f7f3190 100644 --- a/src/expr/term_canonize.cpp +++ b/src/expr/term_canonize.cpp @@ -14,6 +14,8 @@ #include "expr/term_canonize.h" +#include <sstream> + // TODO #1216: move the code in this include #include "theory/quantifiers/term_util.h" diff --git a/src/expr/term_context_node.h b/src/expr/term_context_node.h index ff8187bbc..061cf1ed2 100644 --- a/src/expr/term_context_node.h +++ b/src/expr/term_context_node.h @@ -18,11 +18,11 @@ #define CVC4__EXPR__TERM_CONTEXT_NODE_H #include "expr/node.h" -#include "expr/term_context.h" namespace CVC4 { class TCtxStack; +class TermContext; /** * A (term-context) sensitive term. This is a wrapper around a Node that diff --git a/src/expr/term_context_stack.cpp b/src/expr/term_context_stack.cpp index 64cab7035..f35514fa6 100644 --- a/src/expr/term_context_stack.cpp +++ b/src/expr/term_context_stack.cpp @@ -14,6 +14,8 @@ #include "expr/term_context_stack.h" +#include "expr/term_context.h" + namespace CVC4 { TCtxStack::TCtxStack(const TermContext* tctx) : d_tctx(tctx) {} diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp index d37ccf914..a47214ae1 100644 --- a/src/expr/term_conversion_proof_generator.cpp +++ b/src/expr/term_conversion_proof_generator.cpp @@ -14,6 +14,9 @@ #include "expr/term_conversion_proof_generator.h" +#include "expr/proof_checker.h" +#include "expr/proof_node.h" +#include "expr/term_context.h" #include "expr/term_context_stack.h" using namespace CVC4::kind; diff --git a/src/expr/term_conversion_proof_generator.h b/src/expr/term_conversion_proof_generator.h index dcf8b3fa4..4d6a169cb 100644 --- a/src/expr/term_conversion_proof_generator.h +++ b/src/expr/term_conversion_proof_generator.h @@ -20,11 +20,12 @@ #include "context/cdhashmap.h" #include "expr/lazy_proof.h" #include "expr/proof_generator.h" -#include "expr/proof_node_manager.h" -#include "expr/term_context.h" namespace CVC4 { +class ProofNodeManager; +class TermContext; + /** A policy for how rewrite steps are applied in TConvProofGenerator */ enum class TConvPolicy : uint32_t { diff --git a/src/expr/type.cpp b/src/expr/type.cpp index dadbdc91d..cbc15e153 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -16,6 +16,7 @@ #include "expr/type.h" #include <iostream> +#include <sstream> #include <string> #include <vector> diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp index e7685dba8..f5a729b36 100644 --- a/src/expr/type_checker_template.cpp +++ b/src/expr/type_checker_template.cpp @@ -14,6 +14,8 @@ ** TypeChecker implementation. **/ +#include <sstream> + #include "expr/node_manager.h" #include "expr/node_manager_attributes.h" #include "expr/type_checker.h" diff --git a/src/expr/type_checker_util.h b/src/expr/type_checker_util.h index 312ffe53a..32c1254de 100644 --- a/src/expr/type_checker_util.h +++ b/src/expr/type_checker_util.h @@ -19,6 +19,8 @@ #include "cvc4_private.h" +#include <sstream> + #include "expr/kind.h" #include "expr/node.h" #include "expr/node_manager.h" diff --git a/src/expr/type_matcher.h b/src/expr/type_matcher.h index 47fc36eee..126175582 100644 --- a/src/expr/type_matcher.h +++ b/src/expr/type_matcher.h @@ -19,7 +19,6 @@ #include <vector> -#include "expr/node.h" #include "expr/type_node.h" namespace CVC4 { |