mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

Fix finite_set::is_fully_interp to check element sort interpretation (#7982)

Browse source 
* Initial plan

* Implement finite_set is_fully_interp to check element sort

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Refine is_fully_interp implementation with SASSERT

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
Copilot 2025-10-15 21:47:32 +02:00 • committed by GitHub
parent e781648499
commit 2bb22c6489
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 36 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/finite_set_decl_plugin.cpp
View file

@ -183,7 +183,9 @@ expr * finite_set_decl_plugin::get_some_value(sort * s) {
}
bool finite_set_decl_plugin::is_fully_interp(sort * s) const {
return false;
SASSERT(is_finite_set(s));
sort* element_sort = get_element_sort(s);
return element_sort && m_manager->is_fully_interp(element_sort);
}
bool finite_set_decl_plugin::is_value(app * e) const {