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

fixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-10-11 16:17:54 -07:00
parent 9eb6f97e6b
commit 46252b669c
3 changed files with 13 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/ast/sls/sls_context.cpp
View file

@ -52,8 +52,7 @@ namespace sls {
m_plugins.set(p->fid(), p); m_plugins.set(p->fid(), p);
} }
void context::ensure_plugin(expr* e) { void context::ensure_plugin(family_id fid) {
auto fid = get_fid(e);
if (m_plugins.get(fid, nullptr)) if (m_plugins.get(fid, nullptr))
return; return;
else if (fid == arith_family_id) else if (fid == arith_family_id)
@ -67,9 +66,14 @@ namespace sls {
else if (fid == array_util(m).get_family_id()) else if (fid == array_util(m).get_family_id())
register_plugin(alloc(array_plugin, *this)); register_plugin(alloc(array_plugin, *this));
else else
verbose_stream() << "did not find plugin for " << mk_bounded_pp(e, m) << "\n"; verbose_stream() << "did not find plugin for " << fid << "\n";
}
// add arrays and bv dynamically too.
void context::ensure_plugin(expr* e) {
auto fid = get_fid(e);
ensure_plugin(fid);
fid = e->get_sort()->get_family_id();
ensure_plugin(fid);
} }

1
src/ast/sls/sls_context.h
View file

@ -136,6 +136,7 @@ namespace sls {
void repair_literals(); void repair_literals();
void ensure_plugin(expr* e); void ensure_plugin(expr* e);
void ensure_plugin(family_id fid);
family_id get_fid(expr* e) const; family_id get_fid(expr* e) const;

4
src/ast/sls/sls_euf_plugin.cpp
View file

@ -24,6 +24,7 @@ Todo:
#include "ast/sls/sls_euf_plugin.h" #include "ast/sls/sls_euf_plugin.h"
#include "ast/ast_ll_pp.h" #include "ast/ast_ll_pp.h"
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
#include "params/sls_params.hpp"
namespace sls { namespace sls {
@ -37,7 +38,8 @@ namespace sls {
euf_plugin::~euf_plugin() {} euf_plugin::~euf_plugin() {}
void euf_plugin::initialize() { void euf_plugin::initialize() {
m_incremental = ctx.get_params().get_bool("euf_incremental", m_incremental); sls_params sp(ctx.get_params());
m_incremental = sp.euf_incremental();
IF_VERBOSE(2, verbose_stream() << "sls.euf: incremental " << m_incremental << "\n"); IF_VERBOSE(2, verbose_stream() << "sls.euf: incremental " << m_incremental << "\n");
} }