From 3e6de62d11dcb3cf266f58e68def2f2c2ce728c3 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 11 Sep 2019 16:29:21 -0500 Subject: [PATCH] Fix constructor type printing (#3246) --- src/printer/smt2/smt2_printer.cpp | 184 +++++++++--------- test/regress/CMakeLists.txt | 1 + .../datatypes/dt-param-2.6-print.smt2 | 20 ++ 3 files changed, 118 insertions(+), 87 deletions(-) create mode 100644 test/regress/regress0/datatypes/dt-param-2.6-print.smt2 diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index bd2d053e5..e9e8f2ea0 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -270,7 +270,7 @@ void Smt2Printer::toStream(std::ostream& out, } break; } - + case kind::UNINTERPRETED_CONSTANT: { const UninterpretedConstant& uc = n.getConst(); std::stringstream ss; @@ -473,12 +473,14 @@ void Smt2Printer::toStream(std::ostream& out, 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 + Kind k = n.getKind(); if(n.getNumChildren() != 0 && - n.getKind() != kind::INST_PATTERN_LIST && - n.getKind() != kind::APPLY_TYPE_ASCRIPTION) { + k != kind::INST_PATTERN_LIST && + k != kind::APPLY_TYPE_ASCRIPTION && + k != kind::CONSTRUCTOR_TYPE) { out << '('; } - switch(Kind k = n.getKind()) { + switch(k) { // builtin theory case kind::EQUAL: case kind::DISTINCT: @@ -781,102 +783,110 @@ void Smt2Printer::toStream(std::ostream& out, stillNeedToPrintParams = false; break; - case kind::APPLY_CONSTRUCTOR: + case kind::APPLY_CONSTRUCTOR: + { + typeChildren = true; + const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr()); + if (dt.isTuple()) { - typeChildren = true; - const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr()); - if (dt.isTuple()) - { - stillNeedToPrintParams = false; - out << "mkTuple" << ( dt[0].getNumArgs()==0 ? "" : " "); - } + stillNeedToPrintParams = false; + out << "mkTuple" << ( dt[0].getNumArgs()==0 ? "" : " "); } + break; + } + case kind::CONSTRUCTOR_TYPE: + { + out << n[n.getNumChildren()-1]; + return; + break; + } + 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, d_variant) << " "; break; + + case kind::SEP_NIL: + out << "(as sep.nil " << n.getType() << ")"; + break; - 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, d_variant) << " "; break; - - 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) + // 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 << n[2]; - out << ")"; + out << "(! "; } + } + if (n.getNumChildren() == 3) + { + out << n[2]; 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 << ")"; + 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(); + out << ')'; + if (++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++) + } + out << ')'; + return; + } + case kind::INST_PATTERN: break; + case kind::INST_PATTERN_LIST: + { + for (const Node& nc : n) + { + if (nc.getKind() == kind::INST_ATTRIBUTE) { - if (n[i].getKind() == kind::INST_ATTRIBUTE) - { - if (n[i][0].getAttribute(theory::FunDefAttribute())) - { - out << ":fun-def"; - } - } - else + if (nc[0].getAttribute(theory::FunDefAttribute())) { - out << ":pattern " << n[i]; + out << ":fun-def"; } } - 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() << ' '; + else + { + out << ":pattern " << nc; + } + } + 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() << ' '; } if( n.getMetaKind() == kind::metakind::PARAMETERIZED && stillNeedToPrintParams ) { diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 5b44128fc..56010858d 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -360,6 +360,7 @@ set(regress_0_tests regress0/datatypes/dt-2.6.smt2 regress0/datatypes/dt-match-pat-param-2.6.smt2 regress0/datatypes/dt-param-2.6.smt2 + regress0/datatypes/dt-param-2.6-print.smt2 regress0/datatypes/dt-param-card4-bool-sat.smt2 regress0/datatypes/dt-sel-2.6.smt2 regress0/datatypes/empty_tuprec.cvc diff --git a/test/regress/regress0/datatypes/dt-param-2.6-print.smt2 b/test/regress/regress0/datatypes/dt-param-2.6-print.smt2 new file mode 100644 index 000000000..165de0dba --- /dev/null +++ b/test/regress/regress0/datatypes/dt-param-2.6-print.smt2 @@ -0,0 +1,20 @@ +; EXPECT: sat +; EXPECT: (model +; EXPECT: (declare-datatypes ((Pair 2)) ((par (X Y)((mkPair (first X) (second Y)))))) +; EXPECT: (define-fun x () (Pair Int Real) ((as mkPair (Pair Int Real)) 2 (/ 3 2))) +; EXPECT: ) + +(set-logic ALL) +(set-option :produce-models true) +(set-info :status sat) +(declare-datatypes ( (Pair 2) ) ( +(par ( X Y ) ( (mkPair (first X) (second Y)))) +)) + + +(declare-fun x () (Pair Int Real)) + +(assert (= x (mkPair 2 1.5))) + +(check-sat) +(get-model) -- 2.30.2