diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-08-04 18:45:13 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-08-04 18:45:13 +0000 |
commit | 1467abb8bd69050c2518f87a1775590cd5a9882e (patch) | |
tree | 30c269deec8189fde2b8db2abd4bee9600ad8a2f /test | |
parent | c956906a5dc4cb51b4676c3bba80159cbe76fdbc (diff) |
isConst() rule for datatypes
Diffstat (limited to 'test')
-rw-r--r-- | test/unit/expr/expr_public.h | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h index 491f99584..d4a968e96 100644 --- a/test/unit/expr/expr_public.h +++ b/test/unit/expr/expr_public.h @@ -345,6 +345,8 @@ public: void testIsConst() { /* bool isConst() const; */ + Debug.on("isConst"); + TS_ASSERT(!a_bool->isConst()); TS_ASSERT(!b_bool->isConst()); TS_ASSERT(!c_bool_and->isConst()); @@ -352,6 +354,25 @@ public: 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("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()); } void testGetConst() { |