Appendix: IDP-Z3 developer referenceΒΆ


The contents of this reference are intended for people who want to further develop IDP-Z3.


Despite our best efforts, this documentation may not be complete and up-to-date.

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.