diff options
Diffstat (limited to 'src/theory')
24 files changed, 41 insertions, 1 deletions
diff --git a/src/theory/arith/delta_rational.cpp b/src/theory/arith/delta_rational.cpp index f5a9a2a75..8107136c3 100644 --- a/src/theory/arith/delta_rational.cpp +++ b/src/theory/arith/delta_rational.cpp @@ -18,6 +18,8 @@ #include "theory/arith/delta_rational.h" +#include <sstream> + using namespace std; namespace CVC4 { diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp index 6487b48ec..5e34aebc7 100644 --- a/src/theory/arith/nl/iand_solver.cpp +++ b/src/theory/arith/nl/iand_solver.cpp @@ -22,6 +22,7 @@ #include "theory/arith/arith_utilities.h" #include "theory/arith/inference_manager.h" #include "theory/arith/nl/nl_model.h" +#include "theory/rewriter.h" #include "util/iand.h" using namespace CVC4::kind; diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp index bc4e0c8ae..01b834482 100644 --- a/src/theory/booleans/proof_circuit_propagator.cpp +++ b/src/theory/booleans/proof_circuit_propagator.cpp @@ -16,6 +16,8 @@ #include "theory/booleans/proof_circuit_propagator.h" +#include <sstream> + #include "expr/proof_node_manager.h" namespace CVC4 { diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h index d71fae8d0..a1763d081 100644 --- a/src/theory/bv/bitblast/bitblaster.h +++ b/src/theory/bv/bitblast/bitblaster.h @@ -31,6 +31,7 @@ #include "prop/sat_solver_types.h" #include "smt/smt_engine_scope.h" #include "theory/bv/bitblast/bitblast_strategies_template.h" +#include "theory/theory.h" #include "theory/valuation.h" #include "util/resource_manager.h" diff --git a/src/theory/bv/bv_solver_bitblast.h b/src/theory/bv/bv_solver_bitblast.h index 4eec45e4b..94f74a638 100644 --- a/src/theory/bv/bv_solver_bitblast.h +++ b/src/theory/bv/bv_solver_bitblast.h @@ -21,6 +21,7 @@ #include <unordered_map> +#include "context/cdqueue.h" #include "prop/cnf_stream.h" #include "prop/sat_solver.h" #include "theory/bv/bitblast/simple_bitblaster.h" diff --git a/src/theory/datatypes/sygus_datatype_utils.cpp b/src/theory/datatypes/sygus_datatype_utils.cpp index 6169d3752..e11f773a3 100644 --- a/src/theory/datatypes/sygus_datatype_utils.cpp +++ b/src/theory/datatypes/sygus_datatype_utils.cpp @@ -16,6 +16,8 @@ #include "theory/datatypes/sygus_datatype_utils.h" +#include <sstream> + #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/node_algorithm.h" diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 9105cdfd6..97600f76f 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -16,6 +16,7 @@ #include "theory/datatypes/theory_datatypes.h" #include <map> +#include <sstream> #include "base/check.h" #include "expr/dtype.h" diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index fda694e3d..94f90bc46 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -14,6 +14,8 @@ #include "theory/inference_id.h" +#include <iostream> + namespace CVC4 { namespace theory { diff --git a/src/theory/lazy_tree_proof_generator.cpp b/src/theory/lazy_tree_proof_generator.cpp index 126ce60b9..b6155f19e 100644 --- a/src/theory/lazy_tree_proof_generator.cpp +++ b/src/theory/lazy_tree_proof_generator.cpp @@ -18,6 +18,7 @@ #include "expr/node.h" #include "expr/proof_generator.h" +#include "expr/proof_node.h" #include "expr/proof_node_manager.h" namespace CVC4 { diff --git a/src/theory/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp index f1307f142..842ef59bf 100644 --- a/src/theory/quantifiers/single_inv_partition.cpp +++ b/src/theory/quantifiers/single_inv_partition.cpp @@ -14,6 +14,8 @@ **/ #include "theory/quantifiers/single_inv_partition.h" +#include <sstream> + #include "expr/node_algorithm.h" #include "theory/quantifiers/term_util.h" #include "theory/rewriter.h" diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.h b/src/theory/quantifiers/sygus/cegis_core_connective.h index cdc43658d..69adc9a4b 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.h +++ b/src/theory/quantifiers/sygus/cegis_core_connective.h @@ -18,11 +18,12 @@ #define CVC4__THEORY__QUANTIFIERS__CEGIS_CORE_CONNECTIVE_H #include <unordered_set> + #include "expr/node.h" #include "expr/node_trie.h" - #include "theory/evaluator.h" #include "theory/quantifiers/sygus/cegis.h" +#include "util/result.h" namespace CVC4 { namespace theory { diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp index 67f02b558..e56312362 100644 --- a/src/theory/quantifiers/sygus/sygus_abduct.cpp +++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp @@ -15,6 +15,8 @@ #include "theory/quantifiers/sygus/sygus_abduct.h" +#include <sstream> + #include "expr/dtype.h" #include "expr/node_algorithm.h" #include "expr/sygus_datatype.h" diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp index 3edec96c7..9f8ac0e3c 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.cpp +++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp @@ -16,6 +16,8 @@ #include "theory/quantifiers/sygus/sygus_interpol.h" +#include <sstream> + #include "expr/dtype.h" #include "expr/node_algorithm.h" #include "options/smt_options.h" diff --git a/src/theory/quantifiers/sygus/sygus_utils.cpp b/src/theory/quantifiers/sygus/sygus_utils.cpp index ca87e1049..d793fb718 100644 --- a/src/theory/quantifiers/sygus/sygus_utils.cpp +++ b/src/theory/quantifiers/sygus/sygus_utils.cpp @@ -14,6 +14,8 @@ #include "theory/quantifiers/sygus/sygus_utils.h" +#include <sstream> + #include "expr/node_algorithm.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 275e9a27f..a5be5871f 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -26,6 +26,7 @@ #include "theory/quantifiers/quantifiers_inference_manager.h" #include "theory/quantifiers/quantifiers_state.h" #include "theory/quantifiers/term_util.h" +#include "theory/rewriter.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index a72054f6d..c835369b7 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -23,6 +23,7 @@ #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" #include "theory/quantifiers/lazy_trie.h" +#include "theory/rewriter.h" #include "util/bitvector.h" #include "util/random.h" #include "util/sampler.h" diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 24d2e00bd..21480e8ec 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -16,6 +16,8 @@ #include "theory/strings/regexp_operation.h" +#include <sstream> + #include "expr/node_algorithm.h" #include "options/strings_options.h" #include "theory/rewriter.h" diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp index b807fe1b3..4338d38c4 100644 --- a/src/theory/strings/theory_strings_utils.cpp +++ b/src/theory/strings/theory_strings_utils.cpp @@ -16,6 +16,8 @@ #include "theory/strings/theory_strings_utils.h" +#include <sstream> + #include "options/strings_options.h" #include "theory/rewriter.h" #include "theory/strings/arith_entail.h" diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index e49ca8b05..07b23525e 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -16,6 +16,8 @@ #include "theory/theory_engine.h" +#include <sstream> + #include "base/map_util.h" #include "decision/decision_engine.h" #include "expr/attribute.h" diff --git a/src/theory/theory_engine_proof_generator.cpp b/src/theory/theory_engine_proof_generator.cpp index 2ba0a49ff..1eb191fd7 100644 --- a/src/theory/theory_engine_proof_generator.cpp +++ b/src/theory/theory_engine_proof_generator.cpp @@ -14,6 +14,10 @@ #include "theory/theory_engine_proof_generator.h" +#include <sstream> + +#include "expr/proof_node.h" + using namespace CVC4::kind; namespace CVC4 { diff --git a/src/theory/theory_id.cpp b/src/theory/theory_id.cpp index e9111db8c..5859b5c99 100644 --- a/src/theory/theory_id.cpp +++ b/src/theory/theory_id.cpp @@ -17,6 +17,8 @@ #include "theory/theory_id.h" +#include <sstream> + #include "base/check.h" #include "lib/ffs.h" diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp index 94402e2d9..d2fc4cf9e 100644 --- a/src/theory/uf/cardinality_extension.cpp +++ b/src/theory/uf/cardinality_extension.cpp @@ -14,6 +14,8 @@ #include "theory/uf/cardinality_extension.h" +#include <sstream> + #include "options/smt_options.h" #include "options/uf_options.h" #include "theory/quantifiers/term_database.h" diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp index 58d5f4924..7a164c196 100644 --- a/src/theory/uf/eq_proof.cpp +++ b/src/theory/uf/eq_proof.cpp @@ -17,6 +17,7 @@ #include "base/configuration.h" #include "expr/proof.h" +#include "expr/proof_checker.h" #include "options/uf_options.h" namespace CVC4 { diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index db8b89d89..e6e809533 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -18,6 +18,7 @@ #include "theory/uf/theory_uf.h" #include <memory> +#include <sstream> #include "expr/node_algorithm.h" #include "expr/proof_node_manager.h" |