How to customize functions

[Flians]

I write a function using C:

Z3_ast fun_a(const Z3_ast &A, const Z3_ast &B)
{
    return Z3_mk_ite(logic, Z3_mk_eq(logic, Z3_mk_bvxor(logic, A, B), 3), z3_x, Z3_mk_bvand(logic, A, B));
}

And I call this function repeatedly, which repeatedly calculates the expression. I found the Z3_mk_func_decl used in test_capi.c such as: g = Z3_mk_func_decl(ctx, g_name, 1, g_domain, U);

Can I use Z3_mk_func_decl to customize my function? If so, how can I do it?

[aytey]

Z3_mk_func_decl does (in SMTLIB2) the same as declare-fun, that is, it allows you tell the SMT solver about the existence of an uninterpreted function with a particular signature. It is like, in C, only having the prototype.

In SMTLIB2, there is the notion of define-fun (see the same link as above), where you also give the SMT solver the behaviour of your function (i.e., it is no longer uninterpreted, and it acts "like a macro").

However, as far as I'm aware, this isn't something you can do with Z3's API. See this issue: https://github.com/Z3Prover/z3/issues/1598

[Flians]

Yes, I wanna define my function using define-fun. But this seems infeasible.

Thank you.

[aytey]

Yep, so I don't think you can do that; the recommended way (via the API) is to the use the kind of "expression builders" that you're currently doing already.

I guess the "big difference" is that if you write your instances to a .smt2 file, that you will have the "function expansion" vs. having the SMTLIB2 function definition.

Is there a reason you want to use define-fun over your current way?

[Flians]

Yes, I wanna define some functions and call them repeatedly.

[aytey]

Yes, but is there a reason you want to specially use define-fun over your current approach of "expression builders"?

[Flians]

Yes. If I achieve my function using define-fun and the z3 can handle it in advance, such as the most simplified. In this way, when I call this function multiple times, the solution process can be accelerated. I don't know if z3 has such an optimization.

[aytey]

Yeah, I am not sure that's define-fun works.

It is possible that there are some rewriting optimisation that occur, but, as far as I understand it, define-fun acts like a macro so is just substituted in-place (i.e., abstracting away duplicated code into define-fun does not make the instance any quicker/easier for the SMT solver to solve).

If you're dealing with SMTLIB2 files, it is possible that it makes parsing quicker, but given previous answers to issues, I do not believe define-fun makes solving quicker (but maybe I will be proven wrong!).

[Flians]

OK, I already know what you mean. I wanna accelerate my program using bit-vector.
I try it in many ways. but the effect is not very good.

Thank you very much, too.

[aytey]

Can you share an example instance (in SMTLIB2 format)? We might be able to provide some suggestions about how to improve your encoding/some options you could try.

[Flians]

of course. But I didn't use SMTLIB2 format. I I'd like to check whether the functions of the two circuit netlists are the same. The input of each circuit unit is 0, 1, and unknow. I use two bits to represent them. Finally, I change the netlists into an Z3_ast and check whether it is true.

[Flians]

@andrewvaughanj If you can tell me how to set parameters for FixedSizeBitVectors in z3 to speed up the resolution process, it would be really great. Thank you very much.

[aytey]

Could you try something like: https://z3prover.github.io/api/html/group__capi.html#ga922eb66ace15a857ec7a81d426d580c4 ?

[Flians]

yes, I know how to set params. But I don’t know what the parameters are and what the parameters do

[aytey]

Without knowing your code, it is hard to say, but here are some examples:

• https://github.com/Z3Prover/z3/blob/master/examples/tptp/tptp5.cpp#L2320

• https://github.com/Z3Prover/z3/blob/master/src/test/smt2print_parse.cpp#L22

[NikolajBjorner]

I write a function using C:

Z3_ast fun_a(const Z3_ast &A, const Z3_ast &B)
{
    return Z3_mk_ite(logic, Z3_mk_eq(logic, Z3_mk_bvxor(logic, A, B), 3), z3_x, Z3_mk_bvand(logic, A, B));
}

And I call this function repeatedly, which repeatedly calculates the expression. I found the Z3_mk_func_decl used in test_capi.c such as: g = Z3_mk_func_decl(ctx, g_name, 1, g_domain, U);

Can I use Z3_mk_func_decl to customize my function? If so, how can I do it?

Your code is the right way to do it. There isn't a way to bind a Z3_mk_func_decl to some macro definition. To make things easier for yourself, please use the C++ API. The C API is not for mortals (but backend for machines).

[Flians]

@NikolajBjorner Ok, thank you. I used the C++ API before, but it was very slow. So I changed to use C's API to implement my program.