0

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

arshiamoeini
  • 1
  • I see a link, not an explanation. Whatever text you are asking about should be included, as text, directly in the question. If it is too long (and an excerpt won't do) or if for some reason you cannot include the text directly, then the question is not suited to this site. – John Bollinger May 11 '23 at 14:10

1 Answers1

0

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.

alias
  • 28,120
  • 2
  • 23
  • 40
  • You're right, I'm using the z3 crate, but the seq is not defined in it yet. I was planning to develop it myself so that I can use it. Thank you – arshiamoeini May 12 '23 at 07:27