mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-04 00:06:16 +00:00
Code Activity

Add finite_set_value_factory for creating finite set values in model generation (#7981)

Browse source 
* Initial plan

* Add finite_set_value_factory implementation

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

* Remove unused dl_decl_plugin variable and include

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

* Update copyright and add TODOs in finite_set_value_factory

Updated copyright information and added TODO comments for handling in finite_set_value_factory methods.

* Update copyright information in finite_set_value_factory.h

Updated copyright year from 2006 to 2025.

* Implement finite_set_value_factory using array_util to create singleton sets

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

* Simplify empty set creation in finite_set_value_factory

Refactor finite_set_value_factory to simplify empty set handling and remove array-specific logic.

* Change family ID for finite_set_value_factory

* Fix build error by restoring array_decl_plugin include and implementation

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

* Update finite_set_value_factory.h

* Add SASSERT for finite set check in factory

Added assertion to check if the sort is a finite set.

* Rename member variable from m_util to u

* Refactor finite_set_value_factory for value handling

* Use register_value instead of direct set insertion

Replaced direct insertion into set with register_value calls.

* Update finite_set_value_factory.cpp

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Copilot 2025-10-16 13:16:54 +02:00 • committed by GitHub
parent a179286183
commit 05ffc0a77b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 91 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/model/model.cpp
View file

@ -40,6 +40,7 @@ Revision History:
#include "model/numeral_factory.h"
#include "model/fpa_factory.h"
#include "model/char_factory.h"
#include "model/finite_set_value_factory.h"
model::model(ast_manager & m):
@ -111,6 +112,7 @@ value_factory* model::get_factory(sort* s) {
m_factories.register_plugin(alloc(arith_factory, m));
m_factories.register_plugin(alloc(seq_factory, m, su.get_family_id(), *this));
m_factories.register_plugin(alloc(fpa_value_factory, m, fu.get_family_id()));
m_factories.register_plugin(alloc(finite_set_value_factory, m, m.mk_family_id("finite_set"), *this));
//m_factories.register_plugin(alloc(char_factory, m, char_decl_plugin(m).get_family_id());
}
family_id fid = s->get_family_id();