mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

remove ast_manager get_sort method entirely

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-02-02 13:57:01 -08:00
parent 489df0760f
commit 8f577d3943
72 changed files with 209 additions and 208 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/smt/seq_eq_solver.cpp
View file

@ -114,10 +114,10 @@ bool theory_seq::solve_unit_eq(expr* l, expr* r, dependency* deps) {
}
bool theory_seq::solve_unit_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* deps) {
if (l.size() == 1 && is_var(l[0]) && !occurs(l[0], r) && add_solution(l[0], mk_concat(r, m.get_sort(l[0])), deps)) {
if (l.size() == 1 && is_var(l[0]) && !occurs(l[0], r) && add_solution(l[0], mk_concat(r, l[0]->get_sort()), deps)) {
return true;
}
if (r.size() == 1 && is_var(r[0]) && !occurs(r[0], l) && add_solution(r[0], mk_concat(l, m.get_sort(r[0])), deps)) {
if (r.size() == 1 && is_var(r[0]) && !occurs(r[0], l) && add_solution(r[0], mk_concat(l, r[0]->get_sort()), deps)) {
return true;
}
return false;
@ -410,7 +410,7 @@ bool theory_seq::len_based_split(eq const& e) {
TRACE("seq", tout << "split based on length\n";);
TRACE("seq", display_equation(tout, e););
sort* srt = m.get_sort(ls[0]);
sort* srt = ls[0]->get_sort();
expr_ref x11 = expr_ref(ls[0], m);
expr_ref x12 = mk_concat(ls.size()-1, ls.c_ptr()+1, srt);
expr_ref y11 = expr_ref(rs[0], m);
@ -604,7 +604,7 @@ bool theory_seq::split_lengths(dependency* dep,
else if (m_util.str.is_unit(Y)) {
SASSERT(lenB == lenX);
bs.push_back(Y);
expr_ref bY = mk_concat(bs, m.get_sort(Y));
expr_ref bY = mk_concat(bs, Y->get_sort());
propagate_eq(dep, lits, X, bY, true);
}
else {
@ -1172,7 +1172,7 @@ bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_re
TRACE("seq", tout << mk_pp(l, m) << ": " << ctx.get_scope_level() << " - start:" << start << "\n";);
expr_ref v0(m);
v0 = m_util.str.mk_empty(m.get_sort(l));
v0 = m_util.str.mk_empty(l->get_sort());
if (can_be_equal(ls.size() - 1, ls.c_ptr() + 1, rs.size(), rs.c_ptr())) {
if (assume_equality(l, v0)) {
TRACE("seq", tout << mk_pp(l, m) << " " << v0 << "\n";);
@ -1467,7 +1467,7 @@ bool theory_seq::is_quat_eq(expr_ref_vector const& ls, expr_ref_vector const& rs
if (ls.size() > 1 && is_var(ls[0]) && is_var(ls.back()) &&
rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
unsigned l_start = 1;
sort* srt = m.get_sort(ls[0]);
sort* srt = ls[0]->get_sort();
for (; l_start < ls.size()-1; ++l_start) {
if (m_util.str.is_unit(ls[l_start])) break;
}
@ -1510,7 +1510,7 @@ bool theory_seq::is_quat_eq(expr_ref_vector const& ls, expr_ref_vector const& rs
bool theory_seq::is_ternary_eq_rhs(expr_ref_vector const& ls, expr_ref_vector const& rs,
expr_ref& x, expr_ref_vector& xs, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2) {
if (ls.size() > 1 && rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
sort* srt = m.get_sort(ls[0]);
sort* srt = ls[0]->get_sort();
unsigned l_start = ls.size()-1;
for (; l_start > 0; --l_start) {
if (!m_util.str.is_unit(ls[l_start])) break;
@ -1548,7 +1548,7 @@ bool theory_seq::is_ternary_eq_rhs(expr_ref_vector const& ls, expr_ref_vector co
bool theory_seq::is_ternary_eq_lhs(expr_ref_vector const& ls, expr_ref_vector const& rs,
expr_ref_vector& xs, expr_ref& x, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2) {
if (ls.size() > 1 && rs.size() > 1 && is_var(rs[0]) && is_var(rs.back())) {
sort* srt = m.get_sort(ls[0]);
sort* srt = ls[0]->get_sort();
unsigned l_start = 0;
for (; l_start < ls.size()-1; ++l_start) {
if (!m_util.str.is_unit(ls[l_start])) break;
@ -1600,7 +1600,7 @@ bool theory_seq::solve_nth_eq2(expr_ref_vector const& ls, expr_ref_vector const&
expr_ref_vector ls1(m), rs1(m);
expr_ref idx1(m_autil.mk_add(idx, m_autil.mk_int(1)), m);
m_rewrite(idx1);
expr_ref rhs = mk_concat(rs.size(), rs.c_ptr(), m.get_sort(ls[0]));
expr_ref rhs = mk_concat(rs.size(), rs.c_ptr(), ls[0]->get_sort());
if (m_nth_eq2_cache.contains(std::make_pair(rhs, ls[0])))
return false;
m_nth_eq2_cache.insert(std::make_pair(rhs, ls[0]));
@ -1641,7 +1641,7 @@ bool theory_seq::solve_nth_eq1(expr_ref_vector const& ls, expr_ref_vector const&
}
return false;
}
add_solution(l, mk_concat(rs, m.get_sort(l)), dep);
add_solution(l, mk_concat(rs, l->get_sort()), dep);
return true;
}

2
src/smt/seq_ne_solver.cpp
View file

@ -142,7 +142,7 @@ bool theory_seq::propagate_ne2eq(unsigned idx, expr_ref_vector const& es) {
}
ne const& n = m_nqs[idx];
expr_ref e(m), head(m), tail(m);
e = mk_concat(es, m.get_sort(es[0]));
e = mk_concat(es, es[0]->get_sort());
m_sk.decompose(e, head, tail);
propagate_eq(n.dep(), n.lits(), e, mk_concat(head, tail), false);
return true;

16
src/smt/seq_regex.cpp
View file

@ -55,7 +55,7 @@ namespace smt {
expr* e = ctx.bool_var2expr(lit.var());
expr_ref id(a().mk_int(e->get_id()), m);
VERIFY(str().is_in_re(e, s, r));
sort* seq_sort = m.get_sort(s);
sort* seq_sort = s->get_sort();
vector<expr_ref_vector> patterns;
auto mk_cont = [&](unsigned idx) {
return sk().mk("seq.cont", id, a().mk_int(idx), seq_sort);
@ -158,7 +158,7 @@ namespace smt {
}
else {
//add the literal back
expr_ref r_alias(m.mk_fresh_const(symbol(r->get_id()), m.get_sort(r), false), m);
expr_ref r_alias(m.mk_fresh_const(symbol(r->get_id()), r->get_sort(), false), m);
expr_ref s_in_r_alias(re().mk_in_re(s, r_alias), m);
literal s_in_r_alias_lit = th.mk_literal(s_in_r_alias);
m_const_to_expr.insert(r_alias, r, nullptr);
@ -192,7 +192,7 @@ namespace smt {
*/
expr_ref seq_regex::get_overapprox_regex(expr* s) {
expr_ref s_to_re(re().mk_to_re(s), m);
expr_ref dotstar(re().mk_full_seq(m.get_sort(s_to_re)), m);
expr_ref dotstar(re().mk_full_seq(s_to_re->get_sort()), m);
if (m.is_value(s))
return s_to_re;
@ -209,7 +209,7 @@ namespace smt {
last = e_approx;
}
if (!s_approx)
s_approx = re().mk_epsilon(m.get_sort(s));
s_approx = re().mk_epsilon(s->get_sort());
return s_approx;
}
@ -402,7 +402,7 @@ namespace smt {
expr_ref seq_regex::symmetric_diff(expr* r1, expr* r2) {
expr_ref r(m);
if (r1 == r2)
r = re().mk_empty(m.get_sort(r1));
r = re().mk_empty(r1->get_sort());
else if (re().is_empty(r1))
r = r2;
else if (re().is_empty(r2))
@ -458,7 +458,7 @@ namespace smt {
STRACE("seq_regex", tout << "derivative(" << mk_pp(hd, m) << "): " << mk_pp(r, m) << std::endl;);
// Use canonical variable for head
expr_ref hd_canon(m.mk_var(0, m.get_sort(hd)), m);
expr_ref hd_canon(m.mk_var(0, hd->get_sort()), m);
expr_ref result(re().mk_derivative(hd_canon, r), m);
rewrite(result);
@ -496,7 +496,7 @@ namespace smt {
if (re().is_empty(r))
//trivially true
return;
expr_ref emp(re().mk_empty(m.get_sort(r)), m);
expr_ref emp(re().mk_empty(r->get_sort()), m);
expr_ref f(m.mk_fresh_const("re.char", seq_sort), m);
expr_ref is_empty = sk().mk_is_empty(r, r, f);
// is_empty : (re,re,seq) -> Bool is a Skolem function
@ -516,7 +516,7 @@ namespace smt {
sort* seq_sort = nullptr;
VERIFY(u().is_re(r1, seq_sort));
expr_ref r = symmetric_diff(r1, r2);
expr_ref emp(re().mk_empty(m.get_sort(r)), m);
expr_ref emp(re().mk_empty(r->get_sort()), m);
expr_ref n(m.mk_fresh_const("re.char", seq_sort), m);
expr_ref is_non_empty = sk().mk_is_non_empty(r, r, n);
th.add_axiom(th.mk_eq(r1, r2, false), th.mk_literal(is_non_empty));

10
src/smt/smt_context.cpp
View file

@ -259,7 +259,7 @@ namespace smt {
See comments in theory::mk_eq_atom
*/
app * context::mk_eq_atom(expr * lhs, expr * rhs) {
family_id fid = m.get_sort(lhs)->get_family_id();
family_id fid = lhs->get_sort()->get_family_id();
theory * th = get_theory(fid);
if (th)
return th->mk_eq_atom(lhs, rhs);
@ -474,7 +474,7 @@ namespace smt {
TRACE("add_eq", tout << "assigning: #" << n1->get_owner_id() << " = #" << n2->get_owner_id() << "\n";);
TRACE("add_eq_detail", tout << "assigning\n" << enode_pp(n1, *this) << "\n" << enode_pp(n2, *this) << "\n";
tout << "kind: " << js.get_kind() << "\n";);
SASSERT(m.get_sort(n1->get_owner()) == m.get_sort(n2->get_owner()));
SASSERT(n1->get_owner()->get_sort() == n2->get_owner()->get_sort());
m_stats.m_num_add_eq++;
enode * r1 = n1->get_root();
@ -1115,14 +1115,14 @@ namespace smt {
context.
*/
bool context::is_diseq(enode * n1, enode * n2) const {
SASSERT(m.get_sort(n1->get_owner()) == m.get_sort(n2->get_owner()));
SASSERT(n1->get_owner()->get_sort() == n2->get_owner()->get_sort());
context * _this = const_cast<context*>(this);
if (!m_is_diseq_tmp) {
app * eq = m.mk_eq(n1->get_owner(), n2->get_owner());
m.inc_ref(eq);
_this->m_is_diseq_tmp = enode::mk_dummy(m, m_app2enode, eq);
}
else if (m.get_sort(m_is_diseq_tmp->get_owner()->get_arg(0)) != m.get_sort(n1->get_owner())) {
else if (m_is_diseq_tmp->get_owner()->get_arg(0)->get_sort() != n1->get_owner()->get_sort()) {
m.dec_ref(m_is_diseq_tmp->get_owner());
app * eq = m.mk_eq(n1->get_owner(), n2->get_owner());
m.inc_ref(eq);
@ -4388,7 +4388,7 @@ namespace smt {
bool_var_data & d = get_bdata(v);
d.set_eq_flag();
set_true_first_flag(v);
sort * s = m.get_sort(to_app(eq)->get_arg(0));
sort * s = to_app(eq)->get_arg(0)->get_sort();
theory * th = m_theories.get_plugin(s->get_family_id());
if (th)
th->internalize_eq_eh(to_app(eq), v);

2
src/smt/smt_context.h
View file

@ -1078,7 +1078,7 @@ namespace smt {
void push_eq(enode * lhs, enode * rhs, eq_justification const & js) {
if (lhs->get_root() != rhs->get_root()) {
SASSERT(m.get_sort(lhs->get_owner()) == m.get_sort(rhs->get_owner()));
SASSERT(lhs->get_owner()->get_sort() == rhs->get_owner()->get_sort());
m_eq_propagation_queue.push_back(new_eq(lhs, rhs, js));
}
}

2
src/smt/smt_context_inv.cpp
View file

@ -279,7 +279,7 @@ namespace smt {
if (lhs == rhs)
continue;
TRACE("check_th_diseq_propagation", tout << "num. theory_vars: " << lhs->get_num_th_vars() << " "
<< mk_pp(m.get_sort(lhs->get_owner()), m) << "\n";);
<< mk_pp(lhs->get_owner()->get_sort(), m) << "\n";);
theory_var_list * l = lhs->get_th_var_list();
while (l) {
theory_id th_id = l->get_id();

4
src/smt/smt_implied_equalities.cpp
View file

@ -92,7 +92,7 @@ namespace {
if (j < i && non_values.contains(j)) continue;
if (found_root_value && !non_values.contains(j)) continue;
expr* s = terms[j].term;
SASSERT(m.get_sort(t) == m.get_sort(s));
SASSERT(t->get_sort() == s->get_sort());
++m_stats_calls;
m_solver.push();
m_solver.assert_expr(m.mk_not(m.mk_eq(s, t)));
@ -118,7 +118,7 @@ namespace {
expr* t = terms[i].term;
for (unsigned j = 0; j < i; ++j) {
expr* s = terms[j].term;
SASSERT(m.get_sort(t) == m.get_sort(s));
SASSERT(t->get_sort() == s->get_sort());
++m_stats_calls;
m_stats_timer.start();
m_solver.push();

4
src/smt/smt_model_checker.cpp
View file

@ -94,11 +94,11 @@ namespace smt {
}
for (expr* f : m_fresh_exprs) {
if (m.get_sort(f) == m.get_sort(val)) {
if (f->get_sort() == val->get_sort()) {
return f;
}
}
fresh_term = m.mk_fresh_const("sk", m.get_sort(val));
fresh_term = m.mk_fresh_const("sk", val->get_sort());
}
m_fresh_exprs.push_back(fresh_term);
m_context->ensure_internalized(fresh_term);

10
src/smt/smt_model_generator.cpp
View file

@ -94,7 +94,7 @@ namespace smt {
for (enode * r : m_context->enodes()) {
if (r == r->get_root() && (m_context->is_relevant(r) || m.is_value(r->get_expr()))) {
roots.push_back(r);
sort * s = m.get_sort(r->get_owner());
sort * s = r->get_owner()->get_sort();
model_value_proc * proc = nullptr;
if (m.is_bool(s)) {
CTRACE("model", m_context->get_assignment(r) == l_undef,
@ -117,7 +117,7 @@ namespace smt {
}
else {
TRACE("model", tout << "creating fresh value for #" << r->get_owner_id() << "\n";);
proc = alloc(fresh_value_proc, mk_extra_fresh_value(m.get_sort(r->get_owner())));
proc = alloc(fresh_value_proc, mk_extra_fresh_value(r->get_owner()->get_sort()));
}
}
else {
@ -136,7 +136,7 @@ namespace smt {
SASSERT(r == r->get_root());
expr * n = r->get_owner();
if (!m.is_model_value(n)) {
sort * s = m.get_sort(r->get_owner());
sort * s = r->get_owner()->get_sort();
n = m_model->get_fresh_value(s);
CTRACE("model", n == 0,
tout << mk_pp(r->get_owner(), m) << "\nsort:\n" << mk_pp(s, m) << "\n";
@ -183,12 +183,12 @@ namespace smt {
return true;
bool visited = true;
for (enode * r : roots) {
if (m.get_sort(r->get_owner()) != s)
if (r->get_owner()->get_sort() != s)
continue;
SASSERT(r == r->get_root());
if (root2proc[r]->is_fresh())
continue; // r is associated with a fresh value...
TRACE("mg_top_sort", tout << "fresh!" << src.get_value()->get_idx() << " -> #" << r->get_owner_id() << " " << mk_pp(m.get_sort(r->get_owner()), m) << "\n";);
TRACE("mg_top_sort", tout << "fresh!" << src.get_value()->get_idx() << " -> #" << r->get_owner_id() << " " << mk_pp(r->get_owner()->get_sort(), m) << "\n";);
visit_child(source(r), colors, todo, visited);
TRACE("mg_top_sort", tout << "visited: " << visited << ", todo.size(): " << todo.size() << "\n";);
}

6
src/smt/theory_arith_aux.h
View file

@ -1089,19 +1089,19 @@ namespace smt {
expr* obj = get_enode(v)->get_owner();
expr_ref e(m);
rational r = val.get_rational();
if (m_util.is_int(m.get_sort(obj))) {
if (m_util.is_int(obj->get_sort())) {
if (r.is_int()) {
r += rational::one();
}
else {
r = ceil(r);
}
e = m_util.mk_numeral(r, m.get_sort(obj));
e = m_util.mk_numeral(r, obj->get_sort());
e = m_util.mk_ge(obj, e);
}
else {
// obj is over the reals.
e = m_util.mk_numeral(r, m.get_sort(obj));
e = m_util.mk_numeral(r, obj->get_sort());
if (val.get_infinitesimal().is_neg()) {
e = m_util.mk_ge(obj, e);

2
src/smt/theory_arith_core.h
View file

@ -1376,7 +1376,7 @@ namespace smt {
else {
if (n1->get_owner_id() > n2->get_owner_id())
std::swap(n1, n2);
sort * st = m.get_sort(n1->get_owner());
sort * st = n1->get_owner()->get_sort();
app * minus_one = m_util.mk_numeral(rational::minus_one(), st);
app * s = m_util.mk_add(n1->get_owner(), m_util.mk_mul(minus_one, n2->get_owner()));
ctx.internalize(s, false);

2
src/smt/theory_arith_eq.h
View file

@ -322,7 +322,7 @@ namespace smt {
if (is_equal(x, y))
return;
// I doesn't make sense to propagate an equality (to the core) of variables of different sort.
if (m.get_sort(var2expr(x)) != m.get_sort(var2expr(y))) {
if (var2expr(x)->get_sort() != var2expr(y)->get_sort()) {
TRACE("arith", tout << mk_pp(var2expr(x), m) << " = " << mk_pp(var2expr(y), m) << "\n";);
return;
}

10
src/smt/theory_array_bapa.cpp
View file

@ -229,7 +229,7 @@ namespace smt {
SASSERT(i2.m_is_leaf);
expr* s = sz1->get_arg(0);
expr* t = sz2->get_arg(0);
if (m.get_sort(s) != m.get_sort(t)) {
if (s->get_sort() != t->get_sort()) {
return true;
}
enode* r1 = get_root(s);
@ -369,7 +369,7 @@ namespace smt {
// create skolem function that is injective on integers (ensures uniqueness).
expr_ref mk_index_skolem(app* sz, expr* a, unsigned n) {
func_decls fg;
sort* s = m.get_sort(a);
sort* s = a->get_sort();
if (!m_index_skolems.find(s, fg)) {
sort* idx_sort = get_array_domain(s, 0);
sort* dom1[2] = { s, m_arith.mk_int() };
@ -500,7 +500,7 @@ namespace smt {
expr* s = term->get_arg(0);
expr* n = term->get_arg(1);
mk_th_axiom(~lit, mk_literal(m_arith.mk_ge(n, m_arith.mk_int(0))));
sort_size const& sz = m.get_sort(s)->get_num_elements();
sort_size const& sz = s->get_sort()->get_num_elements();
if (sz.is_infinite()) {
mk_th_axiom(~lit, mk_eq(th.mk_default(s), m.mk_false()));
}
@ -585,7 +585,7 @@ namespace smt {
bool is_size_limit(app* e, expr*& set, expr*& sz) {
func_decl* d = nullptr;
if (e->get_num_args() > 0 && m_size_limit_sort2skolems.find(m.get_sort(e->get_arg(0)), d) && d == e->get_decl()) {
if (e->get_num_args() > 0 && m_size_limit_sort2skolems.find(e->get_arg(0)->get_sort(), d) && d == e->get_decl()) {
set = e->get_arg(0);
sz = e->get_arg(1);
return true;
@ -599,7 +599,7 @@ namespace smt {
app_ref mk_size_limit(expr* set, expr* sz) {
func_decl* sk = nullptr;
sort* s = m.get_sort(set);
sort* s = set->get_sort();
if (!m_size_limit_sort2skolems.find(s, sk)) {
sort* dom[3] = { s, m_arith.mk_int(), m_arith.mk_int() };
sk = m.mk_fresh_func_decl("value-limit", "", 3, dom, m.mk_bool_sort());

2
src/smt/theory_bv.cpp
View file

@ -604,7 +604,7 @@ namespace smt {
TRACE("bv2int_bug", tout << "bv2int:\n" << mk_pp(n, m) << "\n";);
sort * int_sort = n->get_sort();
app * k = to_app(n->get_arg(0));
SASSERT(m_util.is_bv_sort(m.get_sort(k)));
SASSERT(m_util.is_bv_sort(k->get_sort()));
expr_ref_vector k_bits(m);
enode * k_enode = mk_enode(k);
get_bits(k_enode, k_bits);

4
src/smt/theory_datatype.cpp
View file

@ -596,7 +596,7 @@ namespace smt {
}
// explore `arg` (with parent)
expr* earg = arg->get_owner();
sort* s = m.get_sort(earg);
sort* s = earg->get_sort();
if (m_util.is_datatype(s)) {
m_parent.insert(arg->get_root(), parent);
oc_push_stack(arg);
@ -610,7 +610,7 @@ namespace smt {
occurs_check_explain(parent, aarg);
return true;
}
if (m_util.is_datatype(m.get_sort(aarg->get_owner()))) {
if (m_util.is_datatype(aarg->get_owner()->get_sort())) {
m_parent.insert(aarg->get_root(), parent);
oc_push_stack(aarg);
}

4
src/smt/theory_dense_diff_logic_def.h
View file

@ -808,7 +808,7 @@ namespace smt {
// adjust the value of all variables that have the same sort.
for (int v2 = 0; v2 < num_vars; ++v2) {
enode * n2 = get_enode(v2);
if (m.get_sort(n2->get_owner()) == s) {
if (n2->get_owner()->get_sort() == s) {
m_assignment[v2] -= val;
}
}
@ -1106,7 +1106,7 @@ namespace smt {
return f;
}
e = m_autil.mk_numeral(val.get_rational(), m.get_sort(f));
e = m_autil.mk_numeral(val.get_rational(), f->get_sort());
if (val.get_infinitesimal().is_neg()) {
if (is_strict) {

4
src/smt/theory_diff_logic_def.h
View file

@ -1036,7 +1036,7 @@ void theory_diff_logic<Ext>::new_eq_or_diseq(bool is_eq, theory_var v1, theory_v
app* s1 = get_enode(s)->get_owner();
app* t1 = get_enode(t)->get_owner();
s2 = m_util.mk_sub(t1, s1);
t2 = m_util.mk_numeral(k, m.get_sort(s2.get()));
t2 = m_util.mk_numeral(k, s2->get_sort());
// t1 - s1 = k
eq = m.mk_eq(s2.get(), t2.get());
if (m.has_trace_stream()) {
@ -1370,7 +1370,7 @@ expr_ref theory_diff_logic<Ext>::mk_ineq(theory_var v, inf_eps const& val, bool
}
inf_eps new_val = val; // - inf_rational(m_objective_consts[v]);
e = m_util.mk_numeral(new_val.get_rational(), m.get_sort(f));
e = m_util.mk_numeral(new_val.get_rational(), f->get_sort());
if (new_val.get_infinitesimal().is_neg()) {
if (is_strict) {

6
src/smt/theory_dl.cpp
View file

@ -80,7 +80,7 @@ namespace smt {
smt::context& ctx = m_th.get_context();
app* result = nullptr;
expr* n = m_node->get_owner();
sort* s = m_th.m().get_sort(n);
sort* s = n->get_sort();
func_decl* r, *v;
m_th.get_rep(s, r, v);
app_ref rep_of(m_th.m());
@ -175,7 +175,7 @@ namespace smt {
void relevant_eh(app * n) override {
if (u().is_finite_sort(n)) {
sort* s = m().get_sort(n);
sort* s = n->get_sort();
func_decl* r, *v;
get_rep(s, r, v);
@ -247,7 +247,7 @@ namespace smt {
}
void mk_lt(app* x, app* y) {
sort* s = m().get_sort(x);
sort* s = x->get_sort();
func_decl* r, *v;
get_rep(s, r, v);
app_ref lt(m()), le(m());

12
src/smt/theory_fpa.cpp
View file

@ -564,8 +564,8 @@ namespace smt {
a0 = to_app(owner->get_arg(0));
a1 = to_app(owner->get_arg(1));
a2 = to_app(owner->get_arg(2));
unsigned ebits = m_fpa_util.get_ebits(m.get_sort(owner));
unsigned sbits = m_fpa_util.get_sbits(m.get_sort(owner));
unsigned ebits = m_fpa_util.get_ebits(owner->get_sort());
unsigned sbits = m_fpa_util.get_sbits(owner->get_sort());
fpa_value_proc * vp = alloc(fpa_value_proc, this, ebits, sbits);
vp->add_dependency(ctx.get_enode(a0));
vp->add_dependency(ctx.get_enode(a1));
@ -593,8 +593,8 @@ namespace smt {
res = vp;
}
else if (m_fpa_util.is_float(owner)) {
unsigned ebits = m_fpa_util.get_ebits(m.get_sort(owner));
unsigned sbits = m_fpa_util.get_sbits(m.get_sort(owner));
unsigned ebits = m_fpa_util.get_ebits(owner->get_sort());
unsigned sbits = m_fpa_util.get_sbits(owner->get_sort());
fpa_value_proc * vp = alloc(fpa_value_proc, this, ebits, sbits);
enode * en = ctx.get_enode(wrapped);
vp->add_dependency(en);
@ -603,8 +603,8 @@ namespace smt {
}
}
else {
unsigned ebits = m_fpa_util.get_ebits(m.get_sort(owner));
unsigned sbits = m_fpa_util.get_sbits(m.get_sort(owner));
unsigned ebits = m_fpa_util.get_ebits(owner->get_sort());
unsigned sbits = m_fpa_util.get_sbits(owner->get_sort());
return alloc(expr_wrapper_proc, m_fpa_util.mk_pzero(ebits, sbits));
}

10
src/smt/theory_lra.cpp
View file

@ -2295,7 +2295,7 @@ public:
return;
expr* e1 = n1->get_owner();
expr* e2 = n2->get_owner();
if (e1->get_sort() != m.get_sort(e2))
if (e1->get_sort() != e2->get_sort())
return;
if (m.is_ite(e1) || m.is_ite(e2))
return;
@ -3296,7 +3296,7 @@ public:
TRACE("arith", tout << mk_pp(o, m) << " v" << v << " := " << r << "\n";);
SASSERT("integer variables should have integer values: " && (!a.is_int(o) || r.is_int() || m.limit().is_canceled()));
if (a.is_int(o) && !r.is_int()) r = floor(r);
return alloc(expr_wrapper_proc, m_factory->mk_value(r, m.get_sort(o)));
return alloc(expr_wrapper_proc, m_factory->mk_value(r, o->get_sort()));
}
}
@ -3507,18 +3507,18 @@ public:
expr* obj = get_enode(v)->get_owner();
rational r = val.x;
expr_ref e(m);
if (a.is_int(m.get_sort(obj))) {
if (a.is_int(obj->get_sort())) {
if (r.is_int()) {
r += rational::one();
}
else {
r = ceil(r);
}
e = a.mk_numeral(r, m.get_sort(obj));
e = a.mk_numeral(r, obj->get_sort());
e = a.mk_ge(obj, e);
}
else {
e = a.mk_numeral(r, m.get_sort(obj));
e = a.mk_numeral(r, obj->get_sort());
if (val.y.is_neg()) {
e = a.mk_ge(obj, e);
}

10
src/smt/theory_seq.cpp
View file

@ -566,7 +566,7 @@ bool theory_seq::check_extensionality() {
for (theory_var v : seqs) {
enode* n2 = get_enode(v);
expr* o2 = n2->get_owner();
if (m.get_sort(o1) != m.get_sort(o2)) {
if (o1->get_sort() != o2->get_sort()) {
continue;
}
if (ctx.is_diseq(n1, n2) || m_exclude.contains(o1, o2)) {
@ -1773,7 +1773,7 @@ void theory_seq::init_model(expr_ref_vector const& es) {
expr_ref s(m);
if (!canonize(e, eqs, s)) s = e;
if (is_var(s)) {
new_s = m_factory->get_fresh_value(m.get_sort(s));
new_s = m_factory->get_fresh_value(s->get_sort());
m_rep.update(s, new_s, eqs);
}
}
@ -1993,7 +1993,7 @@ app* theory_seq::mk_value(app* e) {
if (is_var(result)) {
SASSERT(m_factory);
expr_ref val(m);
val = m_factory->get_fresh_value(m.get_sort(result));
val = m_factory->get_fresh_value(result->get_sort());
if (val) {
result = val;
}
@ -2013,7 +2013,7 @@ void theory_seq::validate_model(model& mdl) {
for (auto const& eq : m_eqs) {
expr_ref_vector ls = eq.ls();
expr_ref_vector rs = eq.rs();
sort* srt = m.get_sort(ls.get(0));
sort* srt = ls[0]->get_sort();
expr_ref l(m_util.str.mk_concat(ls, srt), m);
expr_ref r(m_util.str.mk_concat(rs, srt), m);
if (!mdl.are_equal(l, r)) {
@ -2719,7 +2719,7 @@ void theory_seq::ensure_nth(literal lit, expr* s, expr* idx) {
s2 = tail;
}
elems.push_back(s2);
conc = mk_concat(elems, m.get_sort(s));
conc = mk_concat(elems, s->get_sort());
propagate_eq(lit, s, conc, true);
}

6
src/smt/theory_seq.h
View file

@ -477,11 +477,11 @@ namespace smt {
bool reduce_length(unsigned i, unsigned j, bool front, expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* deps);
expr_ref mk_empty(sort* s) { return expr_ref(m_util.str.mk_empty(s), m); }
expr_ref mk_concat(unsigned n, expr*const* es) { return expr_ref(m_util.str.mk_concat(n, es, m.get_sort(es[0])), m); }
expr_ref mk_concat(unsigned n, expr*const* es) { return expr_ref(m_util.str.mk_concat(n, es, es[0]->get_sort()), m); }
expr_ref mk_concat(unsigned n, expr*const* es, sort* s) { return expr_ref(m_util.str.mk_concat(n, es, s), m); }
expr_ref mk_concat(expr_ref_vector const& es, sort* s) { return mk_concat(es.size(), es.c_ptr(), s); }
expr_ref mk_concat(expr_ref_vector const& es) { SASSERT(!es.empty()); return expr_ref(m_util.str.mk_concat(es.size(), es.c_ptr(), m.get_sort(es[0])), m); }
expr_ref mk_concat(ptr_vector<expr> const& es) { SASSERT(!es.empty()); return mk_concat(es.size(), es.c_ptr(), m.get_sort(es[0])); }
expr_ref mk_concat(expr_ref_vector const& es) { SASSERT(!es.empty()); return expr_ref(m_util.str.mk_concat(es.size(), es.c_ptr(), es[0]->get_sort()), m); }
expr_ref mk_concat(ptr_vector<expr> const& es) { SASSERT(!es.empty()); return mk_concat(es.size(), es.c_ptr(), es[0]->get_sort()); }
expr_ref mk_concat(expr* e1, expr* e2) { return expr_ref(m_util.str.mk_concat(e1, e2), m); }
expr_ref mk_concat(expr* e1, expr* e2, expr* e3) { return expr_ref(m_util.str.mk_concat(e1, e2, e3), m); }
bool solve_nqs(unsigned i);

20
src/smt/theory_str.cpp
View file

@ -979,7 +979,7 @@ namespace smt {
TRACE("str", tout << "set up basic string axioms on " << mk_pp(str->get_owner(), m) << std::endl;);
{
sort * a_sort = m.get_sort(str->get_owner());
sort * a_sort = str->get_owner()->get_sort();
sort * str_sort = u.str.mk_string_sort();
if (a_sort != str_sort) {
TRACE("str", tout << "WARNING: not setting up string axioms on non-string term " << mk_pp(str->get_owner(), m) << std::endl;);
@ -6545,8 +6545,8 @@ namespace smt {
void theory_str::handle_equality(expr * lhs, expr * rhs) {
ast_manager & m = get_manager();
// both terms must be of sort String
sort * lhs_sort = m.get_sort(lhs);
sort * rhs_sort = m.get_sort(rhs);
sort * lhs_sort = lhs->get_sort();
sort * rhs_sort = rhs->get_sort();
sort * str_sort = u.str.mk_string_sort();
// Pick up new terms added during the search (e.g. recursive function expansion).
@ -6793,7 +6793,7 @@ namespace smt {
// expression throughout the lifetime of theory_str
m_trail.push_back(ex);
sort * ex_sort = m.get_sort(ex);
sort * ex_sort = ex->get_sort();
sort * str_sort = u.str.mk_string_sort();
sort * bool_sort = m.mk_bool_sort();
@ -7123,7 +7123,7 @@ namespace smt {
app * a = to_app(ex);
if (a->get_num_args() == 0) {
// we only care about string variables
sort * s = m.get_sort(ex);
sort * s = ex->get_sort();
sort * string_sort = u.str.mk_string_sort();
if (s != string_sort) {
return;
@ -7339,7 +7339,7 @@ namespace smt {
if (m.is_eq(argAst)) {
TRACE("str", tout
<< "eq ast " << mk_pp(argAst, m) << " is between args of sort "
<< m.get_sort(to_app(argAst)->get_arg(0))->get_name()
<< to_app(argAst)->get_arg(0)->get_sort()->get_name()
<< std::endl;);
classify_ast_by_type(argAst, varMap, concatMap, unrollMap);
}
@ -8454,7 +8454,7 @@ namespace smt {
for (std::set<enode*>::iterator it = eqc_roots.begin(); it != eqc_roots.end(); ++it) {
enode * e = *it;
app * a = e->get_owner();
if (!(m.get_sort(a) == u.str.mk_string_sort())) {
if (!(a->get_sort() == u.str.mk_string_sort())) {
TRACE("str", tout << "EQC root " << mk_pp(a, m) << " not a string term; skipping" << std::endl;);
} else {
TRACE("str", tout << "EQC root " << mk_pp(a, m) << " is a string term. Checking this EQC" << std::endl;);
@ -8950,7 +8950,7 @@ namespace smt {
model_value_proc * theory_str::mk_value(enode * n, model_generator & mg) {
TRACE("str", tout << "mk_value for: " << mk_ismt2_pp(n->get_owner(), get_manager()) <<
" (sort " << mk_ismt2_pp(get_manager().get_sort(n->get_owner()), get_manager()) << ")" << std::endl;);
" (sort " << mk_ismt2_pp(n->get_owner()->get_sort(), get_manager()) << ")" << std::endl;);
ast_manager & m = get_manager();
app_ref owner(m);
owner = n->get_owner();
@ -9208,13 +9208,13 @@ namespace smt {
ast_manager & m = get_manager();
// TRACE("str", tout << "ex " << mk_pp(ex, m) << " target " << target << " length " << length << " sublen " << mk_pp(sublen, m) << " extra " << mk_pp(extra, m) << std::endl;);
sort * ex_sort = m.get_sort(ex);
sort * ex_sort = ex->get_sort();
sort * str_sort = u.str.mk_string_sort();
if (ex_sort == str_sort) {
if (is_app(ex)) {
app * ap = to_app(ex);
if(u.str.is_concat(ap)){
if(u.str.is_concat(ap)) {
unsigned num_args = ap->get_num_args();
bool success = true;
for (unsigned i = 0; i < num_args; i++) {

6
src/smt/theory_str_mc.cpp
View file

@ -958,14 +958,14 @@ namespace smt {
}
}
// reduce string formulas only. ignore others
sort * fSort = m.get_sort(f);
sort * fSort = f->get_sort();
if (fSort == bool_sort && !is_quantifier(f)) {
// extracted terms
expr * subterm;
expr * lhs;
expr * rhs;
if (m.is_eq(f, lhs, rhs)) {
sort * lhs_sort = m.get_sort(lhs);
sort * lhs_sort = lhs->get_sort();
if (lhs_sort == str_sort) {
TRACE("str_fl", tout << "reduce string equality: " << mk_pp(lhs, m) << " == " << mk_pp(rhs, m) << std::endl;);
expr_ref cex(m);
@ -1031,7 +1031,7 @@ namespace smt {
}else if (m.is_not(f, subterm)) {
// if subterm is a string formula such as an equality, reduce it as a disequality
if (m.is_eq(subterm, lhs, rhs)) {
sort * lhs_sort = m.get_sort(lhs);
sort * lhs_sort = lhs->get_sort();
if (lhs_sort == str_sort) {
TRACE("str_fl", tout << "reduce string disequality: " << mk_pp(lhs, m) << " != " << mk_pp(rhs, m) << std::endl;);
expr_ref cex(m);

2
src/smt/theory_utvpi_def.h
View file

@ -173,7 +173,7 @@ namespace smt {
app* s1 = get_enode(s)->get_owner();
app* t1 = get_enode(t)->get_owner();
s2 = a.mk_sub(t1, s1);
t2 = a.mk_numeral(k, m.get_sort(s2.get()));
t2 = a.mk_numeral(k, s2->get_sort());
eq = m.mk_eq(s2.get(), t2.get());
TRACE("utvpi", tout << v1 << " .. " << v2 << "\n" << eq << "\n";);