stanford-centaur · makaimann · Aug 28, 2020 · Aug 28, 2020 · Aug 28, 2020 · Aug 28, 2020
diff --git a/btor/include/boolector_solver.h b/btor/include/boolector_solver.h
@@ -75,7 +75,7 @@ class BoolectorSolver : public AbsSmtSolver
                  const Sort & sort2,
                  const Sort & sort3) const override;
   Sort make_sort(SortKind sk, const SortVec & sorts) const override;
-
+  Sort make_sort(const Sort & sort_con, const SortVec & sorts) const override;
   Sort make_sort(const DatatypeDecl & d) const override;
 
   DatatypeDecl make_datatype_decl(const std::string & s) override;

diff --git a/btor/include/boolector_sort.h b/btor/include/boolector_sort.h
@@ -40,6 +40,8 @@ class BoolectorSortBase : public AbsSort
   SortVec get_domain_sorts() const override;
   Sort get_codomain_sort() const override;
   std::string get_uninterpreted_name() const override;
+  size_t get_arity() const override;
+  SortVec get_uninterpreted_param_sorts() const override;
   Datatype get_datatype() const override;
   bool compare(const Sort s) const override;
   SortKind get_sort_kind() const override { return sk; };

diff --git a/btor/src/boolector_solver.cpp b/btor/src/boolector_solver.cpp
@@ -645,6 +645,14 @@ Sort BoolectorSolver::make_sort(SortKind sk, const SortVec & sorts) const
   }
 }
 
+Sort BoolectorSolver::make_sort(const Sort & sort_con,
+                                const SortVec & sorts) const
+
+{
+  throw IncorrectUsageException(
+      "Boolector does not support uninterpreted sort construction");
+}
+
 Term BoolectorSolver::make_symbol(const std::string name, const Sort & sort)
 {
   // check that name is available

diff --git a/btor/src/boolector_sort.cpp b/btor/src/boolector_sort.cpp
@@ -75,12 +75,23 @@ std::string BoolectorSortBase::get_uninterpreted_name() const
       "Boolector doesn't support uninterpreted sorts.");
 }
 
+size_t BoolectorSortBase::get_arity() const
+{
+  throw NotImplementedException(
+      "Boolector does not support uninterpreted sorts");
+}
 
-Datatype BoolectorSortBase::get_datatype() const {
+SortVec BoolectorSortBase::get_uninterpreted_param_sorts() const
+{
+  throw NotImplementedException(
+      "Boolector does not support uninterpreted sorts.");
+}
+
+Datatype BoolectorSortBase::get_datatype() const
+{
   throw NotImplementedException("get_datatype");
 };
 
-
 bool BoolectorSortBase::compare(const Sort s) const
 {
   std::shared_ptr<BoolectorSortBase> bs =

diff --git a/cvc4/include/cvc4_solver.h b/cvc4/include/cvc4_solver.h
@@ -74,6 +74,7 @@ class CVC4Solver : public AbsSmtSolver
                  const Sort & sort2,
                  const Sort & sort3) const override;
   Sort make_sort(SortKind sk, const SortVec & sorts) const override;
+  Sort make_sort(const Sort & sort_con, const SortVec & sorts) const override;
   Sort make_sort(const DatatypeDecl & d) const override;
 
   DatatypeDecl make_datatype_decl(const std::string & s) override;

diff --git a/cvc4/include/cvc4_sort.h b/cvc4/include/cvc4_sort.h
@@ -42,6 +42,8 @@ namespace smt
     SortVec get_domain_sorts() const override;
     Sort get_codomain_sort() const override;
     std::string get_uninterpreted_name() const override;
+    size_t get_arity() const override;
+    SortVec get_uninterpreted_param_sorts() const override;
     Datatype get_datatype() const override;
     bool compare(const Sort) const override;
     SortKind get_sort_kind() const override;

diff --git a/cvc4/src/cvc4_solver.cpp b/cvc4/src/cvc4_solver.cpp
@@ -592,6 +592,24 @@ Sort CVC4Solver::make_sort(SortKind sk, const SortVec & sorts) const
   }
 }
 
