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

Detecting OP_BSDIV0, etc. as uninterpreted functions in ackermannization.

Browse source
This commit is contained in:
mikolas 2016-01-27 16:22:28 +00:00
parent 4b37140780
commit 956d774299
4 changed files with 32 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/tactic/ackr/ackr_model_converter.cpp
View file

@ -68,7 +68,12 @@ protected:
}; };
void ackr_model_converter::convert(model * source, model * destination) { void ackr_model_converter::convert(model * source, model * destination) {
SASSERT(source->get_num_functions() == 0); //SASSERT(source->get_num_functions() == 0);
for (unsigned i = 0; i < source->get_num_functions(); i++) {
func_decl * const fd = source->get_function(i);
func_interp * const fi = source->get_func_interp(fd);
destination->register_decl(fd, fi);
}
convert_constants(source,destination); convert_constants(source,destination);
convert_sorts(source,destination); convert_sorts(source,destination);
} }

2
src/tactic/ackr/lackr.cpp
View file

@ -177,8 +177,8 @@ void lackr::abstract() {
void lackr::add_term(app* a) { void lackr::add_term(app* a) {
if (a->get_num_args() == 0) return; if (a->get_num_args() == 0) return;
if (!should_ackermannize(a)) return;
func_decl* const fd = a->get_decl(); func_decl* const fd = a->get_decl();
if (!is_uninterp(a)) return;
SASSERT(m_bvutil.is_bv_sort(fd->get_range()) || m_m.is_bool(a)); SASSERT(m_bvutil.is_bv_sort(fd->get_range()) || m_m.is_bool(a));
app_set* ts = 0; app_set* ts = 0;
if (!m_fun2terms.find(fd, ts)) { if (!m_fun2terms.find(fd, ts)) {

19
src/tactic/ackr/lackr.h
View file

@ -122,5 +122,24 @@ class lackr {
// Collect all uninterpreted terms, skipping 0-arity. // Collect all uninterpreted terms, skipping 0-arity.
// //
void collect_terms(); void collect_terms();
inline bool should_ackermannize(app const * a) const;
}; };
inline bool lackr::should_ackermannize(app const * a) const {
if (a->get_family_id() == m_bvutil.get_family_id()) {
switch (a->get_decl_kind()) {
case OP_BSDIV0:
case OP_BUDIV0:
case OP_BSREM0:
case OP_BUREM0:
case OP_BSMOD0:
return true;
default:
return is_uninterp(a);
}
}
return (is_uninterp(a));
}
#endif /* LACKR_H_15079 */ #endif /* LACKR_H_15079 */

6
src/tactic/ackr/lackr_model_constructor.cpp
View file

@ -78,6 +78,12 @@ struct lackr_model_constructor::imp {
destination->register_usort(s, u.size(), u.c_ptr()); destination->register_usort(s, u.size(), u.c_ptr());
} }
} }
for (unsigned i = 0; i < m_abstr_model->get_num_functions(); i++) {
func_decl * const fd = m_abstr_model->get_function(i);
func_interp * const fi = m_abstr_model->get_func_interp(fd);
destination->register_decl(fd, fi);
}
{ {
const app2val_t::iterator e = m_app2val.end(); const app2val_t::iterator e = m_app2val.end();
app2val_t::iterator i = m_app2val.end(); app2val_t::iterator i = m_app2val.end();