From 5079b10597d0b542191130e1ea112d1301674298 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 24 Oct 2025 13:13:52 +0200 Subject: [PATCH] fix up documentation Signed-off-by: Nikolaj Bjorner --- FINITE_SET_API.md | 4 ++-- src/api/z3_api.h | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/FINITE_SET_API.md b/FINITE_SET_API.md index ede624a00..34659b810 100644 --- a/FINITE_SET_API.md +++ b/FINITE_SET_API.md @@ -32,7 +32,7 @@ All functions are declared in `src/api/z3_api.h` and implemented in `src/api/api - `Z3_ast Z3_mk_finite_set_subset(Z3_context c, Z3_ast s1, Z3_ast s2)` - Check subset relation - `Z3_ast Z3_mk_finite_set_map(Z3_context c, Z3_ast f, Z3_ast set)` - Apply function to all elements - `Z3_ast Z3_mk_finite_set_filter(Z3_context c, Z3_ast f, Z3_ast set)` - Filter set with predicate -- `Z3_ast Z3_mk_finite_set_range(Z3_context c, Z3_ast low, Z3_ast high)` - Create range [low, high) +- `Z3_ast Z3_mk_finite_set_range(Z3_context c, Z3_ast low, Z3_ast high)` - Create range [low .. high] ## Python API @@ -56,7 +56,7 @@ All functions are available in `z3.py`: - `FiniteSetSubset(s1, s2)` - Subset test - `FiniteSetMap(f, set)` - Map function over set - `FiniteSetFilter(f, set)` - Filter set -- `FiniteSetRange(low, high)` - Create range +- `FiniteSetRange(low, high)` - Create range [low..high] - `is_finite_set(expr)` - Check if expression is a finite set - `is_finite_set_sort(sort)` - Check if sort is a finite set sort diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 8d0ab3f20..2bf9179a8 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -3483,7 +3483,7 @@ extern "C" { Z3_ast Z3_API Z3_mk_finite_set_filter(Z3_context c, Z3_ast f, Z3_ast set); /** - \brief Create a finite set of integers in the range [low, high). + \brief Create a finite set of integers in the range [low, high]. def_API('Z3_mk_finite_set_range', AST, (_in(CONTEXT), _in(AST), _in(AST))) */