mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity

Implement more cases for finite_set_decl_plugin::are_distinct (#7978)

Browse source 
* Implement more cases for finite_set_decl_plugin::are_distinct

* Adapted distinctive checks for finite sets
This commit is contained in:
kper 2025-10-15 14:35:57 +02:00 • committed by GitHub
parent b24aec3c4c
commit 7446112fbe
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/ast/finite_set_decl_plugin.cpp
View file

@ -204,6 +204,9 @@ bool finite_set_decl_plugin::are_distinct(app* e1, app* e2) const {
return true; return true;
if (r.is_singleton(e1) && r.is_empty(e2)) if (r.is_singleton(e1) && r.is_empty(e2))
return true; return true;
if(r.is_singleton(e1) && r.is_singleton(e2))
return m_manager->are_distinct(e1, e2);
// TODO: could be extended to cases where we can prove the sets are different by containing one element // TODO: could be extended to cases where we can prove the sets are different by containing one element
// that the other doesn't contain. Such as (union (singleton a) (singleton b)) and (singleton c) where c is different from a, b. // that the other doesn't contain. Such as (union (singleton a) (singleton b)) and (singleton c) where c is different from a, b.
return false; return false;