Merge pull request #984 from delcypher/cmake_doxygen

[CMake][Doxygen] Support building/installing API documentation and fix lots of bugs

CMakeLists.txt

@@ -43,10 +43,13 @@ message(STATUS "Z3 version ${Z3_VERSION}")
 # Set various useful variables depending on CMake version
 ################################################################################
 if (("${CMAKE_VERSION}" VERSION_EQUAL "3.2") OR ("${CMAKE_VERSION}" VERSION_GREATER "3.2"))
-  # In CMake >= 3.2 add_custom_command() supports a ``USES_TERMINAL`` argument
+  # In CMake >= 3.2 add_custom_command() and add_custom_target()
+  # supports a ``USES_TERMINAL`` argument
   set(ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG "USES_TERMINAL")
+  set(ADD_CUSTOM_TARGET_USES_TERMINAL_ARG "USES_TERMINAL")
 else()
   set(ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG "")
+  set(ADD_CUSTOM_TARGET_USES_TERMINAL_ARG "")
 endif()
 
 ################################################################################
@@ -528,3 +531,14 @@ option(ENABLE_EXAMPLE_TARGETS "Build Z3 api examples" ON)
 if (ENABLE_EXAMPLE_TARGETS)
   add_subdirectory(examples)
 endif()
+
+################################################################################
+# Documentation
+################################################################################
+option(BUILD_DOCUMENTATION "Build API documentation" OFF)
+if (BUILD_DOCUMENTATION)
+  message(STATUS "Building documentation enabled")
+  add_subdirectory(doc)
+else()
+  message(STATUS "Building documentation disabled")
+endif()

README-CMake.md

@@ -268,6 +268,7 @@ The following useful options can be passed to CMake whilst configuring.
 * ``CMAKE_INSTALL_PKGCONFIGDIR`` - STRING. The path to install pkgconfig files.
 * ``CMAKE_INSTALL_PYTHON_PKG_DIR`` - STRING. The path to install the z3 python bindings. This can be relative (to ``CMAKE_INSTALL_PREFIX``) or absolute.
 * ``CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR`` - STRING. The path to install CMake package files (e.g. ``/usr/lib/cmake/z3``).
+* ``CMAKE_INSTALL_API_BINDINGS_DOC`` - STRING. The path to install documentation for API bindings.
 * ``ENABLE_TRACING_FOR_NON_DEBUG`` - BOOL. If set to ``TRUE`` enable tracing in non-debug builds, if set to ``FALSE`` disable tracing in non-debug builds. Note in debug builds tracing is always enabled.
 * ``BUILD_LIBZ3_SHARED`` - BOOL. If set to ``TRUE`` build libz3 as a shared library otherwise build as a static library.
 * ``ENABLE_EXAMPLE_TARGETS`` - BOOL. If set to ``TRUE`` add the build targets for building the API examples.
@@ -286,6 +287,11 @@ The following useful options can be passed to CMake whilst configuring.
 * ``Z3_JAVA_JNI_LIB_INSTALLDIRR`` - STRING. The path to directory to install the Z3 Java JNI bridge library. This path should be relative to ``CMAKE_INSTALL_PREFIX``.
 * ``INCLUDE_GIT_DESCRIBE`` - BOOL. If set to ``TRUE`` and the source tree of Z3 is a git repository then the output of ``git describe`` will be included in the build.
 * ``INCLUDE_GIT_HASH`` - BOOL. If set to ``TRUE`` and the source tree of Z3 is a git repository then the git hash will be included in the build.
