| LPAREN_TOK
( /* An indexed function application */
- indexedFunctionName[op, kind] termList[args,expr] RPAREN_TOK
- {
- if( kind!=kind::NULL_EXPR ){
+ indexedFunctionName[op, kind] termList[args,expr] RPAREN_TOK {
+ if(kind==CVC4::kind::APPLY_SELECTOR) {
+ //tuple selector case
+ Integer x = op.getConst<CVC4::Rational>().getNumerator();
+ if (!x.fitsUnsignedInt()) {
+ PARSER_STATE->parseError("index of tupSel is larger than size of unsigned int");
+ }
+ unsigned int n = x.toUnsignedInt();
+ if (args.size()>1) {
+ PARSER_STATE->parseError("tupSel applied to more than one tuple argument");
+ }
+ Type t = args[0].getType();
+ if (!t.isTuple()) {
+ PARSER_STATE->parseError("tupSel applied to non-tuple");
+ }
+ size_t length = ((DatatypeType)t).getTupleLength();
+ if (n >= length) {
+ std::stringstream ss;
+ ss << "tuple is of length " << length << "; cannot access index " << n;
+ PARSER_STATE->parseError(ss.str());
+ }
+ const Datatype & dt = ((DatatypeType)t).getDatatype();
+ op = dt[0][n].getSelector();
+ }
+ if (kind!=kind::NULL_EXPR) {
expr = MK_EXPR( kind, op, args );
- }else{
+ } else {
expr = MK_EXPR(op, args);
}
PARSER_STATE->checkOperator(expr.getKind(), args.size());
{ //booleanType is placeholder here since we don't have type info without type annotation
expr = EXPR_MANAGER->mkNullaryOperator(EXPR_MANAGER->booleanType(), kind::SEP_NIL); }
// NOTE: Theory constants go here
+
+ | LPAREN_TOK TUPLE_CONST_TOK termList[args,expr] RPAREN_TOK
+ { std::vector<Type> types;
+ for(std::vector<Expr>::const_iterator i = args.begin(); i != args.end(); ++i) {
+ types.push_back((*i).getType());
+ }
+ DatatypeType t = EXPR_MANAGER->mkTupleType(types);
+ const Datatype& dt = t.getDatatype();
+ args.insert(args.begin(), dt[0].getConstructor());
+ expr = MK_EXPR(kind::APPLY_CONSTRUCTOR, args);
+ }
+
+ | TUPLE_CONST_TOK
+ { std::vector<Type> types;
+ DatatypeType t = EXPR_MANAGER->mkTupleType(types);
+ const Datatype& dt = t.getDatatype();
+ args.insert(args.begin(), dt[0].getConstructor());
+ expr = MK_EXPR(kind::APPLY_CONSTRUCTOR, args);
+ }
;
/**
op = Datatype::datatypeOf(expr)[Datatype::indexOf(expr)].getTester();
kind = CVC4::kind::APPLY_TESTER;
}
+ | TUPLE_SEL_TOK m=INTEGER_LITERAL {
+ kind = CVC4::kind::APPLY_SELECTOR;
+ //put m in op so that the caller (termNonVariable) can deal with this case
+ op = MK_CONST(Rational(AntlrInput::tokenToUnsigned($m)));
+ }
| badIndexedFunctionName
)
RPAREN_TOK
PARSER_STATE->parseError("Illegal set type.");
}
t = EXPR_MANAGER->mkSetType( args[0] );
+ } else if(name == "Tuple") {
+ t = EXPR_MANAGER->mkTupleType(args);
} else if(check == CHECK_DECLARED ||
PARSER_STATE->isDeclared(name, SYM_SORT)) {
t = PARSER_STATE->getSort(name, args);
EMPTYSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'emptyset';
UNIVSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'univset';
NILREF_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SEP) }? 'sep.nil';
+TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }? 'mkTuple';
+TUPLE_SEL_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }? 'tupSel';
// Other set theory operators are not
// tokenized and handled directly when
// processing a term
}
case kind::DATATYPE_TYPE:
+ {
+ const Datatype& dt = (NodeManager::currentNM()->getDatatypeForIndex(
+ n.getConst<DatatypeIndexConstant>().getIndex()));
+ if (dt.isTuple())
+ {
+ unsigned int n = dt[0].getNumArgs();
+ if (n == 0)
+ {
+ out << "Tuple";
+ }
+ else
+ {
+ out << "(Tuple";
+ for (unsigned int i = 0; i < n; i++)
+ {
+ out << " " << dt[0][i].getRangeType();
+ }
+ out << ")";
+ }
+ }
+ else
{
- const Datatype & dt = (NodeManager::currentNM()->getDatatypeForIndex( n.getConst< DatatypeIndexConstant >().getIndex() ));
out << maybeQuoteSymbol(dt.getName());
}
break;
+ }
case kind::UNINTERPRETED_CONSTANT: {
const UninterpretedConstant& uc = n.getConst<UninterpretedConstant>();
case kind::INTERSECTION:
case kind::SETMINUS:
case kind::SUBSET:
+ case kind::CARD:
+ case kind::JOIN:
+ case kind::PRODUCT:
+ case kind::TRANSPOSE:
+ case kind::TCLOSURE:
parametricTypeChildren = true;
out << smtKindString(k) << " ";
break;
return;
}
break;
- case kind::APPLY_CONSTRUCTOR: typeChildren = true;
- case kind::APPLY_TESTER:
- case kind::APPLY_SELECTOR:
- case kind::APPLY_SELECTOR_TOTAL:
- case kind::PARAMETRIC_DATATYPE:
- break;
- //separation logic
- case kind::SEP_EMP:
- case kind::SEP_PTO:
- case kind::SEP_STAR:
- case kind::SEP_WAND:out << smtKindString(k) << " "; break;
+ case kind::APPLY_CONSTRUCTOR:
+ {
+ typeChildren = true;
+ const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
+ if (dt.isTuple())
+ {
+ stillNeedToPrintParams = false;
+ out << "mkTuple" << ( dt[0].getNumArgs()==0 ? "" : " ");
+ }
+ }
+
+ case kind::APPLY_TESTER:
+ case kind::APPLY_SELECTOR:
+ case kind::APPLY_SELECTOR_TOTAL:
+ case kind::PARAMETRIC_DATATYPE: break;
- case kind::SEP_NIL:out << "(as sep.nil " << n.getType() << ")";break;
+ // separation logic
+ case kind::SEP_EMP:
+ case kind::SEP_PTO:
+ case kind::SEP_STAR:
+ case kind::SEP_WAND: out << smtKindString(k) << " "; break;
- // quantifiers
- case kind::FORALL:
- case kind::EXISTS:
- if( k==kind::FORALL ){
- out << "forall ";
- }else{
- out << "exists ";
- }
- for( unsigned i=0; i<2; i++) {
- out << n[i] << " ";
- if( i==0 && n.getNumChildren()==3 ){
- out << "(! ";
+ case kind::SEP_NIL:
+ out << "(as sep.nil " << n.getType() << ")";
+ break;
+
+ // quantifiers
+ case kind::FORALL:
+ case kind::EXISTS:
+ if (k == kind::FORALL)
+ {
+ out << "forall ";
+ }
+ else
+ {
+ out << "exists ";
+ }
+ for (unsigned i = 0; i < 2; i++)
+ {
+ out << n[i] << " ";
+ if (i == 0 && n.getNumChildren() == 3)
+ {
+ out << "(! ";
+ }
+ }
+ if (n.getNumChildren() == 3)
+ {
+ out << n[2];
+ out << ")";
}
- }
- if( n.getNumChildren()==3 ){
- out << n[2];
out << ")";
- }
- out << ")";
- return;
- break;
- case kind::BOUND_VAR_LIST:
- // the left parenthesis is already printed (before the switch)
- for(TNode::iterator i = n.begin(), iend = n.end();
- i != iend; ) {
- out << '(';
- toStream(out, *i, toDepth < 0 ? toDepth : toDepth - 1, types, 0);
- out << ' ';
- out << (*i).getType();
- // The following code do stange things
- // (*i).getType().toStream(out, toDepth < 0 ? toDepth : toDepth - 1,
- // false, language::output::LANG_SMTLIB_V2_5);
- out << ')';
- if(++i != iend) {
+ return;
+ break;
+ case kind::BOUND_VAR_LIST:
+ // the left parenthesis is already printed (before the switch)
+ for (TNode::iterator i = n.begin(), iend = n.end(); i != iend;)
+ {
+ out << '(';
+ toStream(out, *i, toDepth < 0 ? toDepth : toDepth - 1, types, 0);
out << ' ';
+ out << (*i).getType();
+ // The following code do stange things
+ // (*i).getType().toStream(out, toDepth < 0 ? toDepth : toDepth - 1,
+ // false, language::output::LANG_SMTLIB_V2_5);
+ out << ')';
+ if (++i != iend)
+ {
+ out << ' ';
+ }
}
- }
- out << ')';
- return;
- case kind::INST_PATTERN:
- break;
- case kind::INST_PATTERN_LIST:
- for(unsigned i=0; i<n.getNumChildren(); i++) {
- if( n[i].getKind()==kind::INST_ATTRIBUTE ){
- if( n[i][0].getAttribute(theory::FunDefAttribute()) ){
- out << ":fun-def";
+ out << ')';
+ return;
+ case kind::INST_PATTERN: break;
+ case kind::INST_PATTERN_LIST:
+ for (unsigned i = 0; i < n.getNumChildren(); i++)
+ {
+ if (n[i].getKind() == kind::INST_ATTRIBUTE)
+ {
+ if (n[i][0].getAttribute(theory::FunDefAttribute()))
+ {
+ out << ":fun-def";
+ }
+ }
+ else
+ {
+ out << ":pattern " << n[i];
}
- }else{
- out << ":pattern " << n[i];
}
- }
- return;
- break;
+ return;
+ break;
- default:
- // fall back on however the kind prints itself; this probably
- // won't be SMT-LIB v2 compliant, but it will be clear from the
- // output that support for the kind needs to be added here.
- out << n.getKind() << ' ';
+ default:
+ // fall back on however the kind prints itself; this probably
+ // won't be SMT-LIB v2 compliant, but it will be clear from the
+ // output that support for the kind needs to be added here.
+ out << n.getKind() << ' ';
}
if( n.getMetaKind() == kind::metakind::PARAMETERIZED &&
stillNeedToPrintParams ) {
case kind::SINGLETON: return "singleton";
case kind::INSERT: return "insert";
case kind::COMPLEMENT: return "complement";
+ case kind::CARD: return "card";
+ case kind::JOIN: return "join";
+ case kind::PRODUCT: return "product";
+ case kind::TRANSPOSE: return "transpose";
+ case kind::TCLOSURE:
+ return "tclosure";
// fp theory
case kind::FLOATINGPOINT_FP: return "fp";
}
*/
} else {
- out << c << endl;
+ DatatypeDeclarationCommand* c1 = (DatatypeDeclarationCommand*)c;
+ const vector<DatatypeType>& datatypes = c1->getDatatypes();
+ if (!datatypes[0].isTuple()) {
+ out << c << endl;
+ }
}
}
{
const vector<DatatypeType>& datatypes = c->getDatatypes();
out << "(declare-";
- Assert( !datatypes.empty() );
- if( datatypes[0].getDatatype().isCodatatype() ){
+ Assert(!datatypes.empty());
+ if (datatypes[0].getDatatype().isCodatatype())
+ {
out << "co";
}
out << "datatypes";
- if(v == smt2_6_variant) {
+ if (v == smt2_6_variant)
+ {
out << " (";
- for(vector<DatatypeType>::const_iterator i = datatypes.begin(),
- i_end = datatypes.end();
- i != i_end; ++i) {
- const Datatype & d = i->getDatatype();
+ for (vector<DatatypeType>::const_iterator i = datatypes.begin(),
+ i_end = datatypes.end();
+ i != i_end;
+ ++i)
+ {
+ const Datatype& d = i->getDatatype();
out << "(" << maybeQuoteSymbol(d.getName());
out << " " << d.getNumParameters() << ")";
}
out << ") (";
- for(vector<DatatypeType>::const_iterator i = datatypes.begin(),
- i_end = datatypes.end();
- i != i_end; ++i) {
- const Datatype & d = i->getDatatype();
+ for (vector<DatatypeType>::const_iterator i = datatypes.begin(),
+ i_end = datatypes.end();
+ i != i_end;
+ ++i)
+ {
+ const Datatype& d = i->getDatatype();
out << "(";
- toStream( out, d );
+ toStream(out, d);
out << ")" << endl;
}
out << ")";
- }else{
+ }
+ else
+ {
out << " () (";
- for(vector<DatatypeType>::const_iterator i = datatypes.begin(),
- i_end = datatypes.end();
- i != i_end; ++i) {
- const Datatype & d = i->getDatatype();
+ for (vector<DatatypeType>::const_iterator i = datatypes.begin(),
+ i_end = datatypes.end();
+ i != i_end;
+ ++i)
+ {
+ const Datatype& d = i->getDatatype();
out << "(" << maybeQuoteSymbol(d.getName()) << " ";
- toStream( out, d );
+ toStream(out, d);
out << ")" << endl;
}
out << ")";
projects / cvc5.git / commitdiff