diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-04-26 21:37:34 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-04-26 21:37:34 +0000 |
| commit | 3ee48833fd8cffe897a05a986c08a30d9de57213 (patch) | |
| tree | db56dd28b96b12414a763ee9104adc8389225ca5 /test/unit/theory | |
| parent | 96733823eadf9ff566a177cf74e19d1712c48e4b (diff) | |
Adding the intermediary TypeNode to represent (and separate) the Types at the Node level.
Diffstat (limited to 'test/unit/theory')
| -rw-r--r-- | test/unit/theory/theory_black.h | 4 | ||||
| -rw-r--r-- | test/unit/theory/theory_uf_white.h | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 25c22f196..e0dfd7aa8 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -211,8 +211,8 @@ public: void testRegisterTerm() { TS_ASSERT(d_dummy->doneWrapper()); - Type typeX = d_nm->booleanType(); - Type typeF = d_nm->mkFunctionType(typeX, typeX); + TypeNode typeX = d_nm->booleanType(); + TypeNode typeF = d_nm->mkFunctionType(typeX, typeX); Node x = d_nm->mkVar("x",typeX); Node f = d_nm->mkVar("f",typeF); diff --git a/test/unit/theory/theory_uf_white.h b/test/unit/theory/theory_uf_white.h index 44b13c87c..6b14a38d5 100644 --- a/test/unit/theory/theory_uf_white.h +++ b/test/unit/theory/theory_uf_white.h @@ -94,7 +94,7 @@ class TheoryUFWhite : public CxxTest::TestSuite { TheoryUF* d_euf; - Type* d_booleanType; + TypeNode* d_booleanType; public: @@ -107,7 +107,7 @@ public: d_outputChannel.clear(); d_euf = new TheoryUF(d_ctxt, d_outputChannel); - d_booleanType = new Type(d_nm->booleanType()); + d_booleanType = new TypeNode(d_nm->booleanType()); } void tearDown() { |