mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
widen scope of der #5480
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
2704fb5fd5
commit
b7d4501bc3
|
@ -136,8 +136,12 @@ void der::reduce1(quantifier * q, expr_ref & r, proof_ref & pr) {
|
|||
var * v = nullptr;
|
||||
expr_ref t(m);
|
||||
|
||||
if (m.is_or(e)) {
|
||||
unsigned num_args = to_app(e)->get_num_args();
|
||||
if (is_var_diseq(e, num_decls, v, t) && !occurs(v, t))
|
||||
r = m.mk_false();
|
||||
else {
|
||||
expr_ref_vector ors(m);
|
||||
flatten_or(e, ors);
|
||||
unsigned num_args = ors.size();
|
||||
unsigned diseq_count = 0;
|
||||
unsigned largest_vinx = 0;
|
||||
|
||||
|
@ -149,7 +153,7 @@ void der::reduce1(quantifier * q, expr_ref & r, proof_ref & pr) {
|
|||
|
||||
// Find all disequalities
|
||||
for (unsigned i = 0; i < num_args; i++) {
|
||||
if (is_var_diseq(to_app(e)->get_arg(i), num_decls, v, t)) {
|
||||
if (is_var_diseq(ors.get(i), num_decls, v, t)) {
|
||||
unsigned idx = v->get_idx();
|
||||
if (m_map.get(idx, nullptr) == nullptr) {
|
||||
m_map.reserve(idx + 1);
|
||||
|
@ -170,7 +174,7 @@ void der::reduce1(quantifier * q, expr_ref & r, proof_ref & pr) {
|
|||
|
||||
if (!m_order.empty()) {
|
||||
create_substitution(largest_vinx + 1);
|
||||
apply_substitution(q, r);
|
||||
apply_substitution(q, ors, r);
|
||||
}
|
||||
}
|
||||
else {
|
||||
|
@ -180,11 +184,6 @@ void der::reduce1(quantifier * q, expr_ref & r, proof_ref & pr) {
|
|||
}
|
||||
// Remark: get_elimination_order/top-sort checks for cycles, but it is not invoked for unit clauses.
|
||||
// So, we must perform a occurs check here.
|
||||
else if (is_var_diseq(e, num_decls, v, t) && !occurs(v, t)) {
|
||||
r = m.mk_false();
|
||||
}
|
||||
else
|
||||
r = q;
|
||||
|
||||
if (m.proofs_enabled()) {
|
||||
pr = r == q ? nullptr : m.mk_der(q, r);
|
||||
|
@ -327,9 +326,8 @@ void der::create_substitution(unsigned sz) {
|
|||
}
|
||||
}
|
||||
|
||||
void der::apply_substitution(quantifier * q, expr_ref & r) {
|
||||
expr * e = q->get_expr();
|
||||
unsigned num_args=to_app(e)->get_num_args();
|
||||
void der::apply_substitution(quantifier * q, expr_ref_vector& ors, expr_ref & r) {
|
||||
unsigned num_args = ors.size();
|
||||
|
||||
// get a new expression
|
||||
m_new_args.reset();
|
||||
|
@ -338,13 +336,11 @@ void der::apply_substitution(quantifier * q, expr_ref & r) {
|
|||
if (x != -1 && m_map.get(x) != nullptr)
|
||||
continue; // this is a disequality with definition (vanishes)
|
||||
|
||||
m_new_args.push_back(to_app(e)->get_arg(i));
|
||||
m_new_args.push_back(ors.get(i));
|
||||
}
|
||||
|
||||
unsigned sz = m_new_args.size();
|
||||
expr_ref t(m);
|
||||
t = (sz == 1) ? m_new_args[0] : m.mk_or(sz, m_new_args.data());
|
||||
expr_ref new_e = m_subst(t, m_subst_map.size(), m_subst_map.data());
|
||||
expr_ref t = mk_or(m, m_new_args.size(), m_new_args.data());
|
||||
expr_ref new_e = m_subst(t, m_subst_map);
|
||||
|
||||
// don't forget to update the quantifier patterns
|
||||
expr_ref_buffer new_patterns(m);
|
||||
|
|
|
@ -147,7 +147,7 @@ class der {
|
|||
|
||||
void get_elimination_order();
|
||||
void create_substitution(unsigned sz);
|
||||
void apply_substitution(quantifier * q, expr_ref & r);
|
||||
void apply_substitution(quantifier * q, expr_ref_vector& ors, expr_ref & r);
|
||||
|
||||
void reduce1(quantifier * q, expr_ref & r, proof_ref & pr);
|
||||
|
||||
|
|
Loading…
Reference in a new issue