Feature request: API to manually construct a Z3_model objects

[delcypher]

I'm currently using components of Z3 to build my own solver (the parser and some of its tactics) but I use my own custom method external to Z3 to do the solving.

A problem I have is that when my custom method of solving finds a satisfying assignment I have no good way to create a Z3_model object. I need to have the found assignment in this form because I need to feed this model through the Z3 tactics I have used to perform model conversion so that I can give a satisfying assignment to the original problem given to my solver.

The only way I can see of creating a Z3_model in my case is to create a new solver and assert the satisfying assignment as a set of equalities and then ask the solver to find a satisfying assignment.
This approach seems pretty wasteful so what I really need is an API that would just let me build a Z3_model. In my case I'm working in the QF_BV, QF_FPBV, and QF_FP theories so the model I need to create is free from functions (that need an interpretation) and infinite datatypes.

Could something like this be implemented?

[NikolajBjorner]

It's possible. It requires adding a fair amount of additional API functions to

1. create a Z3_model (the reference count should be 0 to follow conventions of other functions).
2. create Z3_func_interp objects
3. populate Z3_func_interp objects with cases and defaults.
4. populate Z3_model objects with constants and functions.
5. add corresponding functions to the Java/.Net/C++/OCaml

[wintersteiger]

+1. The tactic framework should allow tactics to use external solving methods and to support that, we need a model construction API. Ultimately it's probably not significantly faster to construct models via dedicated functions than to assert a bunch of equalities into a fresh solver, but it definitely makes the user-code simpler/more readable.

@delcypher Let me know if you want to tackle this yourself, I'm happy to help if you get stuck.

[NikolajBjorner]

I am adding a first pass.. 392334f

[delcypher]

@wintersteiger

@delcypher Let me know if you want to tackle this yourself, I'm happy to help if you get stuck.

Unfortunately I'm rather busy with my PhD thesis these days. Once I'm done with that I'd happily take a look at this if it isn't already implemented.

[delcypher]

@NikolajBjorner

create a Z3_model (the reference count should be 0 to follow conventions of other functions).

Should Z3_models be partially immutable? I.e. once you assign an interpretation to a function should you be able to change it?

populate Z3_func_interp objects with cases and defaults.

What are "cases" and "default"? Is this for non-constant functions (e.g. a function where it needs to branch on the argument values and give different results)?

[NikolajBjorner]

What are "cases" and "default"? Is this for non-constant functions (e.g. a function where it needs to branch on the argument values and give different results)?

yes

Should Z3_models be partially immutable? I.e. once you assign an interpretation to a function should you be able to change it?

That's possibly a good idea. In the first cut it is not the case.

[delcypher]

@NikolajBjorner

392334f

Wow thanks for doing that so quickly! I can give the new API a try tomorrow. I do have a few questions about the new API you introduced.

• Why is the Z3_ast argument to Z3_add_func_interp() called else? Is this the "default" case for a function interpretation?

• Why are Z3_add_func_interp() and Z3_add_const_interp() two different functions? Would it not be simpler from the user perspective for there to be just a single function. In the implementation it can be checked if the assignment is a constant and appropriate action can take place. I see that one returns void and the other returns a Z3_func_interp so maybe that's the reason you made them separate functions.

• What reference counting function should be used on Z3_func_interp objects? Is there a reason the interpretations aren't just stored in the model (i.e. have the Z3_model lifetime be the same as the Z3_func_interp lifetime)?

• What is the Z3_add_func_entry() function for? I'm not sure what an "entry" is. Presumably this is the "case" you talked about. When you add an "entry" to Z3_add_const_interp() what form does args need to be in? What order are the "entries" applied in when used as an interpretation and do they need to be disjoint?

[delcypher]

@NikolajBjorner

What reference counting function should be used on Z3_func_interp objects? Is there a reason the interpretations aren't just stored in the model (i.e. have the Z3_model lifetime be the same as the Z3_func_interp lifetime)?

Oops. I didn't realise Z3_func_interp objects were already part of Z3's API. So I should use Z3_func_interp_inc_ref() and Z3_func_interp_dec_ref().

