From: Christopher L. Conway Date: Mon, 5 Apr 2010 14:28:55 +0000 (+0000) Subject: Minor refactorings, in response to code review (Bug #73) X-Git-Tag: cvc5-1.0.0~9135 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=57e51c2212f1c626368c66c6fbcf78ea0ce9722e;p=cvc5.git Minor refactorings, in response to code review (Bug #73) --- diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 6a2640080..bb665ef81 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -184,9 +184,9 @@ Type* ExprManager::mkSort(const std::string& name) { return d_nodeManager->mkSort(name); } -Expr ExprManager::mkVar(Type* type, const std::string& name) { +Expr ExprManager::mkVar(const std::string& name, Type* type) { NodeManagerScope nms(d_nodeManager); - return Expr(this, new Node(d_nodeManager->mkVar(type, name))); + return Expr(this, new Node(d_nodeManager->mkVar(name, type))); } Expr ExprManager::mkVar(Type* type) { diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 1c1d6dbd7..82698732c 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -192,7 +192,7 @@ public: Type* mkSort(const std::string& name); // variables are special, because duplicates are permitted - Expr mkVar(Type* type, const std::string& name); + Expr mkVar(const std::string& name, Type* type); Expr mkVar(Type* type); /** Returns the minimum arity of the given kind. */ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 83f28a842..2b403ad36 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -270,11 +270,11 @@ public: Node mkNode(Kind kind, const std::vector >& children); /** - * Create a variable with the given type and name. NOTE that no - * lookup is done on the name. If you mkVar(type, "a") and then - * mkVar(type, "a") again, you have two variables. + * Create a variable with the given name and type. NOTE that no + * lookup is done on the name. If you mkVar("a", type) and then + * mkVar("a", type) again, you have two variables. */ - Node mkVar(Type* type, const std::string& name); + Node mkVar(const std::string& name, Type* type); /** Create a variable with the given type. */ Node mkVar(Type* type); @@ -767,7 +767,7 @@ inline Node NodeManager::mkNode(Kind kind, return NodeBuilder<>(this, kind).append(children); } -inline Node NodeManager::mkVar(Type* type, const std::string& name) { +inline Node NodeManager::mkVar(const std::string& name, Type* type) { Node n = mkVar(type); n.setAttribute(expr::VarNameAttr(), name); return n; diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index 3d9006e04..61d61821b 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -127,8 +127,6 @@ AntlrInput::recoverFromMismatchedToken(pANTLR3_BASE_RECOGNIZER recognizer, } if(recognizer->mismatchIsMissingToken(recognizer, is, follow)) { - // We can fake the missing token and proceed - // matchedSymbol = recognizer->getMissingSymbol(recognizer, is, recognizer->state->exception, ttype, follow); @@ -136,11 +134,8 @@ AntlrInput::recoverFromMismatchedToken(pANTLR3_BASE_RECOGNIZER recognizer, recognizer->state->exception->message = (void*)ANTLR3_MISSING_TOKEN_EXCEPTION_NAME; recognizer->state->exception->token = matchedSymbol; recognizer->state->exception->expecting = ttype; - - // Print out the error after we insert so that ANTLRWorks sees the - // token in the exception. - // } + reportError(recognizer); Unreachable("reportError should have thrown exception in AntlrInput::recoverFromMismatchedToken"); } @@ -178,7 +173,8 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) { if(ex->expecting == ANTLR3_TOKEN_EOF) { ss << "Expected end of file."; } else { - ss << "Expected " << tokenNames[ex->expecting] << "."; + ss << "Expected " << tokenNames[ex->expecting] + << ", found '" << tokenText((pANTLR3_COMMON_TOKEN)ex->token) << "'."; } } break; @@ -235,14 +231,12 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) { break; case ANTLR3_NO_VIABLE_ALT_EXCEPTION: - // We could not pick any alt decision from the input given // so god knows what happened - however when you examine your grammar, // you should. It means that at the point where the current token occurred // that the DFA indicates nowhere to go from here. // - ss << "Cannot match to any predicted input."; - + ss << "Unexpected token: '" << tokenText((pANTLR3_COMMON_TOKEN)ex->token) << "'."; break; case ANTLR3_MISMATCHED_SET_EXCEPTION: @@ -258,7 +252,8 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) { // possible tokens at this point, but we did not see any // member of that set. // - ss << "Unexpected input. Expected one of : "; + ss << "Unexpected input: '" << tokenText((pANTLR3_COMMON_TOKEN)ex->token) + << "'. Expected one of: "; // What tokens could we have accepted at this point in the // parse? @@ -296,7 +291,8 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) { // but found a token that ended that sequence earlier than // we should have done. // - ss << "Missing elements."; + ss << "Sequence terminated early by token: '" + << tokenText((pANTLR3_COMMON_TOKEN)ex->token) << "'."; break; default: diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 428e2432e..16bde1de3 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -138,7 +138,7 @@ declType[CVC4::Type*& t, std::vector& idList] } : /* A sort declaration (e.g., "T : TYPE") */ TYPE_TOK - { PARSER_STATE->newSorts(idList); + { PARSER_STATE->mkSorts(idList); t = EXPR_MANAGER->kindType(); } | /* A variable declaration */ type[t] { PARSER_STATE->mkVars(idList,t); } diff --git a/src/parser/parser_state.cpp b/src/parser/parser_state.cpp index 9e8ff577e..6cc8f6d9c 100644 --- a/src/parser/parser_state.cpp +++ b/src/parser/parser_state.cpp @@ -94,7 +94,7 @@ bool ParserState::isPredicate(const std::string& name) { Expr ParserState::mkVar(const std::string& name, Type* type) { Debug("parser") << "mkVar(" << name << "," << *type << ")" << std::endl; - Expr expr = d_exprManager->mkVar(type, name); + Expr expr = d_exprManager->mkVar(name, type); defineVar(name,expr); return expr; } @@ -104,7 +104,7 @@ ParserState::mkVars(const std::vector names, Type* type) { std::vector vars; for(unsigned i = 0; i < names.size(); ++i) { - vars.push_back(mkVar(names[i], type)); + vars.push_back(mkVar(names[i],type)); } return vars; } @@ -126,14 +126,14 @@ ParserState::undefineVar(const std::string& name) { void ParserState::setLogic(const std::string& name) { if( name == "QF_UF" ) { - newSort("U"); + mkSort("U"); } else { Unhandled(name); } } Type* -ParserState::newSort(const std::string& name) { +ParserState::mkSort(const std::string& name) { Debug("parser") << "newSort(" << name << ")" << std::endl; Assert( !isDeclared(name, SYM_SORT) ) ; Type* type = d_exprManager->mkSort(name); @@ -143,10 +143,10 @@ ParserState::newSort(const std::string& name) { } const std::vector -ParserState::newSorts(const std::vector& names) { +ParserState::mkSorts(const std::vector& names) { std::vector types; for(unsigned i = 0; i < names.size(); ++i) { - types.push_back(newSort(names[i])); + types.push_back(mkSort(names[i])); } return types; } diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h index 07f85623c..dc188b7d1 100644 --- a/src/parser/parser_state.h +++ b/src/parser/parser_state.h @@ -230,13 +230,13 @@ public: /** * Creates a new sort with the given name. */ - Type* newSort(const std::string& name); + Type* mkSort(const std::string& name); /** * Creates a new sorts with the given names. */ const std::vector - newSorts(const std::vector& names); + mkSorts(const std::vector& names); /** Is the symbol bound to a boolean variable? */ bool isBoolean(const std::string& name); diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index c0b184abf..160bd321f 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -322,7 +322,7 @@ sortDeclaration } : sortName[name,CHECK_UNDECLARED] { Debug("parser") << "sort decl: '" << name << "'" << std::endl; - PARSER_STATE->newSort(name); } + PARSER_STATE->mkSort(name); } ; /** diff --git a/test/unit/expr/expr_black.h b/test/unit/expr/expr_black.h index 03d4ba31c..936381cd6 100644 --- a/test/unit/expr/expr_black.h +++ b/test/unit/expr/expr_black.h @@ -51,8 +51,8 @@ public: try { d_em = new ExprManager; - a = new Expr(d_em->mkVar(d_em->booleanType(), "a")); - b = new Expr(d_em->mkVar(d_em->booleanType(), "b")); + a = new Expr(d_em->mkVar("a",d_em->booleanType())); + b = new Expr(d_em->mkVar("b", d_em->booleanType())); c = new Expr(d_em->mkExpr(MULT, *a, *b)); mult = new Expr(d_em->mkConst(MULT)); plus = new Expr(d_em->mkConst(PLUS)); diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 9e199aa9a..17657683d 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -215,8 +215,8 @@ public: /* We don't have access to the ids so we can't test the implementation * in the black box tests. */ - Node a = d_nodeManager->mkVar(d_nodeManager->booleanType(), "a"); - Node b = d_nodeManager->mkVar(d_nodeManager->booleanType(), "b"); + Node a = d_nodeManager->mkVar("a", d_nodeManager->booleanType()); + Node b = d_nodeManager->mkVar("b", d_nodeManager->booleanType()); TS_ASSERT(abooleanType(); - Node w = d_nodeManager->mkVar(booleanType, "w"); - Node x = d_nodeManager->mkVar(booleanType, "x"); - Node y = d_nodeManager->mkVar(booleanType, "y"); - Node z = d_nodeManager->mkVar(booleanType, "z"); + Node w = d_nodeManager->mkVar("w",booleanType); + Node x = d_nodeManager->mkVar("x",booleanType); + Node y = d_nodeManager->mkVar("y",booleanType); + Node z = d_nodeManager->mkVar("z",booleanType); Node m = NodeBuilder<>() << w << x << kind::OR; Node n = NodeBuilder<>() << m << y << z << kind::AND; @@ -505,10 +505,10 @@ public: void testToStream() { Type* booleanType = d_nodeManager->booleanType(); - Node w = d_nodeManager->mkVar(booleanType, "w"); - Node x = d_nodeManager->mkVar(booleanType, "x"); - Node y = d_nodeManager->mkVar(booleanType, "y"); - Node z = d_nodeManager->mkVar(booleanType, "z"); + Node w = d_nodeManager->mkVar("w",booleanType); + Node x = d_nodeManager->mkVar("x",booleanType); + Node y = d_nodeManager->mkVar("y",booleanType); + Node z = d_nodeManager->mkVar("z",booleanType); Node m = NodeBuilder<>() << x << y << kind::OR; Node n = NodeBuilder<>() << w << m << z << kind::AND; Node o = NodeBuilder<>() << n << n << kind::XOR; diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h deleted file mode 100644 index 5a341830b..000000000 --- a/test/unit/parser/parser_black.h +++ /dev/null @@ -1,294 +0,0 @@ -/********************* */ -/** parser_black.h - ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): dejan, mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information. - ** - ** Black box testing of CVC4::parser::SmtParser. - **/ - -#include -//#include -#include - -#include "expr/expr.h" -#include "expr/expr_manager.h" -#include "parser/input.h" -#include "expr/command.h" -#include "util/output.h" - -using namespace CVC4; -using namespace CVC4::parser; -using namespace std; - - -/************************** CVC test inputs ********************************/ - -const string goodCvc4Inputs[] = { - "", // empty string is OK - "ASSERT TRUE;", - "QUERY TRUE;", - "CHECKSAT FALSE;", - "a, b : BOOLEAN;", - "a, b : BOOLEAN; QUERY (a => b) AND a => b;", - "T, U : TYPE; f : T -> U; x : T; CHECKSAT f(x) = x;", - "T : TYPE; x, y : T; a : BOOLEAN; QUERY (IF a THEN x ELSE y ENDIF) = x;", - "%% nothing but a comment", - "% a comment\nASSERT TRUE; %a command\n% another comment", - }; - -const int numGoodCvc4Inputs = sizeof(goodCvc4Inputs) / sizeof(string); - - -/* The following expressions are valid after setupContext. */ -const string goodCvc4Exprs[] = { - "a AND b", - "a AND b OR c", - "(a => b) AND a => b", - "(a <=> b) AND (NOT a)", - "(a XOR b) <=> (a OR b) AND (NOT (a AND b))" -}; - -const int numGoodCvc4Exprs = sizeof(goodCvc4Exprs) / sizeof(string); - -const string badCvc4Inputs[] = { - ";", // no command - "ASSERT;", // no args - "QUERY", - "CHECKSAT", - "a, b : boolean;", // lowercase boolean isn't a type - "0x : INT;", // 0x isn't an identifier - "a, b : BOOLEAN\nQUERY (a => b) AND a => b;", // no semicolon after decl - "a : BOOLEAN; a: BOOLEAN;" // double decl - "a, b: BOOLEAN; QUERY a(b);" // non-function used as function - }; - -const int numBadCvc4Inputs = sizeof(badCvc4Inputs) / sizeof(string); - -/* The following expressions are invalid even after setupContext. */ -const string badCvc4Exprs[] = { - "a AND", // wrong arity - "AND(a,b)", // not infix - "(OR (AND a b) c)", // not infix - "a IMPLIES b", // should be => - "a NOT b", // wrong arity, not infix - "a and b" // wrong case -}; - -const int numBadCvc4Exprs = sizeof(badCvc4Exprs) / sizeof(string); - -/************************** SMT test inputs ********************************/ - -const string goodSmtInputs[] = { - "", // empty string is OK - "(benchmark foo :assumption true)", - "(benchmark bar :formula true)", - "(benchmark qux :formula false)", - "(benchmark baz :extrapreds ( (a) (b) ) )", - "(benchmark zab :extrapreds ( (a) (b) ) :formula (implies (and (implies a b) a) b))", - "(benchmark zub :extrasorts (a) :extrafuns ( (f a a) (x a) ) :formula (= (f x) x))", - "(benchmark fuz :extrasorts (a) :extrafuns ((x a) (y a)) :formula (= (ite true x y) x))", - ";; nothing but a comment", - "; a comment\n(benchmark foo ; hello\n :formula true; goodbye\n)" - }; - -const int numGoodSmtInputs = sizeof(goodSmtInputs) / sizeof(string); - -/* The following expressions are valid after setupContext. */ -const string goodSmtExprs[] = { - "(and a b)", - "(or (and a b) c)", - "(implies (and (implies a b) a) b)", - "(and (iff a b) (not a))", - "(iff (xor a b) (and (or a b) (not (and a b))))", - "(ite a (f x) y)", - "(if_then_else a (f x) y)" -}; - -const int numGoodSmtExprs = sizeof(goodSmtExprs) / sizeof(string); - -const string badSmtInputs[] = { - "(benchmark foo)", // empty benchmark is not OK - "(benchmark bar :assumption)", // no args - "(benchmark bar :formula)", - "(benchmark baz :extrapreds ( (a) (a) ) )", // double decl - "(benchmark zub :extrasorts (a) :extrapreds (p a))" // (p a) needs parens - }; - -const int numBadSmtInputs = sizeof(badSmtInputs) / sizeof(string); - -/* The following expressions are invalid even after setupContext. */ -const string badSmtExprs[] = { - "(and)", // wrong arity - "(and a b", // no closing paren - "(a and b)", // infix - "(OR (AND a b) c)", // wrong case - "(a IMPLIES b)", // infix AND wrong case - "(not a b)", // wrong arity - "not a", // needs parens - "(ite a x)", // wrong arity - "(a b)" // using non-function as function -}; - -const int numBadSmtExprs = sizeof(badSmtExprs) / sizeof(string); - -class ParserBlack : public CxxTest::TestSuite { - ExprManager *d_exprManager; - - /* Set up declaration context for expr inputs */ - - void setupContext(Input* input) { - /* a, b, c: BOOLEAN */ - input->mkVar("a",(Type*)d_exprManager->booleanType()); - input->mkVar("b",(Type*)d_exprManager->booleanType()); - input->mkVar("c",(Type*)d_exprManager->booleanType()); - /* t, u, v: TYPE */ - Type *t = input->newSort("t"); - Type *u = input->newSort("u"); - Type *v = input->newSort("v"); - /* f : t->u; g: u->v; h: v->t; */ - input->mkVar("f", (Type*)d_exprManager->mkFunctionType(t,u)); - input->mkVar("g", (Type*)d_exprManager->mkFunctionType(u,v)); - input->mkVar("h", (Type*)d_exprManager->mkFunctionType(v,t)); - /* x:t; y:u; z:v; */ - input->mkVar("x",t); - input->mkVar("y",u); - input->mkVar("z",v); - } - - void tryGoodInputs(InputLanguage d_lang, const string goodInputs[], int numInputs) { - for(int i = 0; i < numInputs; ++i) { - try { -// Debug.on("parser"); -// Debug.on("parser-extra"); - Debug("test") << "Testing good input: '" << goodInputs[i] << "'\n"; -// istringstream stream(goodInputs[i]); - Input* parser = Input::newStringParser(d_exprManager, d_lang, goodInputs[i], "test"); - TS_ASSERT( !parser->done() ); - Command* cmd; - while((cmd = parser->parseNextCommand())) { - // cout << "Parsed command: " << (*cmd) << endl; - } - TS_ASSERT( parser->parseNextCommand() == NULL ); - TS_ASSERT( parser->done() ); - delete parser; -// Debug.off("parser"); -// Debug.off("parser-extra"); - } catch (Exception& e) { - cout << "\nGood input failed:\n" << goodInputs[i] << endl - << e << endl; -// Debug.off("parser-extra"); - throw; - } - } - } - - void tryBadInputs(InputLanguage d_lang, const string badInputs[], int numInputs) { - for(int i = 0; i < numInputs; ++i) { -// cout << "Testing bad input: '" << badInputs[i] << "'\n"; -// Debug.on("parser"); - Input* parser = Input::newStringParser(d_exprManager, d_lang, badInputs[i], "test"); - TS_ASSERT_THROWS - ( while(parser->parseNextCommand()); - cout << "\nBad input succeeded:\n" << badInputs[i] << endl;, - ParserException ); -// Debug.off("parser"); - delete parser; - } - } - - void tryGoodExprs(InputLanguage d_lang, const string goodBooleanExprs[], int numExprs) { - // cout << "Using context: " << context << endl; -// Debug.on("parser"); -// Debug.on("parser-extra"); - for(int i = 0; i < numExprs; ++i) { - try { - // cout << "Testing good expr: '" << goodBooleanExprs[i] << "'\n"; - // Debug.on("parser"); -// istringstream stream(context + goodBooleanExprs[i]); - Input* parser = Input::newStringParser(d_exprManager, d_lang, - goodBooleanExprs[i], "test"); - TS_ASSERT( !parser->done() ); - setupContext(parser); - TS_ASSERT( !parser->done() ); - Expr e = parser->parseNextExpression(); - TS_ASSERT( !e.isNull() ); - e = parser->parseNextExpression(); - TS_ASSERT( parser->done() ); - TS_ASSERT( e.isNull() ); - delete parser; - } catch (Exception& e) { - cout << "\nGood expr failed:\n" << goodBooleanExprs[i] << endl; - cout << e; - throw e; - } - } - } - - void tryBadExprs(InputLanguage d_lang, const string badBooleanExprs[], int numExprs) { - //Debug.on("parser"); - for(int i = 0; i < numExprs; ++i) { - // cout << "Testing bad expr: '" << badBooleanExprs[i] << "'\n"; -// istringstream stream(context + badBooleanExprs[i]); - Input* parser = Input::newStringParser(d_exprManager, d_lang, - badBooleanExprs[i], "test"); - - TS_ASSERT( !parser->done() ); - setupContext(parser); - TS_ASSERT( !parser->done() ); - TS_ASSERT_THROWS - ( parser->parseNextExpression(); - cout << "\nBad expr succeeded: " << badBooleanExprs[i] << endl;, - ParserException ); - delete parser; - } - //Debug.off("parser"); - } - -public: - void setUp() { - d_exprManager = new ExprManager(); - } - - void tearDown() { - delete d_exprManager; - } - - void testGoodCvc4Inputs() { - tryGoodInputs(LANG_CVC4,goodCvc4Inputs,numGoodCvc4Inputs); - } - - void testBadCvc4Inputs() { - tryBadInputs(LANG_CVC4,badCvc4Inputs,numBadCvc4Inputs); - } - - void testGoodCvc4Exprs() { - tryGoodExprs(LANG_CVC4,goodCvc4Exprs,numGoodCvc4Exprs); - } - - void testBadCvc4Exprs() { - tryBadExprs(LANG_CVC4,badCvc4Exprs,numBadCvc4Exprs); - } - - void testGoodSmtInputs() { - tryGoodInputs(LANG_SMTLIB,goodSmtInputs,numGoodSmtInputs); - } - - void testBadSmtInputs() { - tryBadInputs(LANG_SMTLIB,badSmtInputs,numBadSmtInputs); - } - - void testGoodSmtExprs() { - tryGoodExprs(LANG_SMTLIB,goodSmtExprs,numGoodSmtExprs); - } - - void testBadSmtExprs() { - tryBadExprs(LANG_SMTLIB,badSmtExprs,numBadSmtExprs); - } -}; diff --git a/test/unit/parser/parser_white.h b/test/unit/parser/parser_white.h index 270061c29..d0959cf6f 100644 --- a/test/unit/parser/parser_white.h +++ b/test/unit/parser/parser_white.h @@ -150,9 +150,9 @@ class ParserWhite : public CxxTest::TestSuite { parserState->mkVar("b",(Type*)d_exprManager->booleanType()); parserState->mkVar("c",(Type*)d_exprManager->booleanType()); /* t, u, v: TYPE */ - Type *t = parserState->newSort("t"); - Type *u = parserState->newSort("u"); - Type *v = parserState->newSort("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)); diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index c6da48291..905294c27 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -214,8 +214,8 @@ public: Type* typeX = d_nm->booleanType(); Type* typeF = d_nm->mkFunctionType(typeX, typeX); - Node x = d_nm->mkVar(typeX, "x"); - Node f = d_nm->mkVar(typeF, "f"); + Node x = d_nm->mkVar("x",typeX); + Node f = d_nm->mkVar("f",typeF); Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x); Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x); Node f_x_eq_x = f_x.eqNode(x);