From 022dbeb9e2dc925cf0dcffb75ea57aedf09395de Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Tue, 26 Jan 2021 13:10:33 -0300 Subject: [PATCH] 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. --- src/api/cvc4cpp.cpp | 24 +++++++++ src/api/cvc4cpp.h | 15 ++++++ src/expr/symbol_table.cpp | 52 ++++++++++--------- test/regress/CMakeLists.txt | 3 +- test/regress/regress0/parser/define_sort.smt2 | 5 ++ test/unit/api/solver_black.cpp | 13 +++++ 6 files changed, 86 insertions(+), 26 deletions(-) create mode 100644 test/regress/regress0/parser/define_sort.smt2 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& 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& sorts, + const std::vector& replacements) const +{ + NodeManagerScope scope(d_solver->getNodeManager()); + + std::vector 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 @@ -476,6 +476,21 @@ class CVC4_PUBLIC Sort */ Sort instantiate(const std::vector& 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& sorts, + const std::vector& 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(Debug("sort"), ", ")); - Debug("sort") << p.first.back() << "]" << endl << "parameters ["; - copy(params.begin(), - params.end() - 1, - ostream_iterator(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(Debug("sort"), ", ")); + Debug("sort") << p.first.back() << "]" << std::endl << "parameters ["; + copy(params.begin(), + params.end() - 1, + ostream_iterator(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); -- 2.30.2