+Sort CVC4Solver::make_sort(const Sort & sort_con, const SortVec & sorts) const
+{
+  ::CVC4::api::Sort csort_con =
+      std::static_pointer_cast<CVC4Sort>(sort_con)->sort;
+
+  size_t arity = sorts.size();
+  std::vector<::CVC4::api::Sort> csorts;
+  csorts.reserve(sorts.size());
+  ::CVC4::api::Sort csort;
+  for (uint32_t i = 0; i < arity; i++)
+  {
+    csort = std::static_pointer_cast<CVC4Sort>(sorts[i])->sort;
+    csorts.push_back(csort);
+  }
+
+  return std::make_shared<CVC4Sort>(csort_con.instantiate(csorts));
+}
+
 Term CVC4Solver::make_symbol(const std::string name, const Sort & sort)
 {
   // check that name is available

diff --git a/cvc4/src/cvc4_sort.cpp b/cvc4/src/cvc4_sort.cpp
@@ -67,24 +67,53 @@ Sort CVC4Sort::get_codomain_sort() const
 
 std::string CVC4Sort::get_uninterpreted_name() const { return sort.toString(); }
 
+size_t CVC4Sort::get_arity() const
+{
+  try
+  {
+    if (sort.isUninterpretedSort())
+    {
+      return 0;
+    }
+    else
+    {
+      return sort.getSortConstructorArity();
+    }
+  }
+  catch (::CVC4::api::CVC4ApiException & e)
+  {
+    throw InternalSolverException(e.what());
+  }
+}
+
+SortVec CVC4Sort::get_uninterpreted_param_sorts() const
+{
+  SortVec param_sorts;
+  for (auto cs : sort.getUninterpretedSortParamSorts())
+  {
+    param_sorts.push_back(std::make_shared<CVC4Sort>(cs));
+  }
+  return param_sorts;
+}
+
 bool CVC4Sort::compare(const Sort s) const
 {
-  std::shared_ptr<CVC4Sort> cs = std::static_pointer_cast<CVC4Sort> (s);
+  std::shared_ptr<CVC4Sort> cs = std::static_pointer_cast<CVC4Sort>(s);
   return sort == cs->sort;
 }
 
 Datatype CVC4Sort::get_datatype() const
 {
   try
   {
-    return std::make_shared<CVC4Datatype> (sort.getDatatype());
-  } catch (::CVC4::api::CVC4ApiException & e)
+    return std::make_shared<CVC4Datatype>(sort.getDatatype());
+  }
+  catch (::CVC4::api::CVC4ApiException & e)
   {
     throw InternalSolverException(e.what());
   }
 };
 
-
 SortKind CVC4Sort::get_sort_kind() const
 {
   if (sort.isBoolean())
@@ -115,6 +144,10 @@ SortKind CVC4Sort::get_sort_kind() const
   {
     return UNINTERPRETED;
   }
+  else if (sort.isSortConstructor())
+  {
+    return UNINTERPRETED_CONS;
+  }
   else if (sort.isDatatype())
   {
     return DATATYPE;

diff --git a/include/logging_solver.h b/include/logging_solver.h
@@ -42,6 +42,7 @@ class LoggingSolver : public AbsSmtSolver
                  const Sort & sort2,
                  const Sort & sort3) const override;
   Sort make_sort(const SortKind sk, const SortVec & sorts) const override;
+  Sort make_sort(const Sort & sort_con, const SortVec & sorts) const override;
   Sort make_sort(const DatatypeDecl & d) const override;
 
   DatatypeDecl make_datatype_decl(const std::string & s) override;

diff --git a/include/logging_sort.h b/include/logging_sort.h
@@ -26,6 +26,10 @@ namespace smt {
 // Sort s is the underlying sort
 // all other sorts are LoggingSorts
 Sort make_uninterpreted_logging_sort(Sort s, std::string name, uint64_t arity);
+Sort make_uninterpreted_logging_sort(Sort s,
+                                     std::string name,
+                                     uint64_t arity,
+                                     const SortVec & sorts);
 Sort make_logging_sort(SortKind sk, Sort s);
 Sort make_logging_sort(SortKind sk, Sort s, uint64_t width);
 Sort make_logging_sort(SortKind sk, Sort s, Sort sort1);
@@ -86,6 +90,18 @@ class LoggingSort : public AbsSort
         "get_uninterpreted_name not implemented by generic LoggingSort");
   }
 
