diff options
Diffstat (limited to 'test/unit')
58 files changed, 294 insertions, 67 deletions
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 4d437d2f0..eccbd250f 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -11,6 +11,7 @@ UNIT_TESTS += \ theory/theory_black \ theory/theory_white \ theory/theory_arith_white \ + theory/theory_bv_white \ theory/type_enumerator_white \ expr/node_white \ expr/node_black \ @@ -40,6 +41,7 @@ UNIT_TESTS += \ context/stacking_vector_black \ util/array_store_all_black \ util/assert_white \ + util/binary_heap_black \ util/bitvector_black \ util/datatype_black \ util/configuration_black \ @@ -57,10 +59,6 @@ UNIT_TESTS += \ main/interactive_shell_black endif -# disabled/failing: -# theory/theory_bv_white \ -# - export VERBOSE = 1 # Things that aren't tests but that tests rely on and need to diff --git a/test/unit/context/cdlist_black.h b/test/unit/context/cdlist_black.h index a969ebd42..5f473478c 100644 --- a/test/unit/context/cdlist_black.h +++ b/test/unit/context/cdlist_black.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/context/cdlist_context_memory_black.h b/test/unit/context/cdlist_context_memory_black.h index fed2df5cb..359c3dce5 100644 --- a/test/unit/context/cdlist_context_memory_black.h +++ b/test/unit/context/cdlist_context_memory_black.h @@ -5,7 +5,7 @@ ** Major contributors: Tim King ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/context/cdmap_black.h b/test/unit/context/cdmap_black.h index 3ec697dd9..aad5c49d0 100644 --- a/test/unit/context/cdmap_black.h +++ b/test/unit/context/cdmap_black.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Tim King, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/context/cdmap_white.h b/test/unit/context/cdmap_white.h index e71d2b4ad..84b8242b4 100644 --- a/test/unit/context/cdmap_white.h +++ b/test/unit/context/cdmap_white.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/context/cdo_black.h b/test/unit/context/cdo_black.h index c665423ac..fe04421b4 100644 --- a/test/unit/context/cdo_black.h +++ b/test/unit/context/cdo_black.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/context/cdvector_black.h b/test/unit/context/cdvector_black.h index 87cb19121..c2a5259ee 100644 --- a/test/unit/context/cdvector_black.h +++ b/test/unit/context/cdvector_black.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/context/context_black.h b/test/unit/context/context_black.h index bc7f5a639..494db312c 100644 --- a/test/unit/context/context_black.h +++ b/test/unit/context/context_black.h @@ -5,7 +5,7 @@ ** Major contributors: Morgan Deters ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/context/context_mm_black.h b/test/unit/context/context_mm_black.h index 8c249996d..e58b22895 100644 --- a/test/unit/context/context_mm_black.h +++ b/test/unit/context/context_mm_black.h @@ -5,7 +5,7 @@ ** Major contributors: Morgan Deters ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/context/context_white.h b/test/unit/context/context_white.h index 0461e9124..7ad70f061 100644 --- a/test/unit/context/context_white.h +++ b/test/unit/context/context_white.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/context/stacking_map_black.h b/test/unit/context/stacking_map_black.h index 92a9546c2..91e12a25e 100644 --- a/test/unit/context/stacking_map_black.h +++ b/test/unit/context/stacking_map_black.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/context/stacking_vector_black.h b/test/unit/context/stacking_vector_black.h index 82966a564..c7e185735 100644 --- a/test/unit/context/stacking_vector_black.h +++ b/test/unit/context/stacking_vector_black.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h index b27d556c1..8fee6571d 100644 --- a/test/unit/expr/attribute_black.h +++ b/test/unit/expr/attribute_black.h @@ -5,7 +5,7 @@ ** Major contributors: Morgan Deters, Tim King ** Minor contributors (to current version): Christopher L. Conway ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h index 7fa9972a6..11063cd1b 100644 --- a/test/unit/expr/attribute_white.h +++ b/test/unit/expr/attribute_white.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Dejan Jovanovic, Christopher L. Conway ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/expr/expr_manager_public.h b/test/unit/expr/expr_manager_public.h index f7c7f403a..727abe984 100644 --- a/test/unit/expr/expr_manager_public.h +++ b/test/unit/expr/expr_manager_public.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h index 4a9d73cb7..b70c51276 100644 --- a/test/unit/expr/expr_public.h +++ b/test/unit/expr/expr_public.h @@ -5,7 +5,7 @@ ** Major contributors: Christopher L. Conway, Dejan Jovanovic ** Minor contributors (to current version): Tim King, Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/expr/kind_black.h b/test/unit/expr/kind_black.h index d591f0c9f..9deb8ce71 100644 --- a/test/unit/expr/kind_black.h +++ b/test/unit/expr/kind_black.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/expr/kind_map_black.h b/test/unit/expr/kind_map_black.h index 605dd92b5..489aaaa21 100644 --- a/test/unit/expr/kind_map_black.h +++ b/test/unit/expr/kind_map_black.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 6cf85fb7e..9f8ecb69e 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -5,7 +5,7 @@ ** Major contributors: Tim King ** Minor contributors (to current version): Christopher L. Conway, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index 1467b90c5..c71ba48c5 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -5,7 +5,7 @@ ** Major contributors: Christopher L. Conway, Morgan Deters ** Minor contributors (to current version): Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h index 4c2cc97e2..9ca086d06 100644 --- a/test/unit/expr/node_manager_black.h +++ b/test/unit/expr/node_manager_black.h @@ -5,7 +5,7 @@ ** Major contributors: Morgan Deters, Dejan Jovanovic ** Minor contributors (to current version): Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h index b272cb692..7bc279f47 100644 --- a/test/unit/expr/node_manager_white.h +++ b/test/unit/expr/node_manager_white.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/expr/node_self_iterator_black.h b/test/unit/expr/node_self_iterator_black.h index 31de84643..9f90bd1b0 100644 --- a/test/unit/expr/node_self_iterator_black.h +++ b/test/unit/expr/node_self_iterator_black.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h index 58ef7134f..bcb3155e1 100644 --- a/test/unit/expr/node_white.h +++ b/test/unit/expr/node_white.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Tim King, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/expr/symbol_table_black.h b/test/unit/expr/symbol_table_black.h index 386bcaa91..2acd1ebae 100644 --- a/test/unit/expr/symbol_table_black.h +++ b/test/unit/expr/symbol_table_black.h @@ -5,7 +5,7 @@ ** Major contributors: Christopher L. Conway ** Minor contributors (to current version): Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/expr/type_cardinality_public.h b/test/unit/expr/type_cardinality_public.h index 3c2609e3e..8eb59952a 100644 --- a/test/unit/expr/type_cardinality_public.h +++ b/test/unit/expr/type_cardinality_public.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/expr/type_node_white.h b/test/unit/expr/type_node_white.h index ae6e00616..ce1ce1534 100644 --- a/test/unit/expr/type_node_white.h +++ b/test/unit/expr/type_node_white.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h index fa2a3f0e2..b09246d95 100644 --- a/test/unit/main/interactive_shell_black.h +++ b/test/unit/main/interactive_shell_black.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/memory.h b/test/unit/memory.h index 44eec00d0..2809edee7 100644 --- a/test/unit/memory.h +++ b/test/unit/memory.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index 8ff62c25a..c157db8c4 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -5,7 +5,7 @@ ** Major contributors: Morgan Deters ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h index 58432ff86..c2c7cc18d 100644 --- a/test/unit/parser/parser_builder_black.h +++ b/test/unit/parser/parser_builder_black.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h index ccba0164a..665126059 100644 --- a/test/unit/prop/cnf_stream_white.h +++ b/test/unit/prop/cnf_stream_white.h @@ -5,7 +5,7 @@ ** Major contributors: Dejan Jovanovic, Christopher L. Conway ** Minor contributors (to current version): Liana Hadarean ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h index d568f8c1f..007378528 100644 --- a/test/unit/theory/logic_info_white.h +++ b/test/unit/theory/logic_info_white.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: Morgan Deters ** Major contributors: none - ** Minor contributors (to current version): Tianyi Liang + ** Minor contributors (to current version): Kshitij Bansal, Tianyi Liang ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/theory/stacking_map_black.h b/test/unit/theory/stacking_map_black.h index d867ef7fa..8097220ad 100644 --- a/test/unit/theory/stacking_map_black.h +++ b/test/unit/theory/stacking_map_black.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index c99c66fff..58bbe7a2b 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: Tim King ** Major contributors: Morgan Deters - ** Minor contributors (to current version): Dejan Jovanovic + ** Minor contributors (to current version): Kshitij Bansal, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -103,6 +103,7 @@ public: d_em = new ExprManager(); d_nm = NodeManager::fromExprManager(d_em); d_smt = new SmtEngine(d_em); + d_smt->setOption("incremental", 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_black.h b/test/unit/theory/theory_black.h index 4644d3385..bafd572c3 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: Tim King ** Major contributors: Clark Barrett - ** Minor contributors (to current version): none + ** Minor contributors (to current version): Liana Hadarean ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h index 4999ec3d4..eed173366 100644 --- a/test/unit/theory/theory_bv_white.h +++ b/test/unit/theory/theory_bv_white.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: Liana Hadarean ** Major contributors: none - ** Minor contributors (to current version): Dejan Jovanovic, Morgan Deters + ** Minor contributors (to current version): Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -21,7 +21,8 @@ #include "theory/theory.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" -#include "theory/bv/eager_bitblaster.h" +#include "theory/bv/theory_bv.h" +#include "theory/bv/bitblaster_template.h" #include "expr/node.h" #include "expr/node_manager.h" #include "context/context.h" @@ -59,7 +60,7 @@ public: d_smt = new SmtEngine(d_em); d_scope = new SmtScope(d_smt); d_smt->setOption("bitblast", SExpr("eager")); - d_bb = new EagerBitblaster(); + d_bb = new EagerBitblaster(NULL); } void tearDown() { diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index e32e49801..7440de350 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -5,7 +5,7 @@ ** Major contributors: Dejan Jovanovic ** Minor contributors (to current version): Andrew Reynolds, Christopher L. Conway, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h index 3259381ad..08447b86d 100644 --- a/test/unit/theory/theory_white.h +++ b/test/unit/theory/theory_white.h @@ -5,7 +5,7 @@ ** Major contributors: Tim King ** Minor contributors (to current version): Dejan Jovanovic, Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h index 4e80b7d20..3dcb2db85 100644 --- a/test/unit/theory/type_enumerator_white.h +++ b/test/unit/theory/type_enumerator_white.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/util/array_store_all_black.h b/test/unit/util/array_store_all_black.h index 094368703..ea7b89191 100644 --- a/test/unit/util/array_store_all_black.h +++ b/test/unit/util/array_store_all_black.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/util/assert_white.h b/test/unit/util/assert_white.h index 6ecd013c9..38dfe87e6 100644 --- a/test/unit/util/assert_white.h +++ b/test/unit/util/assert_white.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/util/binary_heap_black.h b/test/unit/util/binary_heap_black.h new file mode 100644 index 000000000..41e4d0e75 --- /dev/null +++ b/test/unit/util/binary_heap_black.h @@ -0,0 +1,227 @@ +/********************* */ +/*! \file binary_heap_black.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Black box testing of CVC4::BinaryHeap + ** + ** Black box testing of CVC4::BinaryHeap. + **/ + +#include <cxxtest/TestSuite.h> + +#include <iostream> +#include <sstream> + +#include "util/bin_heap.h" + +using namespace CVC4; +using namespace std; + +class BinaryHeapBlack : public CxxTest::TestSuite { +public: + + void setUp() { + } + + void tearDown() { + } + + /** + * Test a a series of simple heaps (push a few then pop all then do others). + * Done as a series to test if the heap structure falls into a bad state + * after prolonged use. + */ + void testHeapSeries() { + BinaryHeap<int> heap; + + // First test a heap of 1 element + TS_ASSERT_EQUALS(heap.size(), 0u); + TS_ASSERT(heap.empty()); +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS_ANYTHING(heap.top()); + TS_ASSERT_THROWS_ANYTHING(heap.pop()); +#endif /* CVC4_ASSERTIONS */ + TS_ASSERT_EQUALS(heap.begin(), heap.end()); + + BinaryHeap<int>::handle h5 = heap.push(5); + TS_ASSERT(h5 == h5); + TS_ASSERT_EQUALS(heap.top(), 5); + TS_ASSERT_EQUALS(heap.size(), 1u); + TS_ASSERT(! heap.empty()); + TS_ASSERT_DIFFERS(heap.begin(), heap.end()); + TS_ASSERT_EQUALS(*h5, 5); + TS_ASSERT_EQUALS(*heap.begin(), 5); + TS_ASSERT_THROWS_NOTHING(heap.erase(h5)); + TS_ASSERT(heap.empty()); + TS_ASSERT_EQUALS(heap.size(), 0u); +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS_ANYTHING(heap.top()); + TS_ASSERT_THROWS_ANYTHING(heap.pop()); +#endif /* CVC4_ASSERTIONS */ + + // Next test a heap of 4 elements + h5 = heap.push(5); + BinaryHeap<int>::handle h3 = heap.push(3); + BinaryHeap<int>::handle h10 = heap.push(10); + BinaryHeap<int>::handle h2 = heap.push(2); + TS_ASSERT_DIFFERS(h5, h3); + TS_ASSERT_DIFFERS(h5, h10); + TS_ASSERT_DIFFERS(h5, h2); + TS_ASSERT_DIFFERS(h3, h10); + TS_ASSERT_DIFFERS(h3, h2); + TS_ASSERT_DIFFERS(h10, h2); + TS_ASSERT_DIFFERS(heap.begin(), heap.end()); + TS_ASSERT_EQUALS(*heap.begin(), 10); + TS_ASSERT_EQUALS(*h2, 2); + TS_ASSERT_EQUALS(*h3, 3); + TS_ASSERT_EQUALS(*h5, 5); + TS_ASSERT_EQUALS(*h10, 10); + TS_ASSERT_EQUALS(heap.top(), 10); + // test the iterator (note the order of elements isn't guaranteed!) + BinaryHeap<int>::const_iterator i = heap.begin(); + TS_ASSERT_DIFFERS(i, heap.end()); + TS_ASSERT_THROWS_NOTHING(*i++); + TS_ASSERT_DIFFERS(i, heap.end()); + TS_ASSERT_THROWS_NOTHING(*i++); + TS_ASSERT_DIFFERS(i, heap.end()); + TS_ASSERT_THROWS_NOTHING(*i++); + TS_ASSERT_DIFFERS(i, heap.end()); + TS_ASSERT_THROWS_NOTHING(*i++); + TS_ASSERT_EQUALS(i, heap.end()); + TS_ASSERT(!heap.empty()); + TS_ASSERT_EQUALS(heap.size(), 4u); + TS_ASSERT_THROWS_NOTHING(heap.pop()); + TS_ASSERT_DIFFERS(heap.begin(), heap.end()); + TS_ASSERT_EQUALS(*heap.begin(), 5); + TS_ASSERT_EQUALS(heap.top(), 5); + TS_ASSERT(!heap.empty()); + TS_ASSERT_EQUALS(heap.size(), 3u); + TS_ASSERT_THROWS_NOTHING(heap.pop()); + TS_ASSERT_DIFFERS(heap.begin(), heap.end()); + TS_ASSERT_EQUALS(*heap.begin(), 3); + TS_ASSERT_EQUALS(heap.top(), 3); + TS_ASSERT(!heap.empty()); + TS_ASSERT_EQUALS(heap.size(), 2u); + TS_ASSERT_THROWS_NOTHING(heap.pop()); + TS_ASSERT_DIFFERS(heap.begin(), heap.end()); + TS_ASSERT_EQUALS(*heap.begin(), 2); + TS_ASSERT_EQUALS(heap.top(), 2); + TS_ASSERT(!heap.empty()); + TS_ASSERT_EQUALS(heap.size(), 1u); + TS_ASSERT_THROWS_NOTHING(heap.pop()); + TS_ASSERT_EQUALS(heap.begin(), heap.end()); + TS_ASSERT(heap.empty()); + TS_ASSERT_EQUALS(heap.size(), 0u); +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS_ANYTHING(heap.top()); + TS_ASSERT_THROWS_ANYTHING(heap.pop()); +#endif /* CVC4_ASSERTIONS */ + + // Now with a few updates + h5 = heap.push(5); + h3 = heap.push(3); + h10 = heap.push(10); + h2 = heap.push(2); + + TS_ASSERT_EQUALS(*h5, 5); + TS_ASSERT_EQUALS(*h3, 3); + TS_ASSERT_EQUALS(*h10, 10); + TS_ASSERT_EQUALS(*h2, 2); + + TS_ASSERT_EQUALS(heap.top(), 10); + heap.update(h10, -10); + TS_ASSERT_EQUALS(*h10, -10); + TS_ASSERT_EQUALS(heap.top(), 5); + heap.erase(h2); + TS_ASSERT_EQUALS(heap.top(), 5); + heap.update(h3, -20); + TS_ASSERT_EQUALS(*h3, -20); + TS_ASSERT_EQUALS(heap.top(), 5); + heap.pop(); + TS_ASSERT_EQUALS(heap.top(), -10); + heap.pop(); + TS_ASSERT_EQUALS(heap.top(), -20); + } + + struct Elem { + int x; + Elem(int y) : x(y) {} + };/* struct Elem */ + + struct Cmp { + bool valid; + Cmp() : valid(false) {} + Cmp(int x) : valid(true) {} + bool operator()(Elem x, Elem y) const { + // ensure BinaryHeap<> calls our Cmp instance and not some fresh one + TS_ASSERT(valid); + return x.x > y.x; + } + };/* struct Cmp */ + + void testLargeHeap() { + BinaryHeap<Elem, Cmp> heap(Cmp(0)); + vector<BinaryHeap<Elem, Cmp>::handle> handles; + TS_ASSERT(heap.empty()); + for(int x = 0; x < 1000; ++x) { + handles.push_back(heap.push(Elem(x))); + } + TS_ASSERT(!heap.empty()); + TS_ASSERT_EQUALS(heap.size(), 1000u); + heap.update(handles[100], 50); + heap.update(handles[100], -50); + heap.update(handles[600], 2); + heap.update(handles[184], -9); + heap.update(handles[987], 9555); + heap.update(handles[672], -1003); + heap.update(handles[781], 481); + heap.update(handles[9], 9619); + heap.update(handles[919], 111); + TS_ASSERT_EQUALS(heap.size(), 1000u); + heap.erase(handles[10]); + TS_ASSERT_EQUALS(heap.size(), 999u); + TS_ASSERT(!heap.empty()); + handles.clear(); + Elem last = heap.top(); + for(int x = 0; x < 800; ++x) { + TS_ASSERT_LESS_THAN_EQUALS(last.x, heap.top().x); + last = heap.top(); + heap.pop(); + TS_ASSERT_EQUALS(heap.size(), 998u - x); + TS_ASSERT(!heap.empty()); + } + TS_ASSERT_EQUALS(heap.size(), 199u); + for(int x = 0; x < 10000; ++x) { + // two-thirds of the time insert large value, one-third insert small value + handles.push_back(heap.push(Elem(4 * ((x % 3 == 0) ? -x : x)))); + if(x % 10 == 6) { + // also every tenth insert somewhere in the middle + handles.push_back(heap.push(Elem(x / 10))); + } + // change a few + heap.update(handles[x / 10], 4 * (*handles[x / 10]).x); + heap.update(handles[x / 105], (*handles[x / 4]).x - 294); + heap.update(handles[x / 33], 6 * (*handles[x / 82]).x / 5 - 1); + TS_ASSERT_EQUALS(heap.size(), size_t(x) + ((x + 4) / 10) + 200); + } + TS_ASSERT_EQUALS(heap.size(), 11199u); + TS_ASSERT(!heap.empty()); + last = heap.top(); + while(!heap.empty()) { + TS_ASSERT_LESS_THAN_EQUALS(last.x, heap.top().x); + last = heap.top(); + heap.pop(); + } + TS_ASSERT(heap.empty()); + heap.clear(); + TS_ASSERT(heap.empty()); + } + +};/* class BinaryHeapBlack */ diff --git a/test/unit/util/bitvector_black.h b/test/unit/util/bitvector_black.h index 505aa3e7f..b93bfafc3 100644 --- a/test/unit/util/bitvector_black.h +++ b/test/unit/util/bitvector_black.h @@ -5,7 +5,7 @@ ** Major contributors: Morgan Deters ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/util/boolean_simplification_black.h b/test/unit/util/boolean_simplification_black.h index e032f48cc..e2937ccb2 100644 --- a/test/unit/util/boolean_simplification_black.h +++ b/test/unit/util/boolean_simplification_black.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/util/cardinality_public.h b/test/unit/util/cardinality_public.h index 8d05f96f8..732bb0dbb 100644 --- a/test/unit/util/cardinality_public.h +++ b/test/unit/util/cardinality_public.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/util/configuration_black.h b/test/unit/util/configuration_black.h index 978b73eab..2d7378a67 100644 --- a/test/unit/util/configuration_black.h +++ b/test/unit/util/configuration_black.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h index 0bb98c3f2..addd716e5 100644 --- a/test/unit/util/datatype_black.h +++ b/test/unit/util/datatype_black.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/util/exception_black.h b/test/unit/util/exception_black.h index 1dab7c6a6..d2ae7d3e5 100644 --- a/test/unit/util/exception_black.h +++ b/test/unit/util/exception_black.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/util/integer_black.h b/test/unit/util/integer_black.h index de5669c11..36de17cba 100644 --- a/test/unit/util/integer_black.h +++ b/test/unit/util/integer_black.h @@ -5,7 +5,7 @@ ** Major contributors: Morgan Deters ** Minor contributors (to current version): Christopher L. Conway ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/util/integer_white.h b/test/unit/util/integer_white.h index 70b692412..12eabfbb2 100644 --- a/test/unit/util/integer_white.h +++ b/test/unit/util/integer_white.h @@ -5,7 +5,7 @@ ** Major contributors: Morgan Deters ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/util/output_black.h b/test/unit/util/output_black.h index c507d8552..0b151ef3f 100644 --- a/test/unit/util/output_black.h +++ b/test/unit/util/output_black.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/util/rational_black.h b/test/unit/util/rational_black.h index 7cd4c4ce4..d25c9473c 100644 --- a/test/unit/util/rational_black.h +++ b/test/unit/util/rational_black.h @@ -5,7 +5,7 @@ ** Major contributors: Morgan Deters ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/util/rational_white.h b/test/unit/util/rational_white.h index b9d0002f8..dfd0fa43b 100644 --- a/test/unit/util/rational_white.h +++ b/test/unit/util/rational_white.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/util/recursion_breaker_black.h b/test/unit/util/recursion_breaker_black.h index 9cbecae93..8bbc4c3b0 100644 --- a/test/unit/util/recursion_breaker_black.h +++ b/test/unit/util/recursion_breaker_black.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/util/stats_black.h b/test/unit/util/stats_black.h index 02daf8066..67deede75 100644 --- a/test/unit/util/stats_black.h +++ b/test/unit/util/stats_black.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: Morgan Deters ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): Kshitij Bansal ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/util/subrange_bound_white.h b/test/unit/util/subrange_bound_white.h index 2261c0bbb..71947b297 100644 --- a/test/unit/util/subrange_bound_white.h +++ b/test/unit/util/subrange_bound_white.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/test/unit/util/trans_closure_black.h b/test/unit/util/trans_closure_black.h index f2ae8fbe1..1c88ae427 100644 --- a/test/unit/util/trans_closure_black.h +++ b/test/unit/util/trans_closure_black.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** |