Microsoft Research Community

Hello - I apologize up-front for the newbie question.  I'm trying to get started using the Z3 C API, and am looking for documentation for getting the environment situated, building, linking, and executing programs which use this API.  I'm on a windows machine and have LCC, but also Cygwin with GCC.  Any intro information would be extremely helpful.  

 Thanks very much.

 -Ben 

The release comes with an examples\c directory. Invoke the build.cmd script from that directory.

The build script assumes the Visual C++ compiler "cl" on your path. If you don't have Visual Studio, you can download one from http://www.microsoft.com/express/download/#webInstall

Thanks

Nikolaj

 I have trouble getting started.  I downloaded and installed Visual C++.  Is there a documentation on getting started?  Any small examples of creating and executing Z3? I feel lost on what should I do next in order to execute Z3.

 Thank you

Ewa

Try the following steps:

1. Download and install Z3.
2. Open "All Programs \ Microsoft Visual Studio (product version) \ Visual (product version) Studio Tools \ Visual Studio (product version) Command Prompt". With admininstrator privileges to make sure you have write access to the directory where Z3 is installed. You can run in admin mode by right clicking and selecting "Run as Administrator". In other words, go to the windows logo and select the "All Programs" button. Then select the visual studio distribution, under this there is a folder with tools where you will find a command tool. The command prompt that pops up will load the environment variables that supply the paths for visual studio include files and libraries and executables.
3. In the command prompt that opened do "cd C:\program files\Microsoft Research\Z3-1.3.6\examples\c". This brings you into a directory with a C program that exercises Z3's native C API. The sample is called test_capi.c.
4. Type "build.bat" This builds the sample called test_capi.c.
5. Type "copy ..\..\bin\z3.dll". The sample will not run without a reference to this DLL. Our installer does not register the DLL globally. You can register a DLL globally using regsvr32, but no need to do this.
6. Type "test_capi.exe"

You should then see the output:

 Z3 1.3.0.0

simple_example
CONTEXT:
Main clauses:
Learned clauses:
Transient clauses:
Asserted literals:
Assignment:
@true := @true
@false := @false
Disequalities:
Theory vars:
END OF CONTEXT

DeMorgan
DeMorgan is valid

find_model...... <snip>

Hope this helps

 Perfect! Thank you 

 Now I just need to play around with it to see if I can create my own example.

Ewa

 Just to complete for the future users

To successfuly run a single test example (for example DeMorgan):

•  Edit the test_capi.c file by removing all the following example functions and leave the demorgan() only
  
•     display_version()
•     simple_example()
•     find_model_example1()
•     find_model_example2()
•     prove_example1()
•     prove_example2()
•     push_pop_example1()
•     quantifier_example1()
•     array_example1()
•     array_example2()
•     array_example3()
•     tuple_example1()
•     bitvector_example1()
•     bitvector_example2()
•     eval_example1()
•     two_contexts_example1()
•     error_code_example1()
•     error_code_example2()
•     parser_example1()
•     parser_example2()
•     parser_example3()
•     parser_example4()
•     parser_example5()
•     ite_example()
•     simplifier_example()
•     traverse_term_example()
• Edit the main function to be the following:

• Save as a .c file anywhere on your system
• Copy the build.cmd file and z3.dll into the directory of your newly created .c file
• Edit build.cmd  I found that full path is better as I can easily move the build.cmd to another location for another project and just change the file name (here my file name is test.c).

            Ex:

            cl /I "D:\Program Files\Microsoft Research\Z3-1.3.6\include" "D:\Program Files\Microsoft Research\Z3-1.3.6\bin\z3.lib" test.c

• Run the compiler by running 'build' from the Visual Studio command line
• Run the .exe file it creates 
• The output is the following:

D:\Program Files\Microsoft Research\Z3-1.3.6\mytests>test.exe

DeMorgan
DeMorgan is valid

D:\Program Files\Microsoft Research\Z3-1.3.6\mytests>

Enjoy

Ewa