Parametric and mutually recursive datatypes

include/generic_datatype.h

@@ -25,11 +25,16 @@ class GenericDatatypeDecl : public AbsDatatypeDecl
  public:
   GenericDatatypeDecl(const std::string name);
   virtual ~GenericDatatypeDecl(){};
-  std::string get_name();
+  std::string get_name() const;
+  int get_param_count() const;
+  std::vector<Sort> get_param_sorts();
+  void register_param_sort(std::string param_name);
 
  protected:
   friend class GenericSolver;
   std::string dt_name;
+  int param_count;
+  std::vector<Sort> param_sorts;
 };
 
 class GenericDatatypeConstructorDecl : public AbsDatatypeConstructorDecl
@@ -46,10 +51,13 @@ class GenericDatatypeConstructorDecl : public AbsDatatypeConstructorDecl
   int get_selector_count() const;
   bool compare(const DatatypeConstructorDecl & d) const override;
   std::string get_dt_name() const;
+  void add_selector_param(const std::string & name, int param_num);
 
  protected:
   std::vector<SelectorComponents> selector_vector;
   std::string cons_name;
+  bool contains_param;
+
   DatatypeDecl dt_decl;
   // Setter for the dt_decl member. Only to be used when a constructor
   // is added to a datatype. datatype_decl: The DatatypeDecl of the datatype.
@@ -85,6 +93,7 @@ class GenericDatatype : public AbsDatatype
 
  protected:
   DatatypeDecl dt_decl;
+
   std::vector<DatatypeConstructorDecl> cons_decl_vector;
 
   friend class GenericSolver;

include/generic_solver.h

@@ -50,7 +50,9 @@ class GenericSolver : public AbsSmtSolver
   Sort make_sort(const Sort & sort_con, const SortVec & sorts) const override;
   // Mutually recursive datatypes are currently not supported.
   Sort make_sort(const DatatypeDecl & d) const override;
+
   DatatypeDecl make_datatype_decl(const std::string & s) override;
+
   DatatypeConstructorDecl make_datatype_constructor_decl(
       const std::string s) override;
   void add_constructor(DatatypeDecl & dt,
@@ -60,11 +62,16 @@ class GenericSolver : public AbsSmtSolver
                     const Sort & s) const override;
   void add_selector_self(DatatypeConstructorDecl & dt,
                          const std::string & name) const override;
+  Sort get_unresolved_sort(DatatypeDecl dt_decl);
+
   Term get_constructor(const Sort & s, std::string name) const override;
   Term get_tester(const Sort & s, std::string name) const override;
   Term get_selector(const Sort & s,
                     std::string con,
                     std::string name) const override;
+  SortVec make_datatype_sorts(
+      const std::vector<DatatypeDecl> & decls,
+      const UnorderedSortSet & uninterp_sorts) const override;
 
   /***************************************************************/
   /* methods from AbsSmtSolver that are implemented              */
@@ -266,6 +273,7 @@ class GenericSolver : public AbsSmtSolver
   std::unique_ptr<
       std::unordered_map<std::shared_ptr<GenericDatatype>, std::string>>
       datatype_name_map;
+  std::unique_ptr<std::unordered_map<int, std::string>> par_map;
 };
 
 }  // namespace smt

include/generic_sort.h

@@ -26,6 +26,7 @@
 namespace smt {
 
 class GenericDatatye;
+
 /* Helper functions for creating generic sorts */
 Sort make_uninterpreted_generic_sort(std::string name, uint64_t arity);
 Sort make_uninterpreted_generic_sort(Sort sort_cons, const SortVec& sorts);
@@ -37,6 +38,9 @@ Sort make_generic_sort(SortKind sk, Sort sort1, Sort sort2, Sort sort3);
 Sort make_generic_sort(SortKind sk, SortVec sorts);
 Sort make_generic_sort(Datatype dt);
 Sort make_generic_sort(SortKind sk, std::string cons_name, Sort dt);
+Sort make_generic_param_sort(std::string param_name);
+Sort make_generic_datatype_sort(Datatype dt);
+Sort make_generic_unresolved_sort(DatatypeDecl dt);
 /* smtlib representation of sort kinds */
 std::string to_smtlib(SortKind);
 
@@ -232,4 +236,32 @@ class DatatypeComponentSort : public GenericSort
   Sort selector_sort;
 };
 
