From 7b815181bfd58100478970f52b80461638fd42a8 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 1 Aug 2018 19:10:47 -0500 Subject: [PATCH] Fix issues with printing parametric datatypes in smt2 (#2213) --- src/expr/expr_manager_template.cpp | 9 ++-- src/expr/expr_manager_template.h | 3 +- src/expr/node_manager.cpp | 6 ++- src/expr/node_manager.h | 6 ++- src/parser/parser.cpp | 14 ++++-- src/parser/parser.h | 5 +- src/parser/smt2/Smt2.g | 4 +- src/printer/smt2/smt2_printer.cpp | 73 +++++++++++++++++++++++++++++- src/smt/smt_engine.cpp | 7 ++- 9 files changed, 108 insertions(+), 19 deletions(-) diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 457e54d9b..de128b3e5 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -831,10 +831,13 @@ SortType ExprManager::mkSort(const std::string& name, uint32_t flags) const { } SortConstructorType ExprManager::mkSortConstructor(const std::string& name, - size_t arity) const { + size_t arity, + uint32_t flags) const +{ NodeManagerScope nms(d_nodeManager); - return SortConstructorType(Type(d_nodeManager, - new TypeNode(d_nodeManager->mkSortConstructor(name, arity)))); + return SortConstructorType( + Type(d_nodeManager, + new TypeNode(d_nodeManager->mkSortConstructor(name, arity, flags)))); } /** diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index f211aa4c8..a9cdfc587 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -434,7 +434,8 @@ public: /** Make a sort constructor from a name and arity. */ SortConstructorType mkSortConstructor(const std::string& name, - size_t arity) const; + size_t arity, + uint32_t flags = SORT_FLAG_NONE) const; /** * Get the type of an expression. diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index d03bc4b54..74701cf11 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -645,7 +645,9 @@ TypeNode NodeManager::mkSort(TypeNode constructor, } TypeNode NodeManager::mkSortConstructor(const std::string& name, - size_t arity) { + size_t arity, + uint32_t flags) +{ Assert(arity > 0); NodeBuilder<> nb(this, kind::SORT_TYPE); Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG); @@ -654,7 +656,7 @@ TypeNode NodeManager::mkSortConstructor(const std::string& name, setAttribute(type, expr::VarNameAttr(), name); setAttribute(type, expr::SortArityAttr(), arity); for(std::vector::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { - (*i)->nmNotifyNewSortConstructor(type); + (*i)->nmNotifyNewSortConstructor(type, flags); } return type; } diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 996caad87..71082ef9d 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -60,7 +60,7 @@ class NodeManagerListener { public: virtual ~NodeManagerListener() {} virtual void nmNotifyNewSort(TypeNode tn, uint32_t flags) {} - virtual void nmNotifyNewSortConstructor(TypeNode tn) {} + virtual void nmNotifyNewSortConstructor(TypeNode tn, uint32_t flags) {} virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort, uint32_t flags) {} virtual void nmNotifyNewDatatypes( @@ -875,7 +875,9 @@ public: uint32_t flags = ExprManager::SORT_FLAG_NONE); /** Make a new sort with the given name and arity. */ - TypeNode mkSortConstructor(const std::string& name, size_t arity); + TypeNode mkSortConstructor(const std::string& name, + size_t arity, + uint32_t flags = ExprManager::SORT_FLAG_NONE); /** * Get the type for the given node and optionally do type checking. diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 1f9c3fd2b..47124a589 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -324,10 +324,13 @@ SortType Parser::mkSort(const std::string& name, uint32_t flags) { } SortConstructorType Parser::mkSortConstructor(const std::string& name, - size_t arity) { + size_t arity, + uint32_t flags) +{ Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")" << std::endl; - SortConstructorType type = d_exprManager->mkSortConstructor(name, arity); + SortConstructorType type = + d_exprManager->mkSortConstructor(name, arity, flags); defineType(name, vector(arity), type); return type; } @@ -340,7 +343,8 @@ SortType Parser::mkUnresolvedType(const std::string& name) { SortConstructorType Parser::mkUnresolvedTypeConstructor(const std::string& name, size_t arity) { - SortConstructorType unresolved = mkSortConstructor(name, arity); + SortConstructorType unresolved = + mkSortConstructor(name, arity, ExprManager::SORT_FLAG_PLACEHOLDER); d_unresolved.insert(unresolved); return unresolved; } @@ -349,8 +353,8 @@ SortConstructorType Parser::mkUnresolvedTypeConstructor( const std::string& name, const std::vector& params) { Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size() << ")" << std::endl; - SortConstructorType unresolved = - d_exprManager->mkSortConstructor(name, params.size()); + SortConstructorType unresolved = d_exprManager->mkSortConstructor( + name, params.size(), ExprManager::SORT_FLAG_PLACEHOLDER); defineType(name, params, unresolved); Type t = getSort(name, params); d_unresolved.insert(unresolved); diff --git a/src/parser/parser.h b/src/parser/parser.h index 769f4c812..78cbcaafb 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -540,7 +540,10 @@ public: /** * Creates a new sort constructor with the given name and arity. */ - SortConstructorType mkSortConstructor(const std::string& name, size_t arity); + SortConstructorType mkSortConstructor( + const std::string& name, + size_t arity, + uint32_t flags = ExprManager::SORT_FLAG_NONE); /** * Creates a new "unresolved type," used only during parsing. diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index b52be77bb..d3bec9d42 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1479,7 +1479,7 @@ datatypes_2_5_DefCommand[bool isCo, std::unique_ptr* cmd] PARSER_STATE->pushScope(true); } LPAREN_TOK /* parametric sorts */ ( symbol[name,CHECK_UNDECLARED,SYM_SORT] - { sorts.push_back( PARSER_STATE->mkSort(name) ); } + { sorts.push_back( PARSER_STATE->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER) ); } )* RPAREN_TOK LPAREN_TOK ( LPAREN_TOK datatypeDef[isCo, dts, sorts] RPAREN_TOK )+ RPAREN_TOK @@ -1550,7 +1550,7 @@ datatypesDef[bool isCo, } ( PAR_TOK { PARSER_STATE->pushScope(true); } LPAREN_TOK ( symbol[name,CHECK_UNDECLARED,SYM_SORT] - { params.push_back( PARSER_STATE->mkSort(name) ); } + { params.push_back( PARSER_STATE->mkSort(name, ExprManager::SORT_FLAG_PLACEHOLDER) ); } )* RPAREN_TOK { // if the arity was fixed by prelude and is not equal to the number of parameters diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 64a52c23f..9c3bdc539 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -836,6 +836,18 @@ void Smt2Printer::toStream(std::ostream& out, // APPLY_UF, APPLY_CONSTRUCTOR, etc. Assert( n.hasOperator() ); TypeNode opt = n.getOperator().getType(); + if (n.getKind() == kind::APPLY_CONSTRUCTOR) + { + Type tn = n.getType().toType(); + // may be parametric, in which case the constructor type must be + // specialized + const Datatype& dt = static_cast(tn).getDatatype(); + if (dt.isParametric()) + { + unsigned ci = Datatype::indexOf(n.getOperator().toExpr()); + opt = TypeNode::fromType(dt[ci].getSpecializedConstructorType(tn)); + } + } Assert( opt.getNumChildren() == n.getNumChildren() + 1 ); for(size_t i = 0; i < n.getNumChildren(); ++i ) { force_child_type[i] = opt[i]; @@ -1908,15 +1920,74 @@ static void toStream(std::ostream& out, ++i) { const Datatype& d = i->getDatatype(); + if (d.isParametric()) + { + out << "(par ("; + for (unsigned p = 0, nparam = d.getNumParameters(); p < nparam; p++) + { + out << (p > 0 ? " " : "") << d.getParameter(p); + } + out << ")"; + } out << "("; toStream(out, d); out << ")"; + if (d.isParametric()) + { + out << ")"; + } } out << ")"; } else { - out << " () ("; + out << " ("; + // Can only print if all datatypes in this block have the same parameters. + // In theory, given input language 2.6 and output language 2.5, it could + // be impossible to print a datatype block where datatypes were given + // different parameter lists. + bool success = true; + const Datatype& d = datatypes[0].getDatatype(); + unsigned nparam = d.getNumParameters(); + for (unsigned j = 1, ndt = datatypes.size(); j < ndt; j++) + { + const Datatype& dj = datatypes[j].getDatatype(); + if (dj.getNumParameters() != nparam) + { + success = false; + } + else + { + // must also have identical parameter lists + for (unsigned k = 0; k < nparam; k++) + { + if (dj.getParameter(k) != d.getParameter(k)) + { + success = false; + break; + } + } + } + if (!success) + { + break; + } + } + if (success) + { + for (unsigned j = 0; j < nparam; j++) + { + out << (j > 0 ? " " : "") << d.getParameter(j); + } + } + else + { + out << std::endl; + out << "ERROR: datatypes in each block must have identical parameter " + "lists."; + out << std::endl; + } + out << ") ("; for (vector::const_iterator i = datatypes.begin(), i_end = datatypes.end(); i != i_end; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index cfafd63c4..116d2fe23 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -759,12 +759,15 @@ public: } } - void nmNotifyNewSortConstructor(TypeNode tn) override + void nmNotifyNewSortConstructor(TypeNode tn, uint32_t flags) override { DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()), tn.getAttribute(expr::SortArityAttr()), tn.toType()); - d_smt.addToModelCommandAndDump(c); + if ((flags & ExprManager::SORT_FLAG_PLACEHOLDER) == 0) + { + d_smt.addToModelCommandAndDump(c); + } } void nmNotifyNewDatatypes(const std::vector& dtts) override -- 2.30.2