mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 12:53:38 +00:00
Code Activity

#5917

Browse source 
Add model.user_functions (default true) to control whether user functions are added to the model.
This commit is contained in:
Nikolaj Bjorner 2022-03-23 09:49:44 -07:00
parent a24a922688
commit d790523c59
3 changed files with 7 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/cmd_context/cmd_context.cpp
View file

@ -1815,6 +1815,9 @@ void cmd_context::display_model(model_ref& mdl) {
} }
void cmd_context::add_declared_functions(model& mdl) { void cmd_context::add_declared_functions(model& mdl) {
model_params p;
if (!p.user_functions())
return;
for (auto const& kv : m_func_decls) { for (auto const& kv : m_func_decls) {
func_decl* f = kv.m_value.first(); func_decl* f = kv.m_value.first();
if (f->get_family_id() == null_family_id && !mdl.has_interpretation(f)) { if (f->get_family_id() == null_family_id && !mdl.has_interpretation(f)) {

1
src/model/model_params.pyg
View file

@ -5,6 +5,7 @@ def_module_params('model',
('v2', BOOL, False, 'use Z3 version 2.x (x <= 16) pretty printer'), ('v2', BOOL, False, 'use Z3 version 2.x (x <= 16) pretty printer'),
('compact', BOOL, True, 'try to compact function graph (i.e., function interpretations that are lookup tables)'), ('compact', BOOL, True, 'try to compact function graph (i.e., function interpretations that are lookup tables)'),
('inline_def', BOOL, False, 'inline local function definitions ignoring possible expansion'), ('inline_def', BOOL, False, 'inline local function definitions ignoring possible expansion'),
('user_functions', BOOL, True, 'include user defined functions in model'),
('completion', BOOL, False, 'enable/disable model completion'), ('completion', BOOL, False, 'enable/disable model completion'),
)) ))

4
src/smt/smt_context.cpp
View file

@ -29,6 +29,7 @@ Revision History:
#include "ast/proofs/proof_checker.h" #include "ast/proofs/proof_checker.h"
#include "ast/ast_util.h" #include "ast/ast_util.h"
#include "ast/well_sorted.h" #include "ast/well_sorted.h"
#include "model/model_params.hpp"
#include "model/model.h" #include "model/model.h"
#include "model/model_pp.h" #include "model/model_pp.h"
#include "smt/smt_context.h" #include "smt/smt_context.h"
@ -4638,7 +4639,8 @@ namespace smt {
} }
void context::add_rec_funs_to_model() { void context::add_rec_funs_to_model() {
if (m_model) model_params p;
if (m_model && p.user_functions())
m_model->add_rec_funs(); m_model->add_rec_funs();
} }