mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-30 07:53:15 +00:00
Code Activity

add -> as another array sort constructor

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-06-22 21:35:23 -07:00
parent 5ad1647061
commit 98043873d0
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/array_decl_plugin.cpp
View file

@ -568,6 +568,7 @@ func_decl * array_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
void array_decl_plugin::get_sort_names(svector<builtin_name>& sort_names, symbol const & logic) {
sort_names.push_back(builtin_name(ARRAY_SORT_STR, ARRAY_SORT));
sort_names.push_back(builtin_name("=>", ARRAY_SORT));
sort_names.push_back(builtin_name("->", ARRAY_SORT));
if (logic == symbol::null || logic == symbol("HORN") || logic == symbol("ALL")) {
// this could easily break users even though it is already used in CVC4:
sort_names.push_back(builtin_name("Set", _SET_SORT));