CODEWITHSUNDEEP
clogicz3theorem-provingsmt-lib
arshiamoeini
arshiamoeini

Reputation: 1

What is the function associated with seq.map in C API of z3?

I want to know is their function in z3.h that is related to seq.map in SMT-LIB2 that explained below text

thanks for any help

i searched and saw z3.h but cant find any function

Upvotes: 0

Views: 45

Answers (1)

alias
alias

Reputation: 30497

Essentially, you're looking for z3_mk_map: https://github.com/Z3Prover/z3/blob/12e45c9d17aa48151b2c20573fb3b527b32fdb54/src/api/api_array.cpp#L166-L189

But the C api is quite clunky when it comes to using sequence based functions, though of course it's doable. I'd recommend going for a higher-level api instead of using C for this purpose, if you can avoid it.

Upvotes: 0

Related Questions