Invoke another solver instance inside a theory implementation

[guluchen]

I am developing a theory of string plug-in and inside the theory solver, we need to ask the question that is only relevant to the arithmetic theory. We use the following code to create a new solver instance https://github.com/guluchen/z3/blob/master/src/smt/theory_str/str_solver.h#L510

and invoke it using the code below https://github.com/guluchen/z3/blob/master/src/smt/theory_str/str_solver.cpp#L1253

The issue is that, my constraints also contain some symbols for string theory which I want to just ignore them in this particular case.

In my current implementation, I made a workaround using some static flags, but there should be a better way. Any suggestions?

[NikolajBjorner]

You can use the expr_solver base class, but I guess your use is not as a symbolic automata plugin. To set the solver you should be able to do something like this;

    seq_expr_solver(ast_manager& m, smt_params& fp, context& ctx):
            m_fp_copy(fp),
            m_kernel(m, m_fp_copy), m(m){
         m_fp_copy.m_string_solver = symbol("none");
      }

where m_fp_copy is a copy of the smt_params fp that can be updated locally. That is, declare smt_params m_fp_copy; on seq_expr_solver.

Then it should be the case that upon initialization of theory solvers, it skips adding a theory solver for stirngs. It pretends that all string functions and predicates are uninterpreted.

[NikolajBjorner]

Regarding the code that checks is_reachable: it is more efficient to use a single solver and initialize it with the assertions from ctx once. Then use push/pop when performing local checks. The single solver would be associated with the theory_str class so it can be shared among different states.

[guluchen]

Many thanks for the very detailed suggestion. I think it would work quite well.

[guluchen]

I follow the suggestion and created an instance of such solver (let's call it int_expr_solver). https://github.com/guluchen/z3/blob/master/src/smt/theory_str/theory_str.h#L117

in particular, I use the following function to initialize the solver at the beginning of the final_check function of my theory solver

https://github.com/guluchen/z3/blob/master/src/smt/theory_str/theory_str.cpp#L1223

An unexpected behavior I have encountered is that the int_expr_solver becomes already UNSAT immediately after the initialization（called at the very beginning of final_check), which means the current assignment and guessed literal have some conflict in the integer part. But I think this should not happen if my theory solver can reach final_check.

I also tried a different version where I only assert relevant assignments, but the same problem still occurs from time to time.

    void int_expr_solver::initialize(context& ctx) {
        if(!initialized){
            initialized=true;
            expr_ref_vector Assigns(m),Literals(m);
            ctx.get_guessed_literals(Literals);
            ctx.get_assignments(Assigns);
            for (unsigned i = 0; i < ctx.get_num_asserted_formulas(); ++i) {
                assert_expr(ctx.get_asserted_formula(i));
            }
            for (auto & e : Assigns){
                if(ctx.is_relevant(e)) {
                    assert_expr(e);
                }
            }
            for (auto & e : Literals){
                assert_expr(e);
            }
        }
    }

[guluchen]

From the source code, it looks like the results of get_guessed_literals is always a subset of get_assignments. Is it correct?

[NikolajBjorner]

There are use cases of using solvers internally under the opt and qe directory. For example qe2.cpp maintains two solvers and uses assumptions. You should not need to interface with "relevancy" from outside a solver. This is used internally for search.

[guluchen]

Many thanks for the suggestion, but I did not find qe2.cpp, do you mean qe.cpp?

[NikolajBjorner]

Sorry, I had this in mind:

https://github.com/Z3Prover/z3/blob/master/src/qe/qsat.cpp#L627

[guluchen]

Many thanks for the pointer.

My case seems to be a bit different from the qsat one, where two independent solvers are maintained. I need to create a solver instance within another solver.

The issue is that I need to copy the context of the current solver to the inner solver, which should include all current "assignments" made by DPLL(T) and the original input formula

I am not sure whether it is correct to just assert at the inner solver

1. all expressions obtained from _ctx.getassignments( )_ , and
2. all original input from _ctx.get_assertedformula( )_ .

[NikolajBjorner]

Yes, this would be a way to do it.

[guluchen]

I did it in this way, but in some cases, the inner solver becomes UNSAT immediately after I added

1. all expressions from ctx.getassignments( ) and
2. all inputs from ctx.get_assertedformula( )

If I only add relevant formula, immediate UNSAT will not happen.

I wonder is it the cases that the integer theory solver did not reach final_check yet, but my own solver already reached it?

Maybe my understanding of relevancy in Z3 is still not correct. Is

https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/tr-2007-140.pdf

a right reference for it?

[NikolajBjorner]

It is likely because the assignment to non-relevant literals causes a theory conflict. In reality the assignment to non-relevant literals should be treated as dont-cares. So there is a different assignment that flips the truth value of the non-relevant literals that can be extended.

[guluchen]

Thanks for the explanation!