Unexpected unknown return when solving some instances

[zmylinxi]

Hi, when I use z3 to solve some instances of different theories, I noticed that sometimes z3 will return some unexpected unknown.

The result is returned unknown when the time limit and memory limit don't exceed.

And the implementation of these theories in z3 are complete, such as QFNRA, QFLRA, etc.

Then I check the source code in z3, I find the or_else_tactical class work like this:

// src/tactic/tactical.cpp:324
void operator()(goal_ref const & in, goal_ref_buffer& result) override {
    goal orig(*(in.get()));
    unsigned sz = m_ts.size();
    unsigned i;
    for (i = 0; i < sz; i++) {
        tactic * t = m_ts[i];
        SASSERT(sz > 0);
        if (i < sz - 1) {
            try {
                t->operator()(in, result);
                return;
            }
            catch (tactic_exception &) {
                result.reset();
            }
            catch (z3_error & ex) {
                IF_VERBOSE(10, verbose_stream() << "z3 error: " << ex.error_code() << " in or-else\n");
                throw;
            }
            catch (z3_exception& ex) {
                IF_VERBOSE(10, verbose_stream() << ex.msg() << " in or-else\n");
                throw;
            }
            catch (const std::exception &ex) {
                IF_VERBOSE(10, verbose_stream() << ex.what() << " in or-else\n");
                throw;
            }
            catch (...) {
                IF_VERBOSE(10, verbose_stream() << " unclassified exception in or-else\n");
                // std::current_exception returns a std::exception_ptr, which apparently 
                // needs to be re-thrown to extract type information.
                // typeid(ex).name() would be nice.
                throw;
            }
        }
        else {
            t->operator()(in, result);
            return;
        }
        in->reset_all();
        in->copy_from(orig);
    }
}

When the tactic which combined by or_else_tactical cannot solve the instance in time or in given configuration, tactic_exception should be thrown, and the goal will be passed to the next tactic to try to solve.

This is exactly what the authors implemented, e.g. nlsat_tactic:

// src/nlsat/nlsat_tactic.cpp:238
void operator()(goal_ref const & in, 
                goal_ref_buffer & result) override {
    try {
        imp local_imp(in->m(), m_params);
        scoped_set_imp setter(*this, local_imp);
        local_imp(in, result);
    }
    catch (z3_error & ex) {
        throw ex;
    }
    catch (z3_exception & ex) {
        // convert all Z3 exceptions into tactic exceptions.
        throw tactic_exception(ex.msg());
    }
}

Convert all z3 exceptions into tactic exceptions, and then the or_else_tactical will catch it and process.

Then we can use or_else_tactical with try_for_tactical to achieve a portfolio solver in z3.

1. try_for_tactical throws default_exception(Z3_CANCELED_MSG) (A derived class based on z3_exception)
2. solver tactic catches default_exception, and convert it into tactic_exception
3. or_else_tactical catches tactic_exception, and process

But it will go wrong between the or_else_tactical and the solver tactic, e.g. qfnra_nlsat_tactic:

// src/nlsat/tactic/qfnra_nlsat_tactic.cpp:32
tactic * mk_qfnra_nlsat_tactic(ast_manager & m, params_ref const & p) {
    params_ref main_p = p;
    main_p.set_bool("elim_and", true);
    main_p.set_bool("blast_distinct", true);
    params_ref purify_p = p;
    purify_p.set_bool("complete", false); // temporary hack, solver does not support uninterpreted functions for encoding (div0 x) applications. So, we replace it application of this kind with an uninterpreted function symbol.

    tactic * factor;
    if (p.get_bool("factor", true))
        factor = mk_factor_tactic(m, p);
    else
        factor = mk_skip_tactic();

    return and_then(
        mk_report_verbose_tactic("(qfnra-nlsat-tactic)", 10),
        and_then(using_params(mk_simplify_tactic(m, p),
                              main_p),
                 using_params(mk_purify_arith_tactic(m, p),
                              purify_p),
                 mk_propagate_values_tactic(m, p),
                 mk_solve_eqs_tactic(m, p),
                 mk_elim_uncnstr_tactic(m, p),
                 mk_elim_term_ite_tactic(m, p),
                 using_params(mk_purify_arith_tactic(m, p),
                              purify_p)),
        and_then(/* mk_degree_shift_tactic(m, p), */ // may affect full dimensionality detection
            factor,
            mk_solve_eqs_tactic(m, p),
            using_params(mk_purify_arith_tactic(m, p),
                         purify_p),
            using_params(mk_simplify_tactic(m, p),
                         main_p),
            mk_tseitin_cnf_core_tactic(m, p),
            using_params(mk_simplify_tactic(m, p),
                         main_p),
            mk_nlsat_tactic(m, p)));
}

