Reestablishing support for define-sort (#5810)

Presumable broken since 3ed42d7ab. This extends the API to have a substitute method for Sort that in needed for doing the Sort substitution in the case of define-sort.

This fixes issue #5809.

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index e845bf876efb428033135098f4ef245ce2aaf8bd..abec4d8ddc07061a2e045aa811e748cf4866ea8d 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1082,6 +1082,30 @@ Sort Sort::instantiate(const std::vector<Sort>& params) const
   return Sort(d_solver, d_solver->getNodeManager()->mkSort(*d_type, tparams));
 }
 
+Sort Sort::substitute(const Sort& sort, const Sort& replacement) const
+{
+  NodeManagerScope scope(d_solver->getNodeManager());
+  return Sort(
+      d_solver,
+      d_type->substitute(sort.getTypeNode(), replacement.getTypeNode()));
+}
+
+Sort Sort::substitute(const std::vector<Sort>& sorts,
+                      const std::vector<Sort>& replacements) const
+{
+  NodeManagerScope scope(d_solver->getNodeManager());
+
+  std::vector<CVC4::TypeNode> tSorts = sortVectorToTypeNodes(sorts),
+                              tReplacements =
+                                  sortVectorToTypeNodes(replacements);
+
+  return Sort(d_solver,
+              d_type->substitute(tSorts.begin(),
+                                 tSorts.end(),
+                                 tReplacements.begin(),
+                                 tReplacements.end()));
+}
+
 std::string Sort::toString() const
 {
   if (d_solver != nullptr)

diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 98752c697fcfe9df768116a0001fefd3e65687a9..66ba4f23b322edb4c2359af0c2296122e1e4c82f 100644 (file)
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -476,6 +476,21 @@ class CVC4_PUBLIC Sort
    */
   Sort instantiate(const std::vector<Sort>& params) const;
 
+  /**
+   * Substitution of Sorts.
+   * @param sort the subsort to be substituted within this sort.
+   * @param replacement the sort replacing the substituted subsort.
+   */
+  Sort substitute(const Sort& sort, const Sort& replacement) const;
+
+  /**
+   * Simultaneous substitution of Sorts.
+   * @param sorts the subsorts to be substituted within this sort.
+   * @param replacements the sort replacing the substituted subsorts.
+   */
+  Sort substitute(const std::vector<Sort>& sorts,
+                  const std::vector<Sort>& replacements) const;
+
   /**
    * Output a string representation of this sort to a given stream.
    * @param out the output stream

diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp
index 4dd43d414a07457aa1c141e2cc204234200994df..8d5e3655473f31248e08be1c6d71c3b42c54d6d2 100644 (file)
--- a/src/expr/symbol_table.cpp
+++ b/src/expr/symbol_table.cpp
@@ -503,35 +503,37 @@ api::Sort SymbolTable::Implementation::lookupType(
     PrettyCheckArgument(p.second.isUninterpretedSort(), name.c_str());
     return p.second;
   }
-  if (p.second.isSortConstructor()) {
-    if (Debug.isOn("sort")) {
-      Debug("sort") << "instantiating using a sort constructor" << endl;
-      Debug("sort") << "have formals [";
-      copy(p.first.begin(),
-           p.first.end() - 1,
-           ostream_iterator<api::Sort>(Debug("sort"), ", "));
-      Debug("sort") << p.first.back() << "]" << endl << "parameters   [";
-      copy(params.begin(),
-           params.end() - 1,
-           ostream_iterator<api::Sort>(Debug("sort"), ", "));
-      Debug("sort") << params.back() << "]" << endl
-                    << "type ctor    " << name << endl
-                    << "type is      " << p.second << endl;
-    }
-
-    api::Sort instantiation = p.second.instantiate(params);
-
-    Debug("sort") << "instance is  " << instantiation << endl;
-
-    return instantiation;
-  } else if (p.second.isDatatype()) {
+  if (p.second.isDatatype())
+  {
     PrettyCheckArgument(
         p.second.isParametricDatatype(), name, "expected parametric datatype");
     return p.second.instantiate(params);
   }
-  // failed to instantiate
-  Unhandled() << "Could not instantiate sort";
-  return p.second;
+  bool isSortConstructor = p.second.isSortConstructor();
+  if (Debug.isOn("sort"))
+  {
+    Debug("sort") << "instantiating using a sort "
+                  << (isSortConstructor ? "constructor" : "substitution")
+                  << std::endl;
+    Debug("sort") << "have formals [";
+    copy(p.first.begin(),
+         p.first.end() - 1,
+         ostream_iterator<api::Sort>(Debug("sort"), ", "));
+    Debug("sort") << p.first.back() << "]" << std::endl << "parameters   [";
+    copy(params.begin(),
+         params.end() - 1,
+         ostream_iterator<api::Sort>(Debug("sort"), ", "));
+    Debug("sort") << params.back() << "]" << endl
+                  << "type ctor    " << name << std::endl
+                  << "type is      " << p.second << std::endl;
+  }
+  api::Sort instantiation = isSortConstructor
+                                ? p.second.instantiate(params)
+                                : p.second.substitute(p.first, params);
+
+  Debug("sort") << "instance is  " << instantiation << std::endl;
+
+  return instantiation;
 }
 
 size_t SymbolTable::Implementation::lookupArity(const string& name) {

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 810ed81282e3350ad1c2104527a43455e7e947d6..ad066cf1ed18b4bed71f86baf92154a625275613 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -719,6 +719,7 @@ set(regress_0_tests
   regress0/parser/bv_nat.smt2
   regress0/parser/constraint.smt2
   regress0/parser/declarefun-emptyset-uf.smt2
+  regress0/parser/define_sort.smt2
   regress0/parser/force_logic_set_logic.smt2
   regress0/parser/force_logic_success.smt2
   regress0/parser/issue5163.smt2
@@ -1547,7 +1548,7 @@ set(regress_1_tests
   regress1/issue3990-sort-inference.smt2
   regress1/issue4273-ext-rew-cache.smt2
   regress1/issue4335-unsat-core.smt2
-  regress1/issue5739-rtf-processed.smt2 
+  regress1/issue5739-rtf-processed.smt2
   regress1/lemmas/clocksynchro_5clocks.main_invar.base.smtv1.smt2
   regress1/lemmas/pursuit-safety-8.smtv1.smt2
   regress1/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2

diff --git a/test/regress/regress0/parser/define_sort.smt2 b/test/regress/regress0/parser/define_sort.smt2
new file mode 100644 (file)
index 0000000..790c21b
--- /dev/null
+++ b/test/regress/regress0/parser/define_sort.smt2
@@ -0,0 +1,5 @@
+; EXPECT: sat
+(set-logic ALIA)
+(define-sort Stream (T) (Array Int T))
+(define-sort IntStream () (Stream Int))
+(check-sat)

diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index e89d31e7de4d8ca4729fb72b921f7979e9663fb2..82a176498f1daca31f21f0804b8976b2e862e985 100644 (file)
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -965,6 +965,19 @@ TEST_F(TestApiSolverBlack, declareSort)
   ASSERT_NO_THROW(d_solver.declareSort("", 2));
 }
 
+TEST_F(TestApiSolverBlack, defineSort)
+{
+  Sort sortVar0 = d_solver.mkParamSort("T0");
+  Sort sortVar1 = d_solver.mkParamSort("T1");
+  Sort intSort = d_solver.getIntegerSort();
+  Sort realSort = d_solver.getRealSort();
+  Sort arraySort0 = d_solver.mkArraySort(sortVar0, sortVar0);
+  Sort arraySort1 = d_solver.mkArraySort(sortVar0, sortVar1);
+  // Now create instantiations of the defined sorts
+  ASSERT_NO_THROW(arraySort0.substitute(sortVar0, intSort));
+  ASSERT_NO_THROW(arraySort1.substitute({sortVar0, sortVar1}, {intSort, realSort}));
+}
+
 TEST_F(TestApiSolverBlack, defineFun)
 {
   Sort bvSort = d_solver.mkBitVectorSort(32);