+  size_t get_arity() const override
+  {
+    throw NotImplementedException(
+        "get_arity not implemented by generic LoggingSort");
+  }
+
+  SortVec get_uninterpreted_param_sorts() const override
+  {
+    throw NotImplementedException(
+        "get_uninterpreted_param_sorts not implemented by generic LoggingSort");
+  }
+
   Datatype get_datatype() const override
   {
     throw NotImplementedException(
@@ -150,15 +166,22 @@ class UninterpretedLoggingSort : public LoggingSort
 {
  public:
   UninterpretedLoggingSort(Sort s, std::string n, uint64_t a);
+  UninterpretedLoggingSort(Sort s,
+                           std::string n,
+                           uint64_t a,
+                           const SortVec & sorts);
   ~UninterpretedLoggingSort();
 
   typedef LoggingSort super;
 
   std::string get_uninterpreted_name() const override;
+  size_t get_arity() const override;
+  SortVec get_uninterpreted_param_sorts() const override;
 
  protected:
   std::string name;
   uint64_t arity;
+  SortVec param_sorts;
 };
 
 }  // namespace smt
diff --git a/include/printing_solver.h b/include/printing_solver.h
@@ -81,6 +81,7 @@ class PrintingSolver : public AbsSmtSolver
                  const Sort & sort2,
                  const Sort & sort3) const override;
   Sort make_sort(const SortKind sk, const SortVec & sorts) const override;
