z3 - 用于访问 MuZ 的 .Net API

Question

rise4fun 的教程提到了用于访问 MuZ 的 .Net API。然而，点击任何提到的方法，例如To add a rule, call: Z3_datalog_add_rule导致死链接。这些方法在哪里描述，目前是否支持？

此外，与这个问题没有直接关系，但我注意到可能使用 SMT-LIB API 的示例使用define-fun命令。.Net API 中是否有等效功能？

谢谢

Answer 1

感谢您报告损坏的链接。

链接：

http://rise4fun.com/Z3/tutorialcontent/group__capi.html#ga0d158891352456e6a4ac9ba398a75653

应该指出：

 http://research.microsoft.com/en-us/um/redmond/projects/z3/group__capi.html 

.NET API 函数的对应链接是：

 http://research.microsoft.com/en-us/um/redmond/projects/z3/class_microsoft_1_1_z3_1_1_context.html

请注意，在 Z3 的最新版本中，.NET API 比rise4fun 中使用的版本进行了重大修订。上面的链接描述了最新的 .NET API。Z3 以前版本中使用的“遗留”.NET API 的链接是：

http://research.microsoft.com/en-us/um/redmond/projects/z3/old/group__mapi.html

这些链接收集在：http ://research.microsoft.com/en-us/um/redmond/projects/z3/

声明函数，最新版本中的 .NET API 称为“MkFuncDecl”。它是上下文对象上的一个方法。它有几个重载：

 FuncDecl  MkFuncDecl (Symbol name, Sort[] domain, Sort range) 
 FuncDecl  MkFuncDecl (Symbol name, Sort domain, Sort range) 
 FuncDecl  MkFuncDecl (string name, Sort[] domain, Sort range) 
 FuncDecl  MkFuncDecl (string name, Sort domain, Sort range) 

上面提到的第二个链接将您带到这些函数的文档。