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

In preparation for eliminating the Expr-level datatype.

1 files changed, 0 insertions, 74 deletions

diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h
index f8ccd23d4..0e17ab1e8 100644
--- 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; */