+  Sort make_sort(const Sort & sort_con, const SortVec & sorts) const override;
   Sort make_sort(const DatatypeDecl & d) const override;
   DatatypeDecl make_datatype_decl(const std::string & s) override;
   DatatypeConstructorDecl make_datatype_constructor_decl(

diff --git a/include/solver.h b/include/solver.h
@@ -174,6 +174,15 @@ class AbsSmtSolver
    */
   virtual Sort make_sort(const SortKind sk, const SortVec & sorts) const = 0;
 
+  /* Create an uninterpreted sort
+   * @param sort_con a sort with SortKind UNINTERPRETED_CONS (must have
+   * nonzero arity)
+   * @param sorts a vector of sorts of size matching sort_con->get_arity()
+   * @return a Sort object
+   */
+  virtual Sort make_sort(const Sort & sort_con,
+                         const SortVec & sorts) const = 0;
+
   /* Create a datatype sort
    * @param d the Datatype Declaration
    * @return a Sort object

diff --git a/include/sort.h b/include/sort.h
@@ -40,6 +40,9 @@ enum SortKind
   REAL,
   FUNCTION,
   UNINTERPRETED,
+  // an uninterpreted sort constructor (has non-zero arity and takes subsort
+  // arguments)
+  UNINTERPRETED_CONS,
   DATATYPE,
 
   /** IMPORTANT: This must stay at the bottom.
@@ -71,6 +74,8 @@ class AbsSort
   virtual std::vector<Sort> get_domain_sorts() const = 0;
   virtual Sort get_codomain_sort() const = 0;
   virtual std::string get_uninterpreted_name() const = 0;
+  virtual size_t get_arity() const = 0;
+  virtual std::vector<Sort> get_uninterpreted_param_sorts() const = 0;
   virtual Datatype get_datatype() const = 0;
   virtual bool compare(const Sort sort) const = 0;
   virtual SortKind get_sort_kind() const = 0;
@@ -103,7 +108,6 @@ template <>
 struct hash<smt::Sort>
 {
   size_t operator()(const smt::Sort & s) const { return s->hash(); }
-  };
-
+};
 }
 
diff --git a/include/term_translator.h b/include/term_translator.h
@@ -63,7 +63,7 @@ class TermTranslator
    *  @param the sort transfer
    *  @return a sort belonging to this solver
    */
-  Sort transfer_sort(const Sort & sort) const;
+  Sort transfer_sort(const Sort & sort);
 
   /** Transfers a term from the other solver to this solver
    *  @param term the term to transfer to the member variable solver
@@ -93,7 +93,7 @@ class TermTranslator
    *  called in this function)
    *  @return a term with the given value
    */
-  Term value_from_smt2(const std::string val, const Sort sort) const;
+  Term value_from_smt2(const std::string val, const Sort sort);
 
   /** identifies relevant casts to perform an operation
    *  assumes the operation is currently not well-sorted
@@ -135,6 +135,10 @@ class TermTranslator
   // it can still call non-const methods of the solver
   SmtSolver solver;  ///< solver to translate terms to
   UnorderedTermMap cache;
+  // map from uninterpreted sort names to the sort in the destination solver
+  // necessary because it needs to be the same exact uninterpreted sort
+  // cannot recreate it with the same name and get the same object back
+  std::unordered_map<std::string, Sort> uninterpreted_sorts;
 };
 }  // namespace smt
 
diff --git a/msat/include/msat_solver.h b/msat/include/msat_solver.h
@@ -87,6 +87,7 @@ class MsatSolver : public AbsSmtSolver
                  const Sort & sort2,
                  const Sort & sort3) const override;
   Sort make_sort(SortKind sk, const SortVec & sorts) const override;
+  Sort make_sort(const Sort & sort_con, const SortVec & sorts) const override;
 
   Sort make_sort(const DatatypeDecl & d) const override;
 

diff --git a/msat/include/msat_sort.h b/msat/include/msat_sort.h
@@ -37,6 +37,8 @@ class MsatSort : public AbsSort
   SortVec get_domain_sorts() const override;
   Sort get_codomain_sort() const override;
   std::string get_uninterpreted_name() const override;
+  size_t get_arity() const override;
+  SortVec get_uninterpreted_param_sorts() const override;
   Datatype get_datatype() const override;
   bool compare(const Sort) const override;
   SortKind get_sort_kind() const override;

diff --git a/msat/src/msat_solver.cpp b/msat/src/msat_solver.cpp
@@ -484,6 +484,11 @@ Sort MsatSolver::make_sort(SortKind sk, const SortVec & sorts) const
   }
 }
 
+Sort MsatSolver::make_sort(const Sort & sort_con, const SortVec & sorts) const
+{
+  throw NotImplementedException(
+      "MathSAT does not support uninterpreted sort constructors");
+}
 
 Sort MsatSolver::make_sort(const DatatypeDecl & d) const {
   throw NotImplementedException("MsatSolver::make_sort");

diff --git a/msat/src/msat_sort.cpp b/msat/src/msat_sort.cpp
@@ -116,11 +116,23 @@ string MsatSort::get_uninterpreted_name() const
   return res;
 }
 
-Datatype MsatSort::get_datatype() const {
+size_t MsatSort::get_arity() const
+{
+  // MathSAT does not support uninterpreted sorts with non-zero arity
+  return 0;
+}
+
+SortVec MsatSort::get_uninterpreted_param_sorts() const
+{
+  throw NotImplementedException(
+      "MathSAT does not support uninterpreted sort constructors");
+}
+
+Datatype MsatSort::get_datatype() const
+{
   throw NotImplementedException("get_datatype");
 };
 
-
 bool MsatSort::compare(const Sort s) const
 {
   std::shared_ptr<MsatSort> msort = std::static_pointer_cast<MsatSort>(s);

diff --git a/src/logging_solver.cpp b/src/logging_solver.cpp
@@ -112,6 +112,24 @@ Sort LoggingSolver::make_sort(SortKind sk, const SortVec & sorts) const
   return make_logging_sort(sk, sort, sorts);
 }
 
+Sort LoggingSolver::make_sort(const Sort & sort_con,
+                              const SortVec & sorts) const
+{
+  Sort sub_sort_con = static_pointer_cast<LoggingSort>(sort_con)->wrapped_sort;
+
+  // convert to sorts stored by LoggingSorts
+  SortVec sub_sorts;
+  for (auto s : sorts)
+  {
+    sub_sorts.push_back(static_pointer_cast<LoggingSort>(s)->wrapped_sort);
+  }
+
+  Sort ressort = wrapped_solver->make_sort(sub_sort_con, sub_sorts);
+  return make_uninterpreted_logging_sort(ressort,
+                                         sort_con->get_uninterpreted_name(),
+                                         0,  // has zero arity after applied
+                                         sorts);
+}
 
 Sort LoggingSolver::make_sort(const DatatypeDecl & d) const {
   throw NotImplementedException("LoggingSolver::make_sort");