+class ParamSort : public GenericSort
+{
+ public:
+  ParamSort(std::string param_name);
+  ~ParamSort(){};
+  std::string get_uninterpreted_name() const override;
+  std::string compute_string() const override;
+
+ protected:
+  std::string name;
+};
+
+class UnresolvedSort : public GenericSort
+{
+ public:
+  UnresolvedSort(DatatypeDecl dt_decl);
+  ~UnresolvedSort(){};
+  std::string compute_string() const override;
+  std::string to_string() const override;
+  DatatypeDecl get_datatype_decl();
+  std::vector<std::string> get_params();
+  void insert_param(std::string new_param);
+
+ protected:
+  DatatypeDecl datatype_decl;
+  std::vector<std::string> params_vector;
+};
+
 }  // namespace smt

include/solver.h

@@ -239,15 +239,15 @@ class AbsSmtSolver
    *  If no symbol of that name has been declared, throws
    *  IncorrectUsageException
    *
-   *  Allows a user to look up a symbol by name. This can be very useful for term
-   *  translation, since we can look up symbols instead of keeping track of the
-   *  mapping via externally populated caches (in the case where the target
+   *  Allows a user to look up a symbol by name. This can be very useful for
+   * term translation, since we can look up symbols instead of keeping track of
+   * the mapping via externally populated caches (in the case where the target
    *  solver has already been used).
    *
-   *  Note, solver backend deals with the implementation. The main motivation for
-   *  this is that each backend solver has to own the symbol table. If the symbol
-   *  table were stored in AbsSmtSolver then it would get destructed after the
-   *  backend solver which has bad refcounting implications for many solvers.
+   *  Note, solver backend deals with the implementation. The main motivation
+   * for this is that each backend solver has to own the symbol table. If the
+   * symbol table were stored in AbsSmtSolver then it would get destructed after
+   * the backend solver which has bad refcounting implications for many solvers.
    *
    *  @param name the name of the symbol to look up
    *  @return the Term representation of the corresponding symbol

include/sort.h

@@ -47,6 +47,8 @@ enum SortKind
   CONSTRUCTOR,
   SELECTOR,
   TESTER,
+  PARAM,
+  UNRESOLVED,
 
   /** IMPORTANT: This must stay at the bottom.
       It's only use is for sizing the kind2str array

src/generic_datatype.cpp

@@ -11,15 +11,37 @@ using namespace std;
 
 namespace smt {
 
-GenericDatatypeDecl::GenericDatatypeDecl(const std::string name) : dt_name(name)
+GenericDatatypeDecl::GenericDatatypeDecl(const std::string name)
+    : dt_name(name), param_count(0)
 {
 }
 
-std::string GenericDatatypeDecl::get_name() { return dt_name; }
+std::string GenericDatatypeDecl::get_name() const { return dt_name; }
+
+int GenericDatatypeDecl::get_param_count() const { return param_count; }
+
+std::vector<Sort> GenericDatatypeDecl::get_param_sorts() { return param_sorts; }
+
+void GenericDatatypeDecl::register_param_sort(std::string param_name)
+{
+  for (unsigned int i = 0; i < param_count; ++i)
+  {
+    // Checks if the selector has already been added
+    if (param_sorts[i]->to_string() == param_name)
+    {
+      // throw "Can't add selector. It already exists in this
+      // datatype!";
+      return;
+    }
+  }
+  Sort new_param = make_generic_param_sort(param_name);
+  param_sorts.push_back(new_param);
+  param_count += 1;
+}
 
 GenericDatatypeConstructorDecl::GenericDatatypeConstructorDecl(
     const std::string & name)
-    : cons_name(name)
+    : cons_name(name), contains_param(false)
 {
 }
 
@@ -87,6 +109,21 @@ void GenericDatatype::add_constructor(
   }
   shared_ptr<GenericDatatypeConstructorDecl> gdt_cons =
       static_pointer_cast<GenericDatatypeConstructorDecl>(dt_cons_decl);
+
+  if (gdt_cons->contains_param == true)
+  {
+    for (int i = 0; i < gdt_cons->get_selector_count(); ++i)
+    {
+      if (gdt_cons->get_selector_vector()[i].sort->get_sort_kind()
+          == SortKind::PARAM)
+      {
+        static_pointer_cast<GenericDatatypeDecl>(dt_decl)->register_param_sort(
+            static_pointer_cast<ParamSort>(
+                gdt_cons->get_selector_vector()[i].sort)
+                ->to_string());
+      }
+    }
+  }
   // Links the constructor to the datatype_decl of the datatype
   gdt_cons->update_stored_dt(dt_decl);
   // Links the datatype to the new constructor