However thinking a little more I think forcing the user to reference count Z3_func_interp is a bit weird given the current API. The Z3_add_func_interp() couples creating a Z3_func_interp with adding it to a model. This means that it isn't possible to re-use a Z3_func_interp by adding it to a different model. If a Z3_func_interp can't be re-used I'm not sure why reference counting is needed because that implies the lifetime of the Z3_func_interp is tied to the lifetime of the model.

[NikolajBjorner]

your suggestion could apply to the existing model API (having the life-time of func_interp live with models), but there is no support for maintaining the func_interp objects. So we use the same reference counting model for these objects as with all other objects.

[delcypher]

Okay. Makes sense. It's bit unfortunate that the API was designed that way but if it's already part of the API design I'd rather not change it as this would introduce unnecessary breakages.

[NikolajBjorner]

It's not necessarily unfortunate: using this convention all the upper layers use the same code to manage objects. See for example how this is manifested in the C++ API that manages func_interp objects. Having a non-uniform memory model would not let us use the same functionality.

[NikolajBjorner]

There will be other design questions about this API feature. For example, I have that the default values are added once and cannot be updated on a func_interp object.

[delcypher]

There will be other design questions about this API feature. For example, I have that the default values are added once and cannot be updated on a func_interp object.

Z3_add_func_interp() currently does three things

• Creates a Z3_func_interp (e.g. Z3_mk_func_interp())
• Associates it with a model (e.g. Z3_model_add_func_interp())
• Adds the default value to the Z3_func_interp (Z3_func_interp_set_default())

It would probably be good to separate out these three actions into three separate API calls (e.g. Z3_mk_func_interp(), Z3_model_add_func_interp(), and Z3_func_interp_set_default()). This would also fix the problem of not being able to update the default value of the Z3_func_interp.

Note I'm assuming that it is possible to create a Z3_func_interp without assigning it to a model first and that it's possible to associate it with one or more models later. If this is not possible then my suggestion needs rethinking.

[NikolajBjorner]

I can't easily separate func_interps from the models they originated from. So the current approach binds func_interps to one model at a time. I added a method to set the default value (set_else to mirror a get_else function). The constructor for func_interp still contains the else value to more systematically enforce that func_interps are well-formed (they should not have an undefined default value).

[delcypher]

@NikolajBjorner

I can't easily separate func_interps from the models they originated from. So the current approach binds func_interps to one model at a time.

Okay understood. As long as the documentation makes this clear this hopefully won't be a problem.

Could you put these changes into a separate PR that I can start to evaluate? These changes are currently in PR #1226 which seems mostly focused on removing the simplifier which seems to me to be unrelated. I don't really want to test the new API with the potentially disruptive changes to the simplifier.

I can do this for you if you like if you tell me which commits to take. At the moment it looks like I should take

• ce84435
• 623cd5d

Once I've given the API some testing I can probably add some example uses of it.

[NikolajBjorner]

I already merged the changesseparately

[delcypher]

@NikolajBjorner So you did. Sorry I missed that. When I have time I'll try out the new API and try and write some examples using it.

[delcypher]

@NikolajBjorner I've started writing examples to test new the API.

I've hit a problem. How do I add to the model an assignment to an array? In the code example below I've created a fresh function that basically has an interpretation (arrayAsFuncInterp) I'd like for the array. However I can't see an API to construct an application of (_ array_array the_fresh_functiion_name) (see FIXME).

Am I missing something?

