From f997af30b7d5dd30e01a72b00ddf3859c0049fdc Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 21 Jun 2017 14:21:45 -0500 Subject: [PATCH] Properly handle subtypes in smt2 printer. --- src/printer/smt2/smt2_printer.cpp | 129 ++++++++++++++++++----- src/printer/smt2/smt2_printer.h | 2 +- test/regress/regress0/arith/mult.02.smt2 | 2 +- 3 files changed, 107 insertions(+), 26 deletions(-) diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 98993dba5..4dd6e73aa 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -61,14 +61,14 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, theory::SubstitutionMap::const_iterator i_end = lets.end(); for(; i != i_end; ++ i) { out << "(let (("; - toStream(out, (*i).second, toDepth, types); + toStream(out, (*i).second, toDepth, types, TypeNode::null()); out << ' '; - toStream(out, (*i).first, toDepth, types); + toStream(out, (*i).first, toDepth, types, TypeNode::null()); out << ")) "; } } Node body = dv.getDagifiedBody(); - toStream(out, body, toDepth, types); + toStream(out, body, toDepth, types, TypeNode::null()); if(!lets.empty()) { theory::SubstitutionMap::const_iterator i = lets.begin(); theory::SubstitutionMap::const_iterator i_end = lets.end(); @@ -77,7 +77,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, } } } else { - toStream(out, n, toDepth, types); + toStream(out, n, toDepth, types, TypeNode::null()); } } @@ -107,14 +107,30 @@ static bool stringifyRegexp(Node n, stringstream& ss) { return true; } +// force_nt is the type that n must have void Smt2Printer::toStream(std::ostream& out, TNode n, - int toDepth, bool types) const throw() { + int toDepth, bool types, TypeNode force_nt) const throw() { // null if(n.getKind() == kind::NULL_EXPR) { out << "null"; return; } + if( !force_nt.isNull() && n.getKind()!=kind::CONST_RATIONAL ){ + if( n.getType()!=force_nt ){ + if( force_nt.isReal() ){ + out << "(" << smtKindString( force_nt.isInteger() ? kind::TO_INTEGER : kind::TO_REAL) << " "; + toStream(out, n, toDepth, types, TypeNode::null()); + out << ")"; + }else{ + Node nn = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, + NodeManager::currentNM()->mkConst(AscriptionType(force_nt.toType())), n ); + toStream(out, nn, toDepth, types, TypeNode::null()); + } + return; + } + } + // variable if(n.isVar()) { string s; @@ -216,10 +232,10 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, if(r < 0) { out << "-" << -r; }else{ - toStreamRational(out, r, false); + toStreamRational(out, r, !force_nt.isNull() && !force_nt.isInteger()); } }else{ - toStreamRational(out, r, false); + toStreamRational(out, r, !force_nt.isNull() && !force_nt.isInteger()); } // Rational r = n.getConst(); // if(r < 0) { @@ -314,8 +330,8 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, } if(n.getNumChildren() != 0) { for(unsigned i = 0; i < n.getNumChildren(); ++i) { - out << ' '; - toStream(out, n[i], toDepth, types); + out << ' '; + toStream(out, n[i], toDepth, types, TypeNode::null()); } out << ')'; } @@ -324,6 +340,8 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, bool stillNeedToPrintParams = true; bool forceBinary = false; // force N-ary to binary when outputing children + bool parametricTypeChildren = false; // parametric operators that are (op t1 ... tn) where t1...tn must have same type + bool typeChildren = false; // operators (op t1...tn) where at least one of t1...tn may require a type cast e.g. Int -> Real // operator if(n.getNumChildren() != 0 && n.getKind() != kind::INST_PATTERN_LIST && @@ -334,7 +352,10 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, // builtin theory case kind::APPLY: break; case kind::EQUAL: - case kind::DISTINCT: out << smtKindString(k) << " "; break; + case kind::DISTINCT: + out << smtKindString(k) << " "; + parametricTypeChildren = true; + break; case kind::CHAIN: break; case kind::FUNCTION_TYPE: for(size_t i = 0; i < n.getNumChildren() - 1; ++i) { @@ -356,7 +377,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::ITE: out << smtKindString(k) << " "; break; // uf theory - case kind::APPLY_UF: break; + case kind::APPLY_UF: typeChildren = true; break; // arith theory case kind::PLUS: @@ -378,7 +399,10 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::IS_INTEGER: case kind::TO_INTEGER: case kind::TO_REAL: - case kind::POW: out << smtKindString(k) << " "; break; + case kind::POW: + parametricTypeChildren = true; + out << smtKindString(k) << " "; + break; case kind::DIVISIBLE: out << "(_ divisible " << n.getOperator().getConst().k << ")"; @@ -387,7 +411,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, // arrays theory case kind::SELECT: - case kind::STORE: + case kind::STORE: typeChildren = true; case kind::PARTIAL_SELECT_0: case kind::PARTIAL_SELECT_1: case kind::ARRAY_TYPE: out << smtKindString(k) << " "; break; @@ -397,7 +421,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, if(d_variant == z3str_variant) { out << "Concat "; for(unsigned i = 0; i < n.getNumChildren(); ++i) { - toStream(out, n[i], -1, types); + toStream(out, n[i], -1, types, TypeNode::null()); if(i + 1 < n.getNumChildren()) { out << ' '; } @@ -416,10 +440,10 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, stringstream ss; if(d_variant == z3str_variant && stringifyRegexp(n[1], ss)) { out << "= "; - toStream(out, n[0], -1, types); + toStream(out, n[0], -1, types, TypeNode::null()); out << " "; Node str = NodeManager::currentNM()->mkConst(String(ss.str())); - toStream(out, str, -1, types); + toStream(out, str, -1, types, TypeNode::null()); out << ")"; return; } @@ -508,7 +532,10 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::INTERSECTION: case kind::SETMINUS: case kind::SUBSET: - case kind::MEMBER: + parametricTypeChildren = true; + out << smtKindString(k) << " "; + break; + case kind::MEMBER: typeChildren = true; case kind::SET_TYPE: case kind::SINGLETON: case kind::COMPLEMENT:out << smtKindString(k) << " "; break; @@ -575,12 +602,12 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, return; } out << "(as "; - toStream(out, n[0], toDepth < 0 ? toDepth : toDepth - 1, types); + toStream(out, n[0], toDepth < 0 ? toDepth : toDepth - 1, types, TypeNode::null()); out << ' ' << (t.isFunctionLike() ? t.getRangeType() : t) << ')'; return; } break; - case kind::APPLY_CONSTRUCTOR: + case kind::APPLY_CONSTRUCTOR: typeChildren = true; case kind::APPLY_TESTER: case kind::APPLY_SELECTOR: case kind::APPLY_SELECTOR_TOTAL: @@ -660,7 +687,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, if(toDepth != 0) { if( d_variant==sygus_variant && n.getKind()==kind::APPLY_CONSTRUCTOR ){ std::stringstream ss; - toStream(ss, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, types); + toStream(ss, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, types, TypeNode::null()); std::string tmp = ss.str(); size_t pos = 0; if((pos = tmp.find("__Enum__", pos)) != std::string::npos){ @@ -672,14 +699,14 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr()); if( d_variant==smt2_6_variant ){ out << "(_ is "; - toStream(out, Node::fromExpr(dt[cindex].getConstructor()), toDepth < 0 ? toDepth : toDepth - 1, types); + toStream(out, Node::fromExpr(dt[cindex].getConstructor()), toDepth < 0 ? toDepth : toDepth - 1, types, TypeNode::null()); out << ")"; }else{ out << "is-"; - toStream(out, Node::fromExpr(dt[cindex].getConstructor()), toDepth < 0 ? toDepth : toDepth - 1, types); + toStream(out, Node::fromExpr(dt[cindex].getConstructor()), toDepth < 0 ? toDepth : toDepth - 1, types, TypeNode::null()); } }else{ - toStream(out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, types); + toStream(out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, types, TypeNode::null()); } } else { out << "(...)"; @@ -689,9 +716,63 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, } } stringstream parens; + + // calculate the child type casts + std::map< unsigned, TypeNode > force_child_type; + if( parametricTypeChildren ){ + if( n.getNumChildren()>1 ){ + TypeNode force_ct = n[0].getType(); + bool do_force = false; + for(size_t i = 1; i < n.getNumChildren(); ++i ) { + TypeNode ct = n[i].getType(); + if( ct!=force_ct ){ + force_ct = TypeNode::leastCommonTypeNode( force_ct, ct ); + do_force = true; + } + } + if( do_force ){ + for(size_t i = 0; i < n.getNumChildren(); ++i ) { + force_child_type[i] = force_ct; + } + } + } + // operators that may require type casting + }else if( typeChildren ){ + if(n.getKind()==kind::SELECT){ + TypeNode indexType = TypeNode::leastCommonTypeNode( n[0].getType().getArrayIndexType(), n[1].getType() ); + TypeNode elemType = n[0].getType().getArrayConstituentType(); + force_child_type[0] = NodeManager::currentNM()->mkArrayType( indexType, elemType ); + force_child_type[1] = indexType; + }else if(n.getKind()==kind::STORE){ + TypeNode indexType = TypeNode::leastCommonTypeNode( n[0].getType().getArrayIndexType(), n[1].getType() ); + TypeNode elemType = TypeNode::leastCommonTypeNode( n[0].getType().getArrayConstituentType(), n[2].getType() ); + force_child_type[0] = NodeManager::currentNM()->mkArrayType( indexType, elemType ); + force_child_type[1] = indexType; + force_child_type[2] = elemType; + }else if(n.getKind()==kind::MEMBER){ + TypeNode elemType = TypeNode::leastCommonTypeNode( n[0].getType(), n[1].getType().getSetElementType() ); + force_child_type[0] = elemType; + force_child_type[1] = NodeManager::currentNM()->mkSetType( elemType ); + }else{ + // APPLY_UF, APPLY_CONSTRUCTOR, etc. + Assert( n.hasOperator() ); + TypeNode opt = n.getOperator().getType(); + Assert( opt.getNumChildren() == n.getNumChildren() + 1 ); + for(size_t i = 0; i < n.getNumChildren(); ++i ) { + force_child_type[i] = opt[i]; + } + } + } + for(size_t i = 0, c = 1; i < n.getNumChildren(); ) { if(toDepth != 0) { - toStream(out, n[i], toDepth < 0 ? toDepth : toDepth - c, types); + Node cn = n[i]; + std::map< unsigned, TypeNode >::iterator itfc = force_child_type.find( i ); + if( itfc!=force_child_type.end() ){ + toStream(out, cn, toDepth < 0 ? toDepth : toDepth - c, types, itfc->second); + }else{ + toStream(out, cn, toDepth < 0 ? toDepth : toDepth - c, types, TypeNode::null()); + } } else { out << "(...)"; } diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index d73f11b59..eeba0b12a 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -38,7 +38,7 @@ enum Variant { class Smt2Printer : public CVC4::Printer { Variant d_variant; - void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw(); + void toStream(std::ostream& out, TNode n, int toDepth, bool types, TypeNode nt) const throw(); void toStream(std::ostream& out, const Model& m, const Command* c) const throw(); public: Smt2Printer(Variant variant = no_variant) : d_variant(variant) { } diff --git a/test/regress/regress0/arith/mult.02.smt2 b/test/regress/regress0/arith/mult.02.smt2 index 54b876d38..57167fc76 100644 --- a/test/regress/regress0/arith/mult.02.smt2 +++ b/test/regress/regress0/arith/mult.02.smt2 @@ -1,5 +1,5 @@ ; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic. -; EXPECT: The fact in question: (>= (* (- 1) (* n n)) (- 1)) +; EXPECT: The fact in question: (>= (* (- 1.0) (* n n)) (- 1.0)) ; EXPECT: ") ; EXIT: 1 (set-logic QF_LRA) -- 2.30.2