Utilities in preparation for print benchmark utility (#7190)

This adds a few utilities in preparation for the print benchmark utility, which will replace our own dumping infrastructure.

diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp
index 31a22b44a96683fbc2a2250c37e00c587ee77d3a..fdb397d3960d7cdd65c04213c5b498c5894d1426 100644 (file)
--- a/src/expr/dtype.cpp
+++ b/src/expr/dtype.cpp
@@ -895,6 +895,19 @@ const std::vector<std::shared_ptr<DTypeConstructor> >& DType::getConstructors()
   return d_constructors;
 }
 
+std::unordered_set<TypeNode> DType::getSubfieldTypes() const
+{
+  std::unordered_set<TypeNode> subFieldTypes;
+  for (std::shared_ptr<DTypeConstructor> ctor : d_constructors)
+  {
+    for (size_t i = 0, nargs = ctor->getNumArgs(); i < nargs; i++)
+    {
+      subFieldTypes.insert(ctor->getArgType(i));
+    }
+  }
+  return subFieldTypes;
+}
+
 std::ostream& operator<<(std::ostream& os, const DType& dt)
 {
   // can only output datatypes in the cvc5 native language

diff --git a/src/expr/dtype.h b/src/expr/dtype.h
index a608b9adb584ee7058074d26ce624463b0bc01d0..4f54f0af79312aac793edd94fc98f49a2a703ba1 100644 (file)
--- a/src/expr/dtype.h
+++ b/src/expr/dtype.h
@@ -425,6 +425,12 @@ class DType
   const std::vector<std::shared_ptr<DTypeConstructor> >& getConstructors()
       const;
 
+  /**
+   * Return the subfield types of this datatype. This is the set of all types T
+   * for which there exists an argument to a constructor of type T.
+   */
+  std::unordered_set<TypeNode> getSubfieldTypes() const;
+
   /** prints this datatype to stream */
   void toStream(std::ostream& out) const;
 

diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index e038952c48d52e6a3d6a04ba332549e9a3f50a7d..9bd68e6971f0629990a34c68a260d4e238e20903 100644 (file)
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -204,6 +204,13 @@ void Printer::toStreamCmdDeclareFunction(std::ostream& out,
   printUnknownCommand(out, "declare-fun");
 }
 
+void Printer::toStreamCmdDeclareFunction(std::ostream& out, const Node& v) const
+{
+  std::stringstream vs;
+  vs << v;
+  toStreamCmdDeclareFunction(out, vs.str(), v.getType());
+}
+
 void Printer::toStreamCmdDeclarePool(std::ostream& out,
                                      const std::string& id,
                                      TypeNode type,
@@ -235,6 +242,25 @@ void Printer::toStreamCmdDefineFunction(std::ostream& out,
   printUnknownCommand(out, "define-fun");
 }
 
+void Printer::toStreamCmdDefineFunction(std::ostream& out,
+                                        Node v,
+                                        Node lambda) const
+{
+  std::stringstream vs;
+  vs << v;
+  std::vector<Node> formals;
+  Node body = lambda;
+  TypeNode rangeType = v.getType();
+  if (body.getKind() == kind::LAMBDA)
+  {
+    formals.insert(formals.end(), lambda[0].begin(), lambda[0].end());
+    body = lambda[1];
+    Assert(rangeType.isFunction());
+    rangeType = rangeType.getRangeType();
+  }
+  toStreamCmdDefineFunction(out, vs.str(), formals, rangeType, body);
+}
+
 void Printer::toStreamCmdDefineFunctionRec(
     std::ostream& out,
     const std::vector<Node>& funcs,
@@ -244,6 +270,32 @@ void Printer::toStreamCmdDefineFunctionRec(
   printUnknownCommand(out, "define-fun-rec");
 }
 
+void Printer::toStreamCmdDefineFunctionRec(
+    std::ostream& out,
+    const std::vector<Node>& funcs,
+    const std::vector<Node>& lambdas) const
+{
+  std::vector<std::vector<Node>> formals;
+  std::vector<Node> formulas;
+  for (const Node& l : lambdas)
+  {
+    std::vector<Node> formalsVec;
+    Node formula;
+    if (l.getKind() == kind::LAMBDA)
+    {
+      formalsVec.insert(formalsVec.end(), l[0].begin(), l[0].end());
+      formula = l[1];
+    }
+    else
+    {
+      formula = l;
+    }
+    formals.emplace_back(formalsVec);
+    formulas.emplace_back(formula);
+  }
+  toStreamCmdDefineFunctionRec(out, funcs, formals, formulas);
+}
+
 void Printer::toStreamCmdSetUserAttribute(std::ostream& out,
                                           const std::string& attr,
                                           Node n) const

diff --git a/src/printer/printer.h b/src/printer/printer.h
index 5e141fe8fdfd0d228b410fdff4499911fb1c1061..5ffe07f775e0ae060f4a4d8682dd3ca653903a52 100644 (file)
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -87,6 +87,8 @@ class Printer
   virtual void toStreamCmdDeclareFunction(std::ostream& out,
                                           const std::string& id,
                                           TypeNode type) const;
+  /** Variant of above for a pre-existing variable */
+  void toStreamCmdDeclareFunction(std::ostream& out, const Node& v) const;
   /** Print declare-pool command */
   virtual void toStreamCmdDeclarePool(std::ostream& out,
                                       const std::string& id,
@@ -109,6 +111,8 @@ class Printer
                                          const std::vector<Node>& formals,
                                          TypeNode range,
                                          Node formula) const;
+  /** Variant of above that takes the definition */
+  void toStreamCmdDefineFunction(std::ostream& out, Node v, Node lambda) const;
 
   /** Print define-fun-rec command */
   virtual void toStreamCmdDefineFunctionRec(
@@ -116,6 +120,10 @@ class Printer
       const std::vector<Node>& funcs,
       const std::vector<std::vector<Node>>& formals,
       const std::vector<Node>& formulas) const;
+  /** Variant of above that takes the definition */
+  void toStreamCmdDefineFunctionRec(std::ostream& out,
+                                    const std::vector<Node>& funcs,
+                                    const std::vector<Node>& lambdas) const;
 
   /** Print set-user-attribute command */
   void toStreamCmdSetUserAttribute(std::ostream& out,

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 522c38040f436367bb381449e61149ec34ffdd35..adfd2f71d75f3882e0b9ff192824e7f328fe376e 100644 (file)
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1186,8 +1186,8 @@ void DeclareFunctionCommand::toStream(std::ostream& out,
                                       size_t dag,
                                       Language language) const
 {
-  Printer::getPrinter(language)->toStreamCmdDeclareFunction(
-      out, d_func.toString(), sortToTypeNode(d_sort));
+  Printer::getPrinter(language)->toStreamCmdDeclareFunction(out,
+                                                            termToNode(d_func));
 }
 
 /* -------------------------------------------------------------------------- */