diff options
| -rw-r--r-- | src/parser/smt2/Smt2.g | 58 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 8 | ||||
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 237 | ||||
| -rw-r--r-- | test/regress/regress0/datatypes/Makefile.am | 4 | ||||
| -rw-r--r-- | test/regress/regress0/datatypes/tuples-empty.smt2 | 14 | ||||
| -rw-r--r-- | test/regress/regress0/datatypes/tuples-multitype.smt2 | 11 | ||||
| -rw-r--r-- | test/regress/regress0/rels/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/rels/relations-ops.smt2 | 23 |
8 files changed, 268 insertions, 90 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 81f62ccf4..d424fefad 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1980,11 +1980,33 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] | 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()); @@ -2347,6 +2369,25 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] { //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); + } ; /** @@ -2565,6 +2606,11 @@ indexedFunctionName[CVC4::Expr& op, CVC4::Kind& kind] 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 @@ -2843,6 +2889,8 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check] 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); @@ -3137,6 +3185,8 @@ INST_CLOSURE_TOK : 'inst-closure'; 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 diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 381a60fa8..e4f6569b8 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -240,14 +240,22 @@ void Smt2::addTheory(Theory theory) { addOperator(kind::INSERT, "insert"); addOperator(kind::CARD, "card"); addOperator(kind::COMPLEMENT, "complement"); + addOperator(kind::JOIN, "join"); + addOperator(kind::PRODUCT, "product"); + addOperator(kind::TRANSPOSE, "transpose"); + addOperator(kind::TCLOSURE, "tclosure"); break; case THEORY_DATATYPES: + { + const std::vector<Type> types; + defineType("Tuple", getExprManager()->mkTupleType(types)); Parser::addOperator(kind::APPLY_CONSTRUCTOR); Parser::addOperator(kind::APPLY_TESTER); Parser::addOperator(kind::APPLY_SELECTOR); Parser::addOperator(kind::APPLY_SELECTOR_TOTAL); break; + } case THEORY_STRINGS: defineType("String", getExprManager()->stringType()); diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index c13c519ae..54fc10719 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -252,11 +252,32 @@ void Smt2Printer::toStream(std::ostream& out, } 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>(); @@ -549,6 +570,11 @@ void Smt2Printer::toStream(std::ostream& out, 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; @@ -624,80 +650,103 @@ void Smt2Printer::toStream(std::ostream& out, 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 ) { @@ -917,6 +966,12 @@ static string smtKindString(Kind k) 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"; @@ -1326,7 +1381,11 @@ void Smt2Printer::toStream(std::ostream& out, } */ } else { - out << c << endl; + DatatypeDeclarationCommand* c1 = (DatatypeDeclarationCommand*)c; + const vector<DatatypeType>& datatypes = c1->getDatatypes(); + if (!datatypes[0].isTuple()) { + out << c << endl; + } } } @@ -1762,38 +1821,48 @@ static void toStream(std::ostream& out, { 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 << ")"; diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index d346c0056..a71c15869 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -84,7 +84,9 @@ TESTS = \ jsat-2.6.smt2 \ acyclicity-sr-ground096.smt2 \ model-subterms-min.smt2 \ - issue1433.smt2 + issue1433.smt2 \ + tuples-empty.smt2 \ + tuples-multitype.smt2 # rec5 -- no longer support subrange types FAILING_TESTS = \ diff --git a/test/regress/regress0/datatypes/tuples-empty.smt2 b/test/regress/regress0/datatypes/tuples-empty.smt2 new file mode 100644 index 000000000..ec7e36ca8 --- /dev/null +++ b/test/regress/regress0/datatypes/tuples-empty.smt2 @@ -0,0 +1,14 @@ +; EXPECT: sat + +(set-logic ALL) +(set-info :status sat) + +(declare-fun t () Tuple) +(declare-fun t1 () (Tuple (Tuple Int Int) (Tuple Int String Int))) +(declare-fun t2 () (Tuple (Tuple Bool Int) String)) + +(assert (= t1 (mkTuple (mkTuple 12 99) (mkTuple 5 "xyz" 17)))) +(assert (= t2 (mkTuple (mkTuple true 14) "abc"))) +(assert (= t mkTuple)) + +(check-sat) diff --git a/test/regress/regress0/datatypes/tuples-multitype.smt2 b/test/regress/regress0/datatypes/tuples-multitype.smt2 new file mode 100644 index 000000000..8e412f2ed --- /dev/null +++ b/test/regress/regress0/datatypes/tuples-multitype.smt2 @@ -0,0 +1,11 @@ +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) + +(declare-fun t () (Tuple Int String)) +(declare-fun i () String) + +(assert (= t (mkTuple 0 "0"))) +(assert (= i ((_ tupSel 1) t))) + +(check-sat) diff --git a/test/regress/regress0/rels/Makefile.am b/test/regress/regress0/rels/Makefile.am index 7f772a8e1..c8fb739d0 100644 --- a/test/regress/regress0/rels/Makefile.am +++ b/test/regress/regress0/rels/Makefile.am @@ -113,7 +113,8 @@ TESTS = \ joinImg_1.cvc \ joinImg_2_1.cvc \ joinImg_2.cvc \ - card_transpose.cvc + card_transpose.cvc \ + relations-ops.smt2 # unsolved : garbage_collect.cvc diff --git a/test/regress/regress0/rels/relations-ops.smt2 b/test/regress/regress0/rels/relations-ops.smt2 new file mode 100644 index 000000000..abb7faf10 --- /dev/null +++ b/test/regress/regress0/rels/relations-ops.smt2 @@ -0,0 +1,23 @@ +; EXPECT: sat +(set-logic ALL) +(set-info :status sat) + +(declare-fun r1 () (Set (Tuple String Int))) +(declare-fun r2 () (Set (Tuple Int String))) +(declare-fun r () (Set (Tuple String String))) +(declare-fun s () (Set (Tuple String String))) +(declare-fun t () (Set (Tuple String Int Int String))) +(declare-fun lt1 () (Set (Tuple Int Int))) +(declare-fun lt2 () (Set (Tuple Int Int))) +(declare-fun i () Int) + +(assert (= r1 (insert (mkTuple "a" 1) (mkTuple "b" 2) (mkTuple "c" 3) (singleton (mkTuple "d" 4))))) +(assert (= r2 (insert (mkTuple 1 "1") (mkTuple 2 "2") (mkTuple 3 "3") (singleton (mkTuple 17 "17"))))) +(assert (= r (join r1 r2))) +(assert (= s (transpose r))) +(assert (= t (product r1 r2))) +(assert (= lt1 (insert (mkTuple 1 2) (mkTuple 2 3) (mkTuple 3 4) (singleton (mkTuple 4 5))))) +(assert (= lt2 (tclosure lt1))) +(assert (= i (card t))) + +(check-sat) |