mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

Added facilities for hiding UFs in smt::model_generator

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-06-09 17:49:45 +01:00
parent 879363157f
commit bfeab9cc15
2 changed files with 8 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/smt/smt_model_generator.cpp
View file

@ -20,6 +20,7 @@ Revision History:
#include"smt_context.h"
#include"smt_model_generator.h"
#include"proto_model.h"
#include"ref_util.h"
#include"for_each_expr.h"
#include"ast_ll_pp.h"
#include"ast_pp.h"
@ -36,6 +37,7 @@ namespace smt {
}
model_generator::~model_generator() {
dec_ref_collection_values(m_manager, m_hidden_ufs);
}
void model_generator::reset() {
@ -386,6 +388,7 @@ namespace smt {
enode * n = *it3;
if (is_uninterp_const(n->get_owner()) && m_context->is_relevant(n)) {
func_decl * d = n->get_owner()->get_decl();
if (m_hidden_ufs.contains(d)) continue;
expr * val = get_value(n);
m_model->register_decl(d, val);
}
@ -404,9 +407,9 @@ namespace smt {
*/
bool model_generator::include_func_interp(func_decl * f) const {
family_id fid = f->get_family_id();
if (fid == null_family_id) return true;
if (fid == null_family_id) return !m_hidden_ufs.contains(f);
if (fid == m_manager.get_basic_family_id()) return false;
theory * th = m_context->get_theory(fid);
theory * th = m_context->get_theory(fid);
if (!th) return true;
return th->include_func_interp(f);
}

3
src/smt/smt_model_generator.h
View file

@ -182,6 +182,7 @@ namespace smt {
obj_map<enode, app *> m_root2value;
ast_ref_vector m_asts;
proto_model * m_model;
obj_hashtable<func_decl> m_hidden_ufs;
void init_model();
void mk_bool_model();
@ -220,6 +221,8 @@ namespace smt {
obj_map<enode, app *> const & get_root2value() const { return m_root2value; }
app * get_value(enode * n) const;
void hide(func_decl * f) { m_hidden_ufs.insert_if_not_there(f); m_manager.inc_ref(f); }
};
};