diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/expr/expr_public.h | 22 | ||||
-rw-r--r-- | test/unit/expr/node_manager_black.h | 7 | ||||
-rw-r--r-- | test/unit/expr/node_manager_white.h | 4 | ||||
-rw-r--r-- | test/unit/expr/node_white.h | 2 |
4 files changed, 14 insertions, 21 deletions
diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h index 853d0086b..491f99584 100644 --- a/test/unit/expr/expr_public.h +++ b/test/unit/expr/expr_public.h @@ -66,8 +66,8 @@ public: d_apply_fun_bool = new Expr(d_em->mkExpr(APPLY_UF, *fun_op, *a_bool)); null = new Expr; - i1 = new Expr(d_em->mkConst(Integer("0"))); - i2 = new Expr(d_em->mkConst(Integer(23))); + i1 = new Expr(d_em->mkConst(Rational("0"))); + i2 = new Expr(d_em->mkConst(Rational(23))); r1 = new Expr(d_em->mkConst(Rational(1, 5))); r2 = new Expr(d_em->mkConst(Rational("0"))); } catch(Exception e) { @@ -218,8 +218,8 @@ public: TS_ASSERT(d_apply_fun_bool->getKind() == APPLY_UF); TS_ASSERT(null->getKind() == NULL_EXPR); - TS_ASSERT(i1->getKind() == CONST_INTEGER); - TS_ASSERT(i2->getKind() == CONST_INTEGER); + TS_ASSERT(i1->getKind() == CONST_RATIONAL); + TS_ASSERT(i2->getKind() == CONST_RATIONAL); TS_ASSERT(r1->getKind() == CONST_RATIONAL); TS_ASSERT(r2->getKind() == CONST_RATIONAL); } @@ -292,8 +292,8 @@ public: TS_ASSERT(d_apply_fun_bool->toString() == "(APPLY_UF f a)"); TS_ASSERT(null->toString() == "null"); - TS_ASSERT(i1->toString() == "(CONST_INTEGER 0)"); - TS_ASSERT(i2->toString() == "(CONST_INTEGER 23)"); + TS_ASSERT(i1->toString() == "(CONST_RATIONAL 0)"); + TS_ASSERT(i2->toString() == "(CONST_RATIONAL 23)"); TS_ASSERT(r1->toString() == "(CONST_RATIONAL 1/5)"); TS_ASSERT(r2->toString() == "(CONST_RATIONAL 0)"); } @@ -324,8 +324,8 @@ public: TS_ASSERT(sd.str() == "(APPLY_UF f a)"); TS_ASSERT(snull.str() == "null"); - TS_ASSERT(si1.str() == "(CONST_INTEGER 0)"); - TS_ASSERT(si2.str() == "(CONST_INTEGER 23)"); + TS_ASSERT(si1.str() == "(CONST_RATIONAL 0)"); + TS_ASSERT(si2.str() == "(CONST_RATIONAL 23)"); TS_ASSERT(sr1.str() == "(CONST_RATIONAL 1/5)"); TS_ASSERT(sr2.str() == "(CONST_RATIONAL 0)"); } @@ -362,14 +362,14 @@ public: TS_ASSERT_THROWS(b_bool->getConst<Kind>(), IllegalArgumentException); TS_ASSERT_THROWS(c_bool_and->getConst<Kind>(), IllegalArgumentException); TS_ASSERT(and_op->getConst<Kind>() == AND); - TS_ASSERT_THROWS(and_op->getConst<Integer>(), IllegalArgumentException); + TS_ASSERT_THROWS(and_op->getConst<Rational>(), IllegalArgumentException); TS_ASSERT(plus_op->getConst<Kind>() == PLUS); TS_ASSERT_THROWS(plus_op->getConst<Rational>(), IllegalArgumentException); TS_ASSERT_THROWS(d_apply_fun_bool->getConst<Kind>(), IllegalArgumentException); TS_ASSERT_THROWS(null->getConst<Kind>(), IllegalArgumentException); - TS_ASSERT(i1->getConst<Integer>() == 0); - TS_ASSERT(i2->getConst<Integer>() == 23); + TS_ASSERT(i1->getConst<Rational>() == 0); + TS_ASSERT(i2->getConst<Rational>() == 23); TS_ASSERT(r1->getConst<Rational>() == Rational(1, 5)); TS_ASSERT(r2->getConst<Rational>() == Rational("0")); diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h index c30e4badb..cca2ff4fc 100644 --- a/test/unit/expr/node_manager_black.h +++ b/test/unit/expr/node_manager_black.h @@ -168,13 +168,6 @@ public: TS_ASSERT_EQUALS(ff.getConst<bool>(),false); } - - void testMkConstInt() { - Integer i("3"); - Node n = d_nodeManager->mkConst(i); - TS_ASSERT_EQUALS(n.getConst<Integer>(),i); - } - void testMkConstRat() { Rational r("3/2"); Node n = d_nodeManager->mkConst(r); diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h index 735fe2ac8..15a178b5c 100644 --- a/test/unit/expr/node_manager_white.h +++ b/test/unit/expr/node_manager_white.h @@ -50,8 +50,8 @@ public: delete d_ctxt; } - void testMkConstInt() { - Integer i("3"); + void testMkConstRational() { + Rational i("3"); Node n = d_nm->mkConst(i); Node m = d_nm->mkConst(i); TS_ASSERT_EQUALS(n.getId(), m.getId()); diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h index ce67004c6..a042b1752 100644 --- a/test/unit/expr/node_white.h +++ b/test/unit/expr/node_white.h @@ -73,7 +73,7 @@ public: Node x = d_nm->mkVar("x", d_nm->integerType()); Node y = d_nm->mkVar("y", d_nm->integerType()); Node x_plus_y = d_nm->mkNode(PLUS, x, y); - Node two = d_nm->mkConst(Integer(2)); + Node two = d_nm->mkConst(Rational(2)); Node x_times_2 = d_nm->mkNode(MULT, x, two); Node n = d_nm->mkNode(PLUS, x_times_2, x_plus_y, y); |