diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-05-22 00:51:09 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2021-05-24 16:30:25 -0700 |
commit | f2655522b3fafcc886676c75cbcf876a8a2f6016 (patch) | |
tree | 5136c16c9a7145fa25250d4ac8631c400239f74b | |
parent | 6dc34856170897d4843a881a59bbc3782a42519f (diff) |
fix tests
23 files changed, 37 insertions, 1 deletions
diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp index 52c15a08d..80732eab4 100644 --- a/src/expr/dtype.cpp +++ b/src/expr/dtype.cpp @@ -20,6 +20,7 @@ #include "expr/node_algorithm.h" #include "expr/skolem_manager.h" #include "expr/type_matcher.h" +#include "util/rational.h" using namespace cvc5::kind; diff --git a/src/theory/arith/nl/cad/proof_generator.cpp b/src/theory/arith/nl/cad/proof_generator.cpp index e11b2df40..a74913d99 100644 --- a/src/theory/arith/nl/cad/proof_generator.cpp +++ b/src/theory/arith/nl/cad/proof_generator.cpp @@ -19,7 +19,6 @@ #include "proof/lazy_tree_proof_generator.h" #include "theory/arith/nl/poly_conversion.h" -#include "theory/lazy_tree_proof_generator.h" #include "util/indexed_root_predicate.h" namespace cvc5 { diff --git a/test/unit/node/node_algorithm_black.cpp b/test/unit/node/node_algorithm_black.cpp index e96d3ec9e..df8fb9383 100644 --- a/test/unit/node/node_algorithm_black.cpp +++ b/test/unit/node/node_algorithm_black.cpp @@ -21,6 +21,7 @@ #include "expr/node_manager.h" #include "test_node.h" #include "theory/bv/theory_bv_utils.h" +#include "util/bitvector.h" #include "util/integer.h" #include "util/rational.h" diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp index 852f06dbc..94a2e5fb6 100644 --- a/test/unit/node/node_black.cpp +++ b/test/unit/node/node_black.cpp @@ -19,6 +19,7 @@ #include <vector> #include "api/cpp/cvc5.h" +#include "expr/array_store_all.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/node.h" @@ -29,6 +30,8 @@ #include "smt/smt_engine.h" #include "test_node.h" #include "theory/rewriter.h" +#include "util/bitvector.h" +#include "util/rational.h" namespace cvc5 { diff --git a/test/unit/node/node_white.cpp b/test/unit/node/node_white.cpp index bf0b8db57..eb6f77bdc 100644 --- a/test/unit/node/node_white.cpp +++ b/test/unit/node/node_white.cpp @@ -18,6 +18,7 @@ #include "base/check.h" #include "expr/node_builder.h" #include "test_node.h" +#include "util/rational.h" namespace cvc5 { diff --git a/test/unit/node/type_node_white.cpp b/test/unit/node/type_node_white.cpp index 4fb057fa9..d8db32a4b 100644 --- a/test/unit/node/type_node_white.cpp +++ b/test/unit/node/type_node_white.cpp @@ -21,6 +21,7 @@ #include "expr/type_node.h" #include "smt/smt_engine.h" #include "test_node.h" +#include "util/rational.h" namespace cvc5 { diff --git a/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp b/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp index 64b93b3db..223cef13b 100644 --- a/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp +++ b/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp @@ -17,6 +17,7 @@ #include "preprocessing/passes/foreign_theory_rewrite.h" #include "smt/smt_engine.h" #include "test_smt.h" +#include "util/rational.h" namespace cvc5 { diff --git a/test/unit/printer/smt2_printer_black.cpp b/test/unit/printer/smt2_printer_black.cpp index a80b27ace..6b778989a 100644 --- a/test/unit/printer/smt2_printer_black.cpp +++ b/test/unit/printer/smt2_printer_black.cpp @@ -21,6 +21,8 @@ #include "options/language.h" #include "smt/smt_engine.h" #include "test_smt.h" +#include "util/regexp.h" +#include "util/string.h" namespace cvc5 { diff --git a/test/unit/theory/sequences_rewriter_white.cpp b/test/unit/theory/sequences_rewriter_white.cpp index bb7f900be..c5a5924d4 100644 --- a/test/unit/theory/sequences_rewriter_white.cpp +++ b/test/unit/theory/sequences_rewriter_white.cpp @@ -26,6 +26,8 @@ #include "theory/strings/sequences_rewriter.h" #include "theory/strings/strings_entail.h" #include "theory/strings/strings_rewriter.h" +#include "util/rational.h" +#include "util/string.h" namespace cvc5 { diff --git a/test/unit/theory/strings_rewriter_white.cpp b/test/unit/theory/strings_rewriter_white.cpp index bc6f400c0..020fb6e8f 100644 --- a/test/unit/theory/strings_rewriter_white.cpp +++ b/test/unit/theory/strings_rewriter_white.cpp @@ -22,6 +22,7 @@ #include "test_smt.h" #include "theory/rewriter.h" #include "theory/strings/strings_rewriter.h" +#include "util/string.h" namespace cvc5 { diff --git a/test/unit/theory/theory_bags_normal_form_white.cpp b/test/unit/theory/theory_bags_normal_form_white.cpp index 88808c018..556a84d45 100644 --- a/test/unit/theory/theory_bags_normal_form_white.cpp +++ b/test/unit/theory/theory_bags_normal_form_white.cpp @@ -14,10 +14,14 @@ */ #include "expr/dtype.h" +#include "expr/emptybag.h" +#include "expr/emptyset.h" #include "test_smt.h" #include "theory/bags/bags_rewriter.h" #include "theory/bags/normal_form.h" #include "theory/strings/type_enumerator.h" +#include "util/rational.h" +#include "util/string.h" namespace cvc5 { diff --git a/test/unit/theory/theory_bags_rewriter_white.cpp b/test/unit/theory/theory_bags_rewriter_white.cpp index 6828e8cdf..f70ff0c5d 100644 --- a/test/unit/theory/theory_bags_rewriter_white.cpp +++ b/test/unit/theory/theory_bags_rewriter_white.cpp @@ -14,9 +14,12 @@ */ #include "expr/dtype.h" +#include "expr/emptybag.h" #include "test_smt.h" #include "theory/bags/bags_rewriter.h" #include "theory/strings/type_enumerator.h" +#include "util/rational.h" +#include "util/string.h" namespace cvc5 { diff --git a/test/unit/theory/theory_bags_type_rules_white.cpp b/test/unit/theory/theory_bags_type_rules_white.cpp index 4d8270ec6..8013d06ea 100644 --- a/test/unit/theory/theory_bags_type_rules_white.cpp +++ b/test/unit/theory/theory_bags_type_rules_white.cpp @@ -17,6 +17,7 @@ #include "test_smt.h" #include "theory/bags/theory_bags_type_rules.h" #include "theory/strings/type_enumerator.h" +#include "util/rational.h" namespace cvc5 { diff --git a/test/unit/theory/theory_black.cpp b/test/unit/theory/theory_black.cpp index db4a1e046..766d696a1 100644 --- a/test/unit/theory/theory_black.cpp +++ b/test/unit/theory/theory_black.cpp @@ -16,11 +16,14 @@ #include <sstream> #include <vector> +#include "expr/array_store_all.h" #include "expr/node.h" #include "expr/node_builder.h" #include "expr/node_value.h" #include "test_smt.h" #include "theory/rewriter.h" +#include "util/bitvector.h" +#include "util/rational.h" namespace cvc5 { diff --git a/test/unit/theory/theory_bv_int_blaster_white.cpp b/test/unit/theory/theory_bv_int_blaster_white.cpp index ff08a2024..1e19b14b4 100644 --- a/test/unit/theory/theory_bv_int_blaster_white.cpp +++ b/test/unit/theory/theory_bv_int_blaster_white.cpp @@ -20,6 +20,7 @@ #include "test_smt.h" #include "theory/bv/int_blaster.h" #include "util/bitvector.h" +#include "util/rational.h" namespace cvc5 { diff --git a/test/unit/theory/theory_bv_opt_white.cpp b/test/unit/theory/theory_bv_opt_white.cpp index 2617472a2..3422b2784 100644 --- a/test/unit/theory/theory_bv_opt_white.cpp +++ b/test/unit/theory/theory_bv_opt_white.cpp @@ -16,6 +16,7 @@ #include "smt/optimization_solver.h" #include "test_smt.h" +#include "util/bitvector.h" namespace cvc5 { diff --git a/test/unit/theory/theory_int_opt_white.cpp b/test/unit/theory/theory_int_opt_white.cpp index 9d5c5c03f..770927544 100644 --- a/test/unit/theory/theory_int_opt_white.cpp +++ b/test/unit/theory/theory_int_opt_white.cpp @@ -16,6 +16,7 @@ #include "smt/optimization_solver.h" #include "test_smt.h" +#include "util/rational.h" namespace cvc5 { diff --git a/test/unit/theory/theory_sets_type_rules_white.cpp b/test/unit/theory/theory_sets_type_rules_white.cpp index ccf26cbbd..81884732a 100644 --- a/test/unit/theory/theory_sets_type_rules_white.cpp +++ b/test/unit/theory/theory_sets_type_rules_white.cpp @@ -16,6 +16,8 @@ #include "expr/dtype.h" #include "test_api.h" #include "test_node.h" +#include "theory/sets/singleton_op.h" +#include "util/rational.h" namespace cvc5 { diff --git a/test/unit/theory/theory_strings_utils_white.cpp b/test/unit/theory/theory_strings_utils_white.cpp index 1860c3be8..4706be523 100644 --- a/test/unit/theory/theory_strings_utils_white.cpp +++ b/test/unit/theory/theory_strings_utils_white.cpp @@ -19,6 +19,7 @@ #include "expr/node.h" #include "test_node.h" #include "theory/strings/theory_strings_utils.h" +#include "util/string.h" namespace cvc5 { diff --git a/test/unit/theory/theory_strings_word_white.cpp b/test/unit/theory/theory_strings_word_white.cpp index 9119cf1af..941c422a1 100644 --- a/test/unit/theory/theory_strings_word_white.cpp +++ b/test/unit/theory/theory_strings_word_white.cpp @@ -20,6 +20,7 @@ #include "expr/node.h" #include "test_node.h" #include "theory/strings/word.h" +#include "util/string.h" namespace cvc5 { diff --git a/test/unit/theory/type_enumerator_white.cpp b/test/unit/theory/type_enumerator_white.cpp index baf3af40e..bb7ef871c 100644 --- a/test/unit/theory/type_enumerator_white.cpp +++ b/test/unit/theory/type_enumerator_white.cpp @@ -22,9 +22,12 @@ #include "expr/dtype.h" #include "expr/kind.h" #include "expr/type_node.h" +#include "expr/uninterpreted_constant.h" #include "options/language.h" #include "test_smt.h" #include "theory/type_enumerator.h" +#include "util/bitvector.h" +#include "util/rational.h" namespace cvc5 { diff --git a/test/unit/util/array_store_all_white.cpp b/test/unit/util/array_store_all_white.cpp index a33848610..1272926db 100644 --- a/test/unit/util/array_store_all_white.cpp +++ b/test/unit/util/array_store_all_white.cpp @@ -14,7 +14,9 @@ */ #include "expr/array_store_all.h" +#include "expr/uninterpreted_constant.h" #include "test_smt.h" +#include "util/rational.h" namespace cvc5 { namespace test { diff --git a/test/unit/util/datatype_black.cpp b/test/unit/util/datatype_black.cpp index a19ab31a1..760bb2f75 100644 --- a/test/unit/util/datatype_black.cpp +++ b/test/unit/util/datatype_black.cpp @@ -19,6 +19,7 @@ #include "expr/dtype_cons.h" #include "expr/type_node.h" #include "test_smt.h" +#include "util/rational.h" namespace cvc5 { namespace test { |