Fix unit tests.

diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 47bd7de66c64c747e44e65c145a1ba6380717da2..1e310251cd5ff01880b38cc91ff7ae8dc9be1abf 100644 (file)
--- 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 eccbd250f1df9b9e6b0269d0cffaeb66712513ac..98bedefbfea233ccc5356c014b05558fd6a9c8da 100644 (file)
--- 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 addd716e5efd72281f002399e5c0682f013b8dee..ff36336ca88223799b2a1ef6b8cef18fa30d0923 100644 (file)
--- 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 (file)
index 8bbc4c3..0000000
--- 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<T>
- **
- ** Black-box testing of RecursionBreaker<T>.
- **/
-
-#include <iostream>
-#include <string>
-
-#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<int> 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 (file)
index 1c88ae4..0000000
--- 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 */