mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-08 06:52:26 +00:00
Code Activity

Fix nested datatype declaration printing (#10420)

Browse source 
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
This commit is contained in:
Nikolaj Bjorner 2026-08-06 22:17:31 -07:00
parent 2c508b3753
commit f05612e750
2 changed files with 69 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

31
src/ast/datatype_decl_plugin.cpp
View file

@ -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);

52
src/test/parametric_datatype.cpp
View file

@ -18,6 +18,7 @@ Author:
#include "api/z3.h"
#include "util/util.h"
#include <iostream>
#include <string>
/**
@ -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();
}