mirror of
https://github.com/Z3Prover/z3
synced 2026-07-14 19:15:41 +00:00
Fix model-finder segfault on invalid AUF variable indices
This commit is contained in:
copilot-swe-agent[bot]
GitHub
parent
06c1d9a224
commit
917abe5f7a
1 changed files with 64 additions and 22 deletions
|
|
@ -1179,6 +1179,14 @@ namespace smt {
|
|||
virtual void populate_inst_sets(quantifier* q, func_decl* mhead, ptr_vector<instantiation_set>& uvar_inst_sets, context* ctx) {}
|
||||
};
|
||||
|
||||
static bool has_uvar(quantifier* q, unsigned i) {
|
||||
return i < q->get_num_decls();
|
||||
}
|
||||
|
||||
static node* get_uvar_if_valid(quantifier* q, unsigned i, auf_solver& s) {
|
||||
return has_uvar(q, i) ? s.get_uvar(q, i) : nullptr;
|
||||
}
|
||||
|
||||
class f_var : public qinfo {
|
||||
protected:
|
||||
func_decl* m_f;
|
||||
|
|
@ -1204,7 +1212,9 @@ namespace smt {
|
|||
|
||||
void process_auf(quantifier* q, auf_solver& s, context* ctx) override {
|
||||
node* n1 = s.get_A_f_i(m_f, m_arg_i);
|
||||
node* n2 = s.get_uvar(q, m_var_j);
|
||||
node* n2 = get_uvar_if_valid(q, m_var_j, s);
|
||||
if (!n2)
|
||||
return;
|
||||
CTRACE(model_finder, n1->get_sort() != n2->get_sort(),
|
||||
tout << "sort bug:\n" << mk_ismt2_pp(q->get_expr(), m) << "\n" << mk_ismt2_pp(q, m) << "\n";
|
||||
tout << "decl(0): " << q->get_decl_name(0) << "\n";
|
||||
|
|
@ -1286,17 +1296,22 @@ namespace smt {
|
|||
void process_auf(quantifier* q, auf_solver& s, context* ctx) override {
|
||||
// just create the nodes
|
||||
/* node * A_f_i = */ s.get_A_f_i(m_f, m_arg_i);
|
||||
/* node * S_j = */ s.get_uvar(q, m_var_j);
|
||||
/* node * S_j = */ get_uvar_if_valid(q, m_var_j, s);
|
||||
}
|
||||
|
||||
void populate_inst_sets(quantifier* q, auf_solver& s, context* ctx) override {
|
||||
// S_j is not necessary equal to A_f_i.
|
||||
node* A_f_i = s.get_A_f_i(m_f, m_arg_i)->get_root();
|
||||
node* S_j = s.get_uvar(q, m_var_j)->get_root();
|
||||
node* S_j = get_uvar_if_valid(q, m_var_j, s);
|
||||
if (!S_j)
|
||||
return;
|
||||
S_j = S_j->get_root();
|
||||
if (A_f_i == S_j) {
|
||||
// there is no finite fixpoint... we just copy the i-th arguments of A_f_i - m_offset
|
||||
// hope for the best...
|
||||
node* S_j = s.get_uvar(q, m_var_j);
|
||||
node* S_j = get_uvar_if_valid(q, m_var_j, s);
|
||||
if (!S_j)
|
||||
return;
|
||||
for (enode* n : ctx->enodes_of(m_f)) {
|
||||
if (ctx->is_relevant(n)) {
|
||||
arith_rewriter arith_rw(m);
|
||||
|
|
@ -1360,7 +1375,10 @@ namespace smt {
|
|||
|
||||
void populate_inst_sets2(quantifier* q, auf_solver& s, context* ctx) override {
|
||||
node* A_f_i = s.get_A_f_i(m_f, m_arg_i)->get_root();
|
||||
node* S_j = s.get_uvar(q, m_var_j)->get_root();
|
||||
node* S_j = get_uvar_if_valid(q, m_var_j, s);
|
||||
if (!S_j)
|
||||
return;
|
||||
S_j = S_j->get_root();
|
||||
// If A_f_i == S_j, then there is no finite fixpoint, so we do nothing here.
|
||||
if (A_f_i != S_j) {
|
||||
// enforce
|
||||
|
|
@ -1399,11 +1417,13 @@ namespace smt {
|
|||
}
|
||||
|
||||
void process_auf(quantifier *q, auf_solver &s, context *ctx) override {
|
||||
/* node * S_i = */ s.get_uvar(q, m_var_i);
|
||||
/* node * S_i = */ get_uvar_if_valid(q, m_var_i, s);
|
||||
}
|
||||
|
||||
void populate_inst_sets(quantifier *q, auf_solver &s, context *ctx) override {
|
||||
node *S = s.get_uvar(q, m_var_i);
|
||||
node* S = get_uvar_if_valid(q, m_var_i, s);
|
||||
if (!S)
|
||||
return;
|
||||
sort *srt = S->get_sort();
|
||||
|
||||
IF_VERBOSE(3, verbose_stream() << "ho_var::populate_inst_sets: " << q->get_id() << " " << mk_pp(srt, m) << "\n";);
|
||||
|
|
@ -1530,7 +1550,9 @@ namespace smt {
|
|||
for (enode* n : arrays) {
|
||||
tout << "#" << n->get_expr_id() << "\n" << mk_pp(n->get_expr(), m) << "\n";
|
||||
});
|
||||
node* n1 = s.get_uvar(q, m_var_j);
|
||||
node* n1 = get_uvar_if_valid(q, m_var_j, s);
|
||||
if (!n1)
|
||||
return;
|
||||
for (enode* n : arrays) {
|
||||
auto ground_array = n->get_expr();
|
||||
func_decl* f = get_array_func_decl(ground_array, s);
|
||||
|
|
@ -1597,8 +1619,10 @@ namespace smt {
|
|||
char const* get_kind() const override { return "x_eq_y"; }
|
||||
|
||||
void process_auf(quantifier* q, auf_solver& s, context* ctx) override {
|
||||
node* n1 = s.get_uvar(q, m_var_i);
|
||||
node* n2 = s.get_uvar(q, m_var_j);
|
||||
node* n1 = get_uvar_if_valid(q, m_var_i, s);
|
||||
node* n2 = get_uvar_if_valid(q, m_var_j, s);
|
||||
if (!n1 || !n2)
|
||||
return;
|
||||
n1->insert_avoid(n2);
|
||||
if (n1 != n2)
|
||||
n2->insert_avoid(n1);
|
||||
|
|
@ -1611,8 +1635,10 @@ namespace smt {
|
|||
char const* get_kind() const override { return "x_neq_y"; }
|
||||
|
||||
void process_auf(quantifier* q, auf_solver& s, context* ctx) override {
|
||||
node* n1 = s.get_uvar(q, m_var_i);
|
||||
node* n2 = s.get_uvar(q, m_var_j);
|
||||
node* n1 = get_uvar_if_valid(q, m_var_i, s);
|
||||
node* n2 = get_uvar_if_valid(q, m_var_j, s);
|
||||
if (!n1 || !n2)
|
||||
return;
|
||||
n1->merge(n2);
|
||||
}
|
||||
};
|
||||
|
|
@ -1623,8 +1649,10 @@ namespace smt {
|
|||
char const* get_kind() const override { return "x_leq_y"; }
|
||||
|
||||
void process_auf(quantifier* q, auf_solver& s, context* ctx) override {
|
||||
node* n1 = s.get_uvar(q, m_var_i);
|
||||
node* n2 = s.get_uvar(q, m_var_j);
|
||||
node* n1 = get_uvar_if_valid(q, m_var_i, s);
|
||||
node* n2 = get_uvar_if_valid(q, m_var_j, s);
|
||||
if (!n1 || !n2)
|
||||
return;
|
||||
n1->merge(n2);
|
||||
n1->set_mono_proj();
|
||||
}
|
||||
|
|
@ -1637,8 +1665,10 @@ namespace smt {
|
|||
char const* get_kind() const override { return "x_sleq_y"; }
|
||||
|
||||
void process_auf(quantifier* q, auf_solver& s, context* ctx) override {
|
||||
node* n1 = s.get_uvar(q, m_var_i);
|
||||
node* n2 = s.get_uvar(q, m_var_j);
|
||||
node* n1 = get_uvar_if_valid(q, m_var_i, s);
|
||||
node* n2 = get_uvar_if_valid(q, m_var_j, s);
|
||||
if (!n1 || !n2)
|
||||
return;
|
||||
n1->merge(n2);
|
||||
n1->set_mono_proj();
|
||||
n1->set_signed_proj();
|
||||
|
|
@ -1673,17 +1703,23 @@ namespace smt {
|
|||
char const* get_kind() const override { return "x_eq_t"; }
|
||||
|
||||
void process_auf(quantifier* q, auf_solver& s, context* ctx) override {
|
||||
node* n1 = s.get_uvar(q, m_var_i);
|
||||
node* n1 = get_uvar_if_valid(q, m_var_i, s);
|
||||
if (!n1)
|
||||
return;
|
||||
n1->insert_exception(m_t);
|
||||
}
|
||||
|
||||
void populate_inst_sets(quantifier* q, auf_solver& slv, context* ctx) override {
|
||||
if (!has_uvar(q, m_var_i))
|
||||
return;
|
||||
unsigned num_vars = q->get_num_decls();
|
||||
sort* s = q->get_decl_sort(num_vars - m_var_i - 1);
|
||||
if (m.is_uninterp(s)) {
|
||||
// For uninterpreted sorts, we add all terms in the context.
|
||||
// See Section 4.1 in the paper "Complete Quantifier Instantiation"
|
||||
node* S_q_i = slv.get_uvar(q, m_var_i);
|
||||
node* S_q_i = get_uvar_if_valid(q, m_var_i, slv);
|
||||
if (!S_q_i)
|
||||
return;
|
||||
for (enode* n : ctx->enodes()) {
|
||||
if (ctx->is_relevant(n) && n->get_expr()->get_sort() == s) {
|
||||
S_q_i->insert(n->get_expr(), n->get_generation());
|
||||
|
|
@ -1701,11 +1737,13 @@ namespace smt {
|
|||
|
||||
void process_auf(quantifier* q, auf_solver& s, context* ctx) override {
|
||||
// make sure that S_q_i is create.
|
||||
s.get_uvar(q, m_var_i);
|
||||
get_uvar_if_valid(q, m_var_i, s);
|
||||
}
|
||||
|
||||
void populate_inst_sets(quantifier* q, auf_solver& s, context* ctx) override {
|
||||
node* S_q_i = s.get_uvar(q, m_var_i);
|
||||
node* S_q_i = get_uvar_if_valid(q, m_var_i, s);
|
||||
if (!S_q_i)
|
||||
return;
|
||||
S_q_i->insert(m_t, 0);
|
||||
}
|
||||
};
|
||||
|
|
@ -1718,12 +1756,16 @@ namespace smt {
|
|||
|
||||
void process_auf(quantifier* q, auf_solver& s, context* ctx) override {
|
||||
// make sure that S_q_i is create.
|
||||
node* n1 = s.get_uvar(q, m_var_i);
|
||||
node* n1 = get_uvar_if_valid(q, m_var_i, s);
|
||||
if (!n1)
|
||||
return;
|
||||
n1->set_mono_proj();
|
||||
}
|
||||
|
||||
void populate_inst_sets(quantifier* q, auf_solver& s, context* ctx) override {
|
||||
node* S_q_i = s.get_uvar(q, m_var_i);
|
||||
node* S_q_i = get_uvar_if_valid(q, m_var_i, s);
|
||||
if (!S_q_i)
|
||||
return;
|
||||
S_q_i->insert(m_t, 0);
|
||||
}
|
||||
};
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue