mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

refactor get_sort

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-02-02 04:45:54 -08:00
parent 4455f6caf8
commit 3ae4c6e9de
129 changed files with 362 additions and 362 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -825,7 +825,7 @@ private:
SASSERT(value.size() == 1);
val = value[0].sign() ? m.mk_not(v) : v;
}
else if (is_uninterp_const(v) && bvutil.is_bv_sort(m.get_sort(v))) {
else if (is_uninterp_const(v) && bvutil.is_bv_sort(v->get_sort())) {
SASSERT(value.size() == bvutil.get_bv_size(v));
if (m_exps.empty()) {
m_exps.push_back(rational::one());

2
src/sat/smt/arith_solver.cpp
View file

@ -313,7 +313,7 @@ namespace arith {
expr* e2 = n2->get_expr();
if (m.is_ite(e1) || m.is_ite(e2))
return;
if (m.get_sort(e1) != m.get_sort(e2))
if (e1->get_sort() != m.get_sort(e2))
return;
reset_evidence();
for (auto const& ev : e)

8
src/sat/smt/array_axioms.cpp
View file

@ -214,7 +214,7 @@ namespace array {
bool solver::assert_extensionality(expr* e1, expr* e2) {
TRACE("array", tout << "extensionality-axiom: " << mk_bounded_pp(e1, m) << " == " << mk_bounded_pp(e2, m) << "\n";);
++m_stats.m_num_extensionality_axiom;
func_decl_ref_vector const& funcs = sort2diff(m.get_sort(e1));
func_decl_ref_vector const& funcs = sort2diff(e1->get_sort());
expr_ref_vector args1(m), args2(m);
args1.push_back(e1);
args2.push_back(e2);
@ -359,7 +359,7 @@ namespace array {
for (unsigned i = 1; i + 1 < num_args; ++i) {
expr* arg = store->get_arg(i);
sort* srt = m.get_sort(arg);
sort* srt = arg->get_sort();
auto ep = mk_epsilon(srt);
eqs.push_back(m.mk_eq(ep.first, arg));
args1.push_back(m.mk_app(ep.second, arg));
@ -400,7 +400,7 @@ namespace array {
bool solver::assert_congruent_axiom(expr* e1, expr* e2) {
TRACE("array", tout << "congruence-axiom: " << mk_bounded_pp(e1, m) << " " << mk_bounded_pp(e2, m) << "\n";);
++m_stats.m_num_congruence_axiom;
sort* srt = m.get_sort(e1);
sort* srt = e1->get_sort();
unsigned dimension = get_array_arity(srt);
expr_ref_vector args1(m), args2(m);
args1.push_back(e1);
@ -504,7 +504,7 @@ namespace array {
for (unsigned j = i; j-- > 0; ) {
theory_var v2 = roots[j];
expr* e2 = var2expr(v2);
if (m.get_sort(e1) != m.get_sort(e2))
if (e1->get_sort() != m.get_sort(e2))
continue;
if (have_different_model_values(v1, v2))
continue;

2
src/sat/smt/array_model.cpp
View file

@ -47,7 +47,7 @@ namespace array {
void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) {
SASSERT(a.is_array(n->get_expr()));
ptr_vector<expr> args;
sort* srt = m.get_sort(n->get_expr());
sort* srt = n->get_expr()->get_sort();
unsigned arity = get_array_arity(srt);
func_decl * f = mk_aux_decl_for_array_sort(m, srt);
func_interp * fi = alloc(func_interp, m, arity);

4
src/sat/smt/bv_ackerman.cpp
View file

@ -165,8 +165,8 @@ namespace bv {
return;
if (!s.var2enode(v1) || !s.var2enode(v2))
return;
sort* s1 = s.m.get_sort(s.var2expr(v1));
sort* s2 = s.m.get_sort(s.var2expr(v2));
sort* s1 = s.var2expr(v1)->get_sort();
sort* s2 = s.var2expr(v2)->get_sort();
if (s1 != s2 || !s.bv.is_bv_sort(s1))
return;
// IF_VERBOSE(0, verbose_stream() << "assert ackerman " << v1 << " " << v2 << "\n");

12
src/sat/smt/dt_solver.cpp
View file

@ -121,7 +121,7 @@ namespace dt {
m_stats.m_assert_cnstr++;
SASSERT(dt.is_constructor(c));
SASSERT(is_datatype(e));
SASSERT(c->get_range() == m.get_sort(e));
SASSERT(c->get_range() == e->get_sort());
m_args.reset();
ptr_vector<func_decl> const& accessors = *dt.get_constructor_accessors(c);
SASSERT(c->get_arity() == accessors.size());
@ -223,7 +223,7 @@ namespace dt {
assert_update_field_axioms(n);
}
else {
sort* s = m.get_sort(n->get_expr());
sort* s = n->get_expr()->get_sort();
if (dt.get_datatype_num_constructors(s) == 1)
assert_is_constructor_axiom(n, dt.get_datatype_constructors(s)->get(0));
else if (get_config().m_dt_lazy_splits == 0 || (get_config().m_dt_lazy_splits == 1 && !s->is_infinite()))
@ -242,7 +242,7 @@ namespace dt {
v = m_find.find(v);
enode* n = var2enode(v);
sort* srt = m.get_sort(n->get_expr());
sort* srt = n->get_expr()->get_sort();
func_decl* non_rec_c = dt.get_non_rec_constructor(srt);
unsigned non_rec_idx = dt.get_constructor_idx(non_rec_c);
var_data* d = m_var_data[v];
@ -388,7 +388,7 @@ namespace dt {
unsigned num_unassigned = 0;
unsigned unassigned_idx = UINT_MAX;
enode* n = var2enode(v);
sort* srt = m.get_sort(n->get_expr());
sort* srt = n->get_expr()->get_sort();
var_data* d = m_var_data[v];
if (d->m_recognizers.empty()) {
theory_var w = recognizer->get_arg(0)->get_th_var(get_id());
@ -565,7 +565,7 @@ namespace dt {
}
// explore `arg` (with parent)
expr* earg = arg->get_expr();
sort* s = m.get_sort(earg);
sort* s = earg->get_sort();
if (dt.is_datatype(s)) {
m_parent.insert(arg->get_root(), parent);
oc_push_stack(arg);
@ -732,7 +732,7 @@ namespace dt {
SASSERT(!n->is_attached_to(get_id()));
if (is_constructor(term) || is_update_field(term)) {
for (enode* arg : euf::enode_args(n)) {
sort* s = m.get_sort(arg->get_expr());
sort* s = arg->get_expr()->get_sort();
if (dt.is_datatype(s))
mk_var(arg);
else if (m_autil.is_array(s) && dt.is_datatype(get_array_range(s))) {

2
src/sat/smt/dt_solver.h
View file

@ -77,7 +77,7 @@ namespace dt {
bool is_accessor(enode * n) const { return is_accessor(n->get_expr()); }
bool is_update_field(enode * n) const { return dt.is_update_field(n->get_expr()); }
bool is_datatype(expr* e) const { return dt.is_datatype(m.get_sort(e)); }
bool is_datatype(expr* e) const { return dt.is_datatype(e->get_sort()); }
bool is_datatype(enode* n) const { return is_datatype(n->get_expr()); }
void assert_eq_axiom(enode * lhs, expr * rhs, literal antecedent = sat::null_literal);

14
src/sat/smt/euf_internalize.cpp
View file

@ -108,15 +108,15 @@ namespace euf {
if (m.is_bool(e))
attach_lit(literal(si.add_bool_var(e), false), e);
if (!m.is_bool(e) && m.get_sort(e)->get_family_id() != null_family_id) {
if (!m.is_bool(e) && e->get_sort()->get_family_id() != null_family_id) {
auto* e_ext = expr2solver(e);
auto* s_ext = sort2solver(m.get_sort(e));
auto* s_ext = sort2solver(e->get_sort());
if (s_ext && s_ext != e_ext)
s_ext->apply_sort_cnstr(n, m.get_sort(e));
s_ext->apply_sort_cnstr(n, e->get_sort());
}
expr* a = nullptr, * b = nullptr;
if (m.is_eq(e, a, b) && m.get_sort(a)->get_family_id() != null_family_id) {
auto* s_ext = sort2solver(m.get_sort(a));
if (m.is_eq(e, a, b) && a->get_sort()->get_family_id() != null_family_id) {
auto* s_ext = sort2solver(a->get_sort());
if (s_ext)
s_ext->eq_internalized(n);
}
@ -195,7 +195,7 @@ namespace euf {
else {
// g(f(x_i)) = x_i
// f(x_1) = a + .... + f(x_n) = a >= 2
sort* srt = m.get_sort(e->get_arg(0));
sort* srt = e->get_arg(0)->get_sort();
SASSERT(!m.is_bool(srt));
sort_ref u(m.mk_fresh_sort("distinct-elems"), m);
sort* u_ptr = u.get();
@ -242,7 +242,7 @@ namespace euf {
}
else {
// dist-f(x_1) = v_1 & ... & dist-f(x_n) = v_n
sort* srt = m.get_sort(e->get_arg(0));
sort* srt = e->get_arg(0)->get_sort();
SASSERT(!m.is_bool(srt));
sort_ref u(m.mk_fresh_sort("distinct-elems"), m);
func_decl_ref f(m.mk_fresh_func_decl("dist-f", "", 1, &srt, u), m);

4
src/sat/smt/euf_model.cpp
View file

@ -90,7 +90,7 @@ namespace euf {
void solver::collect_dependencies(user_sort& us, deps_t& deps) {
for (enode* n : m_egraph.nodes()) {
expr* e = n->get_expr();
sort* srt = m.get_sort(e);
sort* srt = e->get_sort();
auto* mb = sort2solver(srt);
if (mb)
mb->add_dep(n, deps);
@ -148,7 +148,7 @@ namespace euf {
}
continue;
}
sort* srt = m.get_sort(e);
sort* srt = e->get_sort();
if (m.is_uninterp(srt))
us.add(n->get_root(), srt);
else if (auto* mbS = sort2solver(srt))

10
src/sat/smt/fpa_solver.cpp
View file

@ -203,7 +203,7 @@ namespace fpa {
add_units(mk_side_conditions());
}
else
add_unit(eq_internalize(m_converter.unwrap(wrapped, m.get_sort(n)), n));
add_unit(eq_internalize(m_converter.unwrap(wrapped, n->get_sort()), n));
}
}
else if (is_app(n) && to_app(n)->get_family_id() == get_id()) {
@ -295,7 +295,7 @@ namespace fpa {
expr* a = values.get(n->get_arg(0)->get_root_id());
expr* b = values.get(n->get_arg(1)->get_root_id());
expr* c = values.get(n->get_arg(2)->get_root_id());
value = m_converter.bv2fpa_value(m.get_sort(e), a, b, c);
value = m_converter.bv2fpa_value(e->get_sort(), a, b, c);
}
else if (m_fpa_util.is_bv2rm(e)) {
SASSERT(n->num_args() == 1);
@ -307,12 +307,12 @@ namespace fpa {
value = m_fpa_util.mk_round_toward_zero();
else if (m_fpa_util.is_float(e) && is_wrapped()) {
expr* a = values.get(expr2enode(wrapped)->get_root_id());
value = m_converter.bv2fpa_value(m.get_sort(e), a);
value = m_converter.bv2fpa_value(e->get_sort(), a);
}
else {
SASSERT(m_fpa_util.is_float(e));
unsigned ebits = m_fpa_util.get_ebits(m.get_sort(e));
unsigned sbits = m_fpa_util.get_sbits(m.get_sort(e));
unsigned ebits = m_fpa_util.get_ebits(e->get_sort());
unsigned sbits = m_fpa_util.get_sbits(e->get_sort());
value = m_fpa_util.mk_pzero(ebits, sbits);
}
values.set(n->get_root_id(), value);

8
src/sat/smt/q_mbi.cpp
View file

@ -341,7 +341,7 @@ namespace q {
if (!qb.is_free(idx))
continue;
expr* v = qb.vars.get(qb.vars.size() - idx - 1);
sort* srt = m.get_sort(v);
sort* srt = v->get_sort();
expr_ref_vector veqs(m), meqs(m);
auto const& nodes = ctx.get_egraph().nodes();
unsigned sz = nodes.size();
@ -351,7 +351,7 @@ namespace q {
auto* n = nodes[i];
expr* e = n->get_expr();
expr* val = ctx.node2value(n);
if (val && m.get_sort(e) == srt && !m.is_value(e) && !visited.is_marked(val)) {
if (val && e->get_sort() == srt && !m.is_value(e) && !visited.is_marked(val)) {
visited.mark(val);
veqs.push_back(m.mk_eq(v, e));
meqs.push_back(m.mk_eq(v, val));
@ -484,7 +484,7 @@ namespace q {
bool mbqi::next_offset(unsigned_vector& offsets, app_ref_vector const& vars, unsigned index, unsigned start) {
auto* v = vars[index];
sort* srt = m.get_sort(v);
sort* srt = v->get_sort();
auto const& nodes = ctx.get_egraph().nodes();
unsigned sz = nodes.size();
for (unsigned i = start; i < sz; ++i) {
@ -492,7 +492,7 @@ namespace q {
if (n->generation() > 0)
return false;
expr* e = n->get_expr();
if (m.get_sort(e) == srt && !m.is_value(e)) {
if (e->get_sort() == srt && !m.is_value(e)) {
offsets[index] = i;
return true;
}

2
src/sat/smt/q_solver.cpp
View file

@ -184,7 +184,7 @@ namespace q {
if (!n->interpreted() && !m.is_uninterp(m.get_sort(n->get_expr())))
continue;
expr* e = n->get_expr();
sort* s = m.get_sort(e);
sort* s = e->get_sort();
if (m_unit_table.contains(s))
continue;
m_unit_table.insert(s, e);