From f8ca588548491146fffbf22b2e9082986504211c Mon Sep 17 00:00:00 2001 From: Dejan Jovanović Date: Wed, 14 Apr 2010 19:06:53 +0000 Subject: Marging from types 404:415, changes: Massive * Types are now represented as nodes in the attribute table and are managed, i.e. you can say Type booleanType = d_nodeManager->booleanType(); Type t = d_nodeManager->mkFunctionType(booleanType, booleanType); FunctionType ft = (FunctionType)t; Assert(ft.getArgTypes()[0], booleanType); * The attributes now have a table for Nodes and a table for TNodes (both should be used with caution) * Changes the way nodes are extracted from NodeBuilder, added several methods to extract a Node, NodeValue, or Node*, with corresponding methods for extraction * Used the above in the construction of Expr and Type objects * The NodeManager now destroys the attributes in the destructor by pausing the garbage collection * To achive destruction a flag d_inDesctruction has been added to loosen the assertion in NodeValue::dec() (there might be -refcount TNodes leftover) * Beginnings of the Bitvector constants using GMP Not yet in tiptop phase, needs more documentation, and Types should be pulled out to TypeNodes eventually. Also, the types are currently defined in the builting_kinds, and I need to add these to the theory specific definitions with special 'type' constructs. I hate branching and merging. --- test/unit/parser/parser_white.h | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) (limited to 'test/unit/parser') diff --git a/test/unit/parser/parser_white.h b/test/unit/parser/parser_white.h index 653e3a1d7..317817e15 100644 --- a/test/unit/parser/parser_white.h +++ b/test/unit/parser/parser_white.h @@ -146,17 +146,17 @@ class ParserWhite : public CxxTest::TestSuite { void setupContext(ParserState* parserState) { /* a, b, c: BOOLEAN */ - parserState->mkVar("a",(Type*)d_exprManager->booleanType()); - parserState->mkVar("b",(Type*)d_exprManager->booleanType()); - parserState->mkVar("c",(Type*)d_exprManager->booleanType()); + parserState->mkVar("a",d_exprManager->booleanType()); + parserState->mkVar("b",d_exprManager->booleanType()); + parserState->mkVar("c",d_exprManager->booleanType()); /* t, u, v: TYPE */ - Type *t = parserState->mkSort("t"); - Type *u = parserState->mkSort("u"); - Type *v = parserState->mkSort("v"); + Type t = parserState->mkSort("t"); + Type u = parserState->mkSort("u"); + Type v = parserState->mkSort("v"); /* f : t->u; g: u->v; h: v->t; */ - parserState->mkVar("f", (Type*)d_exprManager->mkFunctionType(t,u)); - parserState->mkVar("g", (Type*)d_exprManager->mkFunctionType(u,v)); - parserState->mkVar("h", (Type*)d_exprManager->mkFunctionType(v,t)); + parserState->mkVar("f", d_exprManager->mkFunctionType(t,u)); + parserState->mkVar("g", d_exprManager->mkFunctionType(u,v)); + parserState->mkVar("h", d_exprManager->mkFunctionType(v,t)); /* x:t; y:u; z:v; */ parserState->mkVar("x",t); parserState->mkVar("y",u); -- cgit v1.2.3