From f05612e7501fde0f85a04c9c11fe94d4e8aefcdb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 6 Aug 2026 22:17:31 -0700 Subject: [PATCH] Fix nested datatype declaration printing (#10420) Normalize nested array and sequence accessor sorts before collecting mutually recursive datatype declarations, and cover both solver and benchmark printers. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: a8f87ede-b718-4fe9-9839-cc9eaaf9c3a7 --- src/ast/datatype_decl_plugin.cpp | 31 ++++++++++--------- src/test/parametric_datatype.cpp | 52 ++++++++++++++++++++++++++++++++ 2 files changed, 69 insertions(+), 14 deletions(-) diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index d875262b38..b9452292d0 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -1373,24 +1373,27 @@ namespace datatype { return get_constructor_idx(get_recognizer_constructor(f)); } + static sort* get_nested_sort(ast_manager& m, sort* s) { + array_util autil(m); + seq_util sutil(m); + sort* elem = nullptr; + while (true) { + if (autil.is_array(s)) + s = get_array_range(s); + else if (sutil.is_seq(s, elem)) + s = elem; + else + return s; + } + } + /** \brief Two datatype sorts s1 and s2 are siblings if they were defined together in the same mutually recursive definition. */ bool util::are_siblings(sort * s1, sort * s2) { - array_util autil(m); - seq_util sutil(m); - auto get_nested = [&](sort* s) { - while (true) { - if (autil.is_array(s)) - s = get_array_range(s); - else if (!sutil.is_seq(s, s)) - break; - } - return s; - }; - s1 = get_nested(s1); - s2 = get_nested(s2); + s1 = get_nested_sort(m, s1); + s2 = get_nested_sort(m, s2); if (!is_datatype(s1) || !is_datatype(s2)) return s1 == s2; else @@ -1415,7 +1418,7 @@ namespace datatype { def const& d = get_def(s); for (constructor* c : d) { for (accessor* a : *c) { - sort* s = a->range(); + sort* s = get_nested_sort(m, a->range()); if (are_siblings(s0, s) && !mark.contains(s->get_name())) { mark.push_back(s->get_name()); todo.push_back(s); diff --git a/src/test/parametric_datatype.cpp b/src/test/parametric_datatype.cpp index 005f6a8c96..56b684ffd6 100644 --- a/src/test/parametric_datatype.cpp +++ b/src/test/parametric_datatype.cpp @@ -18,6 +18,7 @@ Author: #include "api/z3.h" #include "util/util.h" #include +#include /** @@ -117,6 +118,57 @@ static void test_polymorphic_datatype_api() { Z3_del_context(ctx); } +static void test_nested_datatype_declaration_printing() { + std::cout << "test_nested_datatype_declaration_printing\n"; + + Z3_config cfg = Z3_mk_config(); + Z3_context ctx = Z3_mk_context(cfg); + Z3_del_config(cfg); + + Z3_symbol v_name = Z3_mk_string_symbol(ctx, "V"); + Z3_sort v_ref = Z3_mk_datatype_sort(ctx, v_name, 0, nullptr); + Z3_sort string_sort = Z3_mk_string_sort(ctx); + Z3_sort array_sort = Z3_mk_array_sort(ctx, string_sort, v_ref); + Z3_sort int_sort = Z3_mk_int_sort(ctx); + + Z3_symbol num_fields[1] = { Z3_mk_string_symbol(ctx, "n") }; + Z3_sort num_sorts[1] = { int_sort }; + unsigned num_refs[1] = { 0 }; + Z3_constructor num = Z3_mk_constructor( + ctx, Z3_mk_string_symbol(ctx, "num"), Z3_mk_string_symbol(ctx, "is_num"), + 1, num_fields, num_sorts, num_refs); + + Z3_symbol obj_fields[1] = { Z3_mk_string_symbol(ctx, "o") }; + Z3_sort obj_sorts[1] = { array_sort }; + unsigned obj_refs[1] = { 0 }; + Z3_constructor obj = Z3_mk_constructor( + ctx, Z3_mk_string_symbol(ctx, "obj"), Z3_mk_string_symbol(ctx, "is_obj"), + 1, obj_fields, obj_sorts, obj_refs); + + Z3_constructor constructors[2] = { num, obj }; + Z3_sort v = Z3_mk_datatype(ctx, v_name, 2, constructors); + Z3_del_constructor(ctx, num); + Z3_del_constructor(ctx, obj); + + Z3_ast c = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "c"), v); + Z3_ast formula = Z3_mk_eq(ctx, c, c); + std::string benchmark = Z3_benchmark_to_smtlib_string( + ctx, "nested-datatype", "ALL", "unknown", "", 0, nullptr, formula); + ENSURE(benchmark.find("(declare-datatypes ((V 0))") != std::string::npos); + ENSURE(benchmark.find("(Array String V)") != std::string::npos); + + Z3_solver solver = Z3_mk_solver(ctx); + Z3_solver_inc_ref(ctx, solver); + Z3_solver_assert(ctx, solver, formula); + std::string solver_text = Z3_solver_to_string(ctx, solver); + ENSURE(solver_text.find("(declare-datatypes ((V 0))") != std::string::npos); + ENSURE(solver_text.find("(Array String V)") != std::string::npos); + Z3_solver_dec_ref(ctx, solver); + + Z3_del_context(ctx); +} + void tst_parametric_datatype() { test_polymorphic_datatype_api(); + test_nested_datatype_declaration_printing(); }