From 267858307741675cb78e829270e619f57cf21a27 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 18 Apr 2011 18:05:39 +0000 Subject: [PATCH] mostly CVC presentation language parsing and printing --- src/expr/expr_manager_template.cpp | 172 +++- src/expr/expr_manager_template.h | 97 ++- src/expr/node_manager.h | 113 ++- src/parser/cvc/Cvc.g | 881 +++++++++++++++----- src/parser/smt2/Smt2.g | 1 + src/printer/cvc/cvc_printer.cpp | 65 ++ test/regress/regress0/precedence/or-xor.cvc | 3 +- test/unit/parser/parser_black.h | 12 +- test/unit/util/datatype_black.h | 4 + 9 files changed, 1078 insertions(+), 270 deletions(-) diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 21fc0a4a1..870c77383 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -136,8 +136,8 @@ IntegerType ExprManager::integerType() const { return IntegerType(Type(d_nodeManager, new TypeNode(d_nodeManager->integerType()))); } -Expr ExprManager::mkExpr(Kind kind, const Expr& child1) { - const unsigned n = 1; +Expr ExprManager::mkExpr(Kind kind, Expr child1) { + const unsigned n = 1 - (kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED ? 1 : 0); CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, "Exprs with kind %s must have at least %u children and " "at most %u children (the one under construction has %u)", @@ -152,8 +152,8 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1) { } } -Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) { - const unsigned n = 2; +Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2) { + const unsigned n = 2 - (kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED ? 1 : 0); CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, "Exprs with kind %s must have at least %u children and " "at most %u children (the one under construction has %u)", @@ -170,9 +170,9 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) { } } -Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, - const Expr& child3) { - const unsigned n = 3; +Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, + Expr child3) { + const unsigned n = 3 - (kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED ? 1 : 0); CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, "Exprs with kind %s must have at least %u children and " "at most %u children (the one under construction has %u)", @@ -190,9 +190,9 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, } } -Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, - const Expr& child3, const Expr& child4) { - const unsigned n = 4; +Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, + Expr child3, Expr child4) { + const unsigned n = 4 - (kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED ? 1 : 0); CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, "Exprs with kind %s must have at least %u children and " "at most %u children (the one under construction has %u)", @@ -211,10 +211,10 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, } } -Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, - const Expr& child3, const Expr& child4, - const Expr& child5) { - const unsigned n = 5; +Expr ExprManager::mkExpr(Kind kind, Expr child1, Expr child2, + Expr child3, Expr child4, + Expr child5) { + const unsigned n = 5 - (kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED ? 1 : 0); CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, "Exprs with kind %s must have at least %u children and " "at most %u children (the one under construction has %u)", @@ -235,7 +235,7 @@ Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, } Expr ExprManager::mkExpr(Kind kind, const std::vector& children) { - const unsigned n = children.size(); + const unsigned n = children.size() - (kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED ? 1 : 0); CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, "Exprs with kind %s must have at least %u children and " "at most %u children (the one under construction has %u)", @@ -259,9 +259,141 @@ Expr ExprManager::mkExpr(Kind kind, const std::vector& children) { } } +Expr ExprManager::mkExpr(Expr opExpr) { + const unsigned n = 0; + Kind kind = kind::operatorKindToKind(opExpr.getKind()); + CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr, + "This Expr constructor is for parameterized kinds only"); + CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); + NodeManagerScope nms(d_nodeManager); + try { + INC_STAT(kind); + return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode())); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} + +Expr ExprManager::mkExpr(Expr opExpr, Expr child1) { + const unsigned n = 1; + Kind kind = kind::operatorKindToKind(opExpr.getKind()); + CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr, + "This Expr constructor is for parameterized kinds only"); + CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); + NodeManagerScope nms(d_nodeManager); + try { + INC_STAT(kind); + return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(), child1.getNode())); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} + +Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2) { + const unsigned n = 2; + Kind kind = kind::operatorKindToKind(opExpr.getKind()); + CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr, + "This Expr constructor is for parameterized kinds only"); + CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); + NodeManagerScope nms(d_nodeManager); + try { + INC_STAT(kind); + return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(), + child1.getNode(), + child2.getNode())); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} + +Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3) { + const unsigned n = 3; + Kind kind = kind::operatorKindToKind(opExpr.getKind()); + CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr, + "This Expr constructor is for parameterized kinds only"); + CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); + NodeManagerScope nms(d_nodeManager); + try { + INC_STAT(kind); + return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(), + child1.getNode(), + child2.getNode(), + child3.getNode())); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} + +Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, + Expr child4) { + const unsigned n = 4; + Kind kind = kind::operatorKindToKind(opExpr.getKind()); + CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr, + "This Expr constructor is for parameterized kinds only"); + CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); + NodeManagerScope nms(d_nodeManager); + try { + INC_STAT(kind); + return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(), + child1.getNode(), + child2.getNode(), + child3.getNode(), + child4.getNode())); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} + +Expr ExprManager::mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, + Expr child4, Expr child5) { + const unsigned n = 5; + Kind kind = kind::operatorKindToKind(opExpr.getKind()); + CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr, + "This Expr constructor is for parameterized kinds only"); + CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, + "Exprs with kind %s must have at least %u children and " + "at most %u children (the one under construction has %u)", + kind::kindToString(kind).c_str(), + minArity(kind), maxArity(kind), n); + NodeManagerScope nms(d_nodeManager); + try { + INC_STAT(kind); + return Expr(this, d_nodeManager->mkNodePtr(opExpr.getNode(), + child1.getNode(), + child2.getNode(), + child3.getNode(), + child4.getNode(), + child5.getNode())); + } catch (const TypeCheckingExceptionPrivate& e) { + throw TypeCheckingException(this, &e); + } +} + Expr ExprManager::mkExpr(Expr opExpr, const std::vector& children) { const unsigned n = children.size(); Kind kind = kind::operatorKindToKind(opExpr.getKind()); + CheckArgument(kind::metaKindOf(kind) == kind::metakind::PARAMETERIZED, opExpr, + "This Expr constructor is for parameterized kinds only"); CheckArgument(n >= minArity(kind) && n <= maxArity(kind), kind, "Exprs with kind %s must have at least %u children and " "at most %u children (the one under construction has %u)", @@ -286,13 +418,13 @@ Expr ExprManager::mkExpr(Expr opExpr, const std::vector& children) { } /** Make a function type from domain to range. */ -FunctionType ExprManager::mkFunctionType(const Type& domain, const Type& range) { +FunctionType ExprManager::mkFunctionType(Type domain, Type range) { NodeManagerScope nms(d_nodeManager); return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(*domain.d_typeNode, *range.d_typeNode)))); } /** Make a function type with input types from argTypes. */ -FunctionType ExprManager::mkFunctionType(const std::vector& argTypes, const Type& range) { +FunctionType ExprManager::mkFunctionType(const std::vector& argTypes, Type range) { NodeManagerScope nms(d_nodeManager); Assert( argTypes.size() >= 1 ); std::vector argTypeNodes; @@ -436,7 +568,7 @@ SortConstructorType ExprManager::mkSortConstructor(const std::string& name, * @param check whether we should check the type as we compute it * (default: false) */ -Type ExprManager::getType(const Expr& e, bool check) throw (TypeCheckingException) { +Type ExprManager::getType(Expr e, bool check) throw (TypeCheckingException) { NodeManagerScope nms(d_nodeManager); Type t; try { @@ -448,7 +580,7 @@ Type ExprManager::getType(const Expr& e, bool check) throw (TypeCheckingExceptio return t; } -Expr ExprManager::mkVar(const std::string& name, const Type& type) { +Expr ExprManager::mkVar(const std::string& name, Type type) { NodeManagerScope nms(d_nodeManager); Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode); Debug("nm") << "set " << name << " on " << *n << std::endl; @@ -456,7 +588,7 @@ Expr ExprManager::mkVar(const std::string& name, const Type& type) { return Expr(this, n); } -Expr ExprManager::mkVar(const Type& type) { +Expr ExprManager::mkVar(Type type) { NodeManagerScope nms(d_nodeManager); INC_STAT_VAR(type); return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode)); diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 415d05878..31ce7855a 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -127,7 +127,7 @@ public: * @param child1 kind the kind of expression * @return the expression */ - Expr mkExpr(Kind kind, const Expr& child1); + Expr mkExpr(Kind kind, Expr child1); /** * Make a binary expression of a given kind (AND, PLUS, ...). @@ -136,7 +136,7 @@ public: * @param child2 the second child of the new expression * @return the expression */ - Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2); + Expr mkExpr(Kind kind, Expr child1, Expr child2); /** * Make a 3-ary expression of a given kind (AND, PLUS, ...). @@ -146,8 +146,7 @@ public: * @param child3 the third child of the new expression * @return the expression */ - Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2, - const Expr& child3); + Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3); /** * Make a 4-ary expression of a given kind (AND, PLUS, ...). @@ -158,8 +157,7 @@ public: * @param child4 the fourth child of the new expression * @return the expression */ - Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2, - const Expr& child3, const Expr& child4); + Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4); /** * Make a 5-ary expression of a given kind (AND, PLUS, ...). @@ -171,11 +169,13 @@ public: * @param child5 the fifth child of the new expression * @return the expression */ - Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2, - const Expr& child3, const Expr& child4, const Expr& child5); + Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, + Expr child5); /** - * Make an n-ary expression of given kind given a vector of it's children + * Make an n-ary expression of given kind given a vector of its + * children + * * @param kind the kind of expression to build * @param children the subexpressions * @return the n-ary expression @@ -183,8 +183,73 @@ public: Expr mkExpr(Kind kind, const std::vector& children); /** - * Make an n-ary expression of given tre operator to appply and a vector of - * it's children + * Make a nullary parameterized expression with the given operator. + * + * @param opExpr the operator expression + * @return the nullary expression + */ + Expr mkExpr(Expr opExpr); + + /** + * Make a unary parameterized expression with the given operator. + * + * @param opExpr the operator expression + * @param child1 the subexpression + * @return the unary expression + */ + Expr mkExpr(Expr opExpr, Expr child1); + + /** + * Make a binary parameterized expression with the given operator. + * + * @param opExpr the operator expression + * @param child1 the first subexpression + * @param child2 the second subexpression + * @return the binary expression + */ + Expr mkExpr(Expr opExpr, Expr child1, Expr child2); + + /** + * Make a ternary parameterized expression with the given operator. + * + * @param opExpr the operator expression + * @param child1 the first subexpression + * @param child2 the second subexpression + * @param child3 the third subexpression + * @return the ternary expression + */ + Expr mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3); + + /** + * Make a quaternary parameterized expression with the given operator. + * + * @param opExpr the operator expression + * @param child1 the first subexpression + * @param child2 the second subexpression + * @param child3 the third subexpression + * @param child4 the fourth subexpression + * @return the quaternary expression + */ + Expr mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, Expr child4); + + /** + * Make a quinary parameterized expression with the given operator. + * + * @param opExpr the operator expression + * @param child1 the first subexpression + * @param child2 the second subexpression + * @param child3 the third subexpression + * @param child4 the fourth subexpression + * @param child5 the fifth subexpression + * @return the quinary expression + */ + Expr mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, Expr child4, + Expr child5); + + /** + * Make an n-ary expression of given operator to apply and a vector + * of its children + * * @param opExpr the operator expression * @param children the subexpressions * @return the n-ary expression @@ -210,13 +275,13 @@ public: /** Make a function type from domain to range. */ - FunctionType mkFunctionType(const Type& domain, const Type& range); + FunctionType mkFunctionType(Type domain, Type range); /** * Make a function type with input types from argTypes. * argTypes must have at least one element. */ - FunctionType mkFunctionType(const std::vector& argTypes, const Type& range); + FunctionType mkFunctionType(const std::vector& argTypes, Type range); /** * Make a function type with input types from @@ -279,12 +344,12 @@ public: size_t arity) const; /** Get the type of an expression */ - Type getType(const Expr& e, bool check = false) + Type getType(Expr e, bool check = false) throw (TypeCheckingException); // variables are special, because duplicates are permitted - Expr mkVar(const std::string& name, const Type& type); - Expr mkVar(const Type& type); + Expr mkVar(const std::string& name, Type type); + Expr mkVar(Type type); /** Returns the minimum arity of the given kind. */ static unsigned minArity(Kind kind); diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 7f7d37a52..94b7e5c40 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -303,7 +303,35 @@ public: template Node* mkNodePtr(Kind kind, const std::vector >& children); - /** Create a node by applying an operator to the children */ + /** Create a node (with no children) by operator. */ + Node mkNode(TNode opNode); + Node* mkNodePtr(TNode opNode); + + /** Create a node with one child by operator. */ + Node mkNode(TNode opNode, TNode child1); + Node* mkNodePtr(TNode opNode, TNode child1); + + /** Create a node with two children by operator. */ + Node mkNode(TNode opNode, TNode child1, TNode child2); + Node* mkNodePtr(TNode opNode, TNode child1, TNode child2); + + /** Create a node with three children by operator. */ + Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3); + Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3); + + /** Create a node with four children by operator. */ + Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3, + TNode child4); + Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3, + TNode child4); + + /** Create a node with five children by operator. */ + Node mkNode(TNode opNode, TNode child1, TNode child2, TNode child3, + TNode child4, TNode child5); + Node* mkNodePtr(TNode opNode, TNode child1, TNode child2, TNode child3, + TNode child4, TNode child5); + + /** Create a node by applying an operator to the children. */ template Node mkNode(TNode opNode, const std::vector >& children); template @@ -1021,6 +1049,85 @@ inline Node* NodeManager::mkNodePtr(Kind kind, return nb.constructNodePtr(); } +// for operators +inline Node NodeManager::mkNode(TNode opNode) { + NodeBuilder<1> nb(this, kind::operatorKindToKind(opNode.getKind())); + nb << opNode; + return nb.constructNode(); +} + +inline Node* NodeManager::mkNodePtr(TNode opNode) { + NodeBuilder<1> nb(this, kind::operatorKindToKind(opNode.getKind())); + nb << opNode; + return nb.constructNodePtr(); +} + +inline Node NodeManager::mkNode(TNode opNode, TNode child1) { + NodeBuilder<2> nb(this, kind::operatorKindToKind(opNode.getKind())); + nb << opNode << child1; + return nb.constructNode(); +} + +inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1) { + NodeBuilder<2> nb(this, kind::operatorKindToKind(opNode.getKind())); + nb << opNode << child1; + return nb.constructNodePtr(); +} + +inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2) { + NodeBuilder<3> nb(this, kind::operatorKindToKind(opNode.getKind())); + nb << opNode << child1 << child2; + return nb.constructNode(); +} + +inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2) { + NodeBuilder<3> nb(this, kind::operatorKindToKind(opNode.getKind())); + nb << opNode << child1 << child2; + return nb.constructNodePtr(); +} + +inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2, + TNode child3) { + NodeBuilder<4> nb(this, kind::operatorKindToKind(opNode.getKind())); + nb << opNode << child1 << child2 << child3; + return nb.constructNode(); +} + +inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2, + TNode child3) { + NodeBuilder<4> nb(this, kind::operatorKindToKind(opNode.getKind())); + nb << opNode << child1 << child2 << child3; + return nb.constructNodePtr(); +} + +inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2, + TNode child3, TNode child4) { + NodeBuilder<5> nb(this, kind::operatorKindToKind(opNode.getKind())); + nb << opNode << child1 << child2 << child3 << child4; + return nb.constructNode(); +} + +inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2, + TNode child3, TNode child4) { + NodeBuilder<5> nb(this, kind::operatorKindToKind(opNode.getKind())); + nb << opNode << child1 << child2 << child3 << child4; + return nb.constructNodePtr(); +} + +inline Node NodeManager::mkNode(TNode opNode, TNode child1, TNode child2, + TNode child3, TNode child4, TNode child5) { + NodeBuilder<6> nb(this, kind::operatorKindToKind(opNode.getKind())); + nb << opNode << child1 << child2 << child3 << child4 << child5; + return nb.constructNode(); +} + +inline Node* NodeManager::mkNodePtr(TNode opNode, TNode child1, TNode child2, + TNode child3, TNode child4, TNode child5) { + NodeBuilder<6> nb(this, kind::operatorKindToKind(opNode.getKind())); + nb << opNode << child1 << child2 << child3 << child4 << child5; + return nb.constructNodePtr(); +} + // N-ary version for operators template inline Node NodeManager::mkNode(TNode opNode, @@ -1034,8 +1141,8 @@ inline Node NodeManager::mkNode(TNode opNode, template inline Node* NodeManager::mkNodePtr(TNode opNode, - const std::vector >& - children) { + const std::vector >& + children) { NodeBuilder<> nb(this, kind::operatorKindToKind(opNode.getKind())); nb << opNode; nb.append(children); diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 33e576a32..96a8346b0 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -24,6 +24,323 @@ options { k = 2; } +tokens { + // Keywords + + AND_TOK = 'AND'; + ASSERT_TOK = 'ASSERT'; + BOOLEAN_TOK = 'BOOLEAN'; + CHECKSAT_TOK = 'CHECKSAT'; + ECHO_TOK = 'ECHO'; + ELSEIF_TOK = 'ELSIF'; + ELSE_TOK = 'ELSE'; + ENDIF_TOK = 'ENDIF'; + FALSE_TOK = 'FALSE'; + IF_TOK = 'IF'; + IN_TOK = 'IN'; + INT_TOK = 'INT'; + LET_TOK = 'LET'; + NOT_TOK = 'NOT'; + OPTION_TOK = 'OPTION'; + OR_TOK = 'OR'; + POPTO_TOK = 'POPTO'; + POP_TOK = 'POP'; + PRINT_TOK = 'PRINT'; + PUSH_TOK = 'PUSH'; + QUERY_TOK = 'QUERY'; + REAL_TOK = 'REAL'; + THEN_TOK = 'THEN'; + TRUE_TOK = 'TRUE'; + TYPE_TOK = 'TYPE'; + XOR_TOK = 'XOR'; + + DATATYPE_TOK = 'DATATYPE'; + END_TOK = 'END'; + + ARRAY_TOK = 'ARRAY'; + OF_TOK = 'OF'; + WITH_TOK = 'WITH'; + + FORALL_TOK = 'FORALL'; + EXISTS_TOK = 'EXISTS'; + + // Symbols + + COLON = ':'; + COMMA = ','; + LPAREN = '('; + RPAREN = ')'; + LBRACE = '{'; + RBRACE = '}'; + LBRACKET = '['; + RBRACKET = ']'; + SEMICOLON = ';'; + BAR = '|'; + DOT = '.'; + + SQHASH = '[#'; + HASHSQ = '#]'; + PARENHASH = '(#'; + HASHPAREN = '#)'; + + // Operators + + ARROW_TOK = '->'; + DIV_TOK = '/'; + EQUAL_TOK = '='; + DISEQUAL_TOK = '/='; + EXP_TOK = '^'; + GT_TOK = '>'; + GEQ_TOK = '>='; + IFF_TOK = '<=>'; + IMPLIES_TOK = '=>'; + LT_TOK = '<'; + LEQ_TOK = '<='; + MINUS_TOK = '-'; + PLUS_TOK = '+'; + STAR_TOK = '*'; + ASSIGN_TOK = ':='; + MOD_TOK = 'MOD'; + INTDIV_TOK = 'DIV'; + FLOOR_TOK = 'FLOOR'; + + //IS_INTEGER_TOK = 'IS_INTEGER'; + + // Bitvectors + + BITVECTOR_TOK = 'BITVECTOR'; + LEFTSHIFT_TOK = '<<'; + RIGHTSHIFT_TOK = '>>'; + BVPLUS_TOK = 'BVPLUS'; + BVSUB_TOK = 'BVSUB'; + BVUDIV_TOK = 'BVUDIV'; + BVSDIV_TOK = 'BVSDIV'; + BVUREM_TOK = 'BVUREM'; + BVSREM_TOK = 'BVSREM'; + BVSMOD_TOK = 'BVSMOD'; + BVSHL_TOK = 'BVSHL'; + BVASHR_TOK = 'BVASHR'; + BVLSHR_TOK = 'BVLSHR'; + BVUMINUS_TOK = 'BVUMINUS'; + BVMULT_TOK = 'BVMULT'; + BVNEG_TOK = '~'; + BVAND_TOK = '&'; + BVXOR_TOK = 'BVXOR'; + BVNAND_TOK = 'BVNAND'; + BVNOR_TOK = 'BVNOR'; + BVCOMP_TOK = 'BVCOMP'; + BVXNOR_TOK = 'BVXNOR'; + CONCAT_TOK = '@'; + BVTOINT_TOK = 'BVTOINT'; + INTTOBV_TOK = 'INTTOBV'; + BOOLEXTRACT_TOK = 'BOOLEXTRACT'; + BVLT_TOK = 'BVLT'; + BVGT_TOK = 'BVGT'; + BVLE_TOK = 'BVLE'; + BVGE_TOK = 'BVGE'; + SX_TOK = 'SX'; + BVZEROEXTEND_TOK = 'BVZEROEXTEND'; + BVREPEAT_TOK = 'BVREPEAT'; + BVROTL_TOK = 'BVROTL'; + BVROTR_TOK = 'BVROTR'; + BVSLT_TOK = 'BVSLT'; + BVSGT_TOK = 'BVSGT'; + BVSLE_TOK = 'BVSLE'; + BVSGE_TOK = 'BVSGE'; +} + +@parser::members { + +// Idea and code guidance from Sam Harwell, +// http://www.antlr.org/wiki/display/ANTLR3/Operator+precedence+parser + +bool isRightToLeft(int type) { + // return true here for any operators that are right-to-left associative + switch(type) { + case IMPLIES_TOK: return true; + default: return false; + } +} + +int getOperatorPrecedence(int type) { + switch(type) { + case BITVECTOR_TOK: return 1; + case DOT: + case LPAREN: + case LBRACE: return 2; + case LBRACKET: return 3; + case ARROW_TOK: return 4; + //case IS_INTEGER_TOK: return 5; + case BVSLT_TOK: + case BVSLE_TOK: + case BVSGT_TOK: + case BVSGE_TOK: return 6; + case BVLT_TOK: + case BVLE_TOK: + case BVGT_TOK: + case BVGE_TOK: return 7; + case LEFTSHIFT_TOK: + case RIGHTSHIFT_TOK: return 8; + case SX_TOK: + case BVZEROEXTEND_TOK: + case BVREPEAT_TOK: + case BVROTL_TOK: + case BVROTR_TOK: return 9; + case BVUDIV_TOK: + case BVSDIV_TOK: + case BVUREM_TOK: + case BVSREM_TOK: + case BVSMOD_TOK: + case BVSHL_TOK: + case BVASHR_TOK: + case BVLSHR_TOK: return 10; + case BVUMINUS_TOK: + case BVPLUS_TOK: + case BVSUB_TOK: return 11; + case BVNEG_TOK: return 12; + case BVXNOR_TOK: return 13; + case BVNOR_TOK: + case BVCOMP_TOK: return 14; + case BVNAND_TOK: return 15; + case BVXOR_TOK: return 16; + case BVAND_TOK: return 17; + case BAR: return 18; + case CONCAT_TOK: return 19; +//case UMINUS_TOK: return 20; + case WITH_TOK: return 21; + case EXP_TOK: return 22; + case STAR_TOK: + case INTDIV_TOK: + case DIV_TOK: + case MOD_TOK: return 23; + case PLUS_TOK: + case MINUS_TOK: return 24; + case LEQ_TOK: + case LT_TOK: + case GEQ_TOK: + case GT_TOK: + case FLOOR_TOK: return 25; + case EQUAL_TOK: + case DISEQUAL_TOK: return 26; + case NOT_TOK: return 27; + case AND_TOK: return 28; + case OR_TOK: + case XOR_TOK: return 29; + case IMPLIES_TOK: return 30;// right-to-left + case IFF_TOK: return 31; + case FORALL_TOK: + case EXISTS_TOK: return 32; + case ASSIGN_TOK: + case IN_TOK: return 33; + + default: + Unhandled(CvcParserTokenNames[type]); + } +} + +Kind getOperatorKind(int type, bool& negate) { + negate = false; + + switch(type) { + // booleanBinop + case IFF_TOK: return kind::IFF; + case IMPLIES_TOK: return kind::IMPLIES; + case OR_TOK: return kind::OR; + case XOR_TOK: return kind::XOR; + case AND_TOK: return kind::AND; + + // comparisonBinop + case EQUAL_TOK: return kind::EQUAL; + case DISEQUAL_TOK: negate = true; return kind::EQUAL; + case GT_TOK: return kind::GT; + case GEQ_TOK: return kind::GEQ; + case LT_TOK: return kind::LT; + case LEQ_TOK: return kind::LEQ; + + // arithmeticBinop + case PLUS_TOK: return kind::PLUS; + case MINUS_TOK: return kind::MINUS; + case STAR_TOK: return kind::MULT; + case INTDIV_TOK: Unhandled(CvcParserTokenNames[type]); + case DIV_TOK: return kind::DIVISION; + case EXP_TOK: Unhandled(CvcParserTokenNames[type]); + + // concatBitwiseBinop + case CONCAT_TOK: return kind::BITVECTOR_CONCAT; + case BAR: return kind::BITVECTOR_OR; + case BVAND_TOK: return kind::BITVECTOR_AND; + + default: + Unhandled(CvcParserTokenNames[type]); + } +} + +unsigned findPivot(const std::vector& operators, + unsigned startIndex, unsigned stopIndex) { + unsigned pivot = startIndex; + unsigned pivotRank = getOperatorPrecedence(operators[pivot]); + /*Debug("prec") << "initial pivot at " << pivot + << "(" << CvcParserTokenNames[operators[pivot]] << ") " + << "level " << pivotRank << std::endl;*/ + for(unsigned i = startIndex + 1; i <= stopIndex; ++i) { + unsigned current = getOperatorPrecedence(operators[i]); + bool rtl = isRightToLeft(operators[i]); + if(current > pivotRank || (current == pivotRank && !rtl)) { + /*Debug("prec") << "new pivot at " << i + << "(" << CvcParserTokenNames[operators[i]] << ") " + << "level " << current << " rtl == " << rtl << std::endl;*/ + pivot = i; + pivotRank = current; + } + } + return pivot; +} + +Expr createPrecedenceTree(ExprManager* em, + const std::vector& expressions, + const std::vector& operators, + unsigned startIndex, unsigned stopIndex) { + Assert(expressions.size() == operators.size() + 1); + Assert(startIndex < expressions.size()); + Assert(stopIndex < expressions.size()); + Assert(startIndex <= stopIndex); + + if(stopIndex == startIndex) { + return expressions[startIndex]; + } + + unsigned pivot = findPivot(operators, startIndex, stopIndex - 1); + //Debug("prec") << "pivot[" << startIndex << "," << stopIndex - 1 << "] at " << pivot << std::endl; + bool negate; + Expr e = em->mkExpr(getOperatorKind(operators[pivot], negate), + createPrecedenceTree(em, expressions, operators, startIndex, pivot), + createPrecedenceTree(em, expressions, operators, pivot + 1, stopIndex)); + return negate ? em->mkExpr(kind::NOT, e) : e; +} + +Expr createPrecedenceTree(ExprManager* em, + const std::vector& expressions, + const std::vector& operators) { + if(Debug.isOn("prec") && operators.size() > 1) { + for(unsigned i = 0; i < expressions.size(); ++i) { + Debug("prec") << expressions[i]; + if(operators.size() > i) { + Debug("prec") << ' ' << CvcParserTokenNames[operators[i]] << ' '; + } + } + Debug("prec") << std::endl; + } + + Expr e = createPrecedenceTree(em, expressions, operators, 0, expressions.size() - 1); + if(Debug.isOn("prec") && operators.size() > 1) { + Expr::setlanguage::Scope ls(Debug("prec"), language::output::LANG_AST); + Debug("prec") << "=> " << e << std::endl; + } + return e; +} + +}/* @parser::members */ + @header { /** ** This file is part of the CVC4 prototype. @@ -178,21 +495,41 @@ declaration[CVC4::Command*& cmd] Debug("parser-extra") << "declaration: " << AntlrInput::tokenText(LT(1)) << std::endl; } : // FIXME: These could be type or function declarations, if that matters. - identifierList[ids, CHECK_UNDECLARED, SYM_VARIABLE] COLON declType[t,ids] SEMICOLON - { cmd = new DeclarationCommand(ids,t); } + identifierList[ids, CHECK_UNDECLARED, SYM_VARIABLE] COLON declType[t, ids] SEMICOLON + { cmd = new DeclarationCommand(ids, t); } ; /** Match the right-hand side of a declaration. Returns the type. */ declType[CVC4::Type& t, std::vector& idList] @init { + Expr f; Debug("parser-extra") << "declType: " << AntlrInput::tokenText(LT(1)) << std::endl; } : /* A sort declaration (e.g., "T : TYPE") */ TYPE_TOK { PARSER_STATE->mkSorts(idList); t = EXPR_MANAGER->kindType(); } + | /* A type alias */ + TYPE_TOK EQUAL_TOK type[t] + { for(std::vector::const_iterator i = idList.begin(); + i != idList.end(); + ++i) { + PARSER_STATE->defineType(*i, t); + } + t = EXPR_MANAGER->kindType(); } | /* A variable declaration */ - type[t] { PARSER_STATE->mkVars(idList,t); } + type[t] ( EQUAL_TOK formula[f] )? + { if(f.isNull()) { + PARSER_STATE->mkVars(idList, t); + } else { + for(std::vector::const_iterator i = idList.begin(), + i_end = idList.end(); + i != i_end; + ++i) { + PARSER_STATE->defineFunction(*i, f); + } + } + } ; /** @@ -206,16 +543,16 @@ type[CVC4::Type& t] Debug("parser-extra") << "type: " << AntlrInput::tokenText(LT(1)) << std::endl; } : /* Simple type */ - baseType[t] + bitvectorType[t] | /* Single-parameter function type */ baseType[t] ARROW_TOK baseType[t2] - { t = EXPR_MANAGER->mkFunctionType(t,t2); } + { t = EXPR_MANAGER->mkFunctionType(t, t2); } | /* Multi-parameter function type */ LPAREN baseType[t] { typeList.push_back(t); } - (COMMA baseType[t] { typeList.push_back(t); } )+ + ( COMMA baseType[t] { typeList.push_back(t); } )* RPAREN ARROW_TOK baseType[t] - { t = EXPR_MANAGER->mkFunctionType(typeList,t); } + { t = EXPR_MANAGER->mkFunctionType(typeList, t); } ; /** @@ -246,6 +583,24 @@ identifier[std::string& id, PARSER_STATE->checkDeclaration(id, check, type); } ; +/** + * Matches a bitvector type. + */ +bitvectorType[CVC4::Type& t] + : arrayType[t] + | BITVECTOR_TOK LPAREN INTEGER_LITERAL RPAREN + { t = EXPR_MANAGER->mkBitVectorType(AntlrInput::tokenToUnsigned($INTEGER_LITERAL)); } + ; + +arrayType[CVC4::Type& t] +@init { + Type t2; +} + : baseType[t] + | ARRAY_TOK baseType[t] OF_TOK baseType[t2] + { t = EXPR_MANAGER->mkArrayType(t, t2); } + ; + /** * Matches a type (which MUST be already declared). * @@ -262,9 +617,7 @@ baseType[CVC4::Type& t] * CHECK_DECLARED and the type is not declared, an exception is * thrown. * - * @return the type identifier - * - * @TODO parse more types + * @return the type identifier in 't', and the id (where applicable) in 'id' */ maybeUndefinedBaseType[CVC4::Type& t, CVC4::parser::DeclarationCheck check] returns [CVC4::parser::cvc::mystring id] @@ -336,7 +689,7 @@ letBinding[CVC4::Expr& f] letDecls IN_TOK letBinding[f] { PARSER_STATE->popScope(); } - | iffFormula[f] + | booleanFormula[f] ; /** @@ -359,193 +712,305 @@ letDecl { PARSER_STATE->defineVar(name, e); } ; -/** - * Matches a Boolean IFF formula (right-associative) - */ -iffFormula[CVC4::Expr& f] +booleanFormula[CVC4::Expr& f] @init { - Expr e; - Debug("parser-extra") << "<=> formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + std::vector expressions; + std::vector operators; + unsigned op; + unsigned notCount = 0; } - : impliesFormula[f] - ( IFF_TOK - iffFormula[e] - { f = MK_EXPR(CVC4::kind::IFF, f, e); } - )? + : ( NOT_TOK { ++notCount; } )* comparison[f] + { while(notCount > 0) { + --notCount; + f = EXPR_MANAGER->mkExpr(kind::NOT, f); + } + expressions.push_back(f); } + ( booleanBinop[op] ( NOT_TOK { ++notCount; } )* comparison[f] + { operators.push_back(op); + while(notCount > 0) { + --notCount; + f = EXPR_MANAGER->mkExpr(kind::NOT, f); + } + expressions.push_back(f); + } + )* + { f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); } ; -/** - * Matches a Boolean IMPLIES formula (right-associative) - */ -impliesFormula[CVC4::Expr& f] +booleanBinop[unsigned& op] @init { - Expr e; - Debug("parser-extra") << "=> Formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + op = LT(1)->getType(LT(1)); } - : orFormula[f] - ( IMPLIES_TOK impliesFormula[e] - { f = MK_EXPR(CVC4::kind::IMPLIES, f, e); } - )? + : IFF_TOK + | IMPLIES_TOK + | OR_TOK + | XOR_TOK + | AND_TOK ; -/** - * Matches a Boolean OR formula (left-associative) - */ -orFormula[CVC4::Expr& f] +comparison[CVC4::Expr& f] @init { - std::vector exprs; - Debug("parser-extra") << "OR Formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + std::vector expressions; + std::vector operators; + unsigned op; } - : xorFormula[f] - ( OR_TOK { exprs.push_back(f); } - xorFormula[f] { exprs.push_back(f); } )* - { - if( exprs.size() > 0 ) { - f = MK_EXPR(CVC4::kind::OR, exprs); - } - } + : term[f] { expressions.push_back(f); } + ( comparisonBinop[op] term[f] + { operators.push_back(op); expressions.push_back(f); } )* + { f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); } ; -/** - * Matches a Boolean XOR formula (left-associative) - */ -xorFormula[CVC4::Expr& f] +comparisonBinop[unsigned& op] @init { - Expr e; - Debug("parser-extra") << "XOR formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + op = LT(1)->getType(LT(1)); } - : andFormula[f] - ( XOR_TOK andFormula[e] - { f = MK_EXPR(CVC4::kind::XOR,f, e); } - )* + : EQUAL_TOK + | DISEQUAL_TOK + | GT_TOK + | GEQ_TOK + | LT_TOK + | LEQ_TOK ; -/** - * Matches a Boolean AND formula (left-associative) - */ -andFormula[CVC4::Expr& f] +term[CVC4::Expr& f] @init { - std::vector exprs; - Debug("parser-extra") << "AND Formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + std::vector expressions; + std::vector operators; + unsigned op; } - : notFormula[f] - ( AND_TOK { exprs.push_back(f); } - notFormula[f] { exprs.push_back(f); } )* - { - if( exprs.size() > 0 ) { - f = MK_EXPR(CVC4::kind::AND, exprs); - } - } + : storeTerm[f] { expressions.push_back(f); } + ( arithmeticBinop[op] storeTerm[f] { operators.push_back(op); expressions.push_back(f); } )* + { f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); } ; -/** - * Parses a NOT formula. - * @return the expression representing the formula - */ -notFormula[CVC4::Expr& f] +arithmeticBinop[unsigned& op] @init { - Debug("parser-extra") << "NOT formula: " << AntlrInput::tokenText(LT(1)) << std::endl; + op = LT(1)->getType(LT(1)); } - : /* negation */ - NOT_TOK notFormula[f] - { f = MK_EXPR(CVC4::kind::NOT, f); } - | /* a boolean atom */ - comparisonFormula[f] + : PLUS_TOK + | MINUS_TOK + | STAR_TOK + | INTDIV_TOK + | DIV_TOK + | EXP_TOK ; -/** Parses a comparison formula (non-associative). - NOTE: equality should technically have higher precedence than - greater-than, less-than, etc., but I don't think this will ever - be relevant in a well-typed formula. -*/ -comparisonFormula[CVC4::Expr& f] +/** Parses an array store term. */ +storeTerm[CVC4::Expr& f] @init { - Expr e; - Kind op; - bool negate; - Debug("parser-extra") << "predicate formula: " << AntlrInput::tokenText(LT(1)) << std::endl; -} - : plusTerm[f] - ( ( EQUAL_TOK { op = CVC4::kind::EQUAL; negate = false; } - | DISEQUAL_TOK { op = CVC4::kind::EQUAL; negate = true; } - | GT_TOK { op = CVC4::kind::GT; negate = false; } - | GEQ_TOK { op = CVC4::kind::GEQ; negate = false; } - | LT_TOK { op = CVC4::kind::LT; negate = false; } - | LEQ_TOK { op = CVC4::kind::LEQ; negate = false; }) - plusTerm[e] - { f = MK_EXPR(op, f, e); - if(negate) { - f = MK_EXPR(CVC4::kind::NOT, f); - } + Expr f2, f3; +} + : uminusTerm[f] ( WITH_TOK + LBRACKET formula[f2] RBRACKET ASSIGN_TOK uminusTerm[f3] + { f = MK_EXPR(CVC4::kind::STORE, f, f2, f3); } + ( COMMA LBRACKET formula[f2] RBRACKET ASSIGN_TOK uminusTerm[f3] + { f = MK_EXPR(CVC4::kind::STORE, f, f2, f3); } )* )* + ; + +/** Parses a unary minus term. */ +uminusTerm[CVC4::Expr& f] +@init { + unsigned minusCount = 0; +} + : /* Unary minus */ +// (MINUS_TOK { ++minusCount; })* concatBitwiseTerm[f] + (MINUS_TOK { ++minusCount; })+ concatBitwiseTerm[f] + { while(minusCount > 0) { --minusCount; f = MK_EXPR(CVC4::kind::UMINUS, f); } } + | concatBitwiseTerm[f] + ; + +/** Parses bitvectors. */ + +concatBitwiseTerm[CVC4::Expr& f] +@init { + std::vector expressions; + std::vector operators; + unsigned op; +} + : bitwiseXorTerm[f] { expressions.push_back(f); } + ( concatBitwiseBinop[op] bitwiseXorTerm[f] { operators.push_back(op); expressions.push_back(f); } )* + { f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); } + ; +concatBitwiseBinop[unsigned& op] +@init { + op = LT(1)->getType(LT(1)); +} + : CONCAT_TOK + | BAR + | BVAND_TOK + ; + +bitwiseXorTerm[CVC4::Expr& f] +@init { + Expr f2; +} + : /* BV xor */ + BVXOR_TOK LPAREN formula[f] COMMA formula[f] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_XOR, f, f2); } + | BVNAND_TOK LPAREN formula[f] COMMA formula[f] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_NAND, f, f2); } + | BVNOR_TOK LPAREN formula[f] COMMA formula[f] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_NOR, f, f2); } + | BVCOMP_TOK LPAREN formula[f] COMMA formula[f] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_COMP, f, f2); } + | BVXNOR_TOK LPAREN formula[f] COMMA formula[f] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_XNOR, f, f2); } + | bvNegTerm[f] + ; +bvNegTerm[CVC4::Expr& f] + : /* BV neg */ + BVNEG_TOK bvNegTerm[f] + { f = MK_EXPR(CVC4::kind::BITVECTOR_NOT, f); } + | bvUminusTerm[f] + ; +bvUminusTerm[CVC4::Expr& f] +@init { + Expr f2; +} + : /* BV unary minus */ + BVUMINUS_TOK LPAREN formula[f] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_NEG, f); } + | BVPLUS_TOK LPAREN INTEGER_LITERAL COMMA formula[f] + ( COMMA formula[f2] { f = MK_EXPR(CVC4::kind::BITVECTOR_PLUS, f, f2); } )+ RPAREN + { unsigned size = BitVectorType(f.getType()).getSize(); + unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); + if(k == 0) { + PARSER_STATE->parseError("BVPLUS(k,_,_,...) must have k > 0"); } - )? + if(k > size) { + f = MK_EXPR(MK_CONST(BitVectorZeroExtend(k)), f); + } else if(k < size) { + f = MK_EXPR(MK_CONST(BitVectorExtract(0, k - 1)), f); + } + } + | BVSUB_TOK LPAREN INTEGER_LITERAL COMMA formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_SUB, f, f2); + unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); + if(k == 0) { + PARSER_STATE->parseError("BVSUB(k,_,_) must have k > 0"); + } + unsigned size = BitVectorType(f.getType()).getSize(); + if(k > size) { + f = MK_EXPR(MK_CONST(BitVectorZeroExtend(k)), f); + } else if(k < size) { + f = MK_EXPR(MK_CONST(BitVectorExtract(0, k - 1)), f); + } + } + | BVMULT_TOK LPAREN INTEGER_LITERAL COMMA formula[f] COMMA formula[f2] RPAREN + { MK_EXPR(CVC4::kind::BITVECTOR_MULT, f, f2); + unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); + if(k == 0) { + PARSER_STATE->parseError("BVMULT(k,_,_) must have k > 0"); + } + unsigned size = BitVectorType(f.getType()).getSize(); + if(k > size) { + f = MK_EXPR(MK_CONST(BitVectorZeroExtend(k)), f); + } else if(k < size) { + f = MK_EXPR(MK_CONST(BitVectorExtract(0, k - 1)), f); + } + } + | BVUDIV_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_UDIV, f, f2); } + | BVSDIV_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_SDIV, f, f2); } + | BVUREM_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_UREM, f, f2); } + | BVSREM_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_SREM, f, f2); } + | BVSMOD_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_SMOD, f, f2); } + | BVSHL_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_SHL, f, f2); } + | BVASHR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_ASHR, f, f2); } + | BVLSHR_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_LSHR, f, f2); } + | SX_TOK LPAREN formula[f] COMMA INTEGER_LITERAL RPAREN + { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); + f = MK_EXPR(MK_CONST(BitVectorSignExtend(k)), f); } + | BVZEROEXTEND_TOK LPAREN formula[f] COMMA INTEGER_LITERAL RPAREN + { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); + f = MK_EXPR(MK_CONST(BitVectorSignExtend(k)), f); } + | BVREPEAT_TOK LPAREN formula[f] COMMA INTEGER_LITERAL RPAREN + { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); + f = MK_EXPR(MK_CONST(BitVectorRepeat(k)), f); } + | BVROTR_TOK LPAREN formula[f] COMMA INTEGER_LITERAL RPAREN + { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); + f = MK_EXPR(MK_CONST(BitVectorSignExtend(k)), f); } + | BVROTL_TOK LPAREN formula[f] COMMA INTEGER_LITERAL RPAREN + { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); + f = MK_EXPR(MK_CONST(BitVectorRotateLeft(k)), f); } + | bvShiftTerm[f] ; -/** Parses a plus/minus term (left-associative). - TODO: This won't take advantage of n-ary PLUS's. */ -plusTerm[CVC4::Expr& f] +bvShiftTerm[CVC4::Expr& f] @init { - Expr e; - Kind op; - std::vector exprs; - Debug("parser-extra") << "plus term: " << AntlrInput::tokenText(LT(1)) << std::endl; -} - : multTerm[f] - ( ( PLUS_TOK { op = CVC4::kind::PLUS; } - | MINUS_TOK { op = CVC4::kind::MINUS; } ) - multTerm[e] - { f = MK_EXPR(op, f, e); } - )* + std::vector expressions; + std::vector operators; + unsigned op; +} + : bvComparison[f] + ( ( LEFTSHIFT_TOK | RIGHTSHIFT_TOK) INTEGER_LITERAL + { unsigned k = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); + f = MK_EXPR(MK_CONST(BitVectorRotateLeft(k)), f); } + )? ; -/** Parses a multiply/divide term (left-associative). - TODO: This won't take advantage of n-ary MULT's. */ -multTerm[CVC4::Expr& f] +bvComparison[CVC4::Expr& f] @init { - Expr e; - Kind op; - Debug("parser-extra") << "multiplication term: " << AntlrInput::tokenText(LT(1)) << std::endl; -} - : expTerm[f] - ( ( STAR_TOK { op = CVC4::kind::MULT; } - | DIV_TOK { op = CVC4::kind::DIVISION; } ) - expTerm[e] - { f = MK_EXPR(op, f, e); } - )* + Expr f2; +} + : /* BV comparison */ + BVLT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_ULT, f, f2); } + | BVLE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_ULE, f, f2); } + | BVGT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_UGT, f, f2); } + | BVGE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_UGE, f, f2); } + | BVSLT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_SLT, f, f2); } + | BVSLE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_SLE, f, f2); } + | BVSGT_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_SGT, f, f2); } + | BVSGE_TOK LPAREN formula[f] COMMA formula[f2] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_SGE, f, f2); } + /* + | IS_INTEGER_TOK LPAREN formula[f] RPAREN + { f = MK_EXPR(CVC4::kind::BITVECTOR_IS_INTEGER, f); } + */ + | selectExtractTerm[f] ; -/** - * Parses an exponential term (left-associative). - * NOTE that the exponent must be a nonnegative integer constant - * (for now). - */ -expTerm[CVC4::Expr& f] +/** Parses an array select. */ +selectExtractTerm[CVC4::Expr& f] @init { - Expr e; - Debug("parser-extra") << "exponential term: " << AntlrInput::tokenText(LT(1)) << std::endl; -} - : unaryTerm[f] - ( EXP_TOK INTEGER_LITERAL - { Integer n = AntlrInput::tokenToInteger($INTEGER_LITERAL); - if(n == 0) { - f = MK_CONST( Integer(1) ); - } else if(n == 1) { - /* f remains the same */ - } else { - std::vector v; - for(Integer i = 0; i < n; i = i + 1) { - v.push_back(f); + Expr f2; + bool extract; +} + : /* array select / bitvector extract */ + simpleTerm[f] + ( { extract = false; } + LBRACKET formula[f2] ( COLON INTEGER_LITERAL { extract = true; } )? RBRACKET + { if(extract) { + if(f2.getKind() != kind::CONST_INTEGER) { + PARSER_STATE->parseError("bitvector extraction requires [INTEGER_LITERAL:INTEGER_LITERAL] range"); } - f = MK_EXPR(CVC4::kind::MULT, v); + unsigned k1 = f2.getConst().getLong(); + unsigned k2 = AntlrInput::tokenToUnsigned($INTEGER_LITERAL); + f = MK_EXPR(MK_CONST(BitVectorExtract(k1, k2)), f); + } else { + f = MK_EXPR(CVC4::kind::SELECT, f, f2); } } )* + ; -/** - * Parses a unary term. - */ -unaryTerm[CVC4::Expr& f] +/** Parses a simple term. */ +simpleTerm[CVC4::Expr& f] @init { std::string name; std::vector args; @@ -574,18 +1039,22 @@ unaryTerm[CVC4::Expr& f] | /* if-then-else */ iteTerm[f] - | /* Unary minus */ - MINUS_TOK unaryTerm[f] { f = MK_EXPR(CVC4::kind::UMINUS, f); } - | /* parenthesized sub-formula */ LPAREN formula[f] RPAREN /* constants */ | TRUE_TOK { f = MK_CONST(true); } | FALSE_TOK { f = MK_CONST(false); } - | INTEGER_LITERAL { f = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); } | DECIMAL_LITERAL { f = MK_CONST( AntlrInput::tokenToRational($DECIMAL_LITERAL) ); } + | HEX_LITERAL + { Assert( AntlrInput::tokenText($HEX_LITERAL).find("0hex") == 0 ); + std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 4); + f = MK_CONST( BitVector(hexString, 16) ); } + | BINARY_LITERAL + { Assert( AntlrInput::tokenText($BINARY_LITERAL).find("0bin") == 0 ); + std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 4); + f = MK_CONST( BitVector(binString, 2) ); } | /* variable */ identifier[name,CHECK_DECLARED,SYM_VARIABLE] @@ -653,7 +1122,7 @@ datatypeDef[std::vector& datatypes] : identifier[id,CHECK_UNDECLARED,SYM_SORT] { datatypes.push_back(Datatype(id)); } EQUAL_TOK constructorDef[datatypes.back()] - ( BAR_TOK constructorDef[datatypes.back()] )* + ( BAR constructorDef[datatypes.back()] )* ; /** @@ -689,7 +1158,13 @@ selector[CVC4::Datatype::Constructor& ctor] std::string id; Type type; } - : identifier[id,CHECK_UNDECLARED,SYM_SORT] COLON maybeUndefinedBaseType[type,CHECK_NONE] + : identifier[id,CHECK_UNDECLARED,SYM_SORT] COLON + maybeUndefinedBaseType[type,CHECK_NONE] + // TODO: this doesn't permit datatype fields of ARRAY or BITVECTOR + // type. This will be problematic, since, after all, you could + // have something nasty like this: + // + // DATATYPE list = cons(car:ARRAY list OF list, cdr:list) | nil END; { if(type.isNull()) { ctor.addArg(id, Datatype::UnresolvedType($maybeUndefinedBaseType.id)); } else { @@ -699,70 +1174,6 @@ selector[CVC4::Datatype::Constructor& ctor] } ; -// Keywords - -AND_TOK : 'AND'; -ASSERT_TOK : 'ASSERT'; -BOOLEAN_TOK : 'BOOLEAN'; -CHECKSAT_TOK : 'CHECKSAT'; -ECHO_TOK : 'ECHO'; -ELSEIF_TOK : 'ELSIF'; -ELSE_TOK : 'ELSE'; -ENDIF_TOK : 'ENDIF'; -FALSE_TOK : 'FALSE'; -IF_TOK : 'IF'; -IN_TOK : 'IN'; -INT_TOK : 'INT'; -LET_TOK : 'LET'; -NOT_TOK : 'NOT'; -OPTION_TOK : 'OPTION'; -OR_TOK : 'OR'; -POPTO_TOK : 'POPTO'; -POP_TOK : 'POP'; -PRINT_TOK : 'PRINT'; -PUSH_TOK : 'PUSH'; -QUERY_TOK : 'QUERY'; -REAL_TOK : 'REAL'; -THEN_TOK : 'THEN'; -TRUE_TOK : 'TRUE'; -TYPE_TOK : 'TYPE'; -XOR_TOK : 'XOR'; - -DATATYPE_TOK : 'DATATYPE'; -END_TOK : 'END'; -BAR_TOK : '|'; - -ARRAY_TOK : 'ARRAY'; -OF_TOK : 'OF'; -WITH_TOK : 'WITH'; - -BITVECTOR_TOK : 'BITVECTOR'; - -// Symbols - -COLON : ':'; -COMMA : ','; -LPAREN : '('; -RPAREN : ')'; -SEMICOLON : ';'; - -// Operators - -ARROW_TOK : '->'; -DIV_TOK : '/'; -EQUAL_TOK : '='; -DISEQUAL_TOK : '/='; -EXP_TOK : '^'; -GT_TOK : '>'; -GEQ_TOK : '>='; -IFF_TOK : '<=>'; -IMPLIES_TOK : '=>'; -LT_TOK : '<'; -LEQ_TOK : '<='; -MINUS_TOK : '-'; -PLUS_TOK : '+'; -STAR_TOK : '*'; - /** * Matches an identifier from the input. An identifier is a sequence of letters, * digits and "_", "'", "." symbols, starting with a letter. @@ -779,6 +1190,20 @@ INTEGER_LITERAL: DIGIT+; */ DECIMAL_LITERAL: DIGIT+ '.' DIGIT+; +/** + * Matches a hexadecimal constant. + */ +HEX_LITERAL + : '0hex' HEX_DIGIT+ + ; + +/** + * Matches a binary constant. + */ +BINARY_LITERAL + : '0bin' ('0' | '1')+ + ; + /** * Matches a double quoted string literal. Escaping is supported, and * escape character '\' has to be escaped. @@ -795,6 +1220,8 @@ fragment ALPHA : 'a'..'z' | 'A'..'Z'; */ fragment DIGIT : '0'..'9'; +fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F'; + /** * Matches and skips whitespace in the input and ignores it. */ diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index a5a633e48..d27abc735 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -448,6 +448,7 @@ term[CVC4::Expr& expr] { Assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 ); std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2); expr = MK_CONST( BitVector(binString, 2) ); } + // NOTE: Theory constants go here ; diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index a048bc3b2..c3253d05a 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -99,6 +99,39 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, case kind::GEQ: out << ">="; break; case kind::IMPLIES: out << "=>"; break; case kind::IFF: out << "<=>"; break; + + // names are slightly different than the kind + case kind::BITVECTOR_PLUS: out << "BVPLUS"; break; + case kind::BITVECTOR_SUB: out << "BVSUB"; break; + case kind::BITVECTOR_XOR: out << "BVXOR"; break; + case kind::BITVECTOR_NAND: out << "BVNAND"; break; + case kind::BITVECTOR_NOR: out << "BVNOR"; break; + case kind::BITVECTOR_XNOR: out << "BVXNOR"; break; + case kind::BITVECTOR_COMP: out << "BVCOMP"; break; + case kind::BITVECTOR_MULT: out << "BVMULT"; break; + case kind::BITVECTOR_UDIV: out << "BVUDIV"; break; + case kind::BITVECTOR_UREM: out << "BVUREM"; break; + case kind::BITVECTOR_SDIV: out << "BVSDIV"; break; + case kind::BITVECTOR_SREM: out << "BVSREM"; break; + case kind::BITVECTOR_SMOD: out << "BVSMOD"; break; + case kind::BITVECTOR_SHL: out << "BVSHL"; break; + case kind::BITVECTOR_LSHR: out << "BVLSHR"; break; + case kind::BITVECTOR_ASHR: out << "BVASHR"; break; + case kind::BITVECTOR_ULT: out << "BVLT"; break; + case kind::BITVECTOR_ULE: out << "BVLE"; break; + case kind::BITVECTOR_UGT: out << "BVGT"; break; + case kind::BITVECTOR_UGE: out << "BVGE"; break; + case kind::BITVECTOR_SLT: out << "BVSLT"; break; + case kind::BITVECTOR_SLE: out << "BVSLE"; break; + case kind::BITVECTOR_SGT: out << "BVSGT"; break; + case kind::BITVECTOR_SGE: out << "BVSGE"; break; + case kind::BITVECTOR_NEG: out << "BVUMINUS"; break; + + case kind::BITVECTOR_NOT: out << "~"; break; + case kind::BITVECTOR_AND: out << "&"; break; + case kind::BITVECTOR_OR: out << "|"; break; + case kind::BITVECTOR_CONCAT: out << "@"; break; + default: out << k; } @@ -159,6 +192,38 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, out << "IF " << n[0] << " THEN " << n[1] << " ELSE " << n[2]; break; + // these are prefix + case kind::BITVECTOR_PLUS: + case kind::BITVECTOR_SUB: + case kind::BITVECTOR_XOR: + case kind::BITVECTOR_NAND: + case kind::BITVECTOR_NOR: + case kind::BITVECTOR_XNOR: + case kind::BITVECTOR_COMP: + case kind::BITVECTOR_MULT: + case kind::BITVECTOR_UDIV: + case kind::BITVECTOR_UREM: + case kind::BITVECTOR_SDIV: + case kind::BITVECTOR_SREM: + case kind::BITVECTOR_SMOD: + case kind::BITVECTOR_SHL: + case kind::BITVECTOR_LSHR: + case kind::BITVECTOR_ASHR: + case kind::BITVECTOR_ULT: + case kind::BITVECTOR_ULE: + case kind::BITVECTOR_UGT: + case kind::BITVECTOR_UGE: + case kind::BITVECTOR_SLT: + case kind::BITVECTOR_SLE: + case kind::BITVECTOR_SGT: + case kind::BITVECTOR_SGE: + out << n.getOperator() << '(' << n[0] << ',' << n[1] << ')'; + break; + + case kind::BITVECTOR_EXTRACT: + out << n[0] << '[' << n.getOperator().getConst() << ']'; + break; + default: if(k == kind::NOT && n[0].getKind() == kind::EQUAL) { // collapse NOT-over-EQUAL diff --git a/test/regress/regress0/precedence/or-xor.cvc b/test/regress/regress0/precedence/or-xor.cvc index 4e19be584..3252647a2 100644 --- a/test/regress/regress0/precedence/or-xor.cvc +++ b/test/regress/regress0/precedence/or-xor.cvc @@ -3,5 +3,6 @@ A, B, C: BOOLEAN; -QUERY (A OR B XOR C) <=> (A OR (B XOR C)); +QUERY ((A OR B XOR C) <=> ((A OR B) XOR C)) + AND ((A XOR B OR C) <=> ((A XOR B) OR C)); % EXIT: 20 diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index af9b7bd0f..dbc8e2281 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -2,10 +2,10 @@ /*! \file parser_black.h ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 @@ -206,7 +206,12 @@ public: tryGoodInput("a, b : BOOLEAN;"); tryGoodInput("a, b : BOOLEAN; QUERY (a => b) AND a => b;"); tryGoodInput("T, U : TYPE; f : T -> U; x : T; y : U; CHECKSAT f(x) = y;"); + tryGoodInput("T : TYPE = BOOLEAN; x : T; CHECKSAT x;"); + tryGoodInput("a : ARRAY INT OF REAL; ASSERT (a WITH [1] := 0.0)[1] = a[0];"); + tryGoodInput("b : BITVECTOR(3); ASSERT b = 0bin101;"); + tryGoodInput("T : TYPE = BOOLEAN; x : T; CHECKSAT x;"); tryGoodInput("T : TYPE; x, y : T; a : BOOLEAN; QUERY (IF a THEN x ELSE y ENDIF) = x;"); + tryGoodInput("CHECKSAT 0bin0000 /= 0hex7;"); tryGoodInput("%% nothing but a comment"); tryGoodInput("% a comment\nASSERT TRUE; %a command\n% another comment"); } @@ -219,6 +224,7 @@ public: tryBadInput("a, b : boolean;"); // lowercase boolean isn't a type tryBadInput("0x : INT;"); // 0x isn't an identifier tryBadInput("a, b : BOOLEAN\nQUERY (a => b) AND a => b;"); // no semicolon after decl + tryBadInput("ASSERT 0bin012 /= 0hex0;"); // bad binary literal tryBadInput("a : BOOLEAN; a: BOOLEAN;"); // double decl tryBadInput("a, b: BOOLEAN; QUERY a(b);"); // non-function used as function } diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h index d0de68e33..991d71364 100644 --- a/test/unit/util/datatype_black.h +++ b/test/unit/util/datatype_black.h @@ -54,6 +54,10 @@ public: cout << nat << std::endl; DatatypeType natType = d_em->mkDatatypeType(nat); cout << natType << std::endl; + + Expr ctor = natType.getDatatype()[1].getConstructor(); + Expr apply = d_em->mkExpr(kind::APPLY_CONSTRUCTOR, ctor); + cout << apply << std::endl; } void testTree() { -- 2.30.2