CODEWITHSUNDEEP
z3
Motorhead
Motorhead

Reputation: 968

.Net API for accessing MuZ

The tutorial at rise4fun mentions a .Net API for accessing MuZ. However, clicking on any of the mentioned methods, eg To add a rule, call: Z3_datalog_add_rule leads to a dead link. Where are these methods described and are they currently supported?

Also, not directly related to this question, but i notice that the examples, which presumably use the SMT-LIB API use a define-fun command. Is there an equivalent function available in the .Net API?

thanks

Upvotes: 0

Views: 168

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

Thanks for reporting the broken links.

The link: 

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

Should have pointed to:

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

The corresponding link to .NET API functions is:

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

Note that in the latest versions of Z3, the .NET API has undergone significant revisions over the version used in rise4fun. The link above describes the up-to-date .NET API. A link to the "legacy" .NET API used in previous versions of Z3 is: 

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

These links are collected on: http://research.microsoft.com/en-us/um/redmond/projects/z3/

The declare functions, the .NET API in the newest version is called "MkFuncDecl". It is a method on a context object. It has several overloads:

 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)

The second link mentioned above takes you to the documentation for these functions.

Upvotes: 1

Related Questions