mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

add missing factory plugins to model

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-10-16 19:47:13 -07:00
parent 0755b2b5f7
commit 6143070157
2 changed files with 12 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/ast/sls/sls_datatype_plugin.cpp
View file

@ -242,14 +242,6 @@ namespace sls {
args.push_back(m.mk_app(a, t)); args.push_back(m.mk_app(a, t));
m_axioms.push_back(m.mk_iff(m.mk_app(r, t), m.mk_eq(t, m.mk_app(c, args)))); m_axioms.push_back(m.mk_iff(m.mk_app(r, t), m.mk_eq(t, m.mk_app(c, args))));
} }
//
// sort_size sz = dt.et_datatype_size(s);
// if (sz.is_finite()) {
// - sz.size()
// - enumerate instances and set t to be one of instances?
// }
//
} }
} }
collect_path_axioms(); collect_path_axioms();
@ -464,6 +456,15 @@ namespace sls {
} }
} }
} }
//
// sort_size sz = dt.et_datatype_size(s);
// if (sz.is_finite())
// - sz.size() < |T of sort s|
// - ensure that there are at most sz.size() distinct elements.
// - not distinct(t1, ..., tn) where n = sz.size() + 1
//
return false; return false;
} }

3
src/model/model.cpp
View file

@ -39,6 +39,7 @@ Revision History:
#include "model/datatype_factory.h" #include "model/datatype_factory.h"
#include "model/numeral_factory.h" #include "model/numeral_factory.h"
#include "model/fpa_factory.h" #include "model/fpa_factory.h"
#include "model/char_factory.h"
model::model(ast_manager & m): model::model(ast_manager & m):
@ -103,12 +104,14 @@ value_factory* model::get_factory(sort* s) {
if (m_factories.plugins().empty()) { if (m_factories.plugins().empty()) {
seq_util su(m); seq_util su(m);
fpa_util fu(m); fpa_util fu(m);
m_factories.register_plugin(alloc(basic_factory, m, 0));
m_factories.register_plugin(alloc(array_factory, m, *this)); m_factories.register_plugin(alloc(array_factory, m, *this));
m_factories.register_plugin(alloc(datatype_factory, m, *this)); m_factories.register_plugin(alloc(datatype_factory, m, *this));
m_factories.register_plugin(alloc(bv_factory, m)); m_factories.register_plugin(alloc(bv_factory, m));
m_factories.register_plugin(alloc(arith_factory, m)); 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(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(fpa_value_factory, m, fu.get_family_id()));
//m_factories.register_plugin(alloc(char_factory, m, char_decl_plugin(m).get_family_id());
} }
family_id fid = s->get_family_id(); family_id fid = s->get_family_id();
return m_factories.get_plugin(fid); return m_factories.get_plugin(fid);