From bdf8f315287b05cc4b8ec143c30c9da534c836a2 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Sat, 14 Feb 2015 11:47:03 +0100 Subject: [PATCH] Fix unit tests. --- src/util/datatype.cpp | 2 +- test/unit/Makefile.am | 2 - test/unit/util/datatype_black.h | 109 ---------------- test/unit/util/recursion_breaker_black.h | 55 -------- test/unit/util/trans_closure_black.h | 153 ----------------------- 5 files changed, 1 insertion(+), 320 deletions(-) delete mode 100644 test/unit/util/recursion_breaker_black.h delete mode 100644 test/unit/util/trans_closure_black.h diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index 47bd7de66..1e310251c 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -316,9 +316,9 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(IllegalArgumentException) { Expr groundTerm = computeGroundTerm( t, processing ); if(!groundTerm.isNull() ) { // we found a ground-term-constructing constructor! + d_ground_term[t] = groundTerm; Debug("datatypes") << "constructed: " << getName() << " => " << groundTerm << std::endl; } - d_ground_term[t] = groundTerm; if( groundTerm.isNull() ){ if( !d_isCo ){ // if we get all the way here, we aren't well-founded diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index eccbd250f..98bedefbf 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -52,10 +52,8 @@ UNIT_TESTS += \ util/rational_black \ util/rational_white \ util/stats_black \ - util/trans_closure_black \ util/boolean_simplification_black \ util/subrange_bound_white \ - util/recursion_breaker_black \ main/interactive_shell_black endif diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h index addd716e5..ff36336ca 100644 --- a/test/unit/util/datatype_black.h +++ b/test/unit/util/datatype_black.h @@ -81,16 +81,6 @@ public: Debug("groundterms") << "ground term of " << colorsType.getDatatype().getName() << endl << " is " << colorsType.mkGroundTerm() << endl; TS_ASSERT(colorsType.mkGroundTerm().getType() == colorsType); - // all ctors should be well-founded too - for(Datatype::const_iterator i = colorsType.getDatatype().begin(), - i_end = colorsType.getDatatype().end(); - i != i_end; - ++i) { - TS_ASSERT((*i).isWellFounded()); - Debug("groundterms") << "ground term of " << *i << endl - << " is " << (*i).mkGroundTerm( colorsType ) << endl; - TS_ASSERT((*i).mkGroundTerm( colorsType ).getType() == colorsType); - } } void testNat() { @@ -118,17 +108,6 @@ public: Debug("groundterms") << "ground term of " << natType.getDatatype().getName() << endl << " is " << natType.mkGroundTerm() << endl; TS_ASSERT(natType.mkGroundTerm().getType() == natType); - // all ctors should be well-founded too - for(Datatype::const_iterator i = natType.getDatatype().begin(), - i_end = natType.getDatatype().end(); - i != i_end; - ++i) { - Debug("datatypes") << "checking " << (*i).getName() << endl; - TS_ASSERT((*i).isWellFounded()); - Debug("groundterms") << "ground term of " << *i << endl - << " is " << (*i).mkGroundTerm( natType ) << endl; - TS_ASSERT((*i).mkGroundTerm( natType ).getType() == natType); - } } void testTree() { @@ -160,16 +139,6 @@ public: Debug("groundterms") << "ground term of " << treeType.getDatatype().getName() << endl << " is " << treeType.mkGroundTerm() << endl; TS_ASSERT(treeType.mkGroundTerm().getType() == treeType); - // all ctors should be well-founded too - for(Datatype::const_iterator i = treeType.getDatatype().begin(), - i_end = treeType.getDatatype().end(); - i != i_end; - ++i) { - TS_ASSERT((*i).isWellFounded()); - Debug("groundterms") << "ground term of " << *i << endl - << " is " << (*i).mkGroundTerm( treeType ) << endl; - TS_ASSERT((*i).mkGroundTerm( treeType ).getType() == treeType); - } } void testListInt() { @@ -195,16 +164,6 @@ public: Debug("groundterms") << "ground term of " << listType.getDatatype().getName() << endl << " is " << listType.mkGroundTerm() << endl; TS_ASSERT(listType.mkGroundTerm().getType() == listType); - // all ctors should be well-founded too - for(Datatype::const_iterator i = listType.getDatatype().begin(), - i_end = listType.getDatatype().end(); - i != i_end; - ++i) { - TS_ASSERT((*i).isWellFounded()); - Debug("groundterms") << "ground term of " << *i << endl - << " is " << (*i).mkGroundTerm( listType ) << endl; - TS_ASSERT((*i).mkGroundTerm( listType ).getType() == listType); - } } void testListReal() { @@ -230,16 +189,6 @@ public: Debug("groundterms") << "ground term of " << listType.getDatatype().getName() << endl << " is " << listType.mkGroundTerm() << endl; TS_ASSERT(listType.mkGroundTerm().getType() == listType); - // all ctors should be well-founded too - for(Datatype::const_iterator i = listType.getDatatype().begin(), - i_end = listType.getDatatype().end(); - i != i_end; - ++i) { - TS_ASSERT((*i).isWellFounded()); - Debug("groundterms") << "ground term of " << *i << endl - << " is " << (*i).mkGroundTerm( listType ) << endl; - TS_ASSERT((*i).mkGroundTerm( listType ).getType() == listType); - } } void testListBoolean() { @@ -264,16 +213,6 @@ public: Debug("groundterms") << "ground term of " << listType.getDatatype().getName() << endl << " is " << listType.mkGroundTerm() << endl; TS_ASSERT(listType.mkGroundTerm().getType() == listType); - // all ctors should be well-founded too - for(Datatype::const_iterator i = listType.getDatatype().begin(), - i_end = listType.getDatatype().end(); - i != i_end; - ++i) { - TS_ASSERT((*i).isWellFounded()); - Debug("groundterms") << "ground term of " << *i << endl - << " is " << (*i).mkGroundTerm( listType ) << endl; - TS_ASSERT((*i).mkGroundTerm( listType ).getType() == listType); - } } void testMutualListTrees() { @@ -329,16 +268,6 @@ public: Debug("groundterms") << "ground term of " << dtts[0].getDatatype().getName() << endl << " is " << dtts[0].mkGroundTerm() << endl; TS_ASSERT(dtts[0].mkGroundTerm().getType() == dtts[0]); - // all ctors should be well-founded too - for(Datatype::const_iterator i = dtts[0].getDatatype().begin(), - i_end = dtts[0].getDatatype().end(); - i != i_end; - ++i) { - TS_ASSERT((*i).isWellFounded()); - Debug("groundterms") << "ground term of " << *i << endl - << " is " << (*i).mkGroundTerm( dtts[0] ) << endl; - TS_ASSERT((*i).mkGroundTerm( dtts[0] ).getType() == dtts[0]); - } TS_ASSERT(! dtts[1].getDatatype().isFinite()); TS_ASSERT(dtts[1].getDatatype().getCardinality().compare(Cardinality::INTEGERS) == Cardinality::EQUAL); @@ -346,16 +275,6 @@ public: Debug("groundterms") << "ground term of " << dtts[1].getDatatype().getName() << endl << " is " << dtts[1].mkGroundTerm() << endl; TS_ASSERT(dtts[1].mkGroundTerm().getType() == dtts[1]); - // all ctors should be well-founded too - for(Datatype::const_iterator i = dtts[1].getDatatype().begin(), - i_end = dtts[1].getDatatype().end(); - i != i_end; - ++i) { - TS_ASSERT((*i).isWellFounded()); - Debug("groundterms") << "ground term of " << *i << endl - << " is " << (*i).mkGroundTerm( dtts[1] ) << endl; - TS_ASSERT((*i).mkGroundTerm( dtts[1] ).getType() == dtts[1]); - } // add another constructor to list datatype resulting in an // "otherNil-list" @@ -377,16 +296,6 @@ public: Debug("groundterms") << "ground term of " << dtts2[0].getDatatype().getName() << endl << " is " << dtts2[0].mkGroundTerm() << endl; TS_ASSERT(dtts2[0].mkGroundTerm().getType() == dtts2[0]); - // all ctors should be well-founded too - for(Datatype::const_iterator i = dtts2[0].getDatatype().begin(), - i_end = dtts2[0].getDatatype().end(); - i != i_end; - ++i) { - TS_ASSERT((*i).isWellFounded()); - Debug("groundterms") << "ground term of " << *i << endl - << " is " << (*i).mkGroundTerm( dtts2[0] ) << endl; - TS_ASSERT((*i).mkGroundTerm( dtts2[0] ).getType() == dtts2[0]); - } TS_ASSERT(! dtts2[1].getDatatype().isParametric()); TS_ASSERT(! dtts2[1].getDatatype().isFinite()); @@ -395,16 +304,6 @@ public: Debug("groundterms") << "ground term of " << dtts2[1].getDatatype().getName() << endl << " is " << dtts2[1].mkGroundTerm() << endl; TS_ASSERT(dtts2[1].mkGroundTerm().getType() == dtts2[1]); - // all ctors should be well-founded too - for(Datatype::const_iterator i = dtts2[1].getDatatype().begin(), - i_end = dtts2[1].getDatatype().end(); - i != i_end; - ++i) { - TS_ASSERT((*i).isWellFounded()); - Debug("groundterms") << "ground term of " << *i << endl - << " is " << (*i).mkGroundTerm( dtts2[1] ) << endl; - TS_ASSERT((*i).mkGroundTerm( dtts2[1] ).getType() == dtts2[1]); - } } void testNotSoWellFounded() { @@ -425,14 +324,6 @@ public: TS_ASSERT(! treeType.getDatatype().isWellFounded()); TS_ASSERT_THROWS_ANYTHING( treeType.mkGroundTerm() ); TS_ASSERT_THROWS_ANYTHING( treeType.getDatatype().mkGroundTerm( treeType ) ); - // all ctors should be not-well-founded either - for(Datatype::const_iterator i = treeType.getDatatype().begin(), - i_end = treeType.getDatatype().end(); - i != i_end; - ++i) { - TS_ASSERT(! (*i).isWellFounded()); - TS_ASSERT_THROWS_ANYTHING( (*i).mkGroundTerm( treeType ) ); - } } void testParametricDatatype() { diff --git a/test/unit/util/recursion_breaker_black.h b/test/unit/util/recursion_breaker_black.h deleted file mode 100644 index 8bbc4c3b0..000000000 --- a/test/unit/util/recursion_breaker_black.h +++ /dev/null @@ -1,55 +0,0 @@ -/********************* */ -/*! \file recursion_breaker_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 RecursionBreaker - ** - ** Black-box testing of RecursionBreaker. - **/ - -#include -#include - -#include "util/recursion_breaker.h" - -using namespace CVC4; -using namespace std; - -class RecursionBreakerBlack : public CxxTest::TestSuite { - int d_count; - -public: - - void setUp() { - d_count = 0; - } - - int foo(int x) { - RecursionBreaker breaker("foo", x); - if(breaker.isRecursion()) { - ++d_count; - return 0; - } - int xfactor = x * x; - if(x > 0) { - xfactor = -xfactor; - } - int y = foo(11 * x + xfactor); - int z = y < 0 ? y : x * y; - cout << "x == " << x << ", y == " << y << " ==> " << z << endl; - return z; - } - - void testFoo() { - foo(5); - TS_ASSERT( d_count == 1 ); - } - -};/* class RecursionBreakerBlack */ diff --git a/test/unit/util/trans_closure_black.h b/test/unit/util/trans_closure_black.h deleted file mode 100644 index 1c88ae427..000000000 --- a/test/unit/util/trans_closure_black.h +++ /dev/null @@ -1,153 +0,0 @@ -/********************* */ -/*! \file trans_closure_black.h - ** \verbatim - ** Original author: Clark Barrett - ** Major contributors: none - ** Minor contributors (to current version): Morgan Deters - ** 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::TransitiveClosure. - ** - ** Black box testing of CVC4::TransitiveClosure. - **/ - - -#include "util/trans_closure.h" - - -using namespace CVC4; -using namespace CVC4::context; -using namespace std; - - -class TransitiveClosureBlack : public CxxTest::TestSuite { - Context* d_context; - TransitiveClosure* d_tc; - -public: - - void setUp() { - d_context = new Context; - d_tc = new TransitiveClosure(d_context); - } - - void tearDown() { - try { - delete d_tc; - delete d_context; - } catch(Exception& e) { - Warning() << std::endl << e << std::endl; - throw; - } - } - - void testSimple() { - bool b; - b = d_tc->addEdge(1,2); - TS_ASSERT(!b); - - b = d_tc->addEdge(2,3); - TS_ASSERT(!b); - - b = d_tc->addEdge(3,1); - TS_ASSERT(b); - - b = d_tc->addEdge(2,4); - TS_ASSERT(!b); - - b = d_tc->addEdge(2,5); - TS_ASSERT(!b); - - b = d_tc->addEdge(4,6); - TS_ASSERT(!b); - - b = d_tc->addEdge(6,2); - TS_ASSERT(b); - } - - - void test1() { - bool b; - b = d_tc->addEdge(1,2); - TS_ASSERT(!b); - - d_context->push(); - - b = d_tc->addEdge(2,3); - TS_ASSERT(!b); - - b = d_tc->addEdge(3,1); - TS_ASSERT(b); - - d_context->pop(); - - b = d_tc->addEdge(3,1); - TS_ASSERT(!b); - - b = d_tc->addEdge(2,3); - TS_ASSERT(b); - - d_context->push(); - - b = d_tc->addEdge(6,4); - TS_ASSERT(!b); - - b = d_tc->addEdge(2,6); - TS_ASSERT(!b); - - b = d_tc->addEdge(4,1); - TS_ASSERT(b); - - d_context->pop(); - - b = d_tc->addEdge(4,1); - - TS_ASSERT(!b); - } - - void test2() { - bool b; - b = d_tc->addEdge(1,2); - TS_ASSERT(!b); - b = d_tc->addEdge(1,3); - TS_ASSERT(!b); - b = d_tc->addEdge(1,4); - TS_ASSERT(!b); - b = d_tc->addEdge(1,5); - TS_ASSERT(!b); - b = d_tc->addEdge(1,6); - TS_ASSERT(!b); - b = d_tc->addEdge(1,7); - TS_ASSERT(!b); - b = d_tc->addEdge(1,8); - TS_ASSERT(!b); - b = d_tc->addEdge(1,9); - TS_ASSERT(!b); - - b = d_tc->addEdge(3,2); - TS_ASSERT(!b); - b = d_tc->addEdge(4,7); - TS_ASSERT(!b); - - b = d_tc->addEdge(2,1); - TS_ASSERT(b); - b = d_tc->addEdge(3,1); - TS_ASSERT(b); - b = d_tc->addEdge(4,1); - TS_ASSERT(b); - b = d_tc->addEdge(5,1); - TS_ASSERT(b); - b = d_tc->addEdge(6,1); - TS_ASSERT(b); - b = d_tc->addEdge(7,1); - TS_ASSERT(b); - b = d_tc->addEdge(8,1); - TS_ASSERT(b); - b = d_tc->addEdge(9,1); - TS_ASSERT(b); - } - -};/* class TransitiveClosureBlack */ -- 2.30.2