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

Cleanliness

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-02-10 14:39:33 +00:00
parent 8c80ed33fa
commit fa68b00563
2 changed files with 9 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/ackermannization/lackr_model_constructor.cpp
View file

@ -24,10 +24,10 @@
struct lackr_model_constructor::imp { struct lackr_model_constructor::imp {
public: public:
imp(ast_manager& m, imp(ast_manager & m,
ackr_info_ref info, ackr_info_ref info,
model_ref& abstr_model, model_ref & abstr_model,
conflict_list& conflicts) conflict_list & conflicts)
: m_m(m) : m_m(m)
, m_info(info) , m_info(info)
, m_abstr_model(abstr_model) , m_abstr_model(abstr_model)
@ -239,7 +239,6 @@ struct lackr_model_constructor::imp {
if (is_val(a)) return true; // skip numerals if (is_val(a)) return true; // skip numerals
TRACE("model_constructor", tout << "mk_value(\n" << mk_ismt2_pp(a, m_m, 2) << ")\n";); TRACE("model_constructor", tout << "mk_value(\n" << mk_ismt2_pp(a, m_m, 2) << ")\n";);
SASSERT(!m_app2val.contains(a)); SASSERT(!m_app2val.contains(a));
const unsigned num = a->get_num_args();
expr_ref result(m_m); expr_ref result(m_m);
if (!evaluate(a, result)) return false; if (!evaluate(a, result)) return false;
SASSERT(is_val(result)); SASSERT(is_val(result));
@ -309,6 +308,7 @@ struct lackr_model_constructor::imp {
return true; return true;
} }
UNREACHABLE(); UNREACHABLE();
return true;
} }
void make_value_interpreted_function(app* a, void make_value_interpreted_function(app* a,
@ -330,16 +330,14 @@ struct lackr_model_constructor::imp {
// theory dispatch for = // theory dispatch for =
SASSERT(num == 2); SASSERT(num == 2);
family_id s_fid = m_m.get_sort(values.get(0))->get_family_id(); family_id s_fid = m_m.get_sort(values.get(0))->get_family_id();
br_status st = BR_FAILED;
if (s_fid == m_bv_rw.get_fid()) if (s_fid == m_bv_rw.get_fid())
st = m_bv_rw.mk_eq_core(values.get(0), values.get(1), result); m_bv_rw.mk_eq_core(values.get(0), values.get(1), result);
} else { } else {
br_status st = m_b_rw.mk_app_core(fd, num, values.c_ptr(), result); m_b_rw.mk_app_core(fd, num, values.c_ptr(), result);
} }
} else { } else {
br_status st = BR_FAILED;
if (fid == m_bv_rw.get_fid()) { if (fid == m_bv_rw.get_fid()) {
st = m_bv_rw.mk_app_core(fd, num, values.c_ptr(), result); m_bv_rw.mk_app_core(fd, num, values.c_ptr(), result);
} }
else { else {
UNREACHABLE(); UNREACHABLE();

2
src/ackermannization/lackr_model_constructor.h
View file

@ -49,9 +49,9 @@ class lackr_model_constructor {
private: private:
struct imp; struct imp;
imp * m_imp; imp * m_imp;
ast_manager & m_m;
enum {CHECKED, CONFLICT, UNKNOWN} m_state; enum {CHECKED, CONFLICT, UNKNOWN} m_state;
conflict_list m_conflicts; conflict_list m_conflicts;
ast_manager& m_m;
const ackr_info_ref m_info; const ackr_info_ref m_info;
unsigned m_ref_count; // reference counting unsigned m_ref_count; // reference counting