Before mk_nlsat_tactic, there are many preprocessing tactic which may not convert the z3_exception to tactic_exception.

If the time limit in try_for_tactical is not long enough to do these preprocessing(That's to say, the instance size is too large, maybe 300MB+), unexpected unknown will be returned.

When a large instance with 300MB+ cannot be preprocess in 5s, or_else_tactical will catch the z3_exception, and throw it.

Then z3 return unknown in 5s, maybe.

As far as I know, QFNRA isn't the only one that returns unexpected unknown.

// src/tactic/smtlogics/qfnra_tactic.cpp:35
tactic * mk_qfnra_tactic(ast_manager & m, params_ref const& p) {
    ...
    return and_then(mk_simplify_tactic(m, p), 
                    mk_propagate_values_tactic(m, p),
                    or_else(try_for(mk_qfnra_nlsat_tactic(m, p0), 5000),
                            try_for(mk_qfnra_nlsat_tactic(m, p1), 10000),
                            mk_qfnra_sat_solver(m, p, 4),
                            and_then(try_for(mk_smt_tactic(m), 5000), mk_fail_if_undecided_tactic()),
                            mk_qfnra_sat_solver(m, p, 6),
                            mk_qfnra_nlsat_tactic(m, p2)));
}

A possible temporary hack as follow, but I don't know if this lead to bugs elsewhere in the program, such as cannot handle other z3_exception properly.

void operator()(goal_ref const & in, goal_ref_buffer& result) override {
    ...
    for (i = 0; i < sz; i++) {
        ...
        if (i < sz - 1) {
            try {
                t->operator()(in, result);
                return;
            }
            ...
// src/tactic/tactical.cpp:343
            catch (z3_exception& ex) {
                IF_VERBOSE(10, verbose_stream() << ex.msg() << " in or-else\n");
                // throw;
                result.reset();
            }
            ...
        }
        ...
    }
}

I don't know if I understand correctly, please criticize and correct me, thanks.

[NikolajBjorner]

I think your understanding is correct: the or-else handler depends on lower-level code that is spread around raise the right kinds of exceptions. This is overall brittle but errs on the side of producing unknown. The code in the nlsat solver is more of a hack in line of what the proposed patch suggests. It might be motivated based on that the nlsat code using libraries where tactic_exception has not been defined (algebraic numbers).

It is safer to fix the places where an exception is treated as a default exception but is really recoverable. Non-recoverable exceptions should still throw. So for the relatively few samples that produce unknown it could be possible to figure out what is going on. Note that the utilities in math/lp all throw a default_exception.

[NikolajBjorner]

The cause of unknowns is definitely in some cases attributed to exceptions raised in the rewriter. By handling these the or-else tactic can recover.

[zmylinxi]

The cause of unknowns is definitely in some cases attributed to exceptions raised in the rewriter. By handling these the or-else tactic can recover.

Oh, I see. When I removed all mk_qfnra_sat_solver in mk_qfnra_tactic, the unknown case number decrease from 40+ to 20+.

But I didn't known why before.

[zmylinxi]

I think your understanding is correct: the or-else handler depends on lower-level code that is spread around raise the right kinds of exceptions. This is overall brittle but errs on the side of producing unknown. The code in the nlsat solver is more of a hack in line of what the proposed patch suggests. It might be motivated based on that the nlsat code using libraries where tactic_exception has not been defined (algebraic numbers).

It is safer to fix the places where an exception is treated as a default exception but is really recoverable. Non-recoverable exceptions should still throw. So for the relatively few samples that produce unknown it could be possible to figure out what is going on. Note that the utilities in math/lp all throw a default_exception.

Yes, it seems more reasonable to catch default_exception.

Instead, it may need large-scale checking and modifying on lower-level code to fix this.

[NikolajBjorner]

(get-info :reason-unknown) 

gives some information of the source of the exception.
It is probably "canceled" in your cases.

Then a debugger can be used to trace where/what exceptions are raised. It gives an idea of the source.

[zmylinxi]

Thanks a lot. I will try it.