mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Fix more issues unintepreted sort tests.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-02-15 16:31:42 -08:00
parent 943e142bfa
commit 0af4384882
2 changed files with 58 additions and 44 deletions
Download patch file Download diff file Expand all files Collapse all files

45
src/ast/static_features.cpp
View file

@ -165,7 +165,8 @@ void static_features::update_core(expr * e) {
// even if a benchmark does not contain any theory interpreted function decls, we still have to install
// the theory if the benchmark contains constants or function applications of an interpreted sort.
sort * s = m_manager.get_sort(e);
mark_theory(s->get_family_id());
if (!m_manager.is_uninterp(s))
mark_theory(s->get_family_id());
bool _is_gate = is_gate(e);
bool _is_eq = m_manager.is_eq(e);
@ -255,9 +256,11 @@ void static_features::update_core(expr * e) {
m_num_simple_eqs++;
}
sort * s = m_manager.get_sort(to_app(e)->get_arg(0));
family_id fid = s->get_family_id();
if (fid != null_family_id && fid != m_bfid)
inc_theory_eqs(fid);
if (!m_manager.is_uninterp(s)) {
family_id fid = s->get_family_id();
if (fid != null_family_id && fid != m_bfid)
inc_theory_eqs(fid);
}
}
if (!m_has_int && m_autil.is_int(e))
m_has_int = true;
@ -295,9 +298,11 @@ void static_features::update_core(expr * e) {
if (to_app(e)->get_num_args() == 0) {
m_num_uninterpreted_constants++;
sort * s = m_manager.get_sort(e);
family_id fid = s->get_family_id();
if (fid != null_family_id && fid != m_bfid)
inc_theory_constants(fid);
if (!m_manager.is_uninterp(s)) {
family_id fid = s->get_family_id();
if (fid != null_family_id && fid != m_bfid)
inc_theory_constants(fid);
}
}
}
func_decl * d = to_app(e)->get_decl();
@ -312,18 +317,20 @@ void static_features::update_core(expr * e) {
for (unsigned i = 0; i < num_args; i++) {
expr * arg = to_app(e)->get_arg(i);
sort * arg_s = m_manager.get_sort(arg);
family_id fid_arg = arg_s->get_family_id();
if (fid_arg != fid && fid_arg != null_family_id) {
m_num_aliens++;
inc_num_aliens(fid_arg);
if (fid_arg == m_afid) {
SASSERT(!_is_le_ge);
m_num_arith_terms++;
rational k;
TRACE("diff_term", tout << "diff_term: " << is_diff_term(arg, k) << "\n" << mk_pp(arg, m_manager) << "\n";);
if (is_diff_term(arg, k)) {
m_num_diff_terms++;
acc_num(k);
if (!m_manager.is_uninterp(arg_s)) {
family_id fid_arg = arg_s->get_family_id();
if (fid_arg != fid && fid_arg != null_family_id) {
m_num_aliens++;
inc_num_aliens(fid_arg);
if (fid_arg == m_afid) {
SASSERT(!_is_le_ge);
m_num_arith_terms++;
rational k;
TRACE("diff_term", tout << "diff_term: " << is_diff_term(arg, k) << "\n" << mk_pp(arg, m_manager) << "\n";);
if (is_diff_term(arg, k)) {
m_num_diff_terms++;
acc_num(k);
}
}
}
}

57
src/smt/proto_model/proto_model.cpp
View file

@ -526,49 +526,56 @@ bool proto_model::is_finite(sort * s) const {
}
expr * proto_model::get_some_value(sort * s) {
family_id fid = s->get_family_id();
if (fid == null_family_id) {
if (m_manager.is_uninterp(s)) {
return m_user_sort_factory->get_some_value(s);
}
else {
family_id fid = s->get_family_id();
value_factory * f = get_factory(fid);
if (f)
return f->get_some_value(s);
// there is no factory for the family id, then assume s is uninterpreted.
return m_user_sort_factory->get_some_value(s);
}
value_factory * f = get_factory(fid);
if (f)
return f->get_some_value(s);
// there is no factory for the family id, then assume s is uninterpreted.
return m_user_sort_factory->get_some_value(s);
}
bool proto_model::get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
family_id fid = s->get_family_id();
if (fid == null_family_id) {
if (m_manager.is_uninterp(s)) {
return m_user_sort_factory->get_some_values(s, v1, v2);
}
value_factory * f = get_factory(fid);
if (f)
return f->get_some_values(s, v1, v2);
else
return false;
else {
family_id fid = s->get_family_id();
value_factory * f = get_factory(fid);
if (f)
return f->get_some_values(s, v1, v2);
else
return false;
}
}
expr * proto_model::get_fresh_value(sort * s) {
family_id fid = s->get_family_id();
if (fid == null_family_id)
return m_user_sort_factory->get_fresh_value(s);
value_factory * f = get_factory(fid);
if (f)
return f->get_fresh_value(s);
else
// Use user_sort_factory if the theory has no support for model construnction.
// This is needed when dummy theories are used for arithmetic or arrays.
if (m_manager.is_uninterp(s)) {
return m_user_sort_factory->get_fresh_value(s);
}
else {
family_id fid = s->get_family_id();
value_factory * f = get_factory(fid);
if (f)
return f->get_fresh_value(s);
else
// Use user_sort_factory if the theory has no support for model construnction.
// This is needed when dummy theories are used for arithmetic or arrays.
return m_user_sort_factory->get_fresh_value(s);
}
}
void proto_model::register_value(expr * n) {
sort * s = m_manager.get_sort(n);
family_id fid = s->get_family_id();
if (fid == null_family_id) {
if (m_manager.is_uninterp(s)) {
m_user_sort_factory->register_value(n);
}
else {
family_id fid = s->get_family_id();
value_factory * f = get_factory(fid);
if (f)
f->register_value(n);