+* ``BUILD_DOCUMENTATION`` - BOOL. If set to ``TRUE`` then documentation for the API bindings can be built by invoking the ``api_docs`` target.
+* ``INSTALL_API_BINDINGS_DOCUMENTATION`` - BOOL. If set to ``TRUE`` and ``BUILD_DOCUMENTATION` is ``TRUE`` then documentation for API bindings will be installed
+    when running the ``install`` target.
+* ``ALWAYS_BUILD_DOCS`` - BOOL. If set to ``TRUE`` and ``BUILD_DOCUMENTATION`` is ``TRUE`` then documentation for API bindings will always be built.
+    Disabling this is useful for faster incremental builds. The documentation can be manually built by invoking the ``api_docs`` target.
 
 On the command line these can be passed to ``cmake`` using the ``-D`` option. In ``ccmake`` and ``cmake-gui`` these can be set in the user interface.
 
@@ -417,6 +423,7 @@ There are a few special targets:
 * ``clean`` all the built targets in the current directory and below
 * ``edit_cache`` will invoke one of the CMake tools (depending on which is available) to let you change configuration options.
 * ``rebuild_cache`` will reinvoke ``cmake`` for the project.
+* ``api_docs`` will build the documentation for the API bindings.
 
 ### Setting build type specific flags
 

contrib/cmake/doc/CMakeLists.txt

@@ -0,0 +1,93 @@
+find_package(Doxygen REQUIRED)
+message(STATUS "DOXYGEN_EXECUTABLE: \"${DOXYGEN_EXECUTABLE}\"")
+message(STATUS "DOXYGEN_VERSION: \"${DOXYGEN_VERSION}\"")
+
+set(DOC_DEST_DIR "${CMAKE_CURRENT_BINARY_DIR}/api")
+set(DOC_TEMP_DIR "${CMAKE_CURRENT_BINARY_DIR}/temp")
+set(MK_API_DOC_SCRIPT "${CMAKE_CURRENT_SOURCE_DIR}/mk_api_doc.py")
+
+set(PYTHON_API_OPTIONS "")
+set(DOTNET_API_OPTIONS "")
+set(JAVA_API_OPTIONS "")
+SET(DOC_EXTRA_DEPENDS "")
+
+if (BUILD_PYTHON_BINDINGS)
+  # FIXME: Don't hard code this path
+  list(APPEND PYTHON_API_OPTIONS "--z3py-package-path" "${CMAKE_BINARY_DIR}/python/z3")
+  list(APPEND DOC_EXTRA_DEPENDS "build_z3_python_bindings")
+else()
+  list(APPEND PYTHON_API_OPTIONS "--no-z3py")
+endif()
+
+if (BUILD_DOTNET_BINDINGS)
+  # FIXME: Don't hard code these paths
+  list(APPEND DOTNET_API_OPTIONS "--dotnet-search-paths"
+    "${CMAKE_SOURCE_DIR}/src/api/dotnet"
+    "${CMAKE_BINARY_DIR}/src/api/dotnet"
+  )
+  list(APPEND DOC_EXTRA_DEPENDS "build_z3_dotnet_bindings")
+else()
+  list(APPEND DOTNET_API_OPTIONS "--no-dotnet")
+endif()
+
+if (BUILD_JAVA_BINDINGS)
+  # FIXME: Don't hard code these paths
+  list(APPEND JAVA_API_OPTIONS "--java-search-paths"
+    "${CMAKE_SOURCE_DIR}/src/api/java"
+    "${CMAKE_BINARY_DIR}/src/api/java"
+  )
+  list(APPEND DOC_EXTRA_DEPENDS "build_z3_java_bindings")
+else()
+  list(APPEND JAVA_API_OPTIONS "--no-java")
+endif()
+
+option(ALWAYS_BUILD_DOCS "Always build documentation for API bindings" ON)
+if (ALWAYS_BUILD_DOCS)
+  set(ALWAYS_BUILD_DOCS_ARG "ALL")
+else()
+  set(ALWAYS_BUILD_DOCS_ARG "")
+  # FIXME: This sucks but there doesn't seem to be a way to make the top level
+  # install target depend on the `api_docs` target.
+  message(WARNING "Building documentation for API bindings is not part of the"
+    " all target. This may result in stale files being installed when running"
+    " the install target. You should run the api_docs target before running"
+    " the install target. Alternatively Set ALWAYS_BUILD_DOCS to ON to"
+    " automatically build documentation when running the install target."
+  )
+endif()
+
+add_custom_target(api_docs ${ALWAYS_BUILD_DOCS_ARG}
+  COMMAND
+  "${PYTHON_EXECUTABLE}" "${MK_API_DOC_SCRIPT}"
+  --doxygen-executable "${DOXYGEN_EXECUTABLE}"
+  --output-dir "${DOC_DEST_DIR}"
+  --temp-dir "${DOC_TEMP_DIR}"
+  ${PYTHON_API_OPTIONS}
+  ${DOTNET_API_OPTIONS}
+  ${JAVA_API_OPTIONS}
+  DEPENDS
+    ${DOC_EXTRA_DEPENDS}
+  BYPRODUCTS "${DOC_DEST_DIR}"
+  COMMENT "Generating documentation"
+  ${ADD_CUSTOM_TARGET_USES_TERMINAL_ARG}
+)
+
+# Remove generated documentation when running `clean` target.
+set_property(DIRECTORY APPEND PROPERTY
+  ADDITIONAL_MAKE_CLEAN_FILES
+  "${DOC_DEST_DIR}"
+)
+
+option(INSTALL_API_BINDINGS_DOCUMENTATION "Install documentation for API bindings" ON)
+set(CMAKE_INSTALL_API_BINDINGS_DOC
+  "${CMAKE_INSTALL_DOCDIR}"
+  CACHE
+  PATH
+  "Path to install documentation for API bindings"
+)
+if (INSTALL_API_BINDINGS_DOCUMENTATION)
+  install(
+    DIRECTORY "${DOC_DEST_DIR}"
+    DESTINATION "${CMAKE_INSTALL_API_BINDINGS_DOC}"
+  )
+endif()

doc/mk_api_doc.py

@@ -1,5 +1,9 @@
 # Copyright (c) Microsoft Corporation 2015
+"""
+Z3 API documentation generator script
+"""
 
+import argparse
 import os
 import shutil
 import re
@@ -11,124 +15,291 @@ import shutil
 
 ML_ENABLED=False
 BUILD_DIR='../build'
-
+DOXYGEN_EXE='doxygen'
-def display_help(exit_code):
+TEMP_DIR=os.path.join(os.getcwd(), 'tmp')
-    print("mk_api_doc.py: Z3 documentation generator\n")
+OUTPUT_DIRECTORY=os.path.join(os.getcwd(), 'api')
-    print("\nOptions:")
+Z3PY_PACKAGE_PATH='../src/api/python/z3'
-    print("  -h, --help                    display this message.")
+Z3PY_ENABLED=True
-    print("  -b <subdir>, --build=<subdir> subdirectory where Z3 is built (default: ../build).")
+DOTNET_ENABLED=True
-    print("  --ml                          include ML/OCaml API documentation.")
+JAVA_ENABLED=True
+DOTNET_API_SEARCH_PATHS=['../src/api/dotnet']
+JAVA_API_SEARCH_PATHS=['../src/api/java']
+SCRIPT_DIR=os.path.abspath(os.path.dirname(__file__))
 
 def parse_options():
-    global ML_ENABLED, BUILD_DIR
+    global ML_ENABLED, BUILD_DIR, DOXYGEN_EXE, TEMP_DIR, OUTPUT_DIRECTORY
-
+    global Z3PY_PACKAGE_PATH, Z3PY_ENABLED, DOTNET_ENABLED, JAVA_ENABLED
-    try:
+    global DOTNET_API_SEARCH_PATHS, JAVA_API_SEARCH_PATHS
-        options, remainder = getopt.gnu_getopt(sys.argv[1:],
+    parser = argparse.ArgumentParser(description=__doc__)
-                                               'b:h',
+    parser.add_argument('-b',
-                                               ['build=', 'help', 'ml'])
+        '--build',
-    except:
+        default=BUILD_DIR,
-        print("ERROR: Invalid command line option")
+        help='Directory where Z3 is built (default: %(default)s)',
-        display_help(1)
+    )
-
+    parser.add_argument('--ml',
-    for opt, arg in options:
+        action='store_true',
-        if opt in ('-b', '--build'):
+        default=False,
-            BUILD_DIR = mk_util.norm_path(arg)
+        help='Include ML/OCaml API documentation'
-        elif opt in ('h', '--help'):
+    )
-            display_help()
+    parser.add_argument('--doxygen-executable',
-            exit(1)
+        dest='doxygen_executable',
-        elif opt in ('--ml'):
+        default=DOXYGEN_EXE,
-            ML_ENABLED=True
+        help='Doxygen executable to use (default: %(default)s)',
-        else:
+    )
-            print("ERROR: Invalid command line option: %s" % opt)
+    parser.add_argument('--temp-dir',
-            display_help(1)
+        dest='temp_dir',
-
+        default=TEMP_DIR,
-
+        help='Path to directory to use as temporary directory. '
-
+             '(default: %(default)s)',
+    )
+    parser.add_argument('--output-dir',
+        dest='output_dir',
+        default=OUTPUT_DIRECTORY,
+        help='Path to output directory (default: %(default)s)',
+    )
+    parser.add_argument('--z3py-package-path',
+        dest='z3py_package_path',
+        default=Z3PY_PACKAGE_PATH,
+        help='Path to directory containing Z3py package (default: %(default)s)',
+    )
+    # FIXME: I would prefer not to have negative options (i.e.  `--z3py`
+    # instead of `--no-z3py`) but historically these bindings have been on by
+    # default so we have options to disable generating documentation for these
+    # bindings rather than enable them.
+    parser.add_argument('--no-z3py',
+        dest='no_z3py',
+        action='store_true',
+        default=False,
+        help='Do not generate documentation for Python bindings',
+    )
+    parser.add_argument('--no-dotnet',
+        dest='no_dotnet',
+        action='store_true',
+        default=False,
+        help='Do not generate documentation for .NET bindings',
+    )
+    parser.add_argument('--no-java',
+        dest='no_java',
+        action='store_true',
+        default=False,
+        help='Do not generate documentation for Java bindings',
+    )
+    parser.add_argument('--dotnet-search-paths',
+        dest='dotnet_search_paths',
+        nargs='+',
+        default=DOTNET_API_SEARCH_PATHS,
+        help='Specify one or more path to look for .NET files (default: %(default)s).',
+    )
+    parser.add_argument('--java-search-paths',
+        dest='java_search_paths',
+        nargs='+',
+        default=JAVA_API_SEARCH_PATHS,
+        help='Specify one or more paths to look for Java files (default: %(default)s).',
+    )
+    pargs = parser.parse_args()
+    ML_ENABLED = pargs.ml
+    BUILD_DIR = pargs.build
+    DOXYGEN_EXE = pargs.doxygen_executable
+    TEMP_DIR = pargs.temp_dir
+    OUTPUT_DIRECTORY = pargs.output_dir
+    Z3PY_PACKAGE_PATH = pargs.z3py_package_path
+    if not os.path.exists(Z3PY_PACKAGE_PATH):
+        raise Exception('"{}" does not exist'.format(Z3PY_PACKAGE_PATH))
+    if not os.path.basename(Z3PY_PACKAGE_PATH) == 'z3':
+        raise Exception('"{}" does not end with "z3"'.format(Z3PY_PACKAGE_PATH))
+    Z3PY_ENABLED = not pargs.no_z3py
+    DOTNET_ENABLED = not pargs.no_dotnet
+    JAVA_ENABLED = not pargs.no_java
+    DOTNET_API_SEARCH_PATHS = pargs.dotnet_search_paths
+    JAVA_API_SEARCH_PATHS = pargs.java_search_paths
+    return
 
 def mk_dir(d):
     if not os.path.exists(d):
         os.makedirs(d)
 
-# Eliminate def_API and extra_API directives from file 'inf'.
+# Eliminate def_API, extra_API, and def_Type directives from file 'inf'.
 # The result is stored in 'outf'.
 def cleanup_API(inf, outf):
     pat1  = re.compile(".*def_API.*")
     pat2  = re.compile(".*extra_API.*")
+    pat3  = re.compile(r".*def_Type\(.*")
     _inf  = open(inf, 'r')
     _outf = open(outf, 'w')
     for line in _inf:
-        if not pat1.match(line) and not pat2.match(line):
+        if not pat1.match(line) and not pat2.match(line) and not pat3.match(line):
             _outf.write(line)
 
+def configure_file(template_file_path, output_file_path, substitutions):
+    """
+        Read a template file ``template_file_path``, perform substitutions
+        found in the ``substitutions`` dictionary and write the result to
+        the output file ``output_file_path``.
+
+        The template file should contain zero or more template strings of the
+        form ``@NAME@``.
+
+        The substitutions dictionary maps old strings (without the ``@``
+        symbols) to their replacements.
+    """
+    assert isinstance(template_file_path, str)
+    assert isinstance(output_file_path, str)
+    assert isinstance(substitutions, dict)
+    assert len(template_file_path) > 0
+    assert len(output_file_path) > 0
+    print("Generating {} from {}".format(output_file_path, template_file_path))
+
+    if not os.path.exists(template_file_path):
+        raise Exception('Could not find template file "{}"'.format(template_file_path))
+
+    # Read whole template file into string
+    template_string = None
+    with open(template_file_path, 'r') as f:
+        template_string = f.read()
+
+    # Do replacements
+    for (old_string, replacement) in substitutions.items():
+        template_string = template_string.replace('@{}@'.format(old_string), replacement)
+
+    # Write the string to the file
+    with open(output_file_path, 'w') as f:
+        f.write(template_string)
+
 try:
     parse_options()
 
-    fi = open('website.dox', 'r')
+    print("Creating temporary directory \"{}\"".format(TEMP_DIR))
-    fo = open('website-adj.dox', 'w')
+    mk_dir(TEMP_DIR)
+    # Short-hand for path to temporary file
+    def temp_path(path):
+        return os.path.join(TEMP_DIR, path)
+    # Short-hand for path to file in `doc` directory
+    def doc_path(path):
+        return os.path.join(SCRIPT_DIR, path)
 
-    for line in fi:
+    # Create configuration file from template
-        if (line != '[ML]\n'):
+    doxygen_config_substitutions = {
-            fo.write(line)
+        'OUTPUT_DIRECTORY': OUTPUT_DIRECTORY,
-        elif (ML_ENABLED):
+        'TEMP_DIR': TEMP_DIR,
-            fo.write('   - <a class="el" href="ml/index.html">ML/OCaml API</a>\n')
+        'CXX_API_SEARCH_PATHS': doc_path('../src/api/c++'),
-    fi.close()
+    }
-    fo.close()
 
-    mk_dir('api/html')
+    if Z3PY_ENABLED:
-    mk_dir('tmp')
+        print("Z3Py documentation enabled")
-    shutil.copyfile('website-adj.dox', 'tmp/website.dox')
+        doxygen_config_substitutions['PYTHON_API_FILES'] = 'z3.py'
-    os.remove('website-adj.dox')
+    else:
-    shutil.copyfile('../src/api/python/z3/z3.py', 'tmp/z3py.py')
+        print("Z3Py documentation disabled")
-    cleanup_API('../src/api/z3_api.h', 'tmp/z3_api.h')
+        doxygen_config_substitutions['PYTHON_API_FILES'] = ''
-    cleanup_API('../src/api/z3_ast_containers.h', 'tmp/z3_ast_containers.h')
+    if DOTNET_ENABLED:
-    cleanup_API('../src/api/z3_algebraic.h', 'tmp/z3_algebraic.h')
+        print(".NET documentation enabled")
-    cleanup_API('../src/api/z3_polynomial.h', 'tmp/z3_polynomial.h')
+        doxygen_config_substitutions['DOTNET_API_FILES'] = '*.cs'
-    cleanup_API('../src/api/z3_rcf.h', 'tmp/z3_rcf.h')
+        dotnet_api_search_path_str = ""
-    cleanup_API('../src/api/z3_fixedpoint.h', 'tmp/z3_fixedpoint.h')
+        for p in DOTNET_API_SEARCH_PATHS:
-    cleanup_API('../src/api/z3_optimization.h', 'tmp/z3_optimization.h')
+            # Quote path so that paths with spaces are handled correctly
-    cleanup_API('../src/api/z3_interp.h', 'tmp/z3_interp.h')
+            dotnet_api_search_path_str += "\"{}\" ".format(p)
-    cleanup_API('../src/api/z3_fpa.h', 'tmp/z3_fpa.h')
+        doxygen_config_substitutions['DOTNET_API_SEARCH_PATHS'] = dotnet_api_search_path_str
+    else:
+        print(".NET documentation disabled")
+        doxygen_config_substitutions['DOTNET_API_FILES'] = ''
+        doxygen_config_substitutions['DOTNET_API_SEARCH_PATHS'] = ''
+    if JAVA_ENABLED:
+        print("Java documentation enabled")
+        doxygen_config_substitutions['JAVA_API_FILES'] = '*.java'
+        java_api_search_path_str = ""
+        for p in JAVA_API_SEARCH_PATHS:
+            # Quote path so that paths with spaces are handled correctly
+            java_api_search_path_str += "\"{}\" ".format(p)
+        doxygen_config_substitutions['JAVA_API_SEARCH_PATHS'] = java_api_search_path_str
+    else:
+        print("Java documentation disabled")
+        doxygen_config_substitutions['JAVA_API_FILES'] = ''
+        doxygen_config_substitutions['JAVA_API_SEARCH_PATHS'] = ''
+
+    doxygen_config_file = temp_path('z3api.cfg')
+    configure_file(
+        doc_path('z3api.cfg.in'),
+        doxygen_config_file,
+        doxygen_config_substitutions)
+
+    website_dox_substitutions = {}
+    bullet_point_prefix='\n   - '
+    if Z3PY_ENABLED:
+        website_dox_substitutions['PYTHON_API'] = (
+            '{prefix}<a class="el" href="namespacez3py.html">Python API</a> '
+            '(also available in <a class="el" href="z3.html">pydoc format</a>)'
+            ).format(
+                prefix=bullet_point_prefix)
+    else:
+        website_dox_substitutions['PYTHON_API'] = ''
+    if DOTNET_ENABLED:
+        website_dox_substitutions['DOTNET_API'] = (
+            '{prefix}'
+            '<a class="el" href="namespace_microsoft_1_1_z3.html">'
+            '.NET API</a>').format(
+                prefix=bullet_point_prefix)
+    else:
+        website_dox_substitutions['DOTNET_API'] = ''
+    if JAVA_ENABLED:
+        website_dox_substitutions['JAVA_API'] = (
+            '{prefix}<a class="el" href="namespacecom_1_1microsoft_1_1z3.html">'
+            'Java API</a>').format(
+                prefix=bullet_point_prefix)
+    else:
+        website_dox_substitutions['JAVA_API'] = ''
+    if ML_ENABLED:
+        website_dox_substitutions['OCAML_API'] = (
+            '<a class="el" href="ml/index.html">ML/OCaml API</a>'
+            ).format(
+                prefix=bullet_point_prefix)
+    else:
+        website_dox_substitutions['OCAML_API'] = ''
+    configure_file(
+        doc_path('website.dox.in'),
+        temp_path('website.dox'),
+        website_dox_substitutions)
+
+    mk_dir(os.path.join(OUTPUT_DIRECTORY, 'html'))
+    if Z3PY_ENABLED:
+        shutil.copyfile(doc_path('../src/api/python/z3/z3.py'), temp_path('z3py.py'))
+    cleanup_API(doc_path('../src/api/z3_api.h'), temp_path('z3_api.h'))
+    cleanup_API(doc_path('../src/api/z3_ast_containers.h'), temp_path('z3_ast_containers.h'))
+    cleanup_API(doc_path('../src/api/z3_algebraic.h'), temp_path('z3_algebraic.h'))
+    cleanup_API(doc_path('../src/api/z3_polynomial.h'), temp_path('z3_polynomial.h'))
+    cleanup_API(doc_path('../src/api/z3_rcf.h'), temp_path('z3_rcf.h'))
+    cleanup_API(doc_path('../src/api/z3_fixedpoint.h'), temp_path('z3_fixedpoint.h'))
+    cleanup_API(doc_path('../src/api/z3_optimization.h'), temp_path('z3_optimization.h'))
+    cleanup_API(doc_path('../src/api/z3_interp.h'), temp_path('z3_interp.h'))
+    cleanup_API(doc_path('../src/api/z3_fpa.h'), temp_path('z3_fpa.h'))
 
     print("Removed annotations from z3_api.h.")
     try:
-        if subprocess.call(['doxygen', 'z3api.dox']) != 0:
+        if subprocess.call([DOXYGEN_EXE, doxygen_config_file]) != 0:
             print("ERROR: doxygen returned nonzero return code")
             exit(1)
     except:
         print("ERROR: failed to execute 'doxygen', make sure doxygen (http://www.doxygen.org) is available in your system.")
         exit(1)
-    print("Generated C and .NET API documentation.")
+    print("Generated Doxygen based documentation")
-    os.remove('tmp/z3_api.h')
+    shutil.rmtree(os.path.realpath(TEMP_DIR))
-    os.remove('tmp/z3_ast_containers.h')
+    print("Removed temporary directory \"{}\"".format(TEMP_DIR))
-    os.remove('tmp/z3_algebraic.h')
+    if Z3PY_ENABLED:
-    os.remove('tmp/z3_polynomial.h')
+        # Put z3py at the beginning of the search path to try to avoid picking up
-    os.remove('tmp/z3_rcf.h')
+        # an installed copy of Z3py.
-    os.remove('tmp/z3_fixedpoint.h')
+        sys.path.insert(0, os.path.dirname(Z3PY_PACKAGE_PATH))
-    os.remove('tmp/z3_optimization.h')
+        pydoc.writedoc('z3')
-    os.remove('tmp/z3_interp.h')
+        shutil.move('z3.html', os.path.join(OUTPUT_DIRECTORY, 'html', 'z3.html'))
-    os.remove('tmp/z3_fpa.h')
+        print("Generated pydoc Z3Py documentation.")
-    print("Removed temporary file header files.")
-
-    os.remove('tmp/website.dox')
-    print("Removed temporary file website.dox")
-    os.remove('tmp/z3py.py')
-    print("Removed temporary file z3py.py")
-    os.removedirs('tmp')
-    print("Removed temporary directory tmp.")
-    sys.path.append('../src/api/python/z3')
-    pydoc.writedoc('z3')
-    shutil.move('z3.html', 'api/html/z3.html')
-    print("Generated Python documentation.")
 
     if ML_ENABLED:
-        mk_dir('api/html/ml')
+        ml_output_dir = os.path.join(OUTPUT_DIRECTORY, 'html', 'ml')
-        if subprocess.call(['ocamldoc', '-html', '-d', 'api\html\ml', '-sort', '-hide', 'Z3', '-I', '%s/api/ml' % BUILD_DIR, '../src/api/ml/z3enums.mli', '../src/api/ml/z3.mli']) != 0:
+        mk_dir(ml_output_dir)
+        if subprocess.call(['ocamldoc', '-html', '-d', ml_output_dir, '-sort', '-hide', 'Z3', '-I', '%s/api/ml' % BUILD_DIR, doc_path('../src/api/ml/z3enums.mli'), doc_path('../src/api/ml/z3.mli')]) != 0:
             print("ERROR: ocamldoc failed.")
             exit(1)
         print("Generated ML/OCaml documentation.")
 
-    print("Documentation was successfully generated at subdirectory './api/html'.")
+    print("Documentation was successfully generated at subdirectory '{}'.".format(OUTPUT_DIRECTORY))
-except:
+except Exception:
     exctype, value = sys.exc_info()[:2]
     print("ERROR: failed to generate documentation: %s" % value)
     exit(1)

doc/website.dox.in

@@ -11,10 +11,6 @@
    This website hosts the automatically generated documentation for the Z3 APIs.
 
    - \ref capi
-   - \ref cppapi
+   - \ref cppapi @DOTNET_API@ @JAVA_API@ @PYTHON_API@ @OCAML_API@
-   - <a class="el" href="class_microsoft_1_1_z3_1_1_context.html">.NET API</a>
-   - <a class="el" href="namespacecom_1_1microsoft_1_1z3.html">Java API</a>
-   - <a class="el" href="namespacez3py.html">Python API</a> (also available in <a class="el" href="z3.html">pydoc format</a>)
-[ML]
    - Try Z3 online at <a href="http://rise4fun.com/z3">RiSE4Fun</a>.
 */

doc/z3api.cfg.in

@@ -52,7 +52,7 @@ PROJECT_LOGO           =
 # If a relative path is entered, it will be relative to the location
 # where doxygen was started. If left blank the current directory will be used.
 
-OUTPUT_DIRECTORY       = api
+OUTPUT_DIRECTORY       = "@OUTPUT_DIRECTORY@"
 
 # If the CREATE_SUBDIRS tag is set to YES, then doxygen will create
 # 4096 sub-directories (in 2 levels) under the output directory of each output
@@ -681,10 +681,9 @@ WARN_LOGFILE           =
 # directories like "/usr/src/myproject". Separate the files or directories
 # with spaces.
 
-INPUT                  = ../src/api/dotnet \
+INPUT                  = "@TEMP_DIR@" \
-                         ../src/api/java \
+                         "@CXX_API_SEARCH_PATHS@" \
-                         ../src/api/c++ \
+                         @DOTNET_API_SEARCH_PATHS@ @JAVA_API_SEARCH_PATHS@
-                         ./tmp
 
 # This tag can be used to specify the character encoding of the source files
 # that doxygen parses. Internally doxygen uses the UTF-8 encoding, which is
@@ -703,16 +702,14 @@ INPUT_ENCODING         = UTF-8
 # *.f90 *.f *.for *.vhd *.vhdl
 
 FILE_PATTERNS          = website.dox \
-			 z3_api.h \
+                         z3_api.h \
-			 z3_algebraic.h \
+                         z3_algebraic.h \
-			 z3_polynomial.h \
+                         z3_polynomial.h \
-			 z3_rcf.h \
+                         z3_rcf.h \
-			 z3_interp.h \
+                         z3_interp.h \
-			 z3_fpa.h \
+                         z3_fpa.h \
                          z3++.h \
-                         z3py.py \
+                         @PYTHON_API_FILES@ @DOTNET_API_FILES@ @JAVA_API_FILES@
-						 *.cs \
-                         *.java
 
 # The RECURSIVE tag can be used to turn specify whether or not subdirectories
 # should be searched for input files as well. Possible values are YES and NO.

src/api/z3_api.h

@@ -1500,7 +1500,7 @@ extern "C" {
        All main interaction with Z3 happens in the context of a \c Z3_context.
 
        In contrast to #Z3_mk_context_rc, the life time of Z3_ast objects
-       are determined by the scope level of #Z3_push and #Z3_pop.
+       are determined by the scope level of #Z3_solver_push and #Z3_solver_pop.
        In other words, a Z3_ast object remains valid until there is a
        call to Z3_pop that takes the current scope below the level where
        the object was created.
@@ -3091,8 +3091,8 @@ extern "C" {
        \brief Create a numeral of a given sort.
 
        \param c logical context.
-       \param numeral A string representing the numeral value in decimal notation. The string may be of the form \code{[num]*[.[num]*][E[+|-][num]+]}.
+       \param numeral A string representing the numeral value in decimal notation. The string may be of the form `[num]*[.[num]*][E[+|-][num]+]`.
-                      If the given sort is a real, then the numeral can be a rational, that is, a string of the form \ccode{[num]* / [num]*}.
+                      If the given sort is a real, then the numeral can be a rational, that is, a string of the form `[num]* / [num]*` .
        \param ty The sort of the numeral. In the current implementation, the given sort can be an int, real, finite-domain, or bit-vectors of arbitrary size.
 
        \sa Z3_mk_int
@@ -3306,7 +3306,7 @@ extern "C" {
     Z3_ast Z3_API Z3_mk_seq_replace(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst);
 
     /**
-       \brief Retrieve from \s the unit sequence positioned at position \c index.
+       \brief Retrieve from \c s the unit sequence positioned at position \c index.
 
        def_API('Z3_mk_seq_at' ,AST ,(_in(CONTEXT), _in(AST), _in(AST)))
      */