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_solver IDP-Z3_command_line --> IDP-Z3_solver IDP-Z3_solver --> 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 solver: performs inferences 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.