diff options
Diffstat (limited to 'test')
36 files changed, 126 insertions, 118 deletions
diff --git a/test/system/ouroborous.cpp b/test/system/ouroborous.cpp index 4fbabf5f1..fd06517a9 100644 --- a/test/system/ouroborous.cpp +++ b/test/system/ouroborous.cpp @@ -29,9 +29,9 @@ #include <string> #include "expr/expr.h" -#include "expr/command.h" #include "parser/parser.h" #include "parser/parser_builder.h" +#include "smt_util/command.h" using namespace CVC4; using namespace CVC4::parser; diff --git a/test/system/smt2_compliance.cpp b/test/system/smt2_compliance.cpp index f754adc0e..108e30b5c 100644 --- a/test/system/smt2_compliance.cpp +++ b/test/system/smt2_compliance.cpp @@ -14,16 +14,16 @@ ** A test of SMT-LIBv2 commands, checks for compliant output. **/ +#include <cassert> #include <iostream> #include <sstream> -#include <cassert> -#include "smt/options.h" -#include "parser/parser.h" #include "expr/expr_manager.h" -#include "expr/command.h" -#include "smt/smt_engine.h" +#include "options/smt_options.h" +#include "parser/parser.h" #include "parser/parser_builder.h" +#include "smt/smt_engine.h" +#include "smt_util/command.h" using namespace CVC4; using namespace CVC4::parser; diff --git a/test/system/statistics.cpp b/test/system/statistics.cpp index f955bd150..baa901540 100644 --- a/test/system/statistics.cpp +++ b/test/system/statistics.cpp @@ -19,8 +19,9 @@ #include <sstream> #include "expr/expr.h" +#include "expr/sexpr.h" +#include "expr/statistics.h" #include "smt/smt_engine.h" -#include "util/statistics.h" using namespace CVC4; using namespace std; @@ -53,7 +54,8 @@ int main() { cout << "stat1 " << (*i).first << " is " << stats.getStatistic((*i).first) << endl; cout << "stat2 " << (*i).first << " is " << (*i).second << endl; if(smt.getStatistic((*i).first) != (*i).second) { - cout << "SMT engine reports different value for statistic " << (*i).first << ": " << smt.getStatistic((*i).first) << endl; + cout << "SMT engine reports different value for statistic " + << (*i).first << ": " << smt.getStatistic((*i).first) << endl; exit(1); } different = different || stats.getStatistic((*i).first) != (*i).second; @@ -68,5 +70,3 @@ int main() { return r == Result::VALID ? 0 : 1; } - - diff --git a/test/unit/context/cdlist_black.h b/test/unit/context/cdlist_black.h index 5f473478c..5980972be 100644 --- a/test/unit/context/cdlist_black.h +++ b/test/unit/context/cdlist_black.h @@ -16,16 +16,14 @@ #include <cxxtest/TestSuite.h> -#include <vector> #include <iostream> - #include <limits.h> +#include <vector> -#include "memory.h" - -#include "util/exception.h" +#include "base/exception.h" #include "context/context.h" #include "context/cdlist.h" +#include "memory.h" using namespace std; using namespace CVC4::context; diff --git a/test/unit/context/cdmap_white.h b/test/unit/context/cdmap_white.h index 84b8242b4..11642c3e9 100644 --- a/test/unit/context/cdmap_white.h +++ b/test/unit/context/cdmap_white.h @@ -16,8 +16,8 @@ #include <cxxtest/TestSuite.h> +#include "base/cvc4_assert.h" #include "context/cdhashmap.h" -#include "util/cvc4_assert.h" using namespace std; using namespace CVC4; diff --git a/test/unit/context/cdo_black.h b/test/unit/context/cdo_black.h index fe04421b4..4ca01df85 100644 --- a/test/unit/context/cdo_black.h +++ b/test/unit/context/cdo_black.h @@ -16,12 +16,13 @@ #include <cxxtest/TestSuite.h> -#include <vector> #include <iostream> -#include "context/context.h" +#include <vector> + +#include "base/cvc4_assert.h" #include "context/cdlist.h" #include "context/cdo.h" -#include "util/cvc4_assert.h" +#include "context/context.h" using namespace std; using namespace CVC4; diff --git a/test/unit/context/context_black.h b/test/unit/context/context_black.h index f72cc05f4..d7148c990 100644 --- a/test/unit/context/context_black.h +++ b/test/unit/context/context_black.h @@ -16,12 +16,14 @@ #include <cxxtest/TestSuite.h> -#include <vector> #include <iostream> -#include "context/context.h" +#include <vector> + +#include "base/cvc4_assert.h" #include "context/cdlist.h" #include "context/cdo.h" -#include "util/cvc4_assert.h" +#include "context/context.h" + using namespace std; using namespace CVC4; diff --git a/test/unit/context/context_white.h b/test/unit/context/context_white.h index 7ad70f061..10f603abd 100644 --- a/test/unit/context/context_white.h +++ b/test/unit/context/context_white.h @@ -16,9 +16,9 @@ #include <cxxtest/TestSuite.h> +#include "base/cvc4_assert.h" #include "context/context.h" #include "context/cdo.h" -#include "util/cvc4_assert.h" using namespace std; using namespace CVC4; diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h index 00ebc8b8d..df7e263d2 100644 --- a/test/unit/expr/attribute_white.h +++ b/test/unit/expr/attribute_white.h @@ -18,18 +18,18 @@ #include <string> -#include "expr/node_value.h" +#include "base/cvc4_assert.h" +#include "expr/attribute.h" +#include "expr/node.h" #include "expr/node_builder.h" #include "expr/node_manager.h" -#include "expr/attribute.h" #include "expr/node_manager_attributes.h" -#include "expr/node.h" +#include "expr/node_value.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" #include "theory/theory.h" #include "theory/theory_engine.h" #include "theory/uf/theory_uf.h" -#include "util/cvc4_assert.h" -#include "smt/smt_engine.h" -#include "smt/smt_engine_scope.h" using namespace CVC4; using namespace CVC4::kind; diff --git a/test/unit/expr/expr_manager_public.h b/test/unit/expr/expr_manager_public.h index 727abe984..040bd7161 100644 --- a/test/unit/expr/expr_manager_public.h +++ b/test/unit/expr/expr_manager_public.h @@ -21,7 +21,7 @@ #include "expr/expr_manager.h" #include "expr/expr.h" -#include "util/exception.h" +#include "base/exception.h" using namespace CVC4; using namespace CVC4::kind; diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h index b70c51276..a83e53780 100644 --- a/test/unit/expr/expr_public.h +++ b/test/unit/expr/expr_public.h @@ -19,9 +19,10 @@ #include <sstream> #include <string> +#include "base/exception.h" #include "expr/expr_manager.h" #include "expr/expr.h" -#include "util/exception.h" +#include "smt/smt_options_handler.h" using namespace CVC4; using namespace CVC4::kind; @@ -31,6 +32,7 @@ class ExprPublic : public CxxTest::TestSuite { private: Options opts; + smt::SmtOptionsHandler* d_handler; ExprManager* d_em; @@ -53,10 +55,12 @@ public: void setUp() { try { + d_handler = new smt::SmtOptionsHandler(NULL); + char *argv[2]; argv[0] = strdup(""); argv[1] = strdup("--output-language=ast"); - opts.parseOptions(2, argv); + opts.parseOptions(2, argv, d_handler); free(argv[0]); free(argv[1]); @@ -98,6 +102,7 @@ public: delete c_bool_and; delete b_bool; delete a_bool; + delete d_handler; delete d_em; } catch(Exception e) { diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 7d6ee523a..3a24057b2 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -25,6 +25,7 @@ #include "expr/node_builder.h" #include "expr/node_manager.h" #include "expr/node.h" +#include "smt/smt_options_handler.h" using namespace CVC4; using namespace CVC4::kind; @@ -34,6 +35,7 @@ class NodeBlack : public CxxTest::TestSuite { private: Options opts; + smt::SmtOptionsHandler* d_handler; NodeManager* d_nodeManager; NodeManagerScope* d_scope; TypeNode* d_booleanType; @@ -42,10 +44,13 @@ private: public: void setUp() { +#warning "TODO: Discuss the effects of this change with Clark." + d_handler = new smt::SmtOptionsHandler(NULL); + char *argv[2]; argv[0] = strdup(""); argv[1] = strdup("--output-language=ast"); - opts.parseOptions(2, argv); + opts.parseOptions(2, argv, d_handler); free(argv[0]); free(argv[1]); @@ -59,6 +64,7 @@ public: delete d_booleanType; delete d_scope; delete d_nodeManager; + delete d_handler; } bool imp(bool a, bool b) const { diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index 9bac0d818..a7ebea2fe 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -20,12 +20,12 @@ #include <limits.h> #include <sstream> -#include "expr/node_builder.h" +#include "base/cvc4_assert.h" #include "expr/convenience_node_builders.h" -#include "expr/node_manager.h" -#include "expr/node.h" #include "expr/kind.h" -#include "util/cvc4_assert.h" +#include "expr/node.h" +#include "expr/node_builder.h" +#include "expr/node_manager.h" #include "util/rational.h" using namespace CVC4; diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h index b94e6a691..781829e36 100644 --- a/test/unit/expr/node_manager_black.h +++ b/test/unit/expr/node_manager_black.h @@ -21,9 +21,8 @@ #include "expr/node_manager.h" #include "expr/node_manager_attributes.h" - -#include "util/rational.h" #include "util/integer.h" +#include "util/rational.h" using namespace CVC4; using namespace CVC4::expr; diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h index aaa3256dd..fa44b837a 100644 --- a/test/unit/expr/node_manager_white.h +++ b/test/unit/expr/node_manager_white.h @@ -19,9 +19,8 @@ #include <string> #include "expr/node_manager.h" - -#include "util/rational.h" #include "util/integer.h" +#include "util/rational.h" using namespace CVC4; using namespace CVC4::expr; diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h index 8a68db269..594a981c8 100644 --- a/test/unit/expr/node_white.h +++ b/test/unit/expr/node_white.h @@ -18,11 +18,11 @@ #include <string> -#include "expr/node_value.h" +#include "base/cvc4_assert.h" +#include "expr/node.h" #include "expr/node_builder.h" #include "expr/node_manager.h" -#include "expr/node.h" -#include "util/cvc4_assert.h" +#include "expr/node_value.h" using namespace CVC4; using namespace CVC4::kind; diff --git a/test/unit/expr/symbol_table_black.h b/test/unit/expr/symbol_table_black.h index 2acd1ebae..2b26ad745 100644 --- a/test/unit/expr/symbol_table_black.h +++ b/test/unit/expr/symbol_table_black.h @@ -19,13 +19,13 @@ #include <sstream> #include <string> +#include "base/cvc4_assert.h" +#include "base/exception.h" #include "context/context.h" -#include "expr/symbol_table.h" -#include "expr/expr_manager.h" #include "expr/expr.h" +#include "expr/expr_manager.h" +#include "expr/symbol_table.h" #include "expr/type.h" -#include "util/cvc4_assert.h" -#include "util/exception.h" using namespace CVC4; using namespace CVC4::kind; diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h index b09246d95..6c3e73d2c 100644 --- a/test/unit/main/interactive_shell_black.h +++ b/test/unit/main/interactive_shell_black.h @@ -22,9 +22,9 @@ #include "expr/expr_manager.h" #include "main/interactive_shell.h" -#include "parser/parser_builder.h" -#include "util/language.h" +#include "options/language.h" #include "options/options.h" +#include "parser/parser_builder.h" using namespace CVC4; using namespace std; diff --git a/test/unit/memory.h b/test/unit/memory.h index 2809edee7..06c4a4a44 100644 --- a/test/unit/memory.h +++ b/test/unit/memory.h @@ -29,7 +29,7 @@ #include <sys/time.h> #include <sys/resource.h> -#include "util/cvc4_assert.h" +#include "base/cvc4_assert.h" namespace CVC4 { namespace test { diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index 61da34460..9b700eda6 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -19,15 +19,16 @@ #include <cxxtest/TestSuite.h> #include <sstream> +#include "base/output.h" #include "expr/expr.h" #include "expr/expr_manager.h" +#include "options/language.h" +#include "options/options.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "parser/smt2/smt2.h" -#include "expr/command.h" -#include "options/options.h" -#include "util/output.h" -#include "util/language.h" +#include "smt_util/command.h" + using namespace CVC4; using namespace CVC4::parser; diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h index c2c7cc18d..029c95ec9 100644 --- a/test/unit/parser/parser_builder_black.h +++ b/test/unit/parser/parser_builder_black.h @@ -15,18 +15,21 @@ **/ #include <cxxtest/TestSuite.h> + #include <ext/stdio_filebuf.h> -#include <fstream> -#include <iostream> #include <stdio.h> #include <string.h> #include <sys/stat.h> #include <unistd.h> -#include "expr/command.h" +#include <fstream> +#include <iostream> + +#include "options/language.h" #include "parser/parser.h" #include "parser/parser_builder.h" -#include "util/language.h" +#include "smt_util/command.h" + typedef __gnu_cxx::stdio_filebuf<char> filebuf_gnu; diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h index db49e2521..e705da409 100644 --- a/test/unit/prop/cnf_stream_white.h +++ b/test/unit/prop/cnf_stream_white.h @@ -18,25 +18,22 @@ /* #include <gmock/gmock.h> */ /* #include <gtest/gtest.h> */ -#include "util/cvc4_assert.h" - +#include "base/cvc4_assert.h" +#include "context/context.h" #include "expr/expr_manager.h" #include "expr/node_manager.h" -#include "context/context.h" #include "prop/cnf_stream.h" #include "prop/prop_engine.h" #include "prop/theory_proxy.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" - +#include "theory/arith/theory_arith.h" +#include "theory/booleans/theory_bool.h" +#include "theory/builtin/theory_builtin.h" #include "theory/theory.h" #include "theory/theory_engine.h" #include "theory/theory_registrar.h" -#include "theory/builtin/theory_builtin.h" -#include "theory/booleans/theory_bool.h" -#include "theory/arith/theory_arith.h" - using namespace CVC4; using namespace CVC4::context; using namespace CVC4::prop; diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h index efc7c5582..1d363ec9c 100644 --- a/test/unit/theory/logic_info_white.h +++ b/test/unit/theory/logic_info_white.h @@ -28,6 +28,8 @@ class LogicInfoWhite : public CxxTest::TestSuite { public: +#warning "This test is of questionable compatiblity with contrib/new-theory. Is the new theory id handled correctly by the Logic info." + void testSmtlibLogics() { LogicInfo info("QF_SAT"); TS_ASSERT( info.isLocked() ); @@ -1300,4 +1302,3 @@ public: } };/* class LogicInfoWhite */ - diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index 58bbe7a2b..d8615eda7 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -15,23 +15,21 @@ ** \todo document this file **/ - #include <cxxtest/TestSuite.h> -#include "theory/theory.h" -#include "theory/theory_engine.h" -#include "theory/arith/theory_arith.h" -#include "theory/quantifiers_engine.h" +#include <vector> + +#include "context/context.h" #include "expr/node.h" #include "expr/node_manager.h" -#include "context/context.h" -#include "util/rational.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" - +#include "theory/arith/theory_arith.h" +#include "theory/quantifiers_engine.h" +#include "theory/theory.h" +#include "theory/theory_engine.h" #include "theory/theory_test_utils.h" - -#include <vector> +#include "util/rational.h" using namespace CVC4; using namespace CVC4::theory; @@ -103,7 +101,7 @@ public: d_em = new ExprManager(); d_nm = NodeManager::fromExprManager(d_em); d_smt = new SmtEngine(d_em); - d_smt->setOption("incremental", false); + d_smt->setOption("incremental", CVC4::SExpr(false)); d_ctxt = d_smt->d_context; d_uctxt = d_smt->d_userContext; d_scope = new SmtScope(d_smt); diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index 7440de350..d1883da9f 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -20,24 +20,24 @@ #include <cxxtest/TestSuite.h> +#include <deque> #include <iostream> #include <string> -#include <deque> -#include "theory/theory.h" -#include "theory/theory_engine.h" -#include "theory/valuation.h" -#include "theory/rewriter.h" +#include "base/cvc4_assert.h" +#include "context/context.h" +#include "expr/kind.h" #include "expr/node.h" #include "expr/node_manager.h" -#include "expr/kind.h" -#include "context/context.h" +#include "options/options.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" -#include "util/rational.h" +#include "theory/rewriter.h" +#include "theory/theory.h" +#include "theory/theory_engine.h" +#include "theory/valuation.h" #include "util/integer.h" -#include "options/options.h" -#include "util/cvc4_assert.h" +#include "util/rational.h" using namespace CVC4; using namespace CVC4::theory; diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h index d9963f78c..993021c5a 100644 --- a/test/unit/theory/type_enumerator_white.h +++ b/test/unit/theory/type_enumerator_white.h @@ -17,13 +17,13 @@ #include <cxxtest/TestSuite.h> -#include "expr/node_manager.h" +#include "expr/array_store_all.h" #include "expr/expr_manager.h" -#include "expr/type_node.h" #include "expr/kind.h" +#include "expr/node_manager.h" +#include "expr/type_node.h" +#include "options/language.h" #include "theory/type_enumerator.h" -#include "util/language.h" -#include "util/array_store_all.h" using namespace CVC4; using namespace CVC4::theory; diff --git a/test/unit/util/array_store_all_black.h b/test/unit/util/array_store_all_black.h index 433dd7601..6a75bc7fa 100644 --- a/test/unit/util/array_store_all_black.h +++ b/test/unit/util/array_store_all_black.h @@ -16,7 +16,7 @@ #include <cxxtest/TestSuite.h> -#include "util/array_store_all.h" +#include "expr/array_store_all.h" #include "expr/expr_manager.h" #include "expr/expr_manager_scope.h" #include "expr/type.h" diff --git a/test/unit/util/assert_white.h b/test/unit/util/assert_white.h index 38dfe87e6..bbc4d02b3 100644 --- a/test/unit/util/assert_white.h +++ b/test/unit/util/assert_white.h @@ -19,7 +19,7 @@ #include <string> #include <cstring> -#include "util/cvc4_assert.h" +#include "base/cvc4_assert.h" using namespace CVC4; using namespace std; diff --git a/test/unit/util/boolean_simplification_black.h b/test/unit/util/boolean_simplification_black.h index db02ce207..ac343ede8 100644 --- a/test/unit/util/boolean_simplification_black.h +++ b/test/unit/util/boolean_simplification_black.h @@ -14,15 +14,15 @@ ** Black box testing of CVC4::BooleanSimplification. **/ -#include "util/language.h" -#include "expr/node.h" -#include "expr/kind.h" -#include "expr/node_manager.h" -#include "util/boolean_simplification.h" - #include <algorithm> -#include <vector> #include <set> +#include <vector> + +#include "expr/kind.h" +#include "expr/node.h" +#include "expr/node_manager.h" +#include "options/language.h" +#include "smt_util/boolean_simplification.h" using namespace CVC4; using namespace std; @@ -214,4 +214,3 @@ public: } };/* class BooleanSimplificationBlack */ - diff --git a/test/unit/util/cardinality_public.h b/test/unit/util/cardinality_public.h index 732bb0dbb..2fcee66b6 100644 --- a/test/unit/util/cardinality_public.h +++ b/test/unit/util/cardinality_public.h @@ -14,11 +14,11 @@ ** Public-box testing of CVC4::Cardinality. **/ -#include "util/cardinality.h" -#include "util/integer.h" - -#include <string> #include <sstream> +#include <string> + +#include "util/integer.h" +#include "util/cardinality.h" using namespace CVC4; using namespace std; diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h index ff36336ca..91a53ddc3 100644 --- a/test/unit/util/datatype_black.h +++ b/test/unit/util/datatype_black.h @@ -17,8 +17,7 @@ #include <cxxtest/TestSuite.h> #include <sstream> -#include "util/datatype.h" - +#include "expr/datatype.h" #include "expr/expr.h" #include "expr/expr_manager.h" #include "expr/expr_manager_scope.h" diff --git a/test/unit/util/exception_black.h b/test/unit/util/exception_black.h index d2ae7d3e5..c2c7f83c0 100644 --- a/test/unit/util/exception_black.h +++ b/test/unit/util/exception_black.h @@ -19,7 +19,7 @@ #include <iostream> #include <sstream> -#include "util/exception.h" +#include "base/exception.h" using namespace CVC4; using namespace std; diff --git a/test/unit/util/integer_black.h b/test/unit/util/integer_black.h index 36de17cba..510afe7b7 100644 --- a/test/unit/util/integer_black.h +++ b/test/unit/util/integer_black.h @@ -15,8 +15,9 @@ **/ #include <cxxtest/TestSuite.h> -#include <sstream> + #include <limits> +#include <sstream> #include "util/integer.h" diff --git a/test/unit/util/output_black.h b/test/unit/util/output_black.h index 0b151ef3f..87423f026 100644 --- a/test/unit/util/output_black.h +++ b/test/unit/util/output_black.h @@ -19,7 +19,7 @@ #include <iostream> #include <sstream> -#include "util/output.h" +#include "base/output.h" using namespace CVC4; using namespace std; diff --git a/test/unit/util/stats_black.h b/test/unit/util/stats_black.h index 249f9a5b1..c0e1ea7fd 100644 --- a/test/unit/util/stats_black.h +++ b/test/unit/util/stats_black.h @@ -19,7 +19,7 @@ #include <string> #include <ctime> -#include "util/statistics_registry.h" +#include "expr/statistics_registry.h" using namespace CVC4; using namespace std; diff --git a/test/unit/util/subrange_bound_white.h b/test/unit/util/subrange_bound_white.h index 71947b297..3b785ae0d 100644 --- a/test/unit/util/subrange_bound_white.h +++ b/test/unit/util/subrange_bound_white.h @@ -14,11 +14,11 @@ ** White-box testing of CVC4::SubrangeBound. **/ -#include "util/subrange_bound.h" -#include "util/integer.h" - -#include <string> #include <sstream> +#include <string> + +#include "util/integer.h" +#include "util/subrange_bound.h" using namespace CVC4; using namespace std; @@ -72,4 +72,3 @@ public: } };/* class SubrangeBoundWhite */ - |