mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
fix build, refactor
This commit is contained in:
parent
3ae4c6e9de
commit
937b61fc88
|
@ -133,7 +133,7 @@ void ackr_model_converter::add_entry(model_evaluator & evaluator,
|
|||
app* A = to_app(term->get_arg(0));
|
||||
expr * e = nullptr, *c = nullptr;
|
||||
if (!array_interpretations.find(A, e)) {
|
||||
e = autil.mk_const_array(m.get_sort(A), value);
|
||||
e = autil.mk_const_array(A->get_sort(), value);
|
||||
}
|
||||
else {
|
||||
// avoid storing the same as the default value.
|
||||
|
|
|
@ -175,12 +175,12 @@ void lackr::abstract_fun(fun2terms_map const& apps) {
|
|||
for (auto const& kv : apps) {
|
||||
func_decl* fd = kv.m_key;
|
||||
for (app * t : kv.m_value->var_args) {
|
||||
app * fc = m.mk_fresh_const(fd->get_name(), m.get_sort(t));
|
||||
app * fc = m.mk_fresh_const(fd->get_name(), t->get_sort());
|
||||
SASSERT(t->get_decl() == fd);
|
||||
m_info->set_abstr(t, fc);
|
||||
}
|
||||
for (app * t : kv.m_value->const_args) {
|
||||
app * fc = m.mk_fresh_const(fd->get_name(), m.get_sort(t));
|
||||
app * fc = m.mk_fresh_const(fd->get_name(), t->get_sort());
|
||||
SASSERT(t->get_decl() == fd);
|
||||
m_info->set_abstr(t, fc);
|
||||
}
|
||||
|
@ -192,11 +192,11 @@ void lackr::abstract_sel(sel2terms_map const& apps) {
|
|||
for (auto const& kv : apps) {
|
||||
func_decl * fd = kv.m_key->get_decl();
|
||||
for (app * t : kv.m_value->const_args) {
|
||||
app * fc = m.mk_fresh_const(fd->get_name(), m.get_sort(t));
|
||||
app * fc = m.mk_fresh_const(fd->get_name(), t->get_sort());
|
||||
m_info->set_abstr(t, fc);
|
||||
}
|
||||
for (app * t : kv.m_value->var_args) {
|
||||
app * fc = m.mk_fresh_const(fd->get_name(), m.get_sort(t));
|
||||
app * fc = m.mk_fresh_const(fd->get_name(), t->get_sort());
|
||||
m_info->set_abstr(t, fc);
|
||||
}
|
||||
}
|
||||
|
|
|
@ -325,7 +325,7 @@ private:
|
|||
if (k == OP_EQ) {
|
||||
// theory dispatch for =
|
||||
SASSERT(num == 2);
|
||||
family_id s_fid = m.get_sort(values.get(0))->get_family_id();
|
||||
family_id s_fid = values[0]->get_sort()->get_family_id();
|
||||
if (s_fid == m_bv_rw.get_fid())
|
||||
m_bv_rw.mk_eq_core(values.get(0), values.get(1), result);
|
||||
} else {
|
||||
|
|
|
@ -2415,7 +2415,7 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args
|
|||
}
|
||||
else if (num == 2 &&
|
||||
m_util.is_rm(args[0]) &&
|
||||
m_util.is_float(m.get_sort(args[1]))) {
|
||||
m_util.is_float(args[1]->get_sort())) {
|
||||
// rm + float -> float
|
||||
mk_to_fp_float(f, f->get_range(), args[0], args[1], result);
|
||||
}
|
||||
|
@ -3223,7 +3223,7 @@ void fpa2bv_converter::mk_to_ieee_bv_unspecified(func_decl * f, unsigned num, ex
|
|||
else {
|
||||
expr_ref nw = nan_wrap(args[0]);
|
||||
|
||||
sort * domain[1] = { m.get_sort(nw) };
|
||||
sort * domain[1] = { nw->get_sort() };
|
||||
func_decl * f_bv = mk_bv_uf(f, domain, f->get_range());
|
||||
result = m.mk_app(f_bv, nw);
|
||||
|
||||
|
@ -3439,7 +3439,7 @@ void fpa2bv_converter::mk_to_bv_unspecified(func_decl * f, unsigned num, expr *
|
|||
else {
|
||||
expr * rm_bv = to_app(args[0])->get_arg(0);
|
||||
expr_ref nw = nan_wrap(args[1]);
|
||||
sort * domain[2] = { m.get_sort(rm_bv), m.get_sort(nw) };
|
||||
sort * domain[2] = { rm_bv->get_sort(), nw->get_sort() };
|
||||
func_decl * f_bv = mk_bv_uf(f, domain, f->get_range());
|
||||
result = m.mk_app(f_bv, rm_bv, nw);
|
||||
}
|
||||
|
@ -3456,7 +3456,7 @@ void fpa2bv_converter::mk_to_real_unspecified(func_decl * f, unsigned num, expr
|
|||
else {
|
||||
expr * n = args[0];
|
||||
expr_ref nw = nan_wrap(n);
|
||||
sort * domain[1] = { m.get_sort(nw) };
|
||||
sort * domain[1] = { nw->get_sort() };
|
||||
func_decl * f_bv = mk_bv_uf(f, domain, f->get_range());
|
||||
result = m.mk_app(f_bv, nw);
|
||||
}
|
||||
|
|
|
@ -64,9 +64,9 @@ struct enum2bv_rewriter::imp {
|
|||
unsigned bv_size = get_bv_size(s);
|
||||
sort_ref bv_sort(m_bv.mk_sort(bv_size), m);
|
||||
if (is_unate(s))
|
||||
return m_bv.mk_numeral(rational((1 << idx) - 1), bv_sort);
|
||||
return m_bv.mk_numeral(rational((1 << idx) - 1), bv_sort.get());
|
||||
else
|
||||
return m_bv.mk_numeral(rational(idx), bv_sort);
|
||||
return m_bv.mk_numeral(rational(idx), bv_sort.get());
|
||||
}
|
||||
|
||||
void constrain_domain(expr* x, sort* s, sort* bv_sort) {
|
||||
|
|
|
@ -99,7 +99,7 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) {
|
|||
if (d) {
|
||||
m_args.push_back(d);
|
||||
arg_differs |= arg != d;
|
||||
SASSERT(arg->get_sort() == m.get_sort(d));
|
||||
SASSERT(arg->get_sort() == d->get_sort());
|
||||
}
|
||||
else {
|
||||
m_todo.push_back(arg);
|
||||
|
|
|
@ -43,7 +43,7 @@ expr_ref func_decl_replace::operator()(expr* e) {
|
|||
if (m_cache.find(arg, d)) {
|
||||
m_args.push_back(d);
|
||||
arg_differs |= arg != d;
|
||||
SASSERT(arg->get_sort() == m.get_sort(d));
|
||||
SASSERT(arg->get_sort() == d->get_sort());
|
||||
}
|
||||
else {
|
||||
m_todo.push_back(arg);
|
||||
|
|
|
@ -327,7 +327,7 @@ bool cmd_context::macros_find(symbol const& s, unsigned n, expr*const* args, exp
|
|||
bool eq = true;
|
||||
coerced_args.reset();
|
||||
for (unsigned i = 0; eq && i < n; ++i) {
|
||||
if (d.m_domain[i] == m().get_sort(args[i])) {
|
||||
if (d.m_domain[i] == args[i]->get_sort()) {
|
||||
coerced_args.push_back(args[i]);
|
||||
continue;
|
||||
}
|
||||
|
@ -1132,7 +1132,7 @@ void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * arg
|
|||
bool first = true;
|
||||
for (unsigned i = 0; i < num_args; ++i, first = false) {
|
||||
if (!first) buffer << " ";
|
||||
buffer << mk_pp(m().get_sort(args[i]), m());
|
||||
buffer << mk_pp(args[i]->get_sort(), m());
|
||||
}
|
||||
buffer << ") ";
|
||||
if (range) buffer << mk_pp(range, m()) << " ";
|
||||
|
|
|
@ -293,7 +293,7 @@ public:
|
|||
throw cmd_exception("invalid command, mismatch between the number of quantified variables and the number of arguments.");
|
||||
unsigned i = num;
|
||||
while (i-- > 0) {
|
||||
sort * s = ctx.m().get_sort(ts[i]);
|
||||
sort * s = ts[i]->get_sort();
|
||||
if (s != m_q->get_decl_sort(i)) {
|
||||
std::ostringstream buffer;
|
||||
buffer << "invalid command, sort mismatch at position " << i;
|
||||
|
|
|
@ -65,6 +65,12 @@ namespace opt {
|
|||
void lns::setup_assumptions(model_ref& mdl, expr_ref_vector const& asms) {
|
||||
m_hardened.reset();
|
||||
m_soft.reset();
|
||||
std::cout << "disjoint cores: " << m_cores.size() << "\n";
|
||||
for (auto const& c : m_cores)
|
||||
std::cout << c.size() << "\n";
|
||||
m_was_flipped.reset();
|
||||
m_in_core.reset();
|
||||
m_cores.reset();
|
||||
for (expr* a : asms) {
|
||||
if (mdl->is_true(a))
|
||||
m_hardened.push_back(a);
|
||||
|
@ -118,6 +124,7 @@ namespace opt {
|
|||
m_hardened.push_back(m.mk_not(soft(i)));
|
||||
for (unsigned k = i; k + 1 < m_soft.size(); ++k)
|
||||
m_soft[k] = soft(k + 1);
|
||||
m_was_flipped.mark(m_hardened.back());
|
||||
m_soft.pop_back();
|
||||
--i;
|
||||
break;
|
||||
|
@ -157,9 +164,14 @@ namespace opt {
|
|||
if (r == l_false) {
|
||||
expr_ref_vector core(m);
|
||||
s.get_unsat_core(core);
|
||||
std::cout << "core size " << core.size() << "\n";
|
||||
if (core.size() == 4)
|
||||
std::cout << core << "\n";
|
||||
bool was_flipped = false;
|
||||
for (expr* c : core)
|
||||
was_flipped |= m_was_flipped.is_marked(c);
|
||||
if (!was_flipped) {
|
||||
for (expr* c : core)
|
||||
m_in_core.mark(c, true);
|
||||
m_cores.push_back(core);
|
||||
}
|
||||
}
|
||||
#endif
|
||||
return r;
|
||||
|
|
|
@ -33,6 +33,11 @@ namespace opt {
|
|||
expr_ref_vector m_soft;
|
||||
unsigned m_max_conflicts { 1000 };
|
||||
unsigned m_num_improves { 0 };
|
||||
|
||||
vector<expr_ref_vector> m_cores;
|
||||
expr_mark m_in_core;
|
||||
expr_mark m_was_flipped;
|
||||
|
||||
std::function<void(model_ref& m)> m_update_model;
|
||||
|
||||
expr* soft(unsigned i) const { return m_soft[i]; }
|
||||
|
|
|
@ -1444,7 +1444,7 @@ namespace smt2 {
|
|||
// compute match condition and substitution
|
||||
// t is shifted by size of subst.
|
||||
expr_ref bind_match(expr* t, expr* pattern, expr_ref_vector& subst) {
|
||||
if (t->get_sort() != m().get_sort(pattern)) {
|
||||
if (t->get_sort() != pattern->get_sort()) {
|
||||
std::ostringstream str;
|
||||
str << "sorts of pattern " << expr_ref(pattern, m()) << " and term "
|
||||
<< expr_ref(t, m()) << " are not aligned";
|
||||
|
@ -2271,7 +2271,7 @@ namespace smt2 {
|
|||
unsigned num_vars = parse_sorted_vars();
|
||||
parse_sort("Invalid function definition");
|
||||
parse_expr();
|
||||
if (m().get_sort(expr_stack().back()) != sort_stack().back())
|
||||
if (expr_stack().back()->get_sort() != sort_stack().back())
|
||||
throw parser_exception("invalid function/constant definition, sort mismatch");
|
||||
sort* const* sorts = sort_stack().c_ptr() + sort_spos;
|
||||
expr* t = expr_stack().back();
|
||||
|
@ -2427,11 +2427,11 @@ namespace smt2 {
|
|||
symbol_stack().shrink(sym_spos);
|
||||
m_env.end_scope();
|
||||
m_num_bindings = 0;
|
||||
if (m().get_sort(body) != f->get_range()) {
|
||||
if (body->get_sort() != f->get_range()) {
|
||||
std::ostringstream buffer;
|
||||
buffer << "invalid function definition, sort mismatch. Expcected "
|
||||
<< mk_pp(f->get_range(), m()) << " but function body has sort "
|
||||
<< mk_pp(m().get_sort(body), m());
|
||||
<< mk_pp(body->get_sort(), m());
|
||||
throw parser_exception(buffer.str());
|
||||
}
|
||||
m_ctx.insert_rec_fun(f, bindings, ids, body);
|
||||
|
@ -2448,7 +2448,7 @@ namespace smt2 {
|
|||
next();
|
||||
parse_sort("Invalid constant definition");
|
||||
parse_expr();
|
||||
if (m().get_sort(expr_stack().back()) != sort_stack().back())
|
||||
if (expr_stack().back()->get_sort() != sort_stack().back())
|
||||
throw parser_exception("invalid constant definition, sort mismatch");
|
||||
m_ctx.insert(id, 0, nullptr, expr_stack().back());
|
||||
check_rparen("invalid constant definition, ')' expected");
|
||||
|
|
|
@ -1257,7 +1257,7 @@ namespace mbp {
|
|||
if (s == m_var->x()) {
|
||||
expr_ref result(t, m);
|
||||
expr_ref_vector args(m);
|
||||
sort* range = get_array_range(m.get_sort(s));
|
||||
sort* range = get_array_range(s->get_sort());
|
||||
for (unsigned i = 0; i < idxs.size(); ++i) {
|
||||
app_ref var(m), sel(m);
|
||||
expr_ref val(m);
|
||||
|
@ -1559,7 +1559,7 @@ namespace mbp {
|
|||
lits.push_back(m.mk_eq(a1, a2));
|
||||
}
|
||||
else {
|
||||
sort* s = m.get_sort(store->get_arg(indices.size() + 1));
|
||||
sort* s = store->get_arg(indices.size() + 1)->get_sort();
|
||||
for (app* idx : *m_indices[s]) {
|
||||
indices.push_back(idx);
|
||||
assert_store_select(indices, store, mdl, tg, lits);
|
||||
|
|
|
@ -67,7 +67,7 @@ namespace nlarith {
|
|||
ast_manager& m = m_lits.get_manager();
|
||||
std::string name = m_x->get_decl()->get_name().str();
|
||||
name += suffix;
|
||||
sort* r = m.get_sort(m_x);
|
||||
sort* r = m_x->get_sort();
|
||||
v= m.mk_const(symbol(name.c_str()), r);
|
||||
}
|
||||
};
|
||||
|
|
|
@ -2075,7 +2075,7 @@ namespace qe {
|
|||
for (unsigned i = 0; i < num_vars; ++i) {
|
||||
contains_app contains_x(m, vars[i]);
|
||||
if (contains_x(fml)) {
|
||||
sorts.push_back(m.get_sort(vars[i]));
|
||||
sorts.push_back(vars[i]->get_sort());
|
||||
names.push_back(vars[i]->get_decl()->get_name());
|
||||
free_vars.push_back(vars[i]);
|
||||
}
|
||||
|
|
|
@ -1037,7 +1037,7 @@ namespace qe {
|
|||
app_ref x(m_ctx.get_var(index-1), m);
|
||||
app_ref z(m);
|
||||
expr_ref p1(m);
|
||||
sort* s = m.get_sort(p);
|
||||
sort* s = p->get_sort();
|
||||
if (is_aux) {
|
||||
// An auxiliary variable was introduced in lieu of 'x'.
|
||||
// it has coefficient 'm' = values[index].
|
||||
|
|
|
@ -92,7 +92,7 @@ namespace qe {
|
|||
for (unsigned i = 0; i < sz; ++i) {
|
||||
expr_ref save(m);
|
||||
save = lhs = args[i].get();
|
||||
args[i] = arith.mk_numeral(rational(0), m.get_sort(lhs));
|
||||
args[i] = arith.mk_numeral(rational(0), lhs->get_sort());
|
||||
rhs = arith.mk_uminus(arith.mk_add(args.size(), args.c_ptr()));
|
||||
if (arith.is_mul(lhs, e1, e2) &&
|
||||
arith.is_numeral(e1, r) &&
|
||||
|
@ -165,7 +165,7 @@ namespace qe {
|
|||
expr_ref store_B_i_t(m);
|
||||
|
||||
unsigned num_args = args[0].size();
|
||||
B = m.mk_fresh_const("B", m.get_sort(A));
|
||||
B = m.mk_fresh_const("B", A->get_sort());
|
||||
ptr_buffer<expr> args2;
|
||||
args2.push_back(B);
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
|
@ -232,7 +232,7 @@ namespace qe {
|
|||
for (unsigned i = args.size(); i > 0; ) {
|
||||
--i;
|
||||
args2.reset();
|
||||
w = m.mk_fresh_const("w", m.get_sort(args[i].back()));
|
||||
w = m.mk_fresh_const("w", args[i].back()->get_sort());
|
||||
args2.push_back(store_T);
|
||||
args2.append(args[i]);
|
||||
|
||||
|
|
|
@ -116,12 +116,12 @@ namespace qe {
|
|||
private:
|
||||
|
||||
bool is_small_domain(contains_app& x, eq_atoms& eqs, uint64_t& domain_size) {
|
||||
VERIFY(m_util.try_get_size(m.get_sort(x.x()), domain_size));
|
||||
VERIFY(m_util.try_get_size(x.x()->get_sort(), domain_size));
|
||||
return domain_size < eqs.num_eqs() + eqs.num_neqs();
|
||||
}
|
||||
|
||||
void assign_small_domain(contains_app & x,eq_atoms& eqs, unsigned value) {
|
||||
expr_ref vl(m_util.mk_numeral(value, m.get_sort(x.x())), m);
|
||||
expr_ref vl(m_util.mk_numeral(value, x.x()->get_sort()), m);
|
||||
expr_ref eq(m.mk_eq(x.x(), vl), m);
|
||||
m_ctx.add_constraint(true, eq);
|
||||
}
|
||||
|
@ -145,7 +145,7 @@ namespace qe {
|
|||
}
|
||||
|
||||
void subst_small_domain(contains_app & x,eq_atoms& eqs, unsigned v,expr_ref & fml) {
|
||||
expr_ref vl(m_util.mk_numeral(v, m.get_sort(x.x())), m);
|
||||
expr_ref vl(m_util.mk_numeral(v, x.x()->get_sort()), m);
|
||||
m_replace.apply_substitution(x.x(), vl, fml);
|
||||
}
|
||||
|
||||
|
|
|
@ -2307,7 +2307,7 @@ public:
|
|||
ptr_vector<sort> sorts;
|
||||
svector<symbol> names;
|
||||
for (unsigned i = 0; i < vars.size(); ++i) {
|
||||
sorts.push_back(m.get_sort(vars[i].get()));
|
||||
sorts.push_back(vars[i]->get_sort());
|
||||
names.push_back(vars[i]->get_decl()->get_name());
|
||||
}
|
||||
q = m.mk_exists(vars.size(), sorts.c_ptr(), names.c_ptr(), tmp, 1, qe_lite);
|
||||
|
|
|
@ -55,7 +55,7 @@ class mbproj::impl {
|
|||
}
|
||||
|
||||
mbp::project_plugin* get_plugin(app* var) {
|
||||
family_id fid = m.get_sort(var)->get_family_id();
|
||||
family_id fid = var->get_sort()->get_family_id();
|
||||
return m_plugins.get(fid, nullptr);
|
||||
}
|
||||
|
||||
|
@ -168,7 +168,7 @@ class mbproj::impl {
|
|||
expr* e1, * e2;
|
||||
if (m_array.is_select(n)) {
|
||||
for (expr* arg : *n) {
|
||||
if (arg->get_sort() == m.get_sort(m_var) && arg != m_var)
|
||||
if (arg->get_sort() == m_var->get_sort() && arg != m_var)
|
||||
m_res.push_back(arg);
|
||||
}
|
||||
}
|
||||
|
|
|
@ -313,7 +313,7 @@ namespace arith {
|
|||
expr* e2 = n2->get_expr();
|
||||
if (m.is_ite(e1) || m.is_ite(e2))
|
||||
return;
|
||||
if (e1->get_sort() != m.get_sort(e2))
|
||||
if (e1->get_sort() != e2->get_sort())
|
||||
return;
|
||||
reset_evidence();
|
||||
for (auto const& ev : e)
|
||||
|
@ -612,7 +612,7 @@ namespace arith {
|
|||
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);
|
||||
value = a.mk_numeral(r, m.get_sort(o));
|
||||
value = a.mk_numeral(r, o->get_sort());
|
||||
}
|
||||
else if (a.is_arith_expr(o)) {
|
||||
expr_ref_vector args(m);
|
||||
|
|
|
@ -425,7 +425,7 @@ namespace array {
|
|||
|
||||
bool solver::has_unitary_domain(app* array_term) {
|
||||
SASSERT(a.is_array(array_term));
|
||||
sort* s = m.get_sort(array_term);
|
||||
sort* s = array_term->get_sort();
|
||||
unsigned dim = get_array_arity(s);
|
||||
for (unsigned i = 0; i < dim; ++i) {
|
||||
sort* d = get_array_domain(s, i);
|
||||
|
@ -437,7 +437,7 @@ namespace array {
|
|||
|
||||
bool solver::has_large_domain(expr* array_term) {
|
||||
SASSERT(a.is_array(array_term));
|
||||
sort* s = m.get_sort(array_term);
|
||||
sort* s = array_term->get_sort();
|
||||
unsigned dim = get_array_arity(s);
|
||||
rational sz(1);
|
||||
for (unsigned i = 0; i < dim; ++i) {
|
||||
|
@ -504,7 +504,7 @@ namespace array {
|
|||
for (unsigned j = i; j-- > 0; ) {
|
||||
theory_var v2 = roots[j];
|
||||
expr* e2 = var2expr(v2);
|
||||
if (e1->get_sort() != m.get_sort(e2))
|
||||
if (e1->get_sort() != e2->get_sort())
|
||||
continue;
|
||||
if (have_different_model_values(v1, v2))
|
||||
continue;
|
||||
|
|
|
@ -511,7 +511,7 @@ namespace dt {
|
|||
};
|
||||
for (enode* arg : euf::enode_args(parentc)) {
|
||||
add(arg);
|
||||
sort* s = m.get_sort(arg->get_expr());
|
||||
sort* s = arg->get_expr()->get_sort();
|
||||
if (m_autil.is_array(s) && dt.is_datatype(get_array_range(s)))
|
||||
for (enode* aarg : get_array_args(arg))
|
||||
add(aarg);
|
||||
|
|
|
@ -553,7 +553,7 @@ namespace q {
|
|||
}
|
||||
|
||||
mbp::project_plugin* mbqi::get_plugin(app* var) {
|
||||
family_id fid = m.get_sort(var)->get_family_id();
|
||||
family_id fid = var->get_sort()->get_family_id();
|
||||
return m_plugins.get(fid, nullptr);
|
||||
}
|
||||
|
||||
|
|
|
@ -181,7 +181,7 @@ namespace q {
|
|||
if (!m_unit_table.empty())
|
||||
return;
|
||||
for (euf::enode* n : ctx.get_egraph().nodes()) {
|
||||
if (!n->interpreted() && !m.is_uninterp(m.get_sort(n->get_expr())))
|
||||
if (!n->interpreted() && !m.is_uninterp(n->get_expr()->get_sort()))
|
||||
continue;
|
||||
expr* e = n->get_expr();
|
||||
sort* s = e->get_sort();
|
||||
|
|
|
@ -170,7 +170,7 @@ namespace smt {
|
|||
ge = m_util.mk_ge(t1, t2);
|
||||
}
|
||||
else {
|
||||
sort * st = m.get_sort(t1);
|
||||
sort * st = t1->get_sort();
|
||||
app_ref minus_one(m_util.mk_numeral(rational::minus_one(), st), m);
|
||||
app_ref zero(m_util.mk_numeral(rational::zero(), st), m);
|
||||
app_ref t3(m_util.mk_mul(minus_one, t2), m);
|
||||
|
|
|
@ -870,7 +870,7 @@ void seq_axioms::add_suffix_axiom(expr* e) {
|
|||
add_axiom(lit, s_gt_t, ~mk_eq(y, s));
|
||||
#else
|
||||
sort* char_sort = nullptr;
|
||||
VERIFY(seq.is_seq(m.get_sort(s), char_sort));
|
||||
VERIFY(seq.is_seq(s->get_sort(), char_sort));
|
||||
expr_ref x = m_sk.mk("seq.suffix.x", s, t);
|
||||
expr_ref y = m_sk.mk("seq.suffix.y", s, t);
|
||||
expr_ref z = m_sk.mk("seq.suffix.z", s, t);
|
||||
|
@ -899,7 +899,7 @@ void seq_axioms::add_prefix_axiom(expr* e) {
|
|||
|
||||
#else
|
||||
sort* char_sort = nullptr;
|
||||
VERIFY(seq.is_seq(m.get_sort(s), char_sort));
|
||||
VERIFY(seq.is_seq(s->get_sort(), char_sort));
|
||||
expr_ref x = m_sk.mk("seq.prefix.x", s, t);
|
||||
expr_ref y = m_sk.mk("seq.prefix.y", s, t);
|
||||
expr_ref z = m_sk.mk("seq.prefix.z", s, t);
|
||||
|
|
|
@ -169,7 +169,7 @@ bool seq_skolem::is_post(expr* e, expr*& s, expr*& start) {
|
|||
expr_ref seq_skolem::mk_unit_inv(expr* n) {
|
||||
expr* u = nullptr;
|
||||
VERIFY(seq.str.is_unit(n, u));
|
||||
sort* s = m.get_sort(u);
|
||||
sort* s = u->get_sort();
|
||||
return mk(symbol("seq.unit-inv"), n, s);
|
||||
}
|
||||
|
||||
|
@ -180,7 +180,7 @@ expr_ref seq_skolem::mk_last(expr* s) {
|
|||
return expr_ref(seq.str.mk_char(str, str.length()-1), m);
|
||||
}
|
||||
sort* char_sort = nullptr;
|
||||
VERIFY(seq.is_seq(m.get_sort(s), char_sort));
|
||||
VERIFY(seq.is_seq(s->get_sort(), char_sort));
|
||||
return mk(m_seq_last, s, char_sort);
|
||||
}
|
||||
|
||||
|
|
|
@ -82,7 +82,7 @@ namespace smt {
|
|||
|
||||
expr_ref mk_tail(expr* s, expr* i) { return mk(m_tail, s, i); }
|
||||
expr_ref mk_post(expr* s, expr* i) { return mk(m_post, s, i); }
|
||||
expr_ref mk_ite(expr* c, expr* t, expr* e) { return mk(symbol("seq.if"), c, t, e, nullptr, m.get_sort(t)); }
|
||||
expr_ref mk_ite(expr* c, expr* t, expr* e) { return mk(symbol("seq.if"), c, t, e, nullptr, t->get_sort()); }
|
||||
expr_ref mk_last(expr* s);
|
||||
expr_ref mk_first(expr* s);
|
||||
expr_ref mk_pre(expr* s, expr* i) { return mk(m_pre, s, i); }
|
||||
|
|
|
@ -318,7 +318,7 @@ namespace smt {
|
|||
}
|
||||
else {
|
||||
if (!pushed) pushed = true, push();
|
||||
expr_ref c(m.mk_fresh_const("a", m.get_sort(a)), m);
|
||||
expr_ref c(m.mk_fresh_const("a", a->get_sort()), m);
|
||||
expr_ref eq(m.mk_eq(c, a), m);
|
||||
assert_expr(eq);
|
||||
assumptions.push_back(c);
|
||||
|
|
|
@ -4487,7 +4487,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
bool context::get_value(enode * n, expr_ref & value) {
|
||||
sort * s = m.get_sort(n->get_owner());
|
||||
sort * s = n->get_owner()->get_sort();
|
||||
family_id fid = s->get_family_id();
|
||||
theory * th = get_theory(fid);
|
||||
if (th == nullptr)
|
||||
|
|
|
@ -57,7 +57,7 @@ namespace {
|
|||
|
||||
void partition_terms(unsigned num_terms, expr* const* terms, sort2term_ids& termids) {
|
||||
for (unsigned i = 0; i < num_terms; ++i) {
|
||||
sort* s = m.get_sort(terms[i]);
|
||||
sort* s = terms[i]->get_sort();
|
||||
term_ids& vec = termids.insert_if_not_there(s, term_ids());
|
||||
vec.push_back(term_id(expr_ref(terms[i],m), i));
|
||||
}
|
||||
|
@ -148,7 +148,7 @@ namespace {
|
|||
|
||||
SASSERT(!terms.empty());
|
||||
|
||||
sort* srt = m.get_sort(terms[0].term);
|
||||
sort* srt = terms[0].term->get_sort();
|
||||
|
||||
if (m_array_util.is_array(srt)) {
|
||||
|
||||
|
@ -249,7 +249,7 @@ namespace {
|
|||
|
||||
void assert_relevant(unsigned num_terms, expr* const* terms) {
|
||||
for (unsigned i = 0; i < num_terms; ++i) {
|
||||
sort* srt = m.get_sort(terms[i]);
|
||||
sort* srt = terms[i]->get_sort();
|
||||
if (!m_array_util.is_array(srt)) {
|
||||
m_solver.assert_expr(m.mk_app(m.mk_func_decl(symbol("Relevant!"), 1, &srt, m.mk_bool_sort()), terms[i]));
|
||||
}
|
||||
|
@ -259,7 +259,7 @@ namespace {
|
|||
void assert_relevant(term_ids& terms) {
|
||||
for (unsigned i = 0; i < terms.size(); ++i) {
|
||||
expr* t = terms[i].term;
|
||||
sort* srt = m.get_sort(t);
|
||||
sort* srt = t->get_sort();
|
||||
if (!m_array_util.is_array(srt)) {
|
||||
m_solver.assert_expr(m.mk_app(m.mk_func_decl(symbol("Relevant!"), 1, &srt, m.mk_bool_sort()), t));
|
||||
}
|
||||
|
|
|
@ -136,7 +136,7 @@ bool induction_lemmas::viable_induction_children(enode* n) {
|
|||
|
||||
bool induction_lemmas::viable_induction_term(enode* p, enode* n) {
|
||||
return
|
||||
viable_induction_sort(m.get_sort(n->get_owner())) &&
|
||||
viable_induction_sort(n->get_owner()->get_sort()) &&
|
||||
viable_induction_parent(p, n) &&
|
||||
viable_induction_children(n);
|
||||
}
|
||||
|
@ -281,7 +281,7 @@ void induction_lemmas::mk_hypothesis_substs(unsigned depth, expr* x, cond_substs
|
|||
}
|
||||
|
||||
void induction_lemmas::mk_hypothesis_substs_rec(unsigned depth, sort* s, expr* y, expr_ref_vector& conds, cond_substs_t& subst) {
|
||||
sort* ys = m.get_sort(y);
|
||||
sort* ys = y->get_sort();
|
||||
for (func_decl* c : *m_dt.get_datatype_constructors(ys)) {
|
||||
func_decl* is_c = m_dt.get_constructor_recognizer(c);
|
||||
conds.push_back(m.mk_app(is_c, y));
|
||||
|
@ -417,7 +417,7 @@ bool induction_lemmas::operator()(literal lit) {
|
|||
for (enode* n : induction_positions(r)) {
|
||||
expr* t = n->get_owner();
|
||||
if (is_uninterp_const(t)) { // for now, to avoid overlapping terms
|
||||
sort* s = m.get_sort(t);
|
||||
sort* s = t->get_sort();
|
||||
expr_ref sk(m.mk_fresh_const("sk", s), m);
|
||||
sks.push_back(sk);
|
||||
rep.insert(t, sk);
|
||||
|
@ -460,7 +460,7 @@ void induction_lemmas::apply_induction(literal lit, induction_positions_t const
|
|||
if (term2skolem.contains(t))
|
||||
continue;
|
||||
if (i == sks.size()) {
|
||||
sk = m.mk_fresh_const("sk", m.get_sort(t));
|
||||
sk = m.mk_fresh_const("sk", t->get_sort());
|
||||
sks.push_back(sk);
|
||||
}
|
||||
else {
|
||||
|
|
|
@ -315,7 +315,7 @@ namespace smt {
|
|||
assert_default(n, pr);
|
||||
return;
|
||||
}
|
||||
sort * s = m.get_sort(n->get_arg(0));
|
||||
sort * s = n->get_arg(0)->get_sort();
|
||||
sort_ref u(m.mk_fresh_sort("distinct-elems"), m);
|
||||
func_decl_ref f(m.mk_fresh_func_decl("distinct-aux-f", "", 1, &s, u), m);
|
||||
for (expr * arg : *n) {
|
||||
|
@ -448,7 +448,7 @@ namespace smt {
|
|||
d.set_eq_flag();
|
||||
TRACE("internalize", tout << mk_pp(n, m) << " " << literal(v, false) << "\n";);
|
||||
|
||||
sort * s = m.get_sort(n->get_arg(0));
|
||||
sort * s = n->get_arg(0)->get_sort();
|
||||
theory * th = m_theories.get_plugin(s->get_family_id());
|
||||
if (th)
|
||||
th->internalize_eq_eh(n, v);
|
||||
|
@ -582,7 +582,7 @@ namespace smt {
|
|||
if (e_internalized(q)) {
|
||||
return;
|
||||
}
|
||||
app_ref lam_name(m.mk_fresh_const("lambda", m.get_sort(q)), m);
|
||||
app_ref lam_name(m.mk_fresh_const("lambda", q->get_sort()), m);
|
||||
app_ref eq(m), lam_app(m);
|
||||
expr_ref_vector vars(m);
|
||||
vars.push_back(lam_name);
|
||||
|
|
|
@ -654,7 +654,7 @@ namespace smt {
|
|||
Remark: this method uses get_fresh_value, so it may fail.
|
||||
*/
|
||||
expr* get_k_interp(app* k) {
|
||||
sort* s = m.get_sort(k);
|
||||
sort* s = k->get_sort();
|
||||
SASSERT(is_infinite(s));
|
||||
func_decl* k_decl = k->get_decl();
|
||||
expr* r = m_model->get_const_interp(k_decl);
|
||||
|
@ -1914,7 +1914,7 @@ namespace smt {
|
|||
if (is_var_and_ground(to_app(atom)->get_arg(0), to_app(atom)->get_arg(1), v, tmp, inv)) {
|
||||
if (inv)
|
||||
le = !le;
|
||||
sort* s = m.get_sort(tmp);
|
||||
sort* s = tmp->get_sort();
|
||||
expr_ref one(m);
|
||||
one = mk_one(s);
|
||||
if (le)
|
||||
|
|
|
@ -307,7 +307,7 @@ namespace smt {
|
|||
enode * n = curr.get_enode();
|
||||
SASSERT(n->get_root() == n);
|
||||
tout << mk_pp(n->get_owner(), m) << "\n";
|
||||
sort * s = m.get_sort(n->get_owner());
|
||||
sort * s = n->get_owner()->get_sort();
|
||||
tout << curr << " " << mk_pp(s, m);
|
||||
tout << " is_fresh: " << root2proc[n]->is_fresh() << "\n";
|
||||
}
|
||||
|
|
|
@ -186,7 +186,7 @@ namespace smt {
|
|||
m_candidate_vectors[i].reset();
|
||||
sort * s = q->get_decl_sort(i);
|
||||
for (unsigned j = 0; j < num_candidates; j++) {
|
||||
if (m_manager.get_sort(candidates[j]) == s) {
|
||||
if (candidates[j]->get_sort() == s) {
|
||||
expr * n = candidates[j];
|
||||
m_context.internalize(n, false);
|
||||
enode * e = m_context.get_enode(n);
|
||||
|
|
|
@ -72,7 +72,7 @@ namespace smt {
|
|||
", is_store: " << is_store(n) << "\n";);
|
||||
d->m_is_array = is_array_sort(n);
|
||||
if (d->m_is_array)
|
||||
register_sort(m.get_sort(n->get_owner()));
|
||||
register_sort(n->get_owner()->get_sort());
|
||||
d->m_is_select = is_select(n);
|
||||
if (is_store(n))
|
||||
d->m_stores.push_back(n);
|
||||
|
|
|
@ -59,7 +59,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
app * theory_array_base::mk_default(expr * a) {
|
||||
sort * s = m.get_sort(a);
|
||||
sort * s = a->get_sort();
|
||||
unsigned num_params = get_dimension(s);
|
||||
parameter const* params = s->get_info()->get_parameters();
|
||||
return m.mk_app(get_family_id(), OP_ARRAY_DEFAULT, num_params, params, 1, & a);
|
||||
|
@ -564,13 +564,13 @@ namespace smt {
|
|||
TRACE("array_bug", tout << "mk_interface_eqs: processing: v" << *it1 << "\n";);
|
||||
theory_var v1 = *it1;
|
||||
enode * n1 = get_enode(v1);
|
||||
sort * s1 = m.get_sort(n1->get_owner());
|
||||
sort * s1 = n1->get_owner()->get_sort();
|
||||
sbuffer<theory_var>::iterator it2 = it1;
|
||||
++it2;
|
||||
for (; it2 != end1; ++it2) {
|
||||
theory_var v2 = *it2;
|
||||
enode * n2 = get_enode(v2);
|
||||
sort * s2 = m.get_sort(n2->get_owner());
|
||||
sort * s2 = n2->get_owner()->get_sort();
|
||||
if (s1 == s2 && !ctx.is_diseq(n1, n2)) {
|
||||
app * eq = mk_eq_atom(n1->get_owner(), n2->get_owner());
|
||||
if (!ctx.b_internalized(eq) || !ctx.is_relevant(eq)) {
|
||||
|
@ -983,7 +983,7 @@ namespace smt {
|
|||
SASSERT(ctx.is_relevant(n));
|
||||
theory_var v = n->get_th_var(get_id());
|
||||
SASSERT(v != null_theory_var);
|
||||
sort * s = m.get_sort(n->get_owner());
|
||||
sort * s = n->get_owner()->get_sort();
|
||||
enode * else_val_n = get_default(v);
|
||||
array_value_proc * result = nullptr;
|
||||
|
||||
|
|
|
@ -46,7 +46,7 @@ namespace smt {
|
|||
bool is_array_ext(app const * n) const { return n->is_app_of(get_id(), OP_ARRAY_EXT); }
|
||||
bool is_as_array(app const * n) const { return n->is_app_of(get_id(), OP_AS_ARRAY); }
|
||||
bool is_array_sort(sort const* s) const { return s->is_sort_of(get_id(), ARRAY_SORT); }
|
||||
bool is_array_sort(app const* n) const { return is_array_sort(get_manager().get_sort(n)); }
|
||||
bool is_array_sort(app const* n) const { return is_array_sort(n->get_sort()); }
|
||||
bool is_set_has_size(app const* n) const { return n->is_app_of(get_id(), OP_SET_HAS_SIZE); }
|
||||
bool is_set_card(app const* n) const { return n->is_app_of(get_id(), OP_SET_CARD); }
|
||||
|
||||
|
|
|
@ -579,7 +579,7 @@ namespace smt {
|
|||
|
||||
bool theory_array_full::has_unitary_domain(app* array_term) {
|
||||
SASSERT(is_array_sort(array_term));
|
||||
sort* s = m.get_sort(array_term);
|
||||
sort* s = array_term->get_sort();
|
||||
unsigned dim = get_dimension(s);
|
||||
parameter const * params = s->get_info()->get_parameters();
|
||||
for (unsigned i = 0; i < dim; ++i) {
|
||||
|
@ -593,7 +593,7 @@ namespace smt {
|
|||
|
||||
bool theory_array_full::has_large_domain(app* array_term) {
|
||||
SASSERT(is_array_sort(array_term));
|
||||
sort* s = m.get_sort(array_term);
|
||||
sort* s = array_term->get_sort();
|
||||
unsigned dim = get_dimension(s);
|
||||
parameter const * params = s->get_info()->get_parameters();
|
||||
rational sz(1);
|
||||
|
|
|
@ -478,7 +478,7 @@ namespace smt {
|
|||
VERIFY(get_fixed_value(v, val));
|
||||
enode* n = get_enode(v);
|
||||
if (ctx.watches_fixed(n)) {
|
||||
expr_ref num(m_util.mk_numeral(val, m.get_sort(n->get_owner())), m);
|
||||
expr_ref num(m_util.mk_numeral(val, n->get_owner()->get_sort()), m);
|
||||
literal_vector& lits = m_tmp_literals;
|
||||
lits.reset();
|
||||
for (literal b : m_bits[v]) {
|
||||
|
|
|
@ -147,7 +147,7 @@ namespace smt {
|
|||
unsigned get_bv_size(app const * n) const { return m_util.get_bv_size(n); }
|
||||
unsigned get_bv_size(enode const * n) const { return m_util.get_bv_size(n->get_owner()); }
|
||||
unsigned get_bv_size(theory_var v) const { return get_bv_size(get_enode(v)); }
|
||||
bool is_bv(app const* n) const { return m_util.is_bv_sort(get_manager().get_sort(n)); }
|
||||
bool is_bv(app const* n) const { return m_util.is_bv_sort(n->get_sort()); }
|
||||
bool is_bv(enode const* n) const { return is_bv(n->get_owner()); }
|
||||
bool is_bv(theory_var v) const { return is_bv(get_enode(v)); }
|
||||
region & get_region() { return m_trail_stack.get_region(); }
|
||||
|
|
|
@ -274,7 +274,7 @@ namespace smt {
|
|||
assert_update_field_axioms(n);
|
||||
}
|
||||
else {
|
||||
sort * s = m.get_sort(n->get_owner());
|
||||
sort * s = n->get_owner()->get_sort();
|
||||
if (m_util.get_datatype_num_constructors(s) == 1) {
|
||||
func_decl * c = m_util.get_datatype_constructors(s)->get(0);
|
||||
assert_is_constructor_axiom(n, c, null_literal);
|
||||
|
@ -333,7 +333,7 @@ namespace smt {
|
|||
//
|
||||
for (unsigned i = 0; i < num_args; i++) {
|
||||
enode * arg = e->get_arg(i);
|
||||
sort * s = m.get_sort(arg->get_owner());
|
||||
sort * s = arg->get_owner()->get_sort();
|
||||
if (m_autil.is_array(s) && m_util.is_datatype(get_array_range(s))) {
|
||||
app_ref def(m_autil.mk_default(arg->get_owner()), m);
|
||||
if (!ctx.e_internalized(def)) {
|
||||
|
@ -528,7 +528,7 @@ namespace smt {
|
|||
}
|
||||
found = true;
|
||||
}
|
||||
sort * s = m.get_sort(arg->get_owner());
|
||||
sort * s = arg->get_owner()->get_sort();
|
||||
if (m_autil.is_array(s) && m_util.is_datatype(get_array_range(s))) {
|
||||
for (enode* aarg : get_array_args(arg)) {
|
||||
if (aarg->get_root() == child->get_root()) {
|
||||
|
@ -864,7 +864,7 @@ namespace smt {
|
|||
unsigned num_unassigned = 0;
|
||||
unsigned unassigned_idx = UINT_MAX;
|
||||
enode * n = get_enode(v);
|
||||
sort * dt = m.get_sort(n->get_owner());
|
||||
sort * dt = n->get_owner()->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());
|
||||
|
@ -947,7 +947,7 @@ namespace smt {
|
|||
void theory_datatype::mk_split(theory_var v) {
|
||||
v = m_find.find(v);
|
||||
enode * n = get_enode(v);
|
||||
sort * s = m.get_sort(n->get_owner());
|
||||
sort * s = n->get_owner()->get_sort();
|
||||
func_decl * non_rec_c = m_util.get_non_rec_constructor(s);
|
||||
unsigned non_rec_idx = m_util.get_constructor_idx(non_rec_c);
|
||||
var_data * d = m_var_data[v];
|
||||
|
|
|
@ -804,7 +804,7 @@ namespace smt {
|
|||
enode * n = get_enode(v);
|
||||
if (m_autil.is_zero(n->get_owner()) && !m_assignment[v].is_zero()) {
|
||||
numeral val = m_assignment[v];
|
||||
sort * s = m.get_sort(n->get_owner());
|
||||
sort * s = n->get_owner()->get_sort();
|
||||
// adjust the value of all variables that have the same sort.
|
||||
for (int v2 = 0; v2 < num_vars; ++v2) {
|
||||
enode * n2 = get_enode(v2);
|
||||
|
|
|
@ -533,7 +533,7 @@ namespace smt {
|
|||
|
||||
model_value_proc * theory_fpa::mk_value(enode * n, model_generator & mg) {
|
||||
TRACE("t_fpa", tout << "mk_value for: " << mk_ismt2_pp(n->get_owner(), m) <<
|
||||
" (sort " << mk_ismt2_pp(m.get_sort(n->get_owner()), m) << ")\n";);
|
||||
" (sort " << mk_ismt2_pp(n->get_owner()->get_sort(), m) << ")\n";);
|
||||
|
||||
app_ref owner(m);
|
||||
owner = get_ite_value(n->get_owner());
|
||||
|
|
|
@ -319,7 +319,7 @@ namespace smt {
|
|||
theory_var theory_str::mk_var(enode* n) {
|
||||
TRACE("str", tout << "mk_var for " << mk_pp(n->get_owner(), get_manager()) << std::endl;);
|
||||
ast_manager & m = get_manager();
|
||||
if (!(m.get_sort(n->get_owner()) == u.str.mk_string_sort())) {
|
||||
if (!(n->get_owner()->get_sort() == u.str.mk_string_sort())) {
|
||||
return null_theory_var;
|
||||
}
|
||||
if (is_attached_to_var(n)) {
|
||||
|
|
|
@ -328,7 +328,7 @@ namespace smt {
|
|||
|
||||
th_var get_zero(sort* s) { return a.is_int(s) ? m_izero : m_rzero; }
|
||||
|
||||
th_var get_zero(expr* e) { return get_zero(get_manager().get_sort(e)); }
|
||||
th_var get_zero(expr* e) { return get_zero(e->get_sort()); }
|
||||
|
||||
void init_zero();
|
||||
|
||||
|
|
|
@ -35,7 +35,7 @@ class eq2bv_tactic : public tactic {
|
|||
expr* z;
|
||||
rational r;
|
||||
if (t.m_fd.find(x, z) && t.a.is_numeral(y, r)) {
|
||||
result = m.mk_eq(z, t.bv.mk_numeral(r, m.get_sort(z)));
|
||||
result = m.mk_eq(z, t.bv.mk_numeral(r, z->get_sort()));
|
||||
return true;
|
||||
}
|
||||
else {
|
||||
|
@ -249,13 +249,13 @@ public:
|
|||
if (m_bounds.has_lower(c, r, strict) && !r.is_neg()) {
|
||||
SASSERT(!strict);
|
||||
expr* d = m_fd.find(c);
|
||||
fml = bv.mk_ule(bv.mk_numeral(r, m.get_sort(d)), d);
|
||||
fml = bv.mk_ule(bv.mk_numeral(r, d->get_sort()), d);
|
||||
g->assert_expr(fml, m_bounds.lower_dep(c));
|
||||
}
|
||||
if (m_bounds.has_upper(c, r, strict) && !r.is_neg()) {
|
||||
SASSERT(!strict);
|
||||
expr* d = m_fd.find(c);
|
||||
fml = bv.mk_ule(d, bv.mk_numeral(r, m.get_sort(d)));
|
||||
fml = bv.mk_ule(d, bv.mk_numeral(r, d->get_sort()));
|
||||
g->assert_expr(fml, m_bounds.upper_dep(c));
|
||||
}
|
||||
}
|
||||
|
|
|
@ -331,11 +331,12 @@ namespace {
|
|||
} else if (m_bound.find(t1, ctx)) {
|
||||
if (ctx.implies(b)) {
|
||||
result = m.mk_true();
|
||||
} else if (!b.intersect(ctx, intr)) {
|
||||
}
|
||||
else if (!b.intersect(ctx, intr)) {
|
||||
result = m.mk_false();
|
||||
} else if (m_propagate_eq && intr.is_singleton()) {
|
||||
result = m.mk_eq(t1, m_bv.mk_numeral(rational(intr.l, rational::ui64()),
|
||||
m.get_sort(t1)));
|
||||
}
|
||||
else if (m_propagate_eq && intr.is_singleton()) {
|
||||
result = m.mk_eq(t1, m_bv.mk_numeral(rational(intr.l, rational::ui64()), t1->get_sort()));
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -630,7 +631,7 @@ namespace {
|
|||
}
|
||||
else if (m_propagate_eq && intr.is_singleton()) {
|
||||
r = m.mk_eq(t1, m_bv.mk_numeral(rational(intr.l, rational::ui64()),
|
||||
m.get_sort(t1)));
|
||||
t1->get_sort()));
|
||||
}
|
||||
else {
|
||||
was_updated = false;
|
||||
|
|
|
@ -144,7 +144,7 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr
|
|||
func_decl_ref f_t(mk_uf_for_array(args[0]), m_manager);
|
||||
func_decl_ref f_s(mk_uf_for_array(args[1]), m_manager);
|
||||
|
||||
sort * sorts[1] = { get_index_sort(m_manager.get_sort(args[0])) };
|
||||
sort * sorts[1] = { get_index_sort(args[0]->get_sort()) };
|
||||
symbol names[1] = { symbol("x") };
|
||||
var_ref x(m_manager.mk_var(0, sorts[0]), m_manager);
|
||||
|
||||
|
@ -167,7 +167,7 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr
|
|||
TRACE("bvarray2uf_rw", tout << "(ite " << c << ", " << f_t->get_name()
|
||||
<< ", " << f_f->get_name() << ")" << std::endl;);
|
||||
|
||||
sort * sorts[1] = { get_index_sort(m_manager.get_sort(args[1])) };
|
||||
sort * sorts[1] = { get_index_sort(args[1]->get_sort()) };
|
||||
symbol names[1] = { symbol("x") };
|
||||
var_ref x(m_manager.mk_var(0, sorts[0]), m_manager);
|
||||
|
||||
|
|
|
@ -258,7 +258,7 @@ private:
|
|||
m_manager(m), m_app2sortid(app2sort), m_max_id(0) {}
|
||||
|
||||
void operator()(app* n) {
|
||||
sort* s = m_manager.get_sort(n);
|
||||
sort* s = n->get_sort();
|
||||
unsigned id;
|
||||
if (!m_sort2id.find(s, id)) {
|
||||
id = m_max_id++;
|
||||
|
|
|
@ -178,7 +178,7 @@ namespace smtfd {
|
|||
return m.mk_fresh_const(name, m.mk_bool_sort());
|
||||
}
|
||||
else if (m_butil.is_bv(t)) {
|
||||
return m.mk_fresh_const(name, m.get_sort(t));
|
||||
return m.mk_fresh_const(name, t->get_sort());
|
||||
}
|
||||
else {
|
||||
++m_nv;
|
||||
|
@ -690,7 +690,7 @@ namespace smtfd {
|
|||
for (unsigned i = 0; i < a.m_t->get_num_args(); ++i) {
|
||||
if (p.values().get(a.m_val_offset+i) != p.values().get(b.m_val_offset+i))
|
||||
return false;
|
||||
if (p.get_manager().get_sort(a.m_t->get_arg(i)) != p.get_manager().get_sort(b.m_t->get_arg(i)))
|
||||
if (a.m_t->get_arg(i)->get_sort() != b.m_t->get_arg(i)->get_sort())
|
||||
return false;
|
||||
}
|
||||
return true;
|
||||
|
@ -793,7 +793,7 @@ namespace smtfd {
|
|||
{}
|
||||
|
||||
void check_term(expr* t, unsigned round) override {
|
||||
sort* s = m.get_sort(t);
|
||||
sort* s = t->get_sort();
|
||||
if (round == 0 && is_uf(t)) {
|
||||
TRACE("smtfd_verbose", tout << "check-term: " << mk_bounded_pp(t, m, 2) << "\n";);
|
||||
enforce_congruence(to_app(t)->get_decl(), to_app(t), s);
|
||||
|
@ -816,7 +816,7 @@ namespace smtfd {
|
|||
}
|
||||
|
||||
bool term_covered(expr* t) override {
|
||||
sort* s = m.get_sort(t);
|
||||
sort* s = t->get_sort();
|
||||
if (sort_covered(s)) {
|
||||
val2elem_t& v2e = get_table(s);
|
||||
expr_ref v = eval_abs(t);
|
||||
|
@ -864,7 +864,7 @@ namespace smtfd {
|
|||
mdl->register_decl(fn, fi);
|
||||
}
|
||||
for (expr* t : subterms(terms)) {
|
||||
if (is_uninterp_const(t) && sort_covered(m.get_sort(t))) {
|
||||
if (is_uninterp_const(t) && sort_covered(t->get_sort())) {
|
||||
expr_ref val = model_value(t);
|
||||
mdl->register_decl(to_app(t)->get_decl(), val);
|
||||
}
|
||||
|
@ -872,7 +872,7 @@ namespace smtfd {
|
|||
}
|
||||
|
||||
expr_ref model_value_core(expr* t) override {
|
||||
sort* s = m.get_sort(t);
|
||||
sort* s = t->get_sort();
|
||||
if (sort_covered(s)) {
|
||||
auto& v2e = ensure_table(s);
|
||||
return expr_ref(v2e[eval_abs(t)], m);
|
||||
|
@ -922,14 +922,14 @@ namespace smtfd {
|
|||
void insert_select(app* t) {
|
||||
expr* a = t->get_arg(0);
|
||||
expr_ref vA = eval_abs(a);
|
||||
check_congruence(vA, t, m.get_sort(a));
|
||||
check_congruence(vA, t, a->get_sort());
|
||||
}
|
||||
|
||||
void check_select(app* t) {
|
||||
expr* a = t->get_arg(0);
|
||||
expr_ref vA = eval_abs(a);
|
||||
TRACE("smtfd", tout << mk_bounded_pp(t, m, 2) << "\n";);
|
||||
enforce_congruence(vA, t, m.get_sort(a));
|
||||
enforce_congruence(vA, t, a->get_sort());
|
||||
}
|
||||
|
||||
// check that (select(t, t.args) = t.value)
|
||||
|
@ -1018,7 +1018,7 @@ namespace smtfd {
|
|||
expr_ref vT = eval_abs(t);
|
||||
expr_ref vA = eval_abs(arg);
|
||||
|
||||
table& tT = ast2table(vT, m.get_sort(t)); // select table of t
|
||||
table& tT = ast2table(vT, t->get_sort()); // select table of t
|
||||
table& tA = ast2table(vA, arg->get_sort()); // select table of arg
|
||||
|
||||
if (vT == vA) {
|
||||
|
@ -1049,7 +1049,7 @@ namespace smtfd {
|
|||
if (m_context.at_max()) {
|
||||
break;
|
||||
}
|
||||
if (m.get_sort(t) != m.get_sort(fA.m_t->get_arg(0))) {
|
||||
if (t->get_sort() != fA.m_t->get_arg(0)->get_sort()) {
|
||||
continue;
|
||||
}
|
||||
if (!tT.find(fA, fT) || (value_of(fA) != value_of(fT) && !eq(m_vargs, fA))) {
|
||||
|
@ -1064,7 +1064,7 @@ namespace smtfd {
|
|||
if (m_context.at_max()) {
|
||||
break;
|
||||
}
|
||||
if (!tA.find(fT, fA) && m.get_sort(t) == m.get_sort(fT.m_t->get_arg(0))) {
|
||||
if (!tA.find(fT, fA) && t->get_sort() == m.get_sort(fT.m_t->get_arg(0))) {
|
||||
TRACE("smtfd", tout << "not found\n";);
|
||||
add_select_store_axiom(t, fT);
|
||||
++r;
|
||||
|
@ -1080,7 +1080,7 @@ namespace smtfd {
|
|||
for (expr* arg : *f.m_t) {
|
||||
m_args.push_back(arg);
|
||||
}
|
||||
SASSERT(m.get_sort(t) == m.get_sort(a));
|
||||
SASSERT(t->get_sort() == a->get_sort());
|
||||
TRACE("smtfd", tout << mk_bounded_pp(t, m, 2) << " " << mk_bounded_pp(f.m_t, m, 2) << "\n";);
|
||||
expr_ref eq = mk_eq_idxs(t, f.m_t);
|
||||
m_args[0] = t;
|
||||
|
@ -1094,7 +1094,7 @@ namespace smtfd {
|
|||
}
|
||||
|
||||
bool same_array_sort(f_app const& fA, f_app const& fT) const {
|
||||
return m.get_sort(fA.m_t->get_arg(0)) == m.get_sort(fT.m_t->get_arg(0));
|
||||
return fA.m_t->get_arg(0)->get_sort() == fT.m_t->get_arg(0)->get_sort();
|
||||
}
|
||||
|
||||
/**
|
||||
|
@ -1105,9 +1105,9 @@ namespace smtfd {
|
|||
m_autil.is_const(t) ||
|
||||
is_lambda(t)) {
|
||||
expr_ref vT = eval_abs(t);
|
||||
table& tT = ast2table(vT, m.get_sort(t));
|
||||
table& tT = ast2table(vT, t->get_sort());
|
||||
for (f_app & f : tT) {
|
||||
if (m.get_sort(t) != m.get_sort(f.m_t->get_arg(0)))
|
||||
if (t->get_sort() != f.m_t->get_arg(0)->get_sort())
|
||||
continue;
|
||||
if (m_context.at_max())
|
||||
break;
|
||||
|
@ -1165,7 +1165,7 @@ namespace smtfd {
|
|||
}
|
||||
|
||||
void enforce_extensionality(expr* a, expr* b) {
|
||||
sort* s = m.get_sort(a);
|
||||
sort* s = a->get_sort();
|
||||
unsigned arity = get_array_arity(s);
|
||||
expr_ref_vector args(m);
|
||||
args.push_back(a);
|
||||
|
@ -1190,7 +1190,7 @@ namespace smtfd {
|
|||
SASSERT(m_autil.is_select(f.m_t));
|
||||
expr_ref v = model_value(f.m_t);
|
||||
if (!value) {
|
||||
sort* s = m.get_sort(f.m_t->get_arg(0));
|
||||
sort* s = f.m_t->get_arg(0)->get_sort();
|
||||
default_value = v;
|
||||
value = m_autil.mk_const_array(s, default_value);
|
||||
}
|
||||
|
@ -1256,7 +1256,7 @@ namespace smtfd {
|
|||
if (m_autil.is_select(t)) {
|
||||
expr* a = to_app(t)->get_arg(0);
|
||||
expr_ref vA = eval_abs(a);
|
||||
insert(mk_app(vA, to_app(t), m.get_sort(a)));
|
||||
insert(mk_app(vA, to_app(t), a->get_sort()));
|
||||
|
||||
}
|
||||
return
|
||||
|
@ -1285,9 +1285,9 @@ namespace smtfd {
|
|||
expr_ref model_value_core(expr* t) override {
|
||||
if (m_autil.is_array(t)) {
|
||||
expr_ref vT = eval_abs(t);
|
||||
table& tb = ast2table(vT, m.get_sort(t));
|
||||
table& tb = ast2table(vT, t->get_sort());
|
||||
if (tb.empty()) {
|
||||
return model_value_core(m.get_sort(t));
|
||||
return model_value_core(t->get_sort());
|
||||
}
|
||||
else {
|
||||
return mk_array_value(tb);
|
||||
|
@ -1345,7 +1345,7 @@ namespace smtfd {
|
|||
for (unsigned j = i + 1; !m_context.at_max() && j < shared.size(); ++j) {
|
||||
expr* s2 = shared.get(j);
|
||||
expr* v2 = sharedvals.get(j);
|
||||
if (v1 != v2 && m.get_sort(s1) == m.get_sort(s2) && same_table(v1, m.get_sort(s1), v2, m.get_sort(s2))) {
|
||||
if (v1 != v2 && s1->get_sort() == s2->get_sort() && same_table(v1, s1->get_sort(), v2, s2->get_sort())) {
|
||||
enforce_extensionality(s1, s2);
|
||||
}
|
||||
}
|
||||
|
@ -1533,8 +1533,8 @@ namespace smtfd {
|
|||
void init_term(expr* t) {
|
||||
if (!m.is_bool(t) && is_ground(t)) {
|
||||
expr_ref v = eval_abs(t);
|
||||
if (!m_val2term.contains(v, m.get_sort(t))) {
|
||||
m_val2term.insert(v, m.get_sort(t), t);
|
||||
if (!m_val2term.contains(v, t->get_sort())) {
|
||||
m_val2term.insert(v, t->get_sort(), t);
|
||||
m_val2term_trail.push_back(v);
|
||||
}
|
||||
}
|
||||
|
@ -1725,7 +1725,7 @@ namespace smtfd {
|
|||
}
|
||||
}
|
||||
for (expr* t : subterms(terms)) {
|
||||
if (!is_forall(t) && !is_exists(t) && (!m_context.term_covered(t) || !m_context.sort_covered(m.get_sort(t)))) {
|
||||
if (!is_forall(t) && !is_exists(t) && (!m_context.term_covered(t) || !m_context.sort_covered(t->get_sort()))) {
|
||||
is_decided = l_false;
|
||||
}
|
||||
}
|
||||
|
@ -1739,9 +1739,9 @@ namespace smtfd {
|
|||
if (is_ground(a) && val0 != val1 && m.get_sort(val0) == m.get_sort(val1)) {
|
||||
tout << mk_bounded_pp(a, m, 2) << " := " << val0 << " " << val1 << "\n";
|
||||
}
|
||||
if (!is_forall(a) && !is_exists(a) && (!m_context.term_covered(a) || !m_context.sort_covered(m.get_sort(a)))) {
|
||||
tout << "not covered: " << mk_pp(a, m) << " " << mk_pp(m.get_sort(a), m) << " ";
|
||||
tout << m_context.term_covered(a) << " " << m_context.sort_covered(m.get_sort(a)) << "\n";
|
||||
if (!is_forall(a) && !is_exists(a) && (!m_context.term_covered(a) || !m_context.sort_covered(a->get_sort()))) {
|
||||
tout << "not covered: " << mk_pp(a, m) << " " << mk_pp(a->get_sort(), m) << " ";
|
||||
tout << m_context.term_covered(a) << " " << m_context.sort_covered(a->get_sort()) << "\n";
|
||||
}
|
||||
}
|
||||
tout << "has quantifier: " << has_q << "\n" << core << "\n";
|
||||
|
|
Loading…
Reference in a new issue