void mk_model_example() {
    printf("\nmk_model_example\n");
    LOG_MSG("mk_model_example");
    Z3_context ctx = mk_context();
    // Construct empty model
    Z3_model m = Z3_mk_model(ctx);
    Z3_model_inc_ref(ctx, m);

    // Create constants "a" and "b"
    Z3_sort intSort = Z3_mk_int_sort(ctx);
    Z3_symbol aSymbol = Z3_mk_string_symbol(ctx, "a");
    Z3_func_decl aFuncDecl = Z3_mk_func_decl(
        ctx,
        aSymbol,
        /*domain_size=*/0,
        /*domain=*/NULL,
        /*range=*/intSort
    );
    Z3_symbol bSymbol = Z3_mk_string_symbol(ctx, "b");
    Z3_func_decl bFuncDecl = Z3_mk_func_decl(
        ctx,
        bSymbol,
        /*domain_size=*/0,
        /*domain=*/NULL,
        /*range=*/intSort
    );

    // Create array "c" that maps int to int.
    Z3_symbol cSymbol = Z3_mk_string_symbol(ctx, "a");
    Z3_sort int2intArraySort = Z3_mk_array_sort(
        ctx,
        /*domain=*/intSort,
        /*range=*/intSort
    );
    Z3_func_decl cFuncDecl = Z3_mk_func_decl(
        ctx,
        cSymbol,
        /*domain_size=*/0,
        /*domain=*/NULL,
        /*range=*/int2intArraySort
    );


    // Create numerals to be used in model
    Z3_ast zeroNumeral = Z3_mk_int(ctx, 0, intSort);
    Z3_ast oneNumeral = Z3_mk_int(ctx, 1, intSort);
    Z3_ast twoNumeral = Z3_mk_int(ctx, 2, intSort);
    Z3_ast threeNumeral = Z3_mk_int(ctx, 3, intSort);
    Z3_ast fourNumeral = Z3_mk_int(ctx, 4, intSort);

    // Add assignments to model
    // a == 1
    Z3_add_const_interp(ctx, m, aFuncDecl, oneNumeral);
    // b == 2
    Z3_add_const_interp(ctx, m, bFuncDecl, twoNumeral);

    // Create a fresh function that represents
    // reading from array.
    Z3_sort arrayDomain[] = { intSort };
    Z3_func_decl cAsFuncDecl = Z3_mk_fresh_func_decl(
        ctx,
        /*prefix=*/"",
        /*domain_size*/1,
        /*domain=*/arrayDomain,
        /*sort=*/ intSort
        );
    // Create function interpretation with default
    // value of "0".
    Z3_func_interp cAsFuncInterp = Z3_add_func_interp(
        ctx,
        m,
        cAsFuncDecl,
        /*default_value=*/zeroNumeral
    );
    Z3_func_interp_inc_ref(ctx, cAsFuncInterp);
    // Add [0] = 3
    Z3_ast_vector zeroArgs = Z3_mk_ast_vector(ctx);
    Z3_ast_vector_inc_ref(ctx, zeroArgs);
    Z3_ast_vector_push(ctx, zeroArgs, zeroNumeral);
    Z3_func_interp_add_entry(
        ctx,
        cAsFuncInterp,
        zeroArgs,
        threeNumeral
    );
    // Add [1] = 4
    Z3_ast_vector oneArgs = Z3_mk_ast_vector(ctx);
    Z3_ast_vector_inc_ref(ctx, oneArgs);
    Z3_ast_vector_push(ctx, oneArgs, oneNumeral);
    Z3_func_interp_add_entry(
        ctx,
        cAsFuncInterp,
        oneArgs,
        fourNumeral
    );

    // Now use the `(_ as_array)` to associate
    // the `cAsFuncInterp` with the `cFuncDecl`
    // in the model
    // FIXME: How do we get an application of
    // `(_ as_array)`?
    /*
    Z3_ast aafdAsApp = ???
    Z3_add_const_interp(
        ctx,
        m,
        cFuncDecl,
        aafdAsApp
    );
    */

    // Print the model
    Z3_string modelAsString = Z3_model_to_string(ctx, m);
    printf("Model:\n%s\n", modelAsString);


    // Evaluate expressions under model
    // TODO:


    Z3_ast_vector_dec_ref(ctx, oneArgs);
    Z3_ast_vector_dec_ref(ctx, zeroArgs);
    Z3_func_interp_dec_ref(ctx, cAsFuncInterp);
    Z3_model_dec_ref(ctx, m);
    Z3_del_context(ctx);
}

[NikolajBjorner]

(as-array f) constructors are not exposed over the API.
A crude workaround could be to parse this inside a dummy formula.

Otherwise, the way to go is to add a new API function that creates the as-array from a function f.

[delcypher]

