Introduce SyGuS datatype API (#3465)

3 files changed, 193 insertions, 0 deletions

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 479b28cfb..0c1044e74 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -48,6 +48,8 @@ libcvc4_add_sources(
   datatype.cpp
   record.cpp
   record.h
+  sygus_datatype.cpp
+  sygus_datatype.h
   uninterpreted_constant.cpp
   uninterpreted_constant.h
 )
diff --git a/src/expr/sygus_datatype.cpp b/src/expr/sygus_datatype.cpp
new file mode 100644
index 000000000..be2b04402
--- /dev/null
+++ b/src/expr/sygus_datatype.cpp
@@ -0,0 +1,81 @@
+/*********************                                                        */
+/*! \file sygus_datatype.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of class for constructing SyGuS datatypes.
+ **/
+
+#include "expr/sygus_datatype.h"
+
+#include "printer/sygus_print_callback.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+
+SygusDatatype::SygusDatatype(const std::string& name) : d_dt(Datatype(name)) {}
+
+std::string SygusDatatype::getName() const { return d_dt.getName(); }
+
+void SygusDatatype::addConstructor(Node op,
+                                   const std::string& name,
+                                   std::shared_ptr<SygusPrintCallback> spc,
+                                   int weight,
+                                   const std::vector<TypeNode>& consTypes)
+{
+  d_ops.push_back(op);
+  d_cons_names.push_back(std::string(name));
+  d_pc.push_back(spc);
+  d_weight.push_back(weight);
+  d_consArgs.push_back(consTypes);
+}
+
+void SygusDatatype::addAnyConstantConstructor(TypeNode tn)
+{
+  // add an "any constant" proxy variable
+  Node av = NodeManager::currentNM()->mkSkolem("_any_constant", tn);
+  // mark that it represents any constant
+  SygusAnyConstAttribute saca;
+  av.setAttribute(saca, true);
+  std::stringstream ss;
+  ss << getName() << "_any_constant";
+  std::string cname(ss.str());
+  std::vector<TypeNode> builtinArg;
+  builtinArg.push_back(tn);
+  addConstructor(
+      av, cname, printer::SygusEmptyPrintCallback::getEmptyPC(), 0, builtinArg);
+}
+
+void SygusDatatype::initializeDatatype(TypeNode sygusType,
+                                       Node sygusVars,
+                                       bool allowConst,
+                                       bool allowAll)
+{
+  /* Use the sygus type to not lose reference to the original types (Bool,
+   * Int, etc) */
+  d_dt.setSygus(sygusType.toType(), sygusVars.toExpr(), allowConst, allowAll);
+  for (unsigned i = 0, size_d_ops = d_ops.size(); i < size_d_ops; ++i)
+  {
+    // must convert to type now
+    std::vector<Type> cargs;
+    for (TypeNode& ct : d_consArgs[i])
+    {
+      cargs.push_back(ct.toType());
+    }
+    // add (sygus) constructor
+    d_dt.addSygusConstructor(
+        d_ops[i].toExpr(), d_cons_names[i], cargs, d_pc[i], d_weight[i]);
+  }
+  Trace("sygus-type-cons") << "...built datatype " << d_dt << " ";
+}
+
+const Datatype& SygusDatatype::getDatatype() const { return d_dt; }
+
+}  // namespace CVC4
diff --git a/src/expr/sygus_datatype.h b/src/expr/sygus_datatype.h
new file mode 100644
index 000000000..d7b18644a
--- /dev/null
+++ b/src/expr/sygus_datatype.h
@@ -0,0 +1,110 @@
+/*********************                                                        */
+/*! \file sygus_datatype.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief A class for constructing SyGuS datatypes.
+ **/
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__SYGUS_DATATYPE_H
+#define CVC4__EXPR__SYGUS_DATATYPE_H
+
+#include <string>
+#include <vector>
+
+#include "expr/attribute.h"
+#include "expr/datatype.h"
+#include "expr/node.h"
+#include "expr/type_node.h"
+
+namespace CVC4 {
+
+/** Attribute true for variables that represent any constant */
+struct SygusAnyConstAttributeId
+{
+};
+typedef expr::Attribute<SygusAnyConstAttributeId, bool> SygusAnyConstAttribute;
+
+/**
+ * Keeps the necessary information for initializing a sygus datatype, which
+ * includes the operators, names, print callbacks and list of argument types
+ * for each constructor.
+ *
+ * It also maintains a datatype to represent the structure of the type node.
+ *
+ * Notice that this class is only responsible for setting SyGuS-related
+ * information regarding the datatype. It is still required that the user
+ * of this class construct the datatype type corresponding to the datatype
+ * e.g. via a call to ExprManager::mkMutualDatatypeTypes().
+ */
+class SygusDatatype
+{
+ public:
+  /** constructor */
+  SygusDatatype(const std::string& name);
+  ~SygusDatatype() {}
+  /** get the name of this datatype */
+  std::string getName() const;
+  /**
+   * Add constructor that encodes an application of builtin operator op.
+   *
+   * op: the builtin operator,
+   * name: the name of the constructor,
+   * spc: the print callback (for custom printing of this node),
+   * weight: the weight of this constructor,
+   * consTypes: the argument types of the constructor (typically other sygus
+   * datatype types).
+   */
+  void addConstructor(Node op,
+                      const std::string& name,
+                      std::shared_ptr<SygusPrintCallback> spc,
+                      int weight,
+                      const std::vector<TypeNode>& consTypes);
+  /**
+   * This adds a constructor that corresponds to the any constant constructor
+   * for the given (builtin) type tn.
+   */
+  void addAnyConstantConstructor(TypeNode tn);
+
+  /** builds a datatype with the information in the type object
+   *
+   * sygusType: the builtin type that this datatype encodes,
+   * sygusVars: the formal argument list of the function-to-synthesize,
+   * allowConst: whether the grammar corresponding to this datatype allows
+   * any constant,
+   * allowAll: whether the grammar corresponding to this datatype allows
+   * any term.
+   */
+  void initializeDatatype(TypeNode sygusType,
+                          Node sygusVars,
+                          bool allowConst,
+                          bool allowAll);
+  /** Get the sygus datatype initialized by this class */
+  const Datatype& getDatatype() const;
+
+ private:
+  //---------- information to build normalized type node
+  /** Operators for each constructor. */
+  std::vector<Node> d_ops;
+  /** Names for each constructor. */
+  std::vector<std::string> d_cons_names;
+  /** Print callbacks for each constructor */
+  std::vector<std::shared_ptr<SygusPrintCallback>> d_pc;
+  /** Weights for each constructor */
+  std::vector<int> d_weight;
+  /** List of argument types for each constructor */
+  std::vector<std::vector<TypeNode>> d_consArgs;
+  /** Datatype to represent type's structure */
+  Datatype d_dt;
+};
+
+}  // namespace CVC4
+
+#endif