diff options
| author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-07-28 22:57:36 +0000 |
|---|---|---|
| committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-07-28 22:57:36 +0000 |
| commit | 88766918615793536224bf50d0bb70ec9f9efd93 (patch) | |
| tree | 5a038bb2c17199f43d7a422063751bc3839b7388 /test/unit/theory | |
| parent | d2787f41e72184fbdf2619d3c0466bed9b6211be (diff) | |
Forcing a type check on Node construction in debug mode (Fixes: #188)
NOTE: mkNode/mkExpr/parsing functions can now throw type checking exceptions
Diffstat (limited to 'test/unit/theory')
| -rw-r--r-- | test/unit/theory/theory_engine_white.h | 16 | ||||
| -rw-r--r-- | test/unit/theory/theory_uf_white.h | 3 |
2 files changed, 12 insertions, 7 deletions
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index 570fa74a4..8132cc262 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -261,10 +261,12 @@ public: } void testRewriterComplicated() { + try { Node x = d_nm->mkVar("x", d_nm->integerType()); Node y = d_nm->mkVar("y", d_nm->realType()); - Node z1 = d_nm->mkVar("z1", d_nm->mkSort("U")); - Node z2 = d_nm->mkVar("z2", d_nm->mkSort("U")); + TypeNode u = d_nm->mkSort("U"); + Node z1 = d_nm->mkVar("z1", u); + Node z2 = d_nm->mkVar("z2", u); Node f = d_nm->mkVar("f", d_nm->mkFunctionType(d_nm->integerType(), d_nm->integerType())); Node g = d_nm->mkVar("g", d_nm->mkFunctionType(d_nm->realType(), @@ -279,10 +281,8 @@ public: Node gy = d_nm->mkNode(APPLY_UF, g, y); Node z1eqz2 = d_nm->mkNode(EQUAL, z1, z2); Node f1eqf2 = d_nm->mkNode(EQUAL, f1, f2); - Node ffxeqgy = d_nm->mkNode(EQUAL, - ffx, - gy); - Node and1 = d_nm->mkNode(AND, ffxeqgy, z1eqz2, ffx); + Node ffxeqgy = d_nm->mkNode(EQUAL, ffx, gy); + Node and1 = d_nm->mkNode(AND, ffxeqgy, z1eqz2); Node ffxeqf1 = d_nm->mkNode(EQUAL, ffx, f1); Node or1 = d_nm->mkNode(OR, and1, ffxeqf1); // make the expression: @@ -350,5 +350,9 @@ public: TS_ASSERT(FakeTheory::nothingMoreExpected()); TS_ASSERT_EQUALS(nOut, nExpected); + } catch( TypeCheckingExceptionPrivate& e ) { + cerr << "Type error: " << e.getMessage() << ": " << e.getNode(); + throw; + } } }; diff --git a/test/unit/theory/theory_uf_white.h b/test/unit/theory/theory_uf_white.h index 8e72c428f..f273de30f 100644 --- a/test/unit/theory/theory_uf_white.h +++ b/test/unit/theory/theory_uf_white.h @@ -74,7 +74,8 @@ public: } void testPushPopSimple() { - Node x = d_nm->mkVar(*d_booleanType); + TypeNode t = d_nm->mkSort(); + Node x = d_nm->mkVar(t); Node x_eq_x = x.eqNode(x); d_ctxt->push(); |