。用於訪問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已經對使用的版本進行了重大修改4fun。 上面的鏈接描述了最新的.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) 

上面提到的第二個鏈接帶你到這些函數的文檔。