Fix issues with printing parametric datatypes in smt2 (#2213)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 2 Aug 2018 00:10:47 +0000 (19:10 -0500)
committerGitHub <noreply@github.com>
Thu, 2 Aug 2018 00:10:47 +0000 (19:10 -0500)
src/expr/expr_manager_template.cpp
src/expr/expr_manager_template.h
src/expr/node_manager.cpp
src/expr/node_manager.h
src/parser/parser.cpp
src/parser/parser.h
src/parser/smt2/Smt2.g
src/printer/smt2/smt2_printer.cpp
src/smt/smt_engine.cpp

index 457e54d9bfe169493a8343e06864146607a54593..de128b3e510e8d0e259957920220a15e4908e32f 100644 (file)
@@ -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))));
 }
 
 /**
index f211aa4c85eaee00f42c0400f25c66fe9f05e353..a9cdfc5874f6cbea0cfa4a9cd0aa1e863863b834 100644 (file)
@@ -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.
index d03bc4b54db8052d7e5bd11954665de69ad93118..74701cf11b2b79ae4b0eba78ed647385607c9003 100644 (file)
@@ -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<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
-    (*i)->nmNotifyNewSortConstructor(type);
+    (*i)->nmNotifyNewSortConstructor(type, flags);
   }
   return type;
 }
index 996caad8760e09261b4af580a0e84121e01d0f4a..71082ef9d8c5922c6c44beb30e8fa43f7912b613 100644 (file)
@@ -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.
index 1f9c3fd2b8883c33864f74787d725e2a984dabaa..47124a58958f71b1613051ef912ac0f5bad69439 100644 (file)
@@ -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<Type>(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<Type>& 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);
index 769f4c81276e84a90068919b7e49319e5f60bdf4..78cbcaafb220e8a32901de1e8dec0c6d0bb48e16 100644 (file)
@@ -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.
index b52be77bba1dc389564901a9553415d5e346d69a..d3bec9d42a2c029969458dbe8f3ef7f1c09bfd41 100644 (file)
@@ -1479,7 +1479,7 @@ datatypes_2_5_DefCommand[bool isCo, std::unique_ptr<CVC4::Command>* 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
index 64a52c23f512b5e36ad4cd3febfe004dc7617101..9c3bdc5392b93df08ded879f9b53da65b27a8dc7 100644 (file)
@@ -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<DatatypeType>(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<DatatypeType>::const_iterator i = datatypes.begin(),
                                               i_end = datatypes.end();
          i != i_end;
index cfafd63c401ad2a07a090a006bc623c3bd336dba..116d2fe233cb87fa9f6f914eddb2fde915cfee5c 100644 (file)
@@ -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<DatatypeType>& dtts) override