Update Expr-level unit tests that depend on datatypes to Node (#4860)

In preparation for eliminating the Expr-level datatype.

diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h
index f8ccd23d4fb4806ceea7b634b1bd20248dc4b462..0e17ab1e827c0aa602c36601bb09f64ce4894f9b 100644 (file)
--- a/test/unit/expr/expr_public.h
+++ b/test/unit/expr/expr_public.h
@@ -339,80 +339,6 @@ class ExprPublic : public CxxTest::TestSuite {
     TS_ASSERT(null->isNull());
   }
 
-  void testIsConst() {
-    /* bool isConst() const; */
-
-    //Debug.on("isConst");
-
-    TS_ASSERT(!a_bool->isConst());
-    TS_ASSERT(!b_bool->isConst());
-    TS_ASSERT(!c_bool_and->isConst());
-    TS_ASSERT(and_op->isConst());
-    TS_ASSERT(plus_op->isConst());
-    TS_ASSERT(!d_apply_fun_bool->isConst());
-    TS_ASSERT(!null->isConst());
-
-    // more complicated "constants" exist in datatypes and arrays theories
-    Datatype list(d_em, "list");
-    DatatypeConstructor consC("cons");
-    consC.addArg("car", d_em->integerType());
-    consC.addArg("cdr", DatatypeSelfType());
-    list.addConstructor(consC);
-    list.addConstructor(DatatypeConstructor("nil"));
-    DatatypeType listType = d_em->mkDatatypeType(list);
-    Expr cons = listType.getDatatype().getConstructor("cons");
-    Expr nil = listType.getDatatype().getConstructor("nil");
-    Expr x = d_em->mkVar("x", d_em->integerType());
-    Expr cons_x_nil = d_em->mkExpr(APPLY_CONSTRUCTOR, cons, x, d_em->mkExpr(APPLY_CONSTRUCTOR, nil));
-    Expr cons_1_nil = d_em->mkExpr(APPLY_CONSTRUCTOR, cons, d_em->mkConst(Rational(1)), d_em->mkExpr(APPLY_CONSTRUCTOR, nil));
-    Expr cons_1_cons_2_nil = d_em->mkExpr(APPLY_CONSTRUCTOR, cons, d_em->mkConst(Rational(1)), d_em->mkExpr(APPLY_CONSTRUCTOR, cons, d_em->mkConst(Rational(2)), d_em->mkExpr(APPLY_CONSTRUCTOR, nil)));
-    TS_ASSERT(d_em->mkExpr(APPLY_CONSTRUCTOR, nil).isConst());
-    TS_ASSERT(!cons_x_nil.isConst());
-    TS_ASSERT(cons_1_nil.isConst());
-    TS_ASSERT(cons_1_cons_2_nil.isConst());
-
-    {
-      ExprManagerScope ems(*d_em);
-      ArrayType arrType =
-          d_em->mkArrayType(d_em->integerType(), d_em->integerType());
-      Expr zero = d_em->mkConst(Rational(0));
-      Expr one = d_em->mkConst(Rational(1));
-      Expr storeAll = d_em->mkConst(
-          ArrayStoreAll(TypeNode::fromType(arrType), Node::fromExpr(zero)));
-      TS_ASSERT(storeAll.isConst());
-
-      Expr arr = d_em->mkExpr(STORE, storeAll, zero, zero);
-      TS_ASSERT(!arr.isConst());
-      arr = d_em->mkExpr(STORE, storeAll, zero, one);
-      TS_ASSERT(arr.isConst());
-      Expr arr2 = d_em->mkExpr(STORE, arr, one, zero);
-      TS_ASSERT(!arr2.isConst());
-      arr2 = d_em->mkExpr(STORE, arr, one, one);
-      TS_ASSERT(arr2.isConst());
-      arr2 = d_em->mkExpr(STORE, arr, zero, one);
-      TS_ASSERT(!arr2.isConst());
-
-      arrType =
-          d_em->mkArrayType(d_em->mkBitVectorType(1), d_em->mkBitVectorType(1));
-      zero = d_em->mkConst(BitVector(1, unsigned(0)));
-      one = d_em->mkConst(BitVector(1, unsigned(1)));
-      storeAll = d_em->mkConst(
-          ArrayStoreAll(TypeNode::fromType(arrType), Node::fromExpr(zero)));
-      TS_ASSERT(storeAll.isConst());
-
-      arr = d_em->mkExpr(STORE, storeAll, zero, zero);
-      TS_ASSERT(!arr.isConst());
-      arr = d_em->mkExpr(STORE, storeAll, zero, one);
-      TS_ASSERT(arr.isConst());
-      arr2 = d_em->mkExpr(STORE, arr, one, zero);
-      TS_ASSERT(!arr2.isConst());
-      arr2 = d_em->mkExpr(STORE, arr, one, one);
-      TS_ASSERT(!arr2.isConst());
-      arr2 = d_em->mkExpr(STORE, arr, zero, one);
-      TS_ASSERT(!arr2.isConst());
-    }
-  }
-
   void testGetConst() {
     /* template <class T>
        const T& getConst() const; */

diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 91242322a263156d4c3588df9242498161d0b0f6..182f742b06bbd1c2d1ba9a16c67f7395c9d99107 100644 (file)
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -23,13 +23,15 @@
 #include <vector>
 
 #include "api/cvc4cpp.h"
-#include "smt/smt_engine.h"
+#include "expr/dtype.h"
 #include "expr/expr_manager.h"
 #include "expr/node.h"
 #include "expr/node_builder.h"
 #include "expr/node_manager.h"
 #include "expr/node_value.h"
+#include "smt/smt_engine.h"
 #include "test_utils.h"
+#include "theory/rewriter.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
@@ -706,6 +708,80 @@ class NodeBlack : public CxxTest::TestSuite {
               std::equal(children.begin(), children.end(), skolems.begin()));
   }
 
+  void testIsConst()
+  {
+    // more complicated "constants" exist in datatypes and arrays theories
+    DType list("list");
+    std::shared_ptr<DTypeConstructor> consC =
+        std::make_shared<DTypeConstructor>("cons");
+    consC->addArg("car", d_nodeManager->integerType());
+    consC->addArgSelf("cdr");
+    list.addConstructor(consC);
+    list.addConstructor(std::make_shared<DTypeConstructor>("nil"));
+    TypeNode listType = d_nodeManager->mkDatatypeType(list);
+    const std::vector<std::shared_ptr<DTypeConstructor> >& lcons =
+        listType.getDType().getConstructors();
+    Node cons = lcons[0]->getConstructor();
+    Node nil = lcons[1]->getConstructor();
+    Node x = d_nodeManager->mkSkolem("x", d_nodeManager->integerType());
+    Node cons_x_nil =
+        d_nodeManager->mkNode(APPLY_CONSTRUCTOR,
+                              cons,
+                              x,
+                              d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil));
+    Node cons_1_nil =
+        d_nodeManager->mkNode(APPLY_CONSTRUCTOR,
+                              cons,
+                              d_nodeManager->mkConst(Rational(1)),
+                              d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil));
+    Node cons_1_cons_2_nil = d_nodeManager->mkNode(
+        APPLY_CONSTRUCTOR,
+        cons,
+        d_nodeManager->mkConst(Rational(1)),
+        d_nodeManager->mkNode(APPLY_CONSTRUCTOR,
+                              cons,
+                              d_nodeManager->mkConst(Rational(2)),
+                              d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil)));
+    TS_ASSERT(d_nodeManager->mkNode(APPLY_CONSTRUCTOR, nil).isConst());
+    TS_ASSERT(!cons_x_nil.isConst());
+    TS_ASSERT(cons_1_nil.isConst());
+    TS_ASSERT(cons_1_cons_2_nil.isConst());
+
+    TypeNode arrType = d_nodeManager->mkArrayType(d_nodeManager->integerType(),
+                                                  d_nodeManager->integerType());
+    Node zero = d_nodeManager->mkConst(Rational(0));
+    Node one = d_nodeManager->mkConst(Rational(1));
+    Node storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero));
+    TS_ASSERT(storeAll.isConst());
+
+    Node arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero);
+    TS_ASSERT(!arr.isConst());
+    arr = d_nodeManager->mkNode(STORE, storeAll, zero, one);
+    TS_ASSERT(arr.isConst());
+    Node arr2 = d_nodeManager->mkNode(STORE, arr, one, zero);
+    TS_ASSERT(!arr2.isConst());
+    arr2 = d_nodeManager->mkNode(STORE, arr, zero, one);
+    TS_ASSERT(!arr2.isConst());
+
+    arrType = d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(1),
+                                         d_nodeManager->mkBitVectorType(1));
+    zero = d_nodeManager->mkConst(BitVector(1, unsigned(0)));
+    one = d_nodeManager->mkConst(BitVector(1, unsigned(1)));
+    storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero));
+    TS_ASSERT(storeAll.isConst());
+
+    arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero);
+    TS_ASSERT(!arr.isConst());
+    arr = d_nodeManager->mkNode(STORE, storeAll, zero, one);
+    TS_ASSERT(arr.isConst());
+    arr2 = d_nodeManager->mkNode(STORE, arr, one, zero);
+    TS_ASSERT(!arr2.isConst());
+    arr2 = d_nodeManager->mkNode(STORE, arr, one, one);
+    TS_ASSERT(!arr2.isConst());
+    arr2 = d_nodeManager->mkNode(STORE, arr, zero, one);
+    TS_ASSERT(!arr2.isConst());
+  }
+
   //  This Test is designed to fail in a way that will cause a segfault,
   //  so it is commented out.
   //  This is for demonstrating what a certain type of user error looks like.

