CODEWITHSUNDEEP
z3adt
Andrew
Andrew

Reputation: 23

how to define adt constructor for `int list` z3 adt dotnet api

how to define adt constructor for int list

Context.MkConstructor(name: string, recognizer: string, ?fieldNames: string array, ?sorts: Sort array, ?sortRefs: uint32 array) : Constructor

The documentation says (https://z3prover.github.io/api/html/class_microsoft_1_1_z3_1_1_context.html#a2a421919ab766bf028ec422723b42e37) "sorts field sorts, 0 if the field sort refers to a recursive sortRefs reference to datatype sort that is an argument to the constructor; if the corresponding sort reference is 0, then the value in sort_refs should be an index referring to one of the recursive datatypes that is declared."

_.MkConstructor("cons", "is_cons", [|"x"; "y"|], [|_.mkIntSort (); ?1], ?2)

what should be instead ?

I tried to set ?1 to null, but I can't understand working principle sortRefs,

Upvotes: 0

Views: 44

Answers (1)

alias
alias

Reputation: 30525

z3 itself comes with an example that does exactly this: https://github.com/Z3Prover/z3/blob/12e45c9d17aa48151b2c20573fb3b527b32fdb54/examples/dotnet/Program.cs#L1503-L1559

Feel free to ask if you've specific questions, but I suppose the above code is exactly what you're looking for.

Upvotes: 1

Related Questions