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)",
}
}
-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)",
}
}
-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)",
}
}
-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)",
}
}
-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)",
}
Expr ExprManager::mkExpr(Kind kind, const std::vector<Expr>& 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)",
}
}
+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<Expr>& 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)",
}
/** 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<Type>& argTypes, const Type& range) {
+FunctionType ExprManager::mkFunctionType(const std::vector<Type>& argTypes, Type range) {
NodeManagerScope nms(d_nodeManager);
Assert( argTypes.size() >= 1 );
std::vector<TypeNode> argTypeNodes;
* @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 {
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;
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));
* @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, ...).
* @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, ...).
* @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, ...).
* @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, ...).
* @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
Expr mkExpr(Kind kind, const std::vector<Expr>& 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
/** 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.
* <code>argTypes</code> must have at least one element.
*/
- FunctionType mkFunctionType(const std::vector<Type>& argTypes, const Type& range);
+ FunctionType mkFunctionType(const std::vector<Type>& argTypes, Type range);
/**
* Make a function type with input types from
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);
template <bool ref_count>
Node* mkNodePtr(Kind kind, const std::vector<NodeTemplate<ref_count> >& 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 <bool ref_count>
Node mkNode(TNode opNode, const std::vector<NodeTemplate<ref_count> >& children);
template <bool ref_count>
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 <bool ref_count>
inline Node NodeManager::mkNode(TNode opNode,
template <bool ref_count>
inline Node* NodeManager::mkNodePtr(TNode opNode,
- const std::vector<NodeTemplate<ref_count> >&
- children) {
+ const std::vector<NodeTemplate<ref_count> >&
+ children) {
NodeBuilder<> nb(this, kind::operatorKindToKind(opNode.getKind()));
nb << opNode;
nb.append(children);
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<unsigned>& 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<CVC4::Expr>& expressions,
+ const std::vector<unsigned>& 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<CVC4::Expr>& expressions,
+ const std::vector<unsigned>& 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.
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<std::string>& 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<std::string>::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<std::string>::const_iterator i = idList.begin(),
+ i_end = idList.end();
+ i != i_end;
+ ++i) {
+ PARSER_STATE->defineFunction(*i, f);
+ }
+ }
+ }
;
/**
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); }
;
/**
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).
*
* 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]
letDecls
IN_TOK letBinding[f]
{ PARSER_STATE->popScope(); }
- | iffFormula[f]
+ | booleanFormula[f]
;
/**
{ 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<CVC4::Expr> expressions;
+ std::vector<unsigned> 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<Expr> exprs;
- Debug("parser-extra") << "OR Formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
+ std::vector<CVC4::Expr> expressions;
+ std::vector<unsigned> 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<Expr> exprs;
- Debug("parser-extra") << "AND Formula: " << AntlrInput::tokenText(LT(1)) << std::endl;
+ std::vector<CVC4::Expr> expressions;
+ std::vector<unsigned> 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<CVC4::Expr> expressions;
+ std::vector<unsigned> 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<Expr> 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<CVC4::Expr> expressions;
+ std::vector<unsigned> 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<Expr> 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<Integer>().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<Expr> args;
| /* 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]
: 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()] )*
;
/**
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 {
}
;
-// 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.
*/
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.
*/
fragment DIGIT : '0'..'9';
+fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F';
+
/**
* Matches and skips whitespace in the input and ignores it.
*/
{ 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
;
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;
}
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<BitVectorExtract>() << ']';
+ break;
+
default:
if(k == kind::NOT && n[0].getKind() == kind::EQUAL) {
// collapse NOT-over-EQUAL
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
/*! \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
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");
}
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
}
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() {
projects / cvc5.git / commitdiff