Issue with tactic

[merlinsun]

Hi,
For this following instance, z3 19e9212 incorrectly gives sat with (check-sat-using (then qe2 smt)).

$ cat z3 small.smt2 
sat
unsat
$ cat small.smt2 
(declare-fun a () (_ BitVec 16))
(assert (forall ((v (_ BitVec 8))) (bvule (bvadd a (_ bv533797 16) ((_ zero_extend 8) v)) (_ bv6 16))))
(check-sat-using (then qe2 smt))
(check-sat)

[NikolajBjorner]

@hgvk94 - qel appears not to project the bit-vector v properly.

Try: z3 6934.smt2 /v:10 /tr:qe /tr:mbp smt.qsat_use_qel=false
vs default option.

[hgvk94]

I traced the problem down to this piece of code. This is intended to mark occurrences of variables in a formula and remove all variables that are not in the formula. For some reason, the expr_sparse_marker marks the variable as being in the formula but then lies in the subsequent query to is_marked. Working on debugging this ...

[NikolajBjorner]

It is not there.
The code

    void operator()(app_ref_vector &vars, expr_ref &fml, model &mdl) {
        if (vars.empty())
            return;

        init(vars, fml, mdl);
        // Apply MBP rules till saturation

        // First, apply rules without splitting on model
        saturate(vars);

        enable_model_splitting();

        // Do complete mbp
        saturate(vars);

        TRACE("mbp_tg",
              tout << "mbp tg " << m_tg.get_lits() << " and vars " << vars;);
        TRACE("mbp_tg_verbose", obj_hashtable<app> vars_tmp;
              collect_uninterp_consts(mk_and(m_tg.get_lits()), vars_tmp);
              for (auto a
                   : vars_tmp) tout
              << mk_pp(a->get_decl(), m) << "\n";
              for (auto b
                   : m_tg.get_lits()) tout
              << expr_ref(b, m) << "\n";
              for (auto a
                   : vars) tout
              << expr_ref(a, m) << " ";);

        // 1. Apply qe_lite to remove all c-ground variables
        // 2. Collect all core variables in the output (variables used as array
        // indices/values)
        // 3. Re-apply qe_lite to remove non-core variables

        // Step 1.
        m_tg.qel(vars, fml);

        // Step 2.
        //  Variables that appear as array indices or values cannot be
        //  eliminated if they are not c-ground. They are core variables All
        //  other Array/ADT variables can be eliminated, they are redundant.
        obj_hashtable<app> core_vars;
        collect_selstore_vars(fml, core_vars, m);

        std::function<bool(app *)> is_red = [&](app *v) {
            if (!m_dt_util.is_datatype(v->get_sort()) &&
                !m_array_util.is_array(v))
                return false;
            return !core_vars.contains(v);
        };
        expr_sparse_mark red_vars;
        for (auto v : vars)
            if (is_red(v)) red_vars.mark(v);
        CTRACE("mbp_tg", !core_vars.empty(), tout << "vars not redundant ";
               for (auto v
                    : core_vars) tout
               << " " << app_ref(v, m);
               tout << "\n";);

        std::function<bool(expr *)> non_core = [&](expr *e) {
            if (is_app(e) && is_partial_eq(to_app(e)))
                return true;
            if (m.is_ite(e) || m.is_or(e) || m.is_implies(e) || m.is_and(e) || m.is_distinct(e))
                return true;
            return red_vars.is_marked(e);
        };

        // Step 3.
        m_tg.qel(vars, fml, &non_core);

        CTRACE("mbp_tg", !vars.empty(),
               tout << "before substitution " << fml << "\n";);
        // for all remaining non-cgr bool, dt, array variables, add v = mdl(v)
        expr_sparse_mark s_vars;
        for (auto v : vars) {
            if (m_dt_util.is_datatype(v->get_sort()) ||
                m_array_util.is_array(v) || m.is_bool(v)) {
                CTRACE("mbp_tg",
                       m_array_util.is_array(v) ||
                           m_dt_util.is_datatype(v->get_sort()),
                       tout << "Could not eliminate  " << v->get_name()
                            << "\n";);
                s_vars.mark(v);
                m_tg.add_eq(v, mdl(v));
            }
        }

        std::function<bool(expr *)> substituted = [&](expr *e) {
            return
                (is_app(e) && is_partial_eq(to_app(e))) ||
                m.is_ite(e) ||
                red_vars.is_marked(e) ||
                s_vars.is_marked(e);
        };

        // remove all substituted variables
        m_tg.qel(vars, fml, &substituted);

uses the same references to bound variables, but sets fml to different values based on literals.
In one of the calls, fml is set to "true". All variables are eliminated. In the last call, fml is set to something that contains v!0. Now v!0 doesn't get projected.

[hgvk94]

You are right. It was because we were removing the most important parts of fml because they were not in the core.

[NikolajBjorner]

In step 3, the variable v!0 occurs under a conjunction.

        std::function<bool(expr *)> non_core = [&](expr *e) {
            if (is_app(e) && is_partial_eq(to_app(e)))
                return true;
            if (m.is_ite(e) || m.is_or(e) || m.is_implies(e) || **m.is_and(e)** || m.is_distinct(e))
                return true;
            return red_vars.is_marked(e);
        };

It then filters out the literal here

    for (expr *a : m_lits) {
        if (!is_internalized(a)) continue;
        if (m_explicit_eq && get_term(a)->is_eq_or_neq()) continue;
        expr_ref r(m);
        r = mk_app(a);
        if (non_core == nullptr || !contains_nc(r)) lits.push_back(r);
    }

because contains_nc returns true.
However, the predicate

        std::function<bool(expr *)> substituted = [&](expr *e) {
            return
                (is_app(e) && is_partial_eq(to_app(e))) ||
                m.is_ite(e) ||
                red_vars.is_marked(e) ||
                s_vars.is_marked(e);
        };

Does not filter out conjunctions.

regarding this code:

    for (auto t : m_deq_distinct) {
        args.reset();
        for (auto c : t) {
            d = mk_app(*(c->get_repr()));
            if (non_core == nullptr || !contains_nc(d)) args.push_back(d);
        }
        if (args.size() < 2) continue;
        if (args.size() == 2)
            distinct = mk_neq(m, args.get(0), args.get(1));
        else
            distinct = m.mk_distinct(args.size(), args.data());
        lits.push_back(distinct);
    }

I try to hoist generic functionality outside of application code. The function to create distinct predicate has a rewriting implementation in ast_util.cpp