Question about mechanism of blocking current assignments in theory_seq.cpp (final_check_eh())

[alan23273850]

Hello! I have a question about the mechanism of blocking current assignments in theory_seq.cpp.

In final_check_eh(), we need to prevent the solver from guessing the same assignment again and again. There seems to be two ways to achieve this goal.

Method 1: alan23273850@9ad4c0e
Use the only line add_axiom(mk_literal(m.mk_false())); in each iteration.

final_check_status theory_seq::final_check_eh() {
    print_formulas("Entering final check:");
    add_axiom(mk_literal(m.mk_false()));
    return FC_CONTINUE;
}

Method 2: alan23273850@2df65fd
Add the negation of conjunction of currently asserted formulas in each iteration.

final_check_status theory_seq::final_check_eh() {
    print_formulas("Entering final check:");
    DEBUG("block",__LINE__ << "[Refinement]\nformulas:\n";)
    literal_vector lits;
    for (const auto& eq : m_rep) {
        if (eq.v && eq.v->get_sort()==m_util.mk_string_sort() &&
            eq.e && eq.e->get_sort()==m_util.mk_string_sort()) {
            expr *const e = m.mk_eq(eq.v, eq.e);
            literal l = mk_literal(m.mk_not(e));
            lits.push_back(l);
            DEBUG("block", "[m_rep] "<<l<<"("<<mk_pp(m.mk_not(e),m)<<") \n";);
        }
    }
    for (const auto& we : m_eqs) {
        expr *const e = m.mk_eq(mk_concat(we.ls), mk_concat(we.rs));
        literal l = mk_literal(m.mk_not(e));
        lits.push_back(l);
        DEBUG("block", "[m_eqs] "<<l<<"("<<mk_pp(m.mk_not(e),m)<<") \n";);
    }
    for (const auto& wi : m_nqs) {
        expr *const e = m.mk_not(m.mk_eq(wi.l(), wi.r()));
        literal l = mk_literal(m.mk_not(e));
        lits.push_back(l);
        DEBUG("block", "[m_nqs] "<<l<<"("<<mk_pp(m.mk_not(e),m)<<") \n";);
    }
    for (const auto& nc : m_ncs) {
        expr *const e = m.mk_not(nc.contains());
        literal l = mk_literal(m.mk_not(e));
        lits.push_back(l);
        DEBUG("block", "[m_ncs] "<<l<<"("<<mk_pp(m.mk_not(e),m)<<") \n";);
    }
    DEBUG("block", "block ";);
    for(auto& lit:lits){
        DEBUG("block", " "<<lit<<"("<<lit<<")";);
    }
    DEBUG("block", "\n";);

    if (!lits.empty()) {
        add_axiom(lits);
    }
    DEBUG("block",__LINE__ << " leave " << __FUNCTION__ << std::endl;)
    return FC_CONTINUE;
}

However, the results obtained from these two ways are different. We used the following file as our example.

(declare-const x String)
(declare-const y String)

(assert (or (and (= (str.++ x "a" y) "abcd") (= (str.len x) (str.len y)))
            (= x y)))

(check-sat)

Method 1 produces the following result.

alan23273850@server:~/z3/experiment$ z3 benchmark_handmade/len_or_eq_sat.smt2 -dbg:input
Entering final check: 
Word Equations:
x.(seq.unit (_ Char 97)).y = (seq.unit (_ Char 97)).(seq.unit (_ Char 98)).(seq.unit (_ Char 99)).(seq.unit (_ Char 100))

unsat

Method 2 produces the following result.

alan23273850@server:~/z3/experiment$ z3 benchmark_handmade/len_or_eq_sat.smt2 -dbg:input 
Entering final check: 
Word Equations:
x.(seq.unit (_ Char 97)).y = (seq.unit (_ Char 97)).(seq.unit (_ Char 98)).(seq.unit (_ Char 99)).(seq.unit (_ Char 100))

Entering final check: 
Word Equations:
x = y
y = x
Word Disequalities:
x.(seq.unit (_ Char 97)).y != (seq.unit (_ Char 97)).(seq.unit (_ Char 98)).(seq.unit (_ Char 99)).(seq.unit (_ Char 100))

unsat

It is apparent that Method 1 ignores the possibility of guessing the branch x = y whereas Method 2 does not. Is there anything we've missed before to understand why the behaviors of these two methods are different?

[NikolajBjorner]

Keep in mind that whatever is asserted by add_axiom is global. It is not scope dependent. The assertion should be valid regardless of scope. So if you add_axiom(false), then you are basically saying false was implied at base level of search.

There are other weird things with your code. It uses m.mk_not(...) all over the place. YOu will likely run into reference counting bugs. You can negate literals using ~. So use

literal l = ~mk_literal(e);
instead of
literal l = mk_literal(m.mk_not(e));

[alan23273850]

Thank you for your advice! Besides, I have one more question about the negation of literals. In my knowledge, the only way to avoid reference counting bugs is to wrap a bare expression with the constructor expr_ref(..., m). However the following code shows that mk_literal already contains such constructor on the 1st line, so I can't understand why mk_literal(m.mk_not(...)) may cause reference counting bugs?

literal theory::mk_literal(expr* _e) {
    expr_ref e(_e, m);
    bool is_not = m.is_not(_e, _e);
    if (!ctx.e_internalized(_e)) {
        ctx.internalize(_e, is_quantifier(_e));
    }
    literal lit = ctx.get_literal(_e);
    ctx.mark_as_relevant(lit);
    if (is_not) lit.neg();
    return lit;
}