@NikolajBjorner I think a new API function is the way to go. (_ as_array). I'll try to give this a go.

[NikolajBjorner]

I am adding it. ETA today.

[delcypher]

@NikolajBjorner Great. Once you've added it please ping me so I can complete the API example, then I'll create a PR for it.

[delcypher]

@NikolajBjorner Thanks for implementing the API. It seems to work but I think there is some missing sanity checking.

I had a typo in my program which meant that I accidentally added a constant interpretation and function interpretation for the same Z3_func_decl which resulted in this model

a -> 1
b -> 2
!0 -> (_ as-array !0)
!0 -> {
  0 -> 3
  1 -> 4
  else -> 0
}

An error should probably be raised if I try to do this. Below is the API example with the bug (see the // TYPO: should be cFuncDecl comment for where my mistake was).

void mk_model_example() {
    printf("\nmk_model_example\n");
    LOG_MSG("mk_model_example");
    Z3_context ctx = mk_context();
    // Construct empty model
    Z3_model m = Z3_mk_model(ctx);
    Z3_model_inc_ref(ctx, m);

    // Create constants "a" and "b"
    Z3_sort intSort = Z3_mk_int_sort(ctx);
    Z3_symbol aSymbol = Z3_mk_string_symbol(ctx, "a");
    Z3_func_decl aFuncDecl = Z3_mk_func_decl(
        ctx,
        aSymbol,
        /*domain_size=*/0,
        /*domain=*/NULL,
        /*range=*/intSort
    );
    Z3_symbol bSymbol = Z3_mk_string_symbol(ctx, "b");
    Z3_func_decl bFuncDecl = Z3_mk_func_decl(
        ctx,
        bSymbol,
        /*domain_size=*/0,
        /*domain=*/NULL,
        /*range=*/intSort
    );

    // Create array "c" that maps int to int.
    Z3_symbol cSymbol = Z3_mk_string_symbol(ctx, "c");
    Z3_sort int2intArraySort = Z3_mk_array_sort(
        ctx,
        /*domain=*/intSort,
        /*range=*/intSort
    );
    Z3_func_decl cFuncDecl = Z3_mk_func_decl(
        ctx,
        cSymbol,
        /*domain_size=*/0,
        /*domain=*/NULL,
        /*range=*/int2intArraySort
    );


    // Create numerals to be used in model
    Z3_ast zeroNumeral = Z3_mk_int(ctx, 0, intSort);
    Z3_ast oneNumeral = Z3_mk_int(ctx, 1, intSort);
    Z3_ast twoNumeral = Z3_mk_int(ctx, 2, intSort);
    Z3_ast threeNumeral = Z3_mk_int(ctx, 3, intSort);
    Z3_ast fourNumeral = Z3_mk_int(ctx, 4, intSort);

    // Add assignments to model
    // a == 1
    Z3_add_const_interp(ctx, m, aFuncDecl, oneNumeral);
    // b == 2
    Z3_add_const_interp(ctx, m, bFuncDecl, twoNumeral);

    // Create a fresh function that represents
    // reading from array.
    Z3_sort arrayDomain[] = { intSort };
    Z3_func_decl cAsFuncDecl = Z3_mk_fresh_func_decl(
        ctx,
        /*prefix=*/"",
        /*domain_size*/1,
        /*domain=*/arrayDomain,
        /*sort=*/ intSort
        );
    // Create function interpretation with default
    // value of "0".
    Z3_func_interp cAsFuncInterp = Z3_add_func_interp(
        ctx,
        m,
        cAsFuncDecl,
        /*default_value=*/zeroNumeral
    );
    Z3_func_interp_inc_ref(ctx, cAsFuncInterp);
    // Add [0] = 3
    Z3_ast_vector zeroArgs = Z3_mk_ast_vector(ctx);
    Z3_ast_vector_inc_ref(ctx, zeroArgs);
    Z3_ast_vector_push(ctx, zeroArgs, zeroNumeral);
    Z3_func_interp_add_entry(
        ctx,
        cAsFuncInterp,
        zeroArgs,
        threeNumeral
    );
    // Add [1] = 4
    Z3_ast_vector oneArgs = Z3_mk_ast_vector(ctx);
    Z3_ast_vector_inc_ref(ctx, oneArgs);
    Z3_ast_vector_push(ctx, oneArgs, oneNumeral);
    Z3_func_interp_add_entry(
        ctx,
        cAsFuncInterp,
        oneArgs,
        fourNumeral
    );

    // Now use the `(_ as_array)` to associate
    // the `cAsFuncInterp` with the `cFuncDecl`
    // in the model
    Z3_ast cFuncDeclAsArray = Z3_mk_as_array(
        ctx,
        cAsFuncDecl
    );
    Z3_add_const_interp(
        ctx,
        m,
        cAsFuncDecl, // TYPO: should be cFuncDecl
        cFuncDeclAsArray
    );

    // Print the model
    Z3_string modelAsString = Z3_model_to_string(ctx, m);
    printf("Model:\n%s\n", modelAsString);


    // Evaluate expressions under model
    // TODO:


    Z3_ast_vector_dec_ref(ctx, oneArgs);
    Z3_ast_vector_dec_ref(ctx, zeroArgs);
    Z3_func_interp_dec_ref(ctx, cAsFuncInterp);
    Z3_model_dec_ref(ctx, m);
    Z3_del_context(ctx);
}

[NikolajBjorner]

I am not sure it qualifies as an error: the name !0 is overloaded.
One version is an array, another is a unary function. They have different types, but the print method you used does not show the types. Identifies don't necessarily have unique types.

[delcypher]

@NikolajBjorner I'm not sure why anyone would want the names in a model to be overloaded. My point wasn't specifically about !0 but was the fact it is possible to call Z3_add_const_interp() and Z3_add_func_interp() on the same Z3_func_decl which results the model having two (possibly conflicting) interpretations for the same Z3_func_decl. It is not clear (at least to me) what the semantics of the model are in this case so I really think the behaviour should be changed.

I think the most intuitive behaviour would be to remove the previous interpretation in the model for the Z3_func_decl provided by the user.

[NikolajBjorner]

So I should understand that Z3 generates the name !0 twice. This would be unfortunate.

[delcypher]

@NikolajBjorner No. There is just a a single unnamed (from a single call to Z3_mk_fresh_func_decl) Z3_func_decl. The naming of this Z3_func_decl is behaving exactly as I expect. The issue is adding multiple interpretations for the same Z3_func_decl to the model.

To try and elucidate my point here are the three important calls from the example I gave above. If you're not sure just copy the code I gave above into the C API example and run it.

    // Create `cAsFuncDecl`
    Z3_func_decl cAsFuncDecl = Z3_mk_fresh_func_decl(
        ctx,
        /*prefix=*/"",
        /*domain_size*/1,
        /*domain=*/arrayDomain,
        /*sort=*/ intSort
        );

   // Do some stuff...

    // Add interpretation for `cAsFuncDecl`
    Z3_func_interp cAsFuncInterp = Z3_add_func_interp(
        ctx,
        m,
        cAsFuncDecl,
        /*default_value=*/zeroNumeral
    );

   // Do some stuff...

       // Try to add interpretation for `cAsFuncDecl` to model.
       // This should overwrite the existing interpretation in the model
       // but instead this seems to add another interpretation for the same
       // Z3_func_decl
       Z3_add_const_interp(
        ctx,
        m,
        cAsFuncDecl, 
        cFuncDeclAsArray
    );

[NikolajBjorner]

OK, got it. Added to test_capi.c and got an assertion violation in debug mode when adding a non-zero ary function as a constant. Added parameter validation to the API for this. Function and constant declarations are two different name spaces and if a new function is added in lieu of an old one, the old is going to be invalidated.

[NikolajBjorner]

can we close this?

[delcypher]

@NikolajBjorner Sure. The API seems sufficient for now. I'll re-open this issue if I run into more problems.

[rainoftime]

@delcypher Are these C APIs such as Z3_mk_model exposed in Z3's C++ API?

[NikolajBjorner]

Yes, there is a constructor for z3::model that takes a context as argument.