mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 01:24:08 +00:00
Code Activity

add model.inline_def option to make #2517 happy

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-08-29 12:08:09 -03:00
parent 35fa24a82a
commit a8bfab3273
4 changed files with 19 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/cmd_context/cmd_context.cpp
View file

@ -1790,7 +1790,9 @@ struct contains_underspecified_op_proc {
\brief Complete the model if necessary. \brief Complete the model if necessary.
*/ */
void cmd_context::complete_model(model_ref& md) const { void cmd_context::complete_model(model_ref& md) const {
if (gparams::get_value("model.completion") != "true" || !md.get()) if (!md.get())
return;
if (gparams::get_value("model.completion") != "true")
return; return;
params_ref p; params_ref p;
@ -2045,6 +2047,8 @@ bool cmd_context::is_model_available(model_ref& md) const {
has_manager() && has_manager() &&
(cs_state() == css_sat || cs_state() == css_unknown)) { (cs_state() == css_sat || cs_state() == css_unknown)) {
get_check_sat_result()->get_model(md); get_check_sat_result()->get_model(md);
params_ref p;
if (md.get()) md->updt_params(p);
complete_model(md); complete_model(md);
return md.get() != nullptr; return md.get() != nullptr;
} }

12
src/model/model.cpp
View file

@ -27,12 +27,14 @@ Revision History:
#include "ast/for_each_expr.h" #include "ast/for_each_expr.h"
#include "ast/for_each_ast.h" #include "ast/for_each_ast.h"
#include "model/model.h" #include "model/model.h"
#include "model/model_params.hpp"
#include "model/model_evaluator.h" #include "model/model_evaluator.h"
model::model(ast_manager & m): model::model(ast_manager & m):
model_core(m), model_core(m),
m_mev(*this), m_mev(*this),
m_cleaned(false) { m_cleaned(false),
m_inline(false) {
} }
model::~model() { model::~model() {
@ -43,6 +45,13 @@ model::~model() {
} }
} }
void model::updt_params(params_ref const & p) {
model_params mp(p);
m_inline = mp.inline_def();
m_mev.updt_params(p);
}
void model::copy_const_interps(model const & source) { void model::copy_const_interps(model const & source) {
for (auto const& kv : source.m_interp) for (auto const& kv : source.m_interp)
register_decl(kv.m_key, kv.m_value); register_decl(kv.m_key, kv.m_value);
@ -353,6 +362,7 @@ bool model::can_inline_def(top_sort& ts, func_decl* f) {
func_interp* fi = get_func_interp(f); func_interp* fi = get_func_interp(f);
if (!fi) return false; if (!fi) return false;
if (fi->get_else() == nullptr) return false; if (fi->get_else() == nullptr) return false;
if (m_inline) return true;
expr* e = fi->get_else(); expr* e = fi->get_else();
obj_hashtable<expr> subs; obj_hashtable<expr> subs;
ptr_buffer<expr> todo; ptr_buffer<expr> todo;

3
src/model/model.h
View file

@ -36,6 +36,7 @@ protected:
sort2universe m_usort2universe; sort2universe m_usort2universe;
model_evaluator m_mev; model_evaluator m_mev;
bool m_cleaned; bool m_cleaned;
bool m_inline;
struct value_proc; struct value_proc;
struct deps_collector; struct deps_collector;
@ -84,7 +85,7 @@ public:
void compress(); void compress();
void set_model_completion(bool f) { m_mev.set_model_completion(f); } void set_model_completion(bool f) { m_mev.set_model_completion(f); }
void updt_params(params_ref const & p) { m_mev.updt_params(p); } void updt_params(params_ref const & p);
/** /**
* evaluation using the model evaluator. Caches results. * evaluation using the model evaluator. Caches results.

1
src/model/model_params.pyg
View file

@ -4,6 +4,7 @@ def_module_params('model',
('v1', BOOL, False, 'use Z3 version 1.x pretty printer'), ('v1', BOOL, False, 'use Z3 version 1.x pretty printer'),
('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, False, 'try to compact function graph (i.e., function interpretations that are lookup tables)'), ('compact', BOOL, False, 'try to compact function graph (i.e., function interpretations that are lookup tables)'),
('inline_def', BOOL, False, 'inline local function definitions ignoring possible expansion'),
('completion', BOOL, False, 'enable/disable model completion'), ('completion', BOOL, False, 'enable/disable model completion'),
)) ))