diff options
| -rw-r--r-- | src/api/cvc4cpp.cpp | 24 | ||||
| -rw-r--r-- | src/api/cvc4cpp.h | 15 | ||||
| -rw-r--r-- | src/expr/symbol_table.cpp | 52 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 3 | ||||
| -rw-r--r-- | test/regress/regress0/parser/define_sort.smt2 | 5 | ||||
| -rw-r--r-- | test/unit/api/solver_black.cpp | 13 |
6 files changed, 86 insertions, 26 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index e845bf876..abec4d8dd 100644 --- 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 98752c697..66ba4f23b 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -477,6 +477,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 4dd43d414..8d5e36554 100644 --- 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 810ed8128..ad066cf1e 100644 --- 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 index 000000000..790c21bde --- /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 e89d31e7d..82a176498 100644 --- 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); |