Appendix: IDP-Z3 internal referenceΒΆ


This reference is only intended for the core IDP-Z3 development team. If you do not work on the IDP-Z3 engine itself, but just want to use it in your applications, please use our Python API instead.

The components of IDP-Z3 are shown below.

graph TD webIDE_client --> IDP-Z3_server Interactive_consultant_client --> IDP-Z3_server Read_the_docs Homepage IDP-Z3_server --> IDP-Z3_engine IDP-Z3_command_line --> IDP-Z3_engine IDP-Z3_engine --> Z3
  • webIDE client: browser-based application to edit and run IDP-Z3 programs

  • Interactive Consultant client: browser-based user-friendly decision support application

  • Read_the_docs : online documentation

  • Homepage

  • IDP-Z3 server: web server for both web applications

  • IDP-Z3 command line interface

  • IDP-Z3 engine: performs reasoning on IDP-Z3 theories

  • Z3: SMT solver developed by Microsoft

The source code of IDP-Z3 is publicly available under the GNU LGPL v3 license. You may want to check the Development and deployment guide.