diff --git a/test/unit/expr/type_cardinality_public.h b/test/unit/expr/type_cardinality_public.h
index 49d6bd9fd82c62c9f4c2e55447f64eee0bfeffea..ba236fdf2c82735c14d82fca7a350cc3e4a49c15 100644 (file)
--- a/test/unit/expr/type_cardinality_public.h
+++ b/test/unit/expr/type_cardinality_public.h
@@ -23,6 +23,7 @@
 #include "api/cvc4cpp.h"
 #include "expr/expr_manager.h"
 #include "expr/kind.h"
+#include "expr/node_manager.h"
 #include "expr/type.h"
 #include "util/cardinality.h"
 
@@ -36,6 +37,7 @@ class TypeCardinalityPublic : public CxxTest::TestSuite {
   {
     d_slv = new api::Solver();
     d_em = d_slv->getExprManager();
+    d_nm = d_slv->getNodeManager();
   }
 
   void tearDown() override { delete d_slv; }
@@ -180,15 +182,20 @@ class TypeCardinalityPublic : public CxxTest::TestSuite {
   }
 
   void testTernaryFunctions() {
-    vector<Type> boolbool; boolbool.push_back(d_em->booleanType()); boolbool.push_back(d_em->booleanType());
-    vector<Type> boolboolbool = boolbool; boolboolbool.push_back(d_em->booleanType());
+    vector<TypeNode> boolbool;
+    boolbool.push_back(d_nm->booleanType());
+    boolbool.push_back(d_nm->booleanType());
+    vector<TypeNode> boolboolbool = boolbool;
+    boolboolbool.push_back(d_nm->booleanType());
 
-    Type boolboolTuple = d_em->mkTupleType(boolbool);
-    Type boolboolboolTuple = d_em->mkTupleType(boolboolbool);
+    TypeNode boolboolTuple = d_nm->mkTupleType(boolbool);
+    TypeNode boolboolboolTuple = d_nm->mkTupleType(boolboolbool);
 
-    Type boolboolboolToBool = d_em->mkFunctionType(boolboolbool, d_em->booleanType());
-    Type boolboolToBoolbool = d_em->mkFunctionType(boolbool, boolboolTuple);
-    Type boolToBoolboolbool = d_em->mkFunctionType(d_em->booleanType(), boolboolboolTuple);
+    TypeNode boolboolboolToBool =
+        d_nm->mkFunctionType(boolboolbool, d_nm->booleanType());
+    TypeNode boolboolToBoolbool = d_nm->mkFunctionType(boolbool, boolboolTuple);
+    TypeNode boolToBoolboolbool =
+        d_nm->mkFunctionType(d_nm->booleanType(), boolboolboolTuple);
 
     TS_ASSERT( boolboolboolToBool.getCardinality().compare(/* 2 ^ 8 */ 1 << 8) == Cardinality::EQUAL );
     TS_ASSERT( boolboolToBoolbool.getCardinality().compare(/* 4 ^ 4 */ 4 * 4 * 4 * 4) == Cardinality::EQUAL );
@@ -232,4 +239,5 @@ class TypeCardinalityPublic : public CxxTest::TestSuite {
  private:
   api::Solver* d_slv;
   ExprManager* d_em;
+  NodeManager* d_nm;
 };/* TypeCardinalityPublic */

diff --git a/test/unit/theory/theory_sets_type_enumerator_white.h b/test/unit/theory/theory_sets_type_enumerator_white.h
index 0a97f4c427003e97ab4e90eed69cddceb1d76ce5..b6726e540d6f89882a9164358896cedb52c62f4b 100644 (file)
--- a/test/unit/theory/theory_sets_type_enumerator_white.h
+++ b/test/unit/theory/theory_sets_type_enumerator_white.h
@@ -18,6 +18,7 @@
 
 #include <cxxtest/TestSuite.h>
 
+#include "expr/dtype.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/sets/theory_sets_type_enumerator.h"
@@ -135,24 +136,20 @@ class SetEnumeratorWhite : public CxxTest::TestSuite
 
   void testSetOfFiniteDatatype()
   {
-    Datatype dt(d_em, "Colors");
-    dt.addConstructor(DatatypeConstructor("red"));
-    dt.addConstructor(DatatypeConstructor("green"));
-    dt.addConstructor(DatatypeConstructor("blue"));
-    TypeNode datatype = TypeNode::fromType(d_em->mkDatatypeType(dt));
+    DType dt("Colors");
+    dt.addConstructor(std::make_shared<DTypeConstructor>("red"));
+    dt.addConstructor(std::make_shared<DTypeConstructor>("green"));
+    dt.addConstructor(std::make_shared<DTypeConstructor>("blue"));
+    TypeNode datatype = d_nm->mkDatatypeType(dt);
+    const std::vector<std::shared_ptr<DTypeConstructor> >& dtcons =
+        datatype.getDType().getConstructors();
     SetEnumerator setEnumerator(d_nm->mkSetType(datatype));
 
-    Node red = d_nm->mkNode(
-        APPLY_CONSTRUCTOR,
-        DatatypeType(datatype.toType()).getDatatype().getConstructor("red"));
+    Node red = d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[0]->getConstructor());
 
-    Node green = d_nm->mkNode(
-        APPLY_CONSTRUCTOR,
-        DatatypeType(datatype.toType()).getDatatype().getConstructor("green"));
+    Node green = d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[1]->getConstructor());
 
-    Node blue = d_nm->mkNode(
-        APPLY_CONSTRUCTOR,
-        DatatypeType(datatype.toType()).getDatatype().getConstructor("blue"));
+    Node blue = d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[2]->getConstructor());
 
     Node actual0 = *setEnumerator;
     Node expected0 =