英文:
how to define adt constructor for `int list` z3 adt dotnet api
问题
Here is the translation of the provided text:
如何为 int list 定义 ADT 构造函数
Context.MkConstructor(name: string, recognizer: string, ?fieldNames: string array, ?sorts: Sort array, ?sortRefs: uint32 array) : Constructor
文档中提到 (https://z3prover.github.io/api/html/class_microsoft_1_1_z3_1_1_context.html#a2a421919ab766bf028ec422723b42e37)
"sorts" 表示字段的排序方式，如果字段的排序方式与递归数据类型有关，可以设置为 0。
"sortRefs" 表示构造函数的参数中引用的数据类型排序方式；如果相应的排序引用为 0，则 "sort_refs" 中的值应该是对已声明的递归数据类型之一的索引。
_.MkConstructor("cons", "is_cons", [|"x"; "y"|], [|.mkIntSort (); ?1|], ?2)
对于 ? 应该使用什么值？
我尝试将 ?1 设置为 null，但我不理解 sortRefs 的工作原理。
英文:
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,
答案1
得分: 1
z3本身提供了一个示例，完全符合您的要求：https://github.com/Z3Prover/z3/blob/12e45c9d17aa48151b2c20573fb3b527b32fdb54/examples/dotnet/Program.cs#L1503-L1559
如果您有具体的问题，请随时提问，但我想上面的代码应该正是您正在寻找的内容。
英文:
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.
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论