From 81ba729aab8d2181244de354f0bdb1ea8415691a Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 24 Apr 2017 15:25:45 +0100 Subject: [PATCH 01/41] [Doxygen] Fix script `--help` functionality. --- doc/mk_api_doc.py | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index edabcbd1b..bb5a19e5f 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -13,11 +13,13 @@ ML_ENABLED=False BUILD_DIR='../build' def display_help(exit_code): + assert isinstance(exit_code, int) print("mk_api_doc.py: Z3 documentation generator\n") print("\nOptions:") print(" -h, --help display this message.") print(" -b , --build= subdirectory where Z3 is built (default: ../build).") print(" --ml include ML/OCaml API documentation.") + sys.exit(exit_code) def parse_options(): global ML_ENABLED, BUILD_DIR @@ -34,8 +36,7 @@ def parse_options(): if opt in ('-b', '--build'): BUILD_DIR = mk_util.norm_path(arg) elif opt in ('h', '--help'): - display_help() - exit(1) + display_help(0) elif opt in ('--ml'): ML_ENABLED=True else: @@ -128,7 +129,7 @@ try: print("Generated ML/OCaml documentation.") print("Documentation was successfully generated at subdirectory './api/html'.") -except: +except Exception: exctype, value = sys.exc_info()[:2] print("ERROR: failed to generate documentation: %s" % value) exit(1) From ca678c3675a7aa1bd5b396b15660b7ab1163c193 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 24 Apr 2017 15:45:57 +0100 Subject: [PATCH 02/41] [Doxygen] Fix bug where `def_Type` directives in `z3.h` would appear in generated doxygen documentation. --- doc/mk_api_doc.py | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index bb5a19e5f..e86205a7a 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -50,15 +50,16 @@ 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) try: From 2cdb45605dcc3f17d0101f9669fb6ad8a4923e83 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 24 Apr 2017 16:24:15 +0100 Subject: [PATCH 03/41] [Doxygen] Switch to using `argparse` to parse command line arguments in `mk_api_doc.py`. Given that we need to add a bunch of new command line options it makes sense to use a less clumsy and concise API. --- doc/mk_api_doc.py | 50 ++++++++++++++++++----------------------------- 1 file changed, 19 insertions(+), 31 deletions(-) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index e86205a7a..d27351015 100644 --- a/doc/mk_api_doc.py +++ b/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 @@ -12,39 +16,23 @@ import shutil ML_ENABLED=False BUILD_DIR='../build' -def display_help(exit_code): - assert isinstance(exit_code, int) - print("mk_api_doc.py: Z3 documentation generator\n") - print("\nOptions:") - print(" -h, --help display this message.") - print(" -b , --build= subdirectory where Z3 is built (default: ../build).") - print(" --ml include ML/OCaml API documentation.") - sys.exit(exit_code) - def parse_options(): global ML_ENABLED, BUILD_DIR - - try: - options, remainder = getopt.gnu_getopt(sys.argv[1:], - 'b:h', - ['build=', 'help', 'ml']) - except: - print("ERROR: Invalid command line option") - display_help(1) - - for opt, arg in options: - if opt in ('-b', '--build'): - BUILD_DIR = mk_util.norm_path(arg) - elif opt in ('h', '--help'): - display_help(0) - elif opt in ('--ml'): - ML_ENABLED=True - else: - print("ERROR: Invalid command line option: %s" % opt) - display_help(1) - - - + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('-b', + '--build', + default=BUILD_DIR, + help='Directory where Z3 is built (default: %(default)s)', + ) + parser.add_argument('--ml', + action='store_true', + default=False, + help='Include ML/OCaml API documentation' + ) + pargs = parser.parse_args() + ML_ENABLED = pargs.ml + BUILD_DIR = pargs.build + return def mk_dir(d): if not os.path.exists(d): From 8a1df3df6293b5f8ac9be6d42d8ba6f23d708864 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 24 Apr 2017 21:52:59 +0100 Subject: [PATCH 04/41] [Doxygen] Add `--doxygen-executable` command line option to `mk_api_doc.py`. This allows a custom path to Doxygen to be specified. --- doc/mk_api_doc.py | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index d27351015..62130d73c 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -15,9 +15,10 @@ import shutil ML_ENABLED=False BUILD_DIR='../build' +DOXYGEN_EXE='doxygen' def parse_options(): - global ML_ENABLED, BUILD_DIR + global ML_ENABLED, BUILD_DIR, DOXYGEN_EXE parser = argparse.ArgumentParser(description=__doc__) parser.add_argument('-b', '--build', @@ -29,9 +30,15 @@ def parse_options(): default=False, help='Include ML/OCaml API documentation' ) + parser.add_argument('--doxygen-executable', + dest='doxygen_executable', + default=DOXYGEN_EXE, + help='Doxygen executable to use (default: %(default)s)', + ) pargs = parser.parse_args() ML_ENABLED = pargs.ml BUILD_DIR = pargs.build + DOXYGEN_EXE = pargs.doxygen_executable return def mk_dir(d): @@ -81,7 +88,7 @@ try: print("Removed annotations from z3_api.h.") try: - if subprocess.call(['doxygen', 'z3api.dox']) != 0: + if subprocess.call([DOXYGEN_EXE, 'z3api.dox']) != 0: print("ERROR: doxygen returned nonzero return code") exit(1) except: From 5f7ae920c6758f1b359fc1827b8492b750243e4b Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 24 Apr 2017 22:25:51 +0100 Subject: [PATCH 05/41] [Doxygen] Teach `mk_api_doc.py` a new command line option (`--temp-dir`) which allows the location of the temporary directory to be controlled. While I'm here also write `website.dox` into the temporary directory where it belongs instead of in the source tree and simplify the logic that deletes the temporary directory and its contents. --- doc/mk_api_doc.py | 61 ++++++++++++++++++++++------------------------- 1 file changed, 29 insertions(+), 32 deletions(-) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index 62130d73c..a8ee1e220 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -16,9 +16,10 @@ import shutil ML_ENABLED=False BUILD_DIR='../build' DOXYGEN_EXE='doxygen' +TEMP_DIR=os.path.join(os.getcwd(), 'tmp') def parse_options(): - global ML_ENABLED, BUILD_DIR, DOXYGEN_EXE + global ML_ENABLED, BUILD_DIR, DOXYGEN_EXE, TEMP_DIR parser = argparse.ArgumentParser(description=__doc__) parser.add_argument('-b', '--build', @@ -35,10 +36,17 @@ def parse_options(): default=DOXYGEN_EXE, help='Doxygen executable to use (default: %(default)s)', ) + parser.add_argument('--temp-dir', + dest='temp_dir', + default=TEMP_DIR, + help='Path to directory to use as temporary directory. ' + '(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 return def mk_dir(d): @@ -60,8 +68,14 @@ def cleanup_API(inf, outf): try: parse_options() + print("Creating temporary directory \"{}\"".format(TEMP_DIR)) + mk_dir(TEMP_DIR) + # Short-hand for path to temporary file + def temp_path(path): + return os.path.join(TEMP_DIR, path) + fi = open('website.dox', 'r') - fo = open('website-adj.dox', 'w') + fo = open(temp_path('website.dox'), 'w') for line in fi: if (line != '[ML]\n'): @@ -71,20 +85,18 @@ try: fi.close() fo.close() + mk_dir('api/html') - mk_dir('tmp') - shutil.copyfile('website-adj.dox', 'tmp/website.dox') - os.remove('website-adj.dox') - shutil.copyfile('../src/api/python/z3/z3.py', 'tmp/z3py.py') - cleanup_API('../src/api/z3_api.h', 'tmp/z3_api.h') - cleanup_API('../src/api/z3_ast_containers.h', 'tmp/z3_ast_containers.h') - cleanup_API('../src/api/z3_algebraic.h', 'tmp/z3_algebraic.h') - cleanup_API('../src/api/z3_polynomial.h', 'tmp/z3_polynomial.h') - cleanup_API('../src/api/z3_rcf.h', 'tmp/z3_rcf.h') - cleanup_API('../src/api/z3_fixedpoint.h', 'tmp/z3_fixedpoint.h') - cleanup_API('../src/api/z3_optimization.h', 'tmp/z3_optimization.h') - cleanup_API('../src/api/z3_interp.h', 'tmp/z3_interp.h') - cleanup_API('../src/api/z3_fpa.h', 'tmp/z3_fpa.h') + shutil.copyfile('../src/api/python/z3/z3.py', temp_path('z3py.py')) + cleanup_API('../src/api/z3_api.h', temp_path('z3_api.h')) + cleanup_API('../src/api/z3_ast_containers.h', temp_path('z3_ast_containers.h')) + cleanup_API('../src/api/z3_algebraic.h', temp_path('z3_algebraic.h')) + cleanup_API('../src/api/z3_polynomial.h', temp_path('z3_polynomial.h')) + cleanup_API('../src/api/z3_rcf.h', temp_path('z3_rcf.h')) + cleanup_API('../src/api/z3_fixedpoint.h', temp_path('z3_fixedpoint.h')) + cleanup_API('../src/api/z3_optimization.h', temp_path('z3_optimization.h')) + cleanup_API('../src/api/z3_interp.h', temp_path('z3_interp.h')) + cleanup_API('../src/api/z3_fpa.h', temp_path('z3_fpa.h')) print("Removed annotations from z3_api.h.") try: @@ -95,23 +107,8 @@ try: 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.") - os.remove('tmp/z3_api.h') - os.remove('tmp/z3_ast_containers.h') - os.remove('tmp/z3_algebraic.h') - os.remove('tmp/z3_polynomial.h') - os.remove('tmp/z3_rcf.h') - os.remove('tmp/z3_fixedpoint.h') - os.remove('tmp/z3_optimization.h') - os.remove('tmp/z3_interp.h') - os.remove('tmp/z3_fpa.h') - 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.") + shutil.rmtree(os.path.realpath(TEMP_DIR)) + print("Removed temporary directory \"{}\"".format(TEMP_DIR)) sys.path.append('../src/api/python/z3') pydoc.writedoc('z3') shutil.move('z3.html', 'api/html/z3.html') From b4f8b001cecb9a341ddacb4e590b1dcaa01889fd Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 24 Apr 2017 22:55:41 +0100 Subject: [PATCH 06/41] [Doxygen] Teach `mk_api_doc.py` a new command line option (`--output-dir`) to control where output files are emitted. This is implemented by making `z3api.dox` a template file (renamed `z3api.cfg.in`) and populating the template at build time with the required settings. --- doc/mk_api_doc.py | 64 +++++++++++++++++++++++++++++---- doc/{z3api.dox => z3api.cfg.in} | 2 +- 2 files changed, 58 insertions(+), 8 deletions(-) rename doc/{z3api.dox => z3api.cfg.in} (99%) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index a8ee1e220..b4a58f392 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -17,9 +17,10 @@ ML_ENABLED=False BUILD_DIR='../build' DOXYGEN_EXE='doxygen' TEMP_DIR=os.path.join(os.getcwd(), 'tmp') +OUTPUT_DIRECTORY=os.path.join(os.getcwd(), 'api') def parse_options(): - global ML_ENABLED, BUILD_DIR, DOXYGEN_EXE, TEMP_DIR + global ML_ENABLED, BUILD_DIR, DOXYGEN_EXE, TEMP_DIR, OUTPUT_DIRECTORY parser = argparse.ArgumentParser(description=__doc__) parser.add_argument('-b', '--build', @@ -42,11 +43,17 @@ def parse_options(): 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)', + ) 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 return def mk_dir(d): @@ -65,6 +72,41 @@ def cleanup_API(inf, outf): 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() @@ -74,6 +116,13 @@ try: def temp_path(path): return os.path.join(TEMP_DIR, path) + # Create configuration file from template + doxygen_config_substitutions = { + 'OUTPUT_DIRECTORY': OUTPUT_DIRECTORY, + } + doxygen_config_file = temp_path('z3api.cfg') + configure_file('z3api.cfg.in', doxygen_config_file, doxygen_config_substitutions) + fi = open('website.dox', 'r') fo = open(temp_path('website.dox'), 'w') @@ -86,7 +135,7 @@ try: fo.close() - mk_dir('api/html') + mk_dir(os.path.join(OUTPUT_DIRECTORY, 'html')) shutil.copyfile('../src/api/python/z3/z3.py', temp_path('z3py.py')) cleanup_API('../src/api/z3_api.h', temp_path('z3_api.h')) cleanup_API('../src/api/z3_ast_containers.h', temp_path('z3_ast_containers.h')) @@ -100,7 +149,7 @@ try: print("Removed annotations from z3_api.h.") try: - if subprocess.call([DOXYGEN_EXE, 'z3api.dox']) != 0: + if subprocess.call([DOXYGEN_EXE, doxygen_config_file]) != 0: print("ERROR: doxygen returned nonzero return code") exit(1) except: @@ -111,17 +160,18 @@ try: print("Removed temporary directory \"{}\"".format(TEMP_DIR)) sys.path.append('../src/api/python/z3') pydoc.writedoc('z3') - shutil.move('z3.html', 'api/html/z3.html') + shutil.move('z3.html', os.path.join(OUTPUT_DIRECTORY, 'html', 'z3.html')) print("Generated Python documentation.") if ML_ENABLED: - mk_dir('api/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: + ml_output_dir = os.path.join(OUTPUT_DIRECTORY, 'html', 'ml') + mk_dir(ml_output_dir) + if subprocess.call(['ocamldoc', '-html', '-d', ml_output_dir, '-sort', '-hide', 'Z3', '-I', '%s/api/ml' % BUILD_DIR, '../src/api/ml/z3enums.mli', '../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 Exception: exctype, value = sys.exc_info()[:2] print("ERROR: failed to generate documentation: %s" % value) diff --git a/doc/z3api.dox b/doc/z3api.cfg.in similarity index 99% rename from doc/z3api.dox rename to doc/z3api.cfg.in index c96a7be73..7e6c81e4f 100644 --- a/doc/z3api.dox +++ b/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 From 5a66f053848c05947a48e2aec953610291b39e28 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 24 Apr 2017 23:38:40 +0100 Subject: [PATCH 07/41] [Doxygen] Teach `mk_api_doc.py` to use `@` style substitutions to control whether OCaml documentation link is emitted. --- doc/mk_api_doc.py | 17 ++++++----------- doc/{website.dox => website.dox.in} | 3 +-- 2 files changed, 7 insertions(+), 13 deletions(-) rename doc/{website.dox => website.dox.in} (92%) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index b4a58f392..0a7efacfa 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -123,17 +123,12 @@ try: doxygen_config_file = temp_path('z3api.cfg') configure_file('z3api.cfg.in', doxygen_config_file, doxygen_config_substitutions) - fi = open('website.dox', 'r') - fo = open(temp_path('website.dox'), 'w') - - for line in fi: - if (line != '[ML]\n'): - fo.write(line) - elif (ML_ENABLED): - fo.write(' - ML/OCaml API\n') - fi.close() - fo.close() - + website_dox_substitutions = {} + if ML_ENABLED: + website_dox_substitutions['OCAML_API'] = '\n - ML/OCaml API\n' + else: + website_dox_substitutions['OCAML_API'] = '' + configure_file('website.dox.in', temp_path('website.dox'), website_dox_substitutions) mk_dir(os.path.join(OUTPUT_DIRECTORY, 'html')) shutil.copyfile('../src/api/python/z3/z3.py', temp_path('z3py.py')) diff --git a/doc/website.dox b/doc/website.dox.in similarity index 92% rename from doc/website.dox rename to doc/website.dox.in index 799949752..b00874c97 100644 --- a/doc/website.dox +++ b/doc/website.dox.in @@ -14,7 +14,6 @@ - \ref cppapi - .NET API - Java API - - Python API (also available in pydoc format) -[ML] + - Python API (also available in pydoc format)@OCAML_API@ - Try Z3 online at RiSE4Fun. */ From c78bf66df34ad6ea9aa104ec13f37b01de30769e Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 24 Apr 2017 23:49:44 +0100 Subject: [PATCH 08/41] [Doxygen] Fix bug in `mk_api_doc.py` where the generated doxygen configuration would not point at the correct path to the temporary directory. --- doc/mk_api_doc.py | 1 + doc/z3api.cfg.in | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index 0a7efacfa..cc59ffa69 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -119,6 +119,7 @@ try: # Create configuration file from template doxygen_config_substitutions = { 'OUTPUT_DIRECTORY': OUTPUT_DIRECTORY, + 'TEMP_DIR': TEMP_DIR } doxygen_config_file = temp_path('z3api.cfg') configure_file('z3api.cfg.in', doxygen_config_file, doxygen_config_substitutions) diff --git a/doc/z3api.cfg.in b/doc/z3api.cfg.in index 7e6c81e4f..bcc7113cc 100644 --- a/doc/z3api.cfg.in +++ b/doc/z3api.cfg.in @@ -684,7 +684,7 @@ WARN_LOGFILE = INPUT = ../src/api/dotnet \ ../src/api/java \ ../src/api/c++ \ - ./tmp + @TEMP_DIR@ # 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 From 33af478ce24b33393b23952833064638fead3e8a Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 24 Apr 2017 23:55:51 +0100 Subject: [PATCH 09/41] [Doxygen] Fix some indentation in doxygen configuration file template. --- doc/z3api.cfg.in | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/doc/z3api.cfg.in b/doc/z3api.cfg.in index bcc7113cc..cb07045b3 100644 --- a/doc/z3api.cfg.in +++ b/doc/z3api.cfg.in @@ -703,15 +703,15 @@ INPUT_ENCODING = UTF-8 # *.f90 *.f *.for *.vhd *.vhdl FILE_PATTERNS = website.dox \ - z3_api.h \ - z3_algebraic.h \ - z3_polynomial.h \ - z3_rcf.h \ - z3_interp.h \ - z3_fpa.h \ + z3_api.h \ + z3_algebraic.h \ + z3_polynomial.h \ + z3_rcf.h \ + z3_interp.h \ + z3_fpa.h \ z3++.h \ z3py.py \ - *.cs \ + *.cs \ *.java # The RECURSIVE tag can be used to turn specify whether or not subdirectories From eb1c985a944b59a1cbbb55912a6fcfb030c5670e Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 25 Apr 2017 00:24:46 +0100 Subject: [PATCH 10/41] [Doxygen] Fixed malformed code blocks in `z3_api.h`. These malformed `\code` blocks caused broken documentation to be generated. --- src/api/z3_api.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 272c94dda..557667b03 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -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]+]}. - If the given sort is a real, then the numeral can be a rational, that is, a string of the form \ccode{[num]* / [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 `[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 From 7242a77a3f377308dbfdd4b62a4dca7d80cb05d2 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 25 Apr 2017 00:31:05 +0100 Subject: [PATCH 11/41] [Doxygen] Fix typo found with Doxygen warning ``` warning: Found unknown command `\s' ``` --- src/api/z3_api.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 557667b03..04f84fa2a 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -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))) */ From fe702d7782db990cb90ff2bea390b100fdd65872 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 25 Apr 2017 00:36:53 +0100 Subject: [PATCH 12/41] [Doxygen] Fix warning about non-existent functions. `Z3_push` and `Z3_pop` should be `Z3_solver_push` and `Z3_solver_pop` respectively. --- src/api/z3_api.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 04f84fa2a..45065f856 100644 --- a/src/api/z3_api.h +++ b/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. From e309174ec968d378f36415611dee1a09be52ccdd Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 25 Apr 2017 11:32:26 +0100 Subject: [PATCH 13/41] [Doxygen] Add `--z3py-package-path` command line option to `mk_api_doc.py` so that the location of the z3py package can be specified. This is needed by the CMake build system because the complete Z3py package is not emitted in the source tree. Also fix a bug in the path added to the module/package search path. The directory containing the `z3` package needs to be added not the `z3` package directory itself. --- doc/mk_api_doc.py | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index cc59ffa69..3a1f8b3f8 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -18,9 +18,10 @@ BUILD_DIR='../build' DOXYGEN_EXE='doxygen' TEMP_DIR=os.path.join(os.getcwd(), 'tmp') OUTPUT_DIRECTORY=os.path.join(os.getcwd(), 'api') +Z3PY_PACKAGE_PATH='../src/api/python/z3' def parse_options(): - global ML_ENABLED, BUILD_DIR, DOXYGEN_EXE, TEMP_DIR, OUTPUT_DIRECTORY + global ML_ENABLED, BUILD_DIR, DOXYGEN_EXE, TEMP_DIR, OUTPUT_DIRECTORY, Z3PY_PACKAGE_PATH parser = argparse.ArgumentParser(description=__doc__) parser.add_argument('-b', '--build', @@ -48,12 +49,22 @@ def parse_options(): 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)', + ) 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)) return def mk_dir(d): @@ -154,7 +165,7 @@ try: print("Generated C and .NET API documentation.") shutil.rmtree(os.path.realpath(TEMP_DIR)) print("Removed temporary directory \"{}\"".format(TEMP_DIR)) - sys.path.append('../src/api/python/z3') + sys.path.append(os.path.dirname(Z3PY_PACKAGE_PATH)) pydoc.writedoc('z3') shutil.move('z3.html', os.path.join(OUTPUT_DIRECTORY, 'html', 'z3.html')) print("Generated Python documentation.") From cb6baa8bcb5f987cf6577307e1f7f0809386d981 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 25 Apr 2017 11:47:50 +0100 Subject: [PATCH 14/41] [Doxygen] Put the path to the directory containing the Z3py package at the beginning of the search path so it is picked up first. This is to try to avoid picking an installed copy of Z3py. --- doc/mk_api_doc.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index 3a1f8b3f8..10b2fcf55 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -165,7 +165,9 @@ try: print("Generated C and .NET API documentation.") shutil.rmtree(os.path.realpath(TEMP_DIR)) print("Removed temporary directory \"{}\"".format(TEMP_DIR)) - sys.path.append(os.path.dirname(Z3PY_PACKAGE_PATH)) + # Put z3py at the beginning of the search path to try to avoid picking up + # an installed copy of Z3py. + sys.path.insert(0, os.path.dirname(Z3PY_PACKAGE_PATH)) pydoc.writedoc('z3') shutil.move('z3.html', os.path.join(OUTPUT_DIRECTORY, 'html', 'z3.html')) print("Generated Python documentation.") From fa8f6f20a5fa59f3e4e180cbfbb0c575d7b4e1ed Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 25 Apr 2017 13:07:30 +0100 Subject: [PATCH 15/41] [Doxygen] Teach `mk_api_doc.py` to prevent ".NET", "Z3py" and "Java" bindings from appearing in the generated documentation. This can be enabled with `--no-dotnet`, `--no-z3py`, and `--no-java` respectively. This fine-grained control is being added for the CMake build system which will need this control. --- doc/mk_api_doc.py | 102 ++++++++++++++++++++++++++++++++++++++++----- doc/website.dox.in | 7 +--- doc/z3api.cfg.in | 9 ++-- 3 files changed, 97 insertions(+), 21 deletions(-) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index 10b2fcf55..b61036d44 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -19,9 +19,13 @@ DOXYGEN_EXE='doxygen' TEMP_DIR=os.path.join(os.getcwd(), 'tmp') OUTPUT_DIRECTORY=os.path.join(os.getcwd(), 'api') Z3PY_PACKAGE_PATH='../src/api/python/z3' +Z3PY_ENABLED=True +DOTNET_ENABLED=True +JAVA_ENABLED=True def parse_options(): - global ML_ENABLED, BUILD_DIR, DOXYGEN_EXE, TEMP_DIR, OUTPUT_DIRECTORY, Z3PY_PACKAGE_PATH + global ML_ENABLED, BUILD_DIR, DOXYGEN_EXE, TEMP_DIR, OUTPUT_DIRECTORY + global Z3PY_PACKAGE_PATH, Z3PY_ENABLED, DOTNET_ENABLED, JAVA_ENABLED parser = argparse.ArgumentParser(description=__doc__) parser.add_argument('-b', '--build', @@ -54,6 +58,28 @@ def parse_options(): 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', + ) pargs = parser.parse_args() ML_ENABLED = pargs.ml BUILD_DIR = pargs.build @@ -65,6 +91,9 @@ def parse_options(): 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 return def mk_dir(d): @@ -132,18 +161,70 @@ try: 'OUTPUT_DIRECTORY': OUTPUT_DIRECTORY, 'TEMP_DIR': TEMP_DIR } + + if Z3PY_ENABLED: + print("Z3Py documentation enabled") + doxygen_config_substitutions['PYTHON_API_FILES'] = 'z3.py' + else: + print("Z3Py documentation disabled") + doxygen_config_substitutions['PYTHON_API_FILES'] = '' + if DOTNET_ENABLED: + print(".NET documentation enabled") + doxygen_config_substitutions['DOTNET_API_FILES'] = '*.cs' + doxygen_config_substitutions['DOTNET_API_SEARCH_PATHS'] = '../src/api/dotnet' + 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' + doxygen_config_substitutions['JAVA_API_SEARCH_PATHS'] = '../src/api/java' + 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('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}Python API ' + '(also available in pydoc format)' + ).format( + prefix=bullet_point_prefix) + else: + website_dox_substitutions['PYTHON_API'] = '' + if DOTNET_ENABLED: + website_dox_substitutions['DOTNET_API'] = ( + '{prefix}' + '' + '.NET API').format( + prefix=bullet_point_prefix) + else: + website_dox_substitutions['DOTNET_API'] = '' + if JAVA_ENABLED: + website_dox_substitutions['JAVA_API'] = ( + '{prefix}' + 'Java API').format( + prefix=bullet_point_prefix) + else: + website_dox_substitutions['JAVA_API'] = '' if ML_ENABLED: - website_dox_substitutions['OCAML_API'] = '\n - ML/OCaml API\n' + website_dox_substitutions['OCAML_API'] = ( + 'ML/OCaml API' + ).format( + prefix=bullet_point_prefix) else: website_dox_substitutions['OCAML_API'] = '' configure_file('website.dox.in', temp_path('website.dox'), website_dox_substitutions) mk_dir(os.path.join(OUTPUT_DIRECTORY, 'html')) - shutil.copyfile('../src/api/python/z3/z3.py', temp_path('z3py.py')) + if Z3PY_ENABLED: + shutil.copyfile('../src/api/python/z3/z3.py', temp_path('z3py.py')) cleanup_API('../src/api/z3_api.h', temp_path('z3_api.h')) cleanup_API('../src/api/z3_ast_containers.h', temp_path('z3_ast_containers.h')) cleanup_API('../src/api/z3_algebraic.h', temp_path('z3_algebraic.h')) @@ -162,15 +243,16 @@ try: 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") shutil.rmtree(os.path.realpath(TEMP_DIR)) print("Removed temporary directory \"{}\"".format(TEMP_DIR)) - # Put z3py at the beginning of the search path to try to avoid picking up - # an installed copy of Z3py. - sys.path.insert(0, os.path.dirname(Z3PY_PACKAGE_PATH)) - pydoc.writedoc('z3') - shutil.move('z3.html', os.path.join(OUTPUT_DIRECTORY, 'html', 'z3.html')) - print("Generated Python documentation.") + if Z3PY_ENABLED: + # Put z3py at the beginning of the search path to try to avoid picking up + # an installed copy of Z3py. + sys.path.insert(0, os.path.dirname(Z3PY_PACKAGE_PATH)) + pydoc.writedoc('z3') + shutil.move('z3.html', os.path.join(OUTPUT_DIRECTORY, 'html', 'z3.html')) + print("Generated pydoc Z3Py documentation.") if ML_ENABLED: ml_output_dir = os.path.join(OUTPUT_DIRECTORY, 'html', 'ml') diff --git a/doc/website.dox.in b/doc/website.dox.in index b00874c97..17a8552d1 100644 --- a/doc/website.dox.in +++ b/doc/website.dox.in @@ -10,10 +10,7 @@ This website hosts the automatically generated documentation for the Z3 APIs. - - \ref capi - - \ref cppapi - - .NET API - - Java API - - Python API (also available in pydoc format)@OCAML_API@ + - \ref capi + - \ref cppapi @DOTNET_API@ @JAVA_API@ @PYTHON_API@ @OCAML_API@ - Try Z3 online at RiSE4Fun. */ diff --git a/doc/z3api.cfg.in b/doc/z3api.cfg.in index cb07045b3..408e981d2 100644 --- a/doc/z3api.cfg.in +++ b/doc/z3api.cfg.in @@ -681,10 +681,9 @@ WARN_LOGFILE = # directories like "/usr/src/myproject". Separate the files or directories # with spaces. -INPUT = ../src/api/dotnet \ - ../src/api/java \ +INPUT = @TEMP_DIR@ \ ../src/api/c++ \ - @TEMP_DIR@ + @DOTNET_API_SEARCH_PATHS@ @JAVA_API_SEARCH_PATHS@ # 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 @@ -710,9 +709,7 @@ FILE_PATTERNS = website.dox \ z3_interp.h \ z3_fpa.h \ z3++.h \ - z3py.py \ - *.cs \ - *.java + @PYTHON_API_FILES@ @DOTNET_API_FILES@ @JAVA_API_FILES@ # 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. From 09d7ebf1adcc3a4dfea3125f126f7a27a059797e Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 25 Apr 2017 13:17:21 +0100 Subject: [PATCH 16/41] [Doxygen] Fix bug where temporary directory and output directory paths were not handled properly if paths contained spaces. --- doc/z3api.cfg.in | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/z3api.cfg.in b/doc/z3api.cfg.in index 408e981d2..7ccad3fbb 100644 --- a/doc/z3api.cfg.in +++ b/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 = @OUTPUT_DIRECTORY@ +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,7 +681,7 @@ WARN_LOGFILE = # directories like "/usr/src/myproject". Separate the files or directories # with spaces. -INPUT = @TEMP_DIR@ \ +INPUT = "@TEMP_DIR@" \ ../src/api/c++ \ @DOTNET_API_SEARCH_PATHS@ @JAVA_API_SEARCH_PATHS@ From e4bec1572aa404298abbacf7693e3f37e7453d04 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 25 Apr 2017 13:36:48 +0100 Subject: [PATCH 17/41] [Doxygen] Teach `mk_api_doc.py` to allow multiple search paths for the ".NET" and "Java" bindings. The CMake build system needs this because the generated files exist in a different directory to the source files. Multiple paths can be specified using the `--dot-search-paths` and `--java-search-paths` options. --- doc/mk_api_doc.py | 29 +++++++++++++++++++++++++++-- 1 file changed, 27 insertions(+), 2 deletions(-) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index b61036d44..e331c60b9 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -22,10 +22,13 @@ Z3PY_PACKAGE_PATH='../src/api/python/z3' Z3PY_ENABLED=True DOTNET_ENABLED=True JAVA_ENABLED=True +DOTNET_API_SEARCH_PATHS=['../src/api/dotnet'] +JAVA_API_SEARCH_PATHS=['../src/api/java'] def parse_options(): global ML_ENABLED, BUILD_DIR, DOXYGEN_EXE, TEMP_DIR, OUTPUT_DIRECTORY global Z3PY_PACKAGE_PATH, Z3PY_ENABLED, DOTNET_ENABLED, JAVA_ENABLED + global DOTNET_API_SEARCH_PATHS, JAVA_API_SEARCH_PATHS parser = argparse.ArgumentParser(description=__doc__) parser.add_argument('-b', '--build', @@ -80,6 +83,18 @@ def parse_options(): 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 @@ -94,6 +109,8 @@ def parse_options(): 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): @@ -171,7 +188,11 @@ try: if DOTNET_ENABLED: print(".NET documentation enabled") doxygen_config_substitutions['DOTNET_API_FILES'] = '*.cs' - doxygen_config_substitutions['DOTNET_API_SEARCH_PATHS'] = '../src/api/dotnet' + dotnet_api_search_path_str = "" + for p in DOTNET_API_SEARCH_PATHS: + # Quote path so that paths with spaces are handled correctly + dotnet_api_search_path_str += "\"{}\" ".format(p) + doxygen_config_substitutions['DOTNET_API_SEARCH_PATHS'] = dotnet_api_search_path_str else: print(".NET documentation disabled") doxygen_config_substitutions['DOTNET_API_FILES'] = '' @@ -179,7 +200,11 @@ try: if JAVA_ENABLED: print("Java documentation enabled") doxygen_config_substitutions['JAVA_API_FILES'] = '*.java' - doxygen_config_substitutions['JAVA_API_SEARCH_PATHS'] = '../src/api/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'] = '' From 121fd06cc2f3dec7fd2412815b9340e8dbfb90c0 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 25 Apr 2017 14:36:02 +0100 Subject: [PATCH 18/41] [Doxygen] Fix `mk_api_doc.py` so it is not required that the current working directory be the `doc` directory in the source tree. --- doc/mk_api_doc.py | 39 +++++++++++++++++++++++++-------------- doc/z3api.cfg.in | 2 +- 2 files changed, 26 insertions(+), 15 deletions(-) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index e331c60b9..6007b77c4 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -24,6 +24,7 @@ DOTNET_ENABLED=True 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, DOXYGEN_EXE, TEMP_DIR, OUTPUT_DIRECTORY @@ -172,11 +173,15 @@ try: # 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) # Create configuration file from template doxygen_config_substitutions = { 'OUTPUT_DIRECTORY': OUTPUT_DIRECTORY, - 'TEMP_DIR': TEMP_DIR + 'TEMP_DIR': TEMP_DIR, + 'CXX_API_SEARCH_PATHS': doc_path('../src/api/c++'), } if Z3PY_ENABLED: @@ -211,7 +216,10 @@ try: doxygen_config_substitutions['JAVA_API_SEARCH_PATHS'] = '' doxygen_config_file = temp_path('z3api.cfg') - configure_file('z3api.cfg.in', doxygen_config_file, doxygen_config_substitutions) + configure_file( + doc_path('z3api.cfg.in'), + doxygen_config_file, + doxygen_config_substitutions) website_dox_substitutions = {} bullet_point_prefix='\n - ' @@ -245,20 +253,23 @@ try: prefix=bullet_point_prefix) else: website_dox_substitutions['OCAML_API'] = '' - configure_file('website.dox.in', temp_path('website.dox'), website_dox_substitutions) + 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('../src/api/python/z3/z3.py', temp_path('z3py.py')) - cleanup_API('../src/api/z3_api.h', temp_path('z3_api.h')) - cleanup_API('../src/api/z3_ast_containers.h', temp_path('z3_ast_containers.h')) - cleanup_API('../src/api/z3_algebraic.h', temp_path('z3_algebraic.h')) - cleanup_API('../src/api/z3_polynomial.h', temp_path('z3_polynomial.h')) - cleanup_API('../src/api/z3_rcf.h', temp_path('z3_rcf.h')) - cleanup_API('../src/api/z3_fixedpoint.h', temp_path('z3_fixedpoint.h')) - cleanup_API('../src/api/z3_optimization.h', temp_path('z3_optimization.h')) - cleanup_API('../src/api/z3_interp.h', temp_path('z3_interp.h')) - cleanup_API('../src/api/z3_fpa.h', temp_path('z3_fpa.h')) + 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: @@ -282,7 +293,7 @@ try: if ML_ENABLED: ml_output_dir = os.path.join(OUTPUT_DIRECTORY, 'html', 'ml') mk_dir(ml_output_dir) - if subprocess.call(['ocamldoc', '-html', '-d', ml_output_dir, '-sort', '-hide', 'Z3', '-I', '%s/api/ml' % BUILD_DIR, '../src/api/ml/z3enums.mli', '../src/api/ml/z3.mli']) != 0: + 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.") diff --git a/doc/z3api.cfg.in b/doc/z3api.cfg.in index 7ccad3fbb..9e946aa7f 100644 --- a/doc/z3api.cfg.in +++ b/doc/z3api.cfg.in @@ -682,7 +682,7 @@ WARN_LOGFILE = # with spaces. INPUT = "@TEMP_DIR@" \ - ../src/api/c++ \ + "@CXX_API_SEARCH_PATHS@" \ @DOTNET_API_SEARCH_PATHS@ @JAVA_API_SEARCH_PATHS@ # This tag can be used to specify the character encoding of the source files From a6a6a9c29f96c63eec7d5efef6860553d366be21 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 25 Apr 2017 15:43:03 +0100 Subject: [PATCH 19/41] [Doxygen] Fix link to ".NET" documentation it should point to the "Microsoft.Z3" namespace, not the "Microsoft.Z3.Context" class. This mirrors the link provided for the Java API. --- doc/mk_api_doc.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py index 6007b77c4..014a152b4 100644 --- a/doc/mk_api_doc.py +++ b/doc/mk_api_doc.py @@ -234,7 +234,7 @@ try: if DOTNET_ENABLED: website_dox_substitutions['DOTNET_API'] = ( '{prefix}' - '' + '' '.NET API').format( prefix=bullet_point_prefix) else: From d4b7b489d072daaf268ee15f3f1517c4388cf8b3 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 25 Apr 2017 14:16:14 +0100 Subject: [PATCH 20/41] [CMake] Teach CMake to build the documentation for the API bindings and install them. The target for building the documentation is `api_docs`. This is off by default but can be enabled with the `BUILD_DOCUMENTATION` option. The C and C++ API documentation is always built but the Python, ".NET", and Java documentation are only built if they are enabled in the build system. The rationale for this is that it would be confusing to install documentation for API bindings that are not installed. By default `ALWAYS_BUILD_DOCS` is on which will slow down builds significantly but will ensure that when the `install` target is invoked the documentation is up-to-date. Unfortunately I couldn't find a better way to do this. `ALWAYS_BUILD_DOCS` can be disabled to get faster builds and still have the `api_docs` target available. --- CMakeLists.txt | 16 +++++- README-CMake.md | 7 +++ contrib/cmake/doc/CMakeLists.txt | 93 ++++++++++++++++++++++++++++++++ 3 files changed, 115 insertions(+), 1 deletion(-) create mode 100644 contrib/cmake/doc/CMakeLists.txt diff --git a/CMakeLists.txt b/CMakeLists.txt index cf46e7012..47a081e75 100644 --- a/CMakeLists.txt +++ b/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() diff --git a/README-CMake.md b/README-CMake.md index 6a78b5d4c..4bbbd36a8 100644 --- a/README-CMake.md +++ b/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 diff --git a/contrib/cmake/doc/CMakeLists.txt b/contrib/cmake/doc/CMakeLists.txt new file mode 100644 index 000000000..86e208ab1 --- /dev/null +++ b/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() From 46ac718790b5cfddc4d5ed215a301618285018de Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Wed, 26 Apr 2017 17:24:05 -0400 Subject: [PATCH 21/41] theory_str frontend changes --- src/ast/ast.cpp | 1 + src/ast/ast.h | 3 ++ src/ast/rewriter/seq_rewriter.cpp | 72 ++++++++++++++++++++++++++++--- src/ast/rewriter/seq_rewriter.h | 2 + src/ast/seq_decl_plugin.cpp | 4 +- 5 files changed, 76 insertions(+), 6 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 7be7300a2..5f2de5170 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -17,6 +17,7 @@ Revision History: --*/ #include +#include #include"ast.h" #include"ast_pp.h" #include"ast_ll_pp.h" diff --git a/src/ast/ast.h b/src/ast/ast.h index 9259d5431..6bb3b01c9 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -117,6 +117,9 @@ public: explicit parameter(symbol const & s): m_kind(PARAM_SYMBOL) { new (m_symbol) symbol(s); } explicit parameter(rational const & r): m_kind(PARAM_RATIONAL) { new (m_rational) rational(r); } explicit parameter(double d):m_kind(PARAM_DOUBLE), m_dval(d) {} + explicit parameter(const char *s):m_kind(PARAM_SYMBOL) { + new (m_symbol) symbol(s); + } explicit parameter(unsigned ext_id, bool):m_kind(PARAM_EXTERNAL), m_ext_id(ext_id) {} parameter(parameter const&); diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 3737f4651..85d2ba749 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -329,7 +329,8 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con switch(f->get_decl_kind()) { case OP_SEQ_UNIT: - return BR_FAILED; + SASSERT(num_args == 1); + return mk_seq_unit(args[0], result); case OP_SEQ_EMPTY: return BR_FAILED; case OP_RE_PLUS: @@ -351,7 +352,8 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con SASSERT(num_args == 2); return mk_re_union(args[0], args[1], result); case OP_RE_RANGE: - return BR_FAILED; + SASSERT(num_args == 2); + return mk_re_range(args[0], args[1], result); case OP_RE_INTERSECT: SASSERT(num_args == 2); return mk_re_inter(args[0], args[1], result); @@ -434,6 +436,33 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con return BR_FAILED; } +/* + * (seq.unit (_ BitVector 8)) ==> String constant + */ +br_status seq_rewriter::mk_seq_unit(expr* e, expr_ref& result) { + sort * s = m().get_sort(e); + bv_util bvu(m()); + + if (is_sort_of(s, bvu.get_family_id(), BV_SORT)) { + // specifically we want (_ BitVector 8) + rational n_val; + unsigned int n_size; + if (bvu.is_numeral(e, n_val, n_size)) { + if (n_size == 8) { + // convert to string constant + char ch = (char)n_val.get_int32(); + TRACE("seq", tout << "rewrite seq.unit of 8-bit value " << n_val.to_string() << " to string constant \"" << ch << "\"" << std::endl;); + char s_tmp[2] = {ch, '\0'}; + symbol s(s_tmp); + result = m_util.str.mk_string(s); + return BR_DONE; + } + } + } + + return BR_FAILED; +} + /* string + string = string a + (b + c) = (a + b) + c @@ -1401,6 +1430,39 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) { return BR_FAILED; } +/* + * (re.range c_1 c_n) = (re.union (str.to.re c1) (str.to.re c2) ... (str.to.re cn)) + */ +br_status seq_rewriter::mk_re_range(expr* lo, expr* hi, expr_ref& result) { + TRACE("seq", tout << "rewrite re.range [" << mk_pp(lo, m()) << " " << mk_pp(hi, m()) << "]\n";); + zstring str_lo, str_hi; + if (m_util.str.is_string(lo, str_lo) && m_util.str.is_string(hi, str_hi)) { + if (str_lo.length() == 1 && str_hi.length() == 1) { + unsigned int c1 = str_lo[0]; + unsigned int c2 = str_hi[0]; + if (c1 > c2) { + // exchange c1 and c2 + unsigned int tmp = c1; + c2 = c1; + c1 = tmp; + } + zstring s(c1); + expr_ref acc(m_util.re.mk_to_re(m_util.str.mk_string(s)), m()); + for (unsigned int ch = c1 + 1; ch <= c2; ++ch) { + zstring s_ch(ch); + expr_ref acc2(m_util.re.mk_to_re(m_util.str.mk_string(s_ch)), m()); + acc = m_util.re.mk_union(acc, acc2); + } + result = acc; + return BR_REWRITE2; + } else { + m().raise_exception("string constants in re.range must have length 1"); + } + } + + return BR_FAILED; +} + /* emp+ = emp all+ = all @@ -1430,9 +1492,9 @@ br_status seq_rewriter::mk_re_plus(expr* a, expr_ref& result) { return BR_DONE; } - return BR_FAILED; -// result = m_util.re.mk_concat(a, m_util.re.mk_star(a)); -// return BR_REWRITE2; + //return BR_FAILED; + result = m_util.re.mk_concat(a, m_util.re.mk_star(a)); + return BR_REWRITE2; } br_status seq_rewriter::mk_re_opt(expr* a, expr_ref& result) { diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 2b434f475..210b2d72c 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -98,6 +98,7 @@ class seq_rewriter { re2automaton m_re2aut; expr_ref_vector m_es, m_lhs, m_rhs; + br_status mk_seq_unit(expr* e, expr_ref& result); br_status mk_seq_concat(expr* a, expr* b, expr_ref& result); br_status mk_seq_length(expr* a, expr_ref& result); br_status mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& result); @@ -119,6 +120,7 @@ class seq_rewriter { br_status mk_re_plus(expr* a, expr_ref& result); br_status mk_re_opt(expr* a, expr_ref& result); br_status mk_re_loop(unsigned num_args, expr* const* args, expr_ref& result); + br_status mk_re_range(expr* lo, expr* hi, expr_ref& result); bool set_empty(unsigned sz, expr* const* es, bool all, expr_ref_vector& lhs, expr_ref_vector& rhs); bool is_subsequence(unsigned n, expr* const* l, unsigned m, expr* const* r, diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index f282043e6..353fb975f 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -573,7 +573,7 @@ void seq_decl_plugin::set_manager(ast_manager* m, family_id id) { m_char = bv.mk_sort(8); m->inc_ref(m_char); parameter param(m_char); - m_string = m->mk_sort(symbol("String"), sort_info(m_family_id, SEQ_SORT, 1, ¶m)); + m_string = m->mk_sort(symbol("StringSequence"), sort_info(m_family_id, SEQ_SORT, 1, ¶m)); m->inc_ref(m_string); parameter paramS(m_string); m_re = m->mk_sort(m_family_id, RE_SORT, 1, ¶mS); @@ -831,7 +831,9 @@ void seq_decl_plugin::get_sort_names(svector & sort_names, symbol init(); sort_names.push_back(builtin_name("Seq", SEQ_SORT)); sort_names.push_back(builtin_name("RegEx", RE_SORT)); + // SMT-LIB 2.5 compatibility sort_names.push_back(builtin_name("String", _STRING_SORT)); + sort_names.push_back(builtin_name("StringSequence", _STRING_SORT)); } app* seq_decl_plugin::mk_string(symbol const& s) { From 7811a91bad1d1f4586f82d221049de956567368a Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Thu, 27 Apr 2017 13:59:02 -0400 Subject: [PATCH 22/41] fix is_string_term() --- src/ast/seq_decl_plugin.h | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 2882e905d..833455ff4 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -273,6 +273,15 @@ public: bool is_in_re(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_IN_RE); } bool is_unit(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_UNIT); } + bool is_string_term(expr const * n) const { + sort * s = get_sort(n); + return (u.is_seq(s) && u.is_string(s)); + } + + bool is_non_string_sequence(expr const * n) const { + sort * s = get_sort(n); + return (u.is_seq(s) && !u.is_string(s)); + } MATCH_BINARY(is_concat); MATCH_UNARY(is_length); From 12dd6d786b238d35ddcebb412d51516aec7a56b1 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Thu, 27 Apr 2017 21:24:40 -0400 Subject: [PATCH 23/41] remove redundant is_seq() check --- src/ast/seq_decl_plugin.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index 833455ff4..76b5ebe31 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -275,7 +275,7 @@ public: bool is_string_term(expr const * n) const { sort * s = get_sort(n); - return (u.is_seq(s) && u.is_string(s)); + return u.is_string(s); } bool is_non_string_sequence(expr const * n) const { From 05958193ab3dc8f1780f1c9e2ae9c1ad7ecc4855 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Thu, 27 Apr 2017 22:30:02 -0400 Subject: [PATCH 24/41] revert change to String sort declaration --- src/ast/seq_decl_plugin.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 353fb975f..bf238d8c5 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -573,7 +573,7 @@ void seq_decl_plugin::set_manager(ast_manager* m, family_id id) { m_char = bv.mk_sort(8); m->inc_ref(m_char); parameter param(m_char); - m_string = m->mk_sort(symbol("StringSequence"), sort_info(m_family_id, SEQ_SORT, 1, ¶m)); + m_string = m->mk_sort(symbol("String"), sort_info(m_family_id, SEQ_SORT, 1, ¶m)); m->inc_ref(m_string); parameter paramS(m_string); m_re = m->mk_sort(m_family_id, RE_SORT, 1, ¶mS); From 88147f7047f85b64c26660717871e0d6be8c3eeb Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Fri, 28 Apr 2017 14:14:28 -0400 Subject: [PATCH 25/41] theory_str static features and cmd_context --- src/ast/static_features.cpp | 8 ++++++++ src/ast/static_features.h | 4 ++++ src/cmd_context/cmd_context.cpp | 7 +++++-- src/cmd_context/cmd_context.h | 1 + 4 files changed, 18 insertions(+), 2 deletions(-) diff --git a/src/ast/static_features.cpp b/src/ast/static_features.cpp index 328128794..daf20e095 100644 --- a/src/ast/static_features.cpp +++ b/src/ast/static_features.cpp @@ -25,6 +25,7 @@ static_features::static_features(ast_manager & m): m_bvutil(m), m_arrayutil(m), m_fpautil(m), + m_sequtil(m), m_bfid(m.get_basic_family_id()), m_afid(m.mk_family_id("arith")), m_lfid(m.mk_family_id("label")), @@ -77,6 +78,8 @@ void static_features::reset() { m_has_real = false; m_has_bv = false; m_has_fpa = false; + m_has_str = false; + m_has_seq_non_str = false; m_has_arrays = false; m_arith_k_sum .reset(); m_num_arith_terms = 0; @@ -279,6 +282,11 @@ void static_features::update_core(expr * e) { m_has_fpa = true; if (!m_has_arrays && m_arrayutil.is_array(e)) m_has_arrays = true; + if (!m_has_str && m_sequtil.str.is_string_term(e)) + m_has_str = true; + if (!m_has_seq_non_str && m_sequtil.str.is_non_string_sequence(e)) { + m_has_seq_non_str = true; + } if (is_app(e)) { family_id fid = to_app(e)->get_family_id(); mark_theory(fid); diff --git a/src/ast/static_features.h b/src/ast/static_features.h index 8b20c5463..e7f69e041 100644 --- a/src/ast/static_features.h +++ b/src/ast/static_features.h @@ -24,6 +24,7 @@ Revision History: #include"bv_decl_plugin.h" #include"array_decl_plugin.h" #include"fpa_decl_plugin.h" +#include"seq_decl_plugin.h" #include"map.h" struct static_features { @@ -32,6 +33,7 @@ struct static_features { bv_util m_bvutil; array_util m_arrayutil; fpa_util m_fpautil; + seq_util m_sequtil; family_id m_bfid; family_id m_afid; family_id m_lfid; @@ -77,6 +79,8 @@ struct static_features { bool m_has_real; // bool m_has_bv; // bool m_has_fpa; // + bool m_has_str; // has String-typed terms + bool m_has_seq_non_str; // has non-String-typed Sequence terms bool m_has_arrays; // rational m_arith_k_sum; // sum of the numerals in arith atoms. unsigned m_num_arith_terms; diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 7060d79ad..f590725a7 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -249,6 +249,7 @@ protected: array_util m_arutil; fpa_util m_futil; seq_util m_sutil; + datalog::dl_decl_util m_dlutil; format_ns::format * pp_fdecl_name(symbol const & s, func_decls const & fs, func_decl * f, unsigned & len) { @@ -277,6 +278,7 @@ public: virtual array_util & get_arutil() { return m_arutil; } virtual fpa_util & get_futil() { return m_futil; } virtual seq_util & get_sutil() { return m_sutil; } + virtual datalog::dl_decl_util& get_dlutil() { return m_dlutil; } virtual bool uses(symbol const & s) const { return @@ -527,6 +529,9 @@ bool cmd_context::logic_has_fpa() const { return !has_logic() || smt_logics::logic_has_fpa(m_logic); } +bool cmd_context::logic_has_str() const { + return !has_logic() || m_logic == "QF_S"; +} bool cmd_context::logic_has_array() const { return !has_logic() || smt_logics::logic_has_array(m_logic); @@ -568,7 +573,6 @@ void cmd_context::init_manager_core(bool new_manager) { load_plugin(symbol("seq"), logic_has_seq(), fids); load_plugin(symbol("fpa"), logic_has_fpa(), fids); load_plugin(symbol("pb"), logic_has_pb(), fids); - svector::iterator it = fids.begin(); svector::iterator end = fids.end(); for (; it != end; ++it) { @@ -616,7 +620,6 @@ void cmd_context::init_external_manager() { init_manager_core(false); } - bool cmd_context::set_logic(symbol const & s) { if (has_logic()) throw cmd_exception("the logic has already been set"); diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 92943c71c..8885bc5d6 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -257,6 +257,7 @@ protected: bool logic_has_array() const; bool logic_has_datatype() const; bool logic_has_fpa() const; + bool logic_has_str() const; void print_unsupported_msg() { regular_stream() << "unsupported" << std::endl; } void print_unsupported_info(symbol const& s, int line, int pos) { if (s != symbol::null) diagnostic_stream() << "; " << s << " line: " << line << " position: " << pos << std::endl;} From 4cc2b292c0cc8759da7a525e63dbfefdb06d6a01 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Fri, 28 Apr 2017 17:59:04 +0100 Subject: [PATCH 26/41] [CMake] Remove compiler flag overrides and support for C language. The setting of overrides was broken (the CXX flags were not set but the C flags were) and we aren't even using the C compiler any more. The C compiler is used by the example C project but that is built as an external project now so we don't need C support anymore. The setting of defaults was also very fragile. CMake has quite complicated support here (e.g. MSVC with a clang based tool chain) which would likely not work properly with the override approach as it existed. This means we loose some of the custom linker flags we were setting for MSVC but we were never doing a great job of replicating the exact set of flags used in the old build system anyway. Subsequent commits will gradually fix this. --- CMakeLists.txt | 4 +- .../cmake/cmake/compiler_flags_override.cmake | 43 ------------------- 2 files changed, 1 insertion(+), 46 deletions(-) delete mode 100644 contrib/cmake/cmake/compiler_flags_override.cmake diff --git a/CMakeLists.txt b/CMakeLists.txt index 47a081e75..ab3976aea 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -24,9 +24,7 @@ if (NOT (EXISTS "${CMAKE_SOURCE_DIR}/src/CMakeLists.txt")) "``python contrib/cmake/bootstrap.py create``") endif() -# This overrides the default flags for the different CMAKE_BUILD_TYPEs -set(CMAKE_USER_MAKE_RULES_OVERRIDE "${CMAKE_CURRENT_SOURCE_DIR}/cmake/compiler_flags_override.cmake") -project(Z3 C CXX) +project(Z3 CXX) ################################################################################ # Project version diff --git a/contrib/cmake/cmake/compiler_flags_override.cmake b/contrib/cmake/cmake/compiler_flags_override.cmake deleted file mode 100644 index c6005396b..000000000 --- a/contrib/cmake/cmake/compiler_flags_override.cmake +++ /dev/null @@ -1,43 +0,0 @@ -# This file overrides the default compiler flags for CMake's built-in -# configurations (CMAKE_BUILD_TYPE). Most compiler flags should not be set here. -# The main purpose is to have very fine grained control of the compiler flags. -if (CMAKE_C_COMPILER_ID) - set(_lang C) -elseif(CMAKE_CXX_COMPILER_ID) - set(_lang CXX) -else() - message(FATAL_ERROR "Unknown language") -endif() - -# TODO: The value of doing this is debatable. The flags set here are pretty -# much the CMake defaults now (they didn't use to be) and makes extra work for -# us when supporting different compilers. Perhaps we should move the remaining -# code that sets non-default flags out into the CMakeLists.txt files and remove -# any overrides here? -if (("${CMAKE_${_lang}_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_${_lang}_COMPILER_ID}" MATCHES "GNU")) - # Taken from Modules/Compiler/GNU.cmake - set(CMAKE_${_lang}_FLAGS_INIT "") - set(CMAKE_${_lang}_FLAGS_DEBUG_INIT "-g -O0") - set(CMAKE_${_lang}_FLAGS_MINSIZEREL_INIT "-Os -DNDEBUG") - set(CMAKE_${_lang}_FLAGS_RELEASE_INIT "-O3 -DNDEBUG") - set(CMAKE_${_lang}_FLAGS_RELWITHDEBINFO_INIT "-O2 -g -DNDEBUG") - # FIXME: Remove "x.." when CMP0054 is set to NEW -elseif ("x${CMAKE_${_lang}_COMPILER_ID}" STREQUAL "xMSVC") - # FIXME: Perhaps we should be using /MD instead? - set(CMAKE_${_lang}_FLAGS_DEBUG_INIT "/MTd /Zi /Ob0 /Od /RTC1") - set(CMAKE_${_lang}_FLAGS_MINSIZEREL_INIT "/MT /O1 /Ob1 /D NDEBUG") - set(CMAKE_${_lang}_FLAGS_RELEASE_INIT "/MT /O2 /Ob2 /D NDEBUG") - set(CMAKE_${_lang}_FLAGS_RELWITHDEBINFO_INIT "/MT /Zi /O2 /Ob1 /D NDEBUG") - # Override linker flags (see Windows-MSVC.cmake for CMake's defaults) - # The stack size comes from the Python build system. - set(_msvc_stack_size "8388608") - set(CMAKE_EXE_LINKER_FLAGS_DEBUG_INIT "/debug /INCREMENTAL:NO /STACK:${_msvc_stack_size}") - set(CMAKE_EXE_LINKER_FLAGS_RELWITHDEBINFO_INIT "/debug /INCREMENTAL:NO /STACK:${_msvc_stack_size}") - set(CMAKE_EXE_LINKER_FLAGS_MINSIZEREL_INIT "/INCREMENTAL:NO /STACK:${_msvc_stack_size}") - set(CMAKE_EXE_LINKER_FLAGS_RELEASE_INIT "/INCREMENTAL:NO /STACK:${_msvc_stack_size}") - unset(_msvc_stack_size) -else() - message(FATAL_ERROR "Overrides not set for ${_lang} compiler \"${CMAKE_${_lang}_COMPILER_ID}\"") -endif() - -unset(_lang) From f568b2478ff743b735f5e1ab03325040ea320cc9 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Fri, 28 Apr 2017 21:30:36 +0100 Subject: [PATCH 27/41] [CMake] Report the various values of CMAKE_CXX_FLAGS, CMAKE_CXX_FLAGS_, CMAKE__LINKER_FLAGS, and CMAKE__LINKER_FLAGS_. This is useful for debugging where some flags come from. Now that we don't explicitly set the defaults it useful to see which default values we are getting from CMake. --- CMakeLists.txt | 24 +++++++++++++++++++++++- 1 file changed, 23 insertions(+), 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index ab3976aea..795a23320 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -153,13 +153,13 @@ set(Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS "") # Build type ################################################################################ message(STATUS "CMake generator: ${CMAKE_GENERATOR}") +set(available_build_types Debug Release RelWithDebInfo MinSizeRel) if (DEFINED CMAKE_CONFIGURATION_TYPES) # Multi-configuration build (e.g. Visual Studio and Xcode). Here # CMAKE_BUILD_TYPE doesn't matter message(STATUS "Available configurations: ${CMAKE_CONFIGURATION_TYPES}") else() # Single configuration generator (e.g. Unix Makefiles, Ninja) - set(available_build_types Debug Release RelWithDebInfo MinSizeRel) if(NOT CMAKE_BUILD_TYPE) message(STATUS "CMAKE_BUILD_TYPE is not set. Setting default") message(STATUS "The available build types are: ${available_build_types}") @@ -374,6 +374,28 @@ if (BUILD_LIBZ3_SHARED) endif() endif() +################################################################################ +# Report default CMake flags +################################################################################ +# This is mainly for debugging. +message(STATUS "CMAKE_CXX_FLAGS: \"${CMAKE_CXX_FLAGS}\"") +message(STATUS "CMAKE_EXE_LINKER_FLAGS: \"${CMAKE_EXE_LINKER_FLAGS}\"") +message(STATUS "CMAKE_STATIC_LINKER_FLAGS: \"${CMAKE_STATIC_LINKER_FLAGS}\"") +message(STATUS "CMAKE_SHARED_LINKER_FLAGS: \"${CMAKE_SHARED_LINKER_FLAGS}\"") +if (DEFINED CMAKE_CONFIGURATION_TYPES) + # Multi configuration generator + string(TOUPPER "${available_build_types}" build_types_to_report) +else() + # Single configuration generator + string(TOUPPER "${CMAKE_BUILD_TYPE}" build_types_to_report) +endif() +foreach (_build_type ${build_types_to_report}) + message(STATUS "CMAKE_CXX_FLAGS_${_build_type}: \"${CMAKE_CXX_FLAGS_${_build_type}}\"") + message(STATUS "CMAKE_EXE_LINKER_FLAGS_${_build_type}: \"${CMAKE_EXE_LINKER_FLAGS_${_build_type}}\"") + message(STATUS "CMAKE_SHARED_LINKER_FLAGS_${_build_type}: \"${CMAKE_SHARED_LINKER_FLAGS_${_build_type}}\"") + message(STATUS "CMAKE_STATIC_LINKER_FLAGS_${_build_type}: \"${CMAKE_STATIC_LINKER_FLAGS_${_build_type}}\"") +endforeach() + ################################################################################ # Report Z3_COMPONENT flags ################################################################################ From fe1af4bcdb7c4f4d85874e449fae3db8cf0a49ad Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Fri, 28 Apr 2017 23:28:04 +0100 Subject: [PATCH 28/41] [CMake] Teach build system to pass `/fp:precise` to compiler when using MSVC. This is set by the old build system but we weren't setting it. This actually MSVC's default but in an effort to try to behave more like the old build system we will set it anyway. --- CMakeLists.txt | 9 +++++++++ contrib/cmake/cmake/z3_add_cxx_flag.cmake | 1 + 2 files changed, 10 insertions(+) diff --git a/CMakeLists.txt b/CMakeLists.txt index 795a23320..6e858a421 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -324,6 +324,15 @@ if (("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") OR ("${TARGET_ARCHITECTURE}" ST unset(SSE_FLAGS) endif() +# FIXME: Remove "x.." when CMP0054 is set to NEW +if ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC") + # This is the default for MSVC already but to replicate the + # python/Makefile build system behaviour this flag is set + # explicitly. + z3_add_cxx_flag("/fp:precise" REQUIRED) +endif() +# There doesn't seem to be an equivalent for clang/gcc + ################################################################################ # Threading support ################################################################################ diff --git a/contrib/cmake/cmake/z3_add_cxx_flag.cmake b/contrib/cmake/cmake/z3_add_cxx_flag.cmake index 0c56bb0f6..8bffd7de3 100644 --- a/contrib/cmake/cmake/z3_add_cxx_flag.cmake +++ b/contrib/cmake/cmake/z3_add_cxx_flag.cmake @@ -7,6 +7,7 @@ function(z3_add_cxx_flag flag) string(REPLACE "/" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") string(REPLACE "=" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") string(REPLACE " " "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") + string(REPLACE ":" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") unset(HAS_${SANITIZED_FLAG_NAME}) CHECK_CXX_COMPILER_FLAG("${flag}" HAS_${SANITIZED_FLAG_NAME}) if (z3_add_flag_REQUIRED AND NOT HAS_${SANITIZED_FLAG_NAME}) From fb403229bd7a2bc422afe574c98dd858035c42aa Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 29 Apr 2017 00:29:26 +0100 Subject: [PATCH 29/41] [CMake] CMake's default value for CMAKE_CXX_FLAGS includes `/W3` remove this so we can have fine grained control of warnings. --- contrib/cmake/cmake/compiler_warnings.cmake | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/contrib/cmake/cmake/compiler_warnings.cmake b/contrib/cmake/cmake/compiler_warnings.cmake index c214e4464..e49e43947 100644 --- a/contrib/cmake/cmake/compiler_warnings.cmake +++ b/contrib/cmake/cmake/compiler_warnings.cmake @@ -15,6 +15,13 @@ elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") # FIXME: Remove "x.." when CMP0054 is set to NEW elseif ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC") list(APPEND WARNING_FLAGS_TO_CHECK ${MSVC_WARNINGS}) + + # CMake's default flags include /W3 already so remove them if + # they already exist. + if ("${CMAKE_CXX_FLAGS}" MATCHES "/W3") + string(REPLACE "/W3" "" _cmake_cxx_flags_remove_w3 "${CMAKE_CXX_FLAGS}") + set(CMAKE_CXX_FLAGS "${_cmake_cxx_flags_remove_w3}" CACHE STRING "" FORCE) + endif() else() message(AUTHOR_WARNING "Unknown compiler") endif() From 0e1343e78db9d396240151af436a1a2028cc40fa Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 29 Apr 2017 01:21:49 +0100 Subject: [PATCH 30/41] [CMake] Add support for link time optimization (LTO). This analogous to the `--optimize` flag in the Python/Makefile build system except that we now support doing LTO with Clang/GCC as well. However it is probably best to avoid doing LTO with Clang or GCC for now because I see a bunch of warnings about ODR violations when building with LTO. LTO can be enabled with the new `LINK_TIME_OPTIMIZATION` option which is off by default. --- CMakeLists.txt | 5 +++ README-CMake.md | 1 + contrib/cmake/cmake/compiler_lto.cmake | 52 ++++++++++++++++++++++++++ 3 files changed, 58 insertions(+) create mode 100644 contrib/cmake/cmake/compiler_lto.cmake diff --git a/CMakeLists.txt b/CMakeLists.txt index 6e858a421..8afc6339b 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -383,6 +383,11 @@ if (BUILD_LIBZ3_SHARED) endif() endif() +################################################################################ +# Link time optimization +################################################################################ +include(${CMAKE_SOURCE_DIR}/cmake/compiler_lto.cmake) + ################################################################################ # Report default CMake flags ################################################################################ diff --git a/README-CMake.md b/README-CMake.md index 4bbbd36a8..9289d40f1 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -292,6 +292,7 @@ The following useful options can be passed to CMake whilst configuring. 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. +* ``LINK_TIME_OPTIMIZATION`` - BOOL. If set to ``TRUE`` link time optimization will be enabled. 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. diff --git a/contrib/cmake/cmake/compiler_lto.cmake b/contrib/cmake/cmake/compiler_lto.cmake new file mode 100644 index 000000000..b90890f59 --- /dev/null +++ b/contrib/cmake/cmake/compiler_lto.cmake @@ -0,0 +1,52 @@ +option(LINK_TIME_OPTIMIZATION "Use link time optimiziation" OFF) + +if (LINK_TIME_OPTIMIZATION) + message(STATUS "LTO enabled") + set(build_types_with_lto "RELEASE" "RELWITHDEBINFO") + if (DEFINED CMAKE_CONFIGURATION_TYPES) + # Multi configuration generator + message(STATUS "Note LTO is only enabled for the following configurations: ${build_types_with_lto}") + else() + # Single configuration generator + string(TOUPPER "${CMAKE_BUILD_TYPE}" _build_type_upper) + list(FIND build_types_with_lto "${_build_type_upper}" _index) + if ("${_index}" EQUAL -1) + message(FATAL_ERROR "Configuration ${CMAKE_BUILD_TYPE} does not support LTO." + "You should set LINK_TIME_OPTIMIZATION to OFF.") + endif() + endif() + + set(_lto_compiler_flag "") + set(_lto_linker_flag "") + if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR + ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")) + set(_lto_compiler_flag "-flto") + set(_lto_linker_flag "-flto") + # FIXME: Remove "x.." when CMP0054 is set to NEW + elseif ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC") + set(_lto_compiler_flag "/GL") + set(_lto_linker_flag "/LTCG") + else() + message(FATAL_ERROR "Can't enable LTO for compiler \"${CMAKE_CXX_COMPILER_ID}\"." + "You should set LINK_TIME_OPTIMIZATION to OFF.") + endif() + CHECK_CXX_COMPILER_FLAG("${_lto_compiler_flag}" HAS_LTO) + if (NOT HAS_LTO) + message(FATAL_ERROR "Compiler does not support LTO") + endif() + + foreach (_config ${build_types_with_lto}) + # Set flags compiler and linker flags globally rather than using + # `Z3_COMPONENT_CXX_FLAGS` and `Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS` + # respectively. We need per configuration compiler and linker flags. The + # `LINK_FLAGS` property (which we populate with + # `Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS`) doesn't seem to support generator + # expressions so we can't do `$<$:${_lto_linker_flag}>`. + set(CMAKE_CXX_FLAGS_${_config} "${CMAKE_CXX_FLAGS_${_config}} ${_lto_compiler_flag}") + set(CMAKE_EXE_LINKER_FLAGS_${_config} "${CMAKE_EXE_LINKER_FLAGS_${_config}} ${_lto_linker_flag}") + set(CMAKE_SHARED_LINKER_FLAGS_${_config} "${CMAKE_SHARED_LINKER_FLAGS_${_config}} ${_lto_linker_flag}") + set(CMAKE_STATIC_LINKER_FLAGS_${_config} "${CMAKE_STATIC_LINKER_FLAGS_${_config}} ${_lto_linker_flag}") + endforeach() +else() + message(STATUS "LTO disabled") +endif() From 870be706e958f37d6bc7a0ca0347704b56a9c08d Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 29 Apr 2017 11:00:27 +0100 Subject: [PATCH 31/41] [CMake] Try to do a better job of matching the old build system's compiler defines and flags when using MSVC. There are lots of defines and flags that I'm unsure about so in some cases I've changed the behaviour slightly (if I'm confident the behaviour in the old build system is wrong) or not added the flag/define at all but just left comments noting what the old build system did and why I disagree with the old build system's choices. --- CMakeLists.txt | 8 ++ contrib/cmake/cmake/msvc_legacy_quirks.cmake | 112 +++++++++++++++++++ 2 files changed, 120 insertions(+) create mode 100644 contrib/cmake/cmake/msvc_legacy_quirks.cmake diff --git a/CMakeLists.txt b/CMakeLists.txt index 8afc6339b..aa347ae66 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -388,6 +388,14 @@ endif() ################################################################################ include(${CMAKE_SOURCE_DIR}/cmake/compiler_lto.cmake) +################################################################################ +# MSVC specific flags inherited from old build system +################################################################################ +# FIXME: Remove "x.." when CMP0054 is set to NEW +if ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC") + include(${CMAKE_SOURCE_DIR}/cmake/msvc_legacy_quirks.cmake) +endif() + ################################################################################ # Report default CMake flags ################################################################################ diff --git a/contrib/cmake/cmake/msvc_legacy_quirks.cmake b/contrib/cmake/cmake/msvc_legacy_quirks.cmake new file mode 100644 index 000000000..050d34553 --- /dev/null +++ b/contrib/cmake/cmake/msvc_legacy_quirks.cmake @@ -0,0 +1,112 @@ +# This file ether sets or notes various compiler and linker flags for MSVC that +# were defined by the old python/Makefile based build system but +# don't obviously belong in the other sections in the CMake build system. + +################################################################################ +# Compiler definitions +################################################################################ +# FIXME: All the commented out defines should be removed once +# we are confident it is correct to not set them. +set(Z3_MSVC_LEGACY_DEFINES + # Don't set `_DEBUG`. The old build sytem sets this but this + # is wrong. MSVC will set this depending on which runtime is being used. + # See https://msdn.microsoft.com/en-us/library/b0084kay.aspx + # _DEBUG + + # The old build system only set `UNICODE` and `_UNICODE` for x86_64 release. + # That seems completly wrong so set it for all configurations. + # According to https://blogs.msdn.microsoft.com/oldnewthing/20040212-00/?p=40643/ + # `UNICODE` affects Windows headers and `_UNICODE` affects C runtime header files. + # There is some discussion of this define at https://msdn.microsoft.com/en-us/library/dybsewaf.aspx + UNICODE + _UNICODE +) + +if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") + list(APPEND Z3_MSVC_LEGACY_DEFINES "" + # Don't set `_LIB`. The old build system sets this for x86_64 release + # build. This flag doesn't seem to be documented but a stackoverflow + # post hints that this is usually set when building a static library. + # See http://stackoverflow.com/questions/35034683/how-to-tell-if-current-project-is-dll-or-static-lib + # This seems wrong give that the old build system set this regardless + # whether or not libz3 was static or shared so its probably best + # to not set for now. + #$<$:_LIB> + #$<$:_LIB> + + # Don't set `_CONSOLE`. The old build system sets for all configurations + # except x86_64 release. It seems ( https://codeyarns.com/2010/12/02/visual-c-windows-and-console-subsystems/ ) + # that `_CONSOLE` used to be defined by older Visual C++ environments. + # Setting this undocumented option seems like a bad idea so let's not do it. + #$<$ + #$<$ + + # Don't set `ASYNC_COMMANDS`. The old build system sets this for x86_64 + # release but this macro does not appear to be used anywhere and is not + # documented so don't set it for now. + #$<$:ASYNC_COMMANDS> + #$<$:ASYNC_COMMANDS> + ) +else() + list(APPEND Z3_MSVC_LEGACY_DEFINES "" + # Don't set `_CONSOLE`. See reasoning above. + #_CONSOLE + ) +endif() + +# Note we don't set WIN32 or _WINDOWS because +# CMake provides that for us. As a sanity check make sure the option +# is present. +if (NOT "${CMAKE_CXX_FLAGS}" MATCHES "/D[ ]*WIN32") + message(FATAL_ERROR "\"/D WIN32\" is missing") +endif() +if (NOT "${CMAKE_CXX_FLAGS}" MATCHES "/D[ ]*_WINDOWS") + message(FATAL_ERROR "\"/D _WINDOWS\" is missing") +endif() + +list(APPEND Z3_COMPONENT_CXX_DEFINES ${Z3_MSVC_LEGACY_DEFINES}) + +################################################################################ +# Compiler flags +################################################################################ +# By default in MSVC this is on but the old build system set this explicitly so +# for completeness set it too. +# See https://msdn.microsoft.com/en-us/library/dh8che7s.aspx +z3_add_cxx_flag("/Zc:wchar_t" REQUIRED) +# By default in MSVC this on but the old build system set this explicitly so +# for completeness set it too. +z3_add_cxx_flag("/Zc:forScope" REQUIRED) + +# FIXME: We might want to move this out somewhere else if we decide +# we want to set `-fno-omit-frame-pointer` for gcc/clang. +# No omit frame pointer +set(NO_OMIT_FRAME_POINTER_MSVC_FLAG "/Oy-") +CHECK_CXX_COMPILER_FLAG(${NO_OMIT_FRAME_POINTER_MSVC_FLAG} HAS_MSVC_NO_OMIT_FRAME_POINTER) +if (NOT HAS_MSVC_NO_OMIT_FRAME_POINTER) + message(FATAL_ERROR "${NO_OMIT_FRAME_POINTER_MSVC_FLAG} flag not supported") +endif() + +# FIXME: This doesn't make a huge amount of sense but the old +# build system kept the frame pointer for all configurations +# except x86_64 release (I don't know why the frame pointer +# is kept for i686 release). +if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") + list(APPEND Z3_COMPONENT_CXX_FLAGS + $<$:${NO_OMIT_FRAME_POINTER_MSVC_FLAG}> + $<$:${NO_OMIT_FRAME_POINTER_MSVC_FLAG}> + ) +else() + list(APPEND Z3_COMPONENT_CXX_FLAGS ${NO_OMIT_FRAME_POINTER_MSVC_FLAG}) +endif() + +if (("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") OR ("${TARGET_ARCHITECTURE}" STREQUAL "i686")) + # Use __cdecl calling convention. Apparently this is MSVC's default + # but the old build system set it so for completeness set it too. + # See https://msdn.microsoft.com/en-us/library/46t77ak2.aspx + z3_add_cxx_flag("/Gd" REQUIRED) +endif() + +# FIXME: The old build system explicitly disables code analysis. +# I don't know why. Duplicate this behaviour for now. +# See https://msdn.microsoft.com/en-us/library/ms173498.aspx +z3_add_cxx_flag("/analyze-" REQUIRED) From 5893aea60250c0e55475fd53326a0929a8028c8a Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 29 Apr 2017 12:12:54 +0100 Subject: [PATCH 32/41] [CMake] When building with MSVC and without `WARNINGS_AS_ERRORS` pass `/WX-` to MSVC. Although this is not necessary this duplicates the behaviour of the old build system. --- contrib/cmake/cmake/compiler_warnings.cmake | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/contrib/cmake/cmake/compiler_warnings.cmake b/contrib/cmake/cmake/compiler_warnings.cmake index e49e43947..e02b28b2c 100644 --- a/contrib/cmake/cmake/compiler_warnings.cmake +++ b/contrib/cmake/cmake/compiler_warnings.cmake @@ -44,4 +44,11 @@ if (WARNINGS_AS_ERRORS) message(STATUS "Treating compiler warnings as errors") else() message(STATUS "Not treating compiler warnings as errors") + # FIXME: Remove "x.." when CMP0054 is set to NEW + if ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC") + # Warnings as errors is off by default for MSVC so setting this + # is not necessary but this duplicates the behaviour of the old + # build system. + list(APPEND Z3_COMPONENT_CXX_FLAGS "/WX-") + endif() endif() From c9aac0ba7787b98b3f2dd4268d252f434d3e2c1a Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 29 Apr 2017 12:48:49 +0100 Subject: [PATCH 33/41] [CMake] When building with MSVC try to disable incremental linking for all builds. --- contrib/cmake/cmake/msvc_legacy_quirks.cmake | 31 ++++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/contrib/cmake/cmake/msvc_legacy_quirks.cmake b/contrib/cmake/cmake/msvc_legacy_quirks.cmake index 050d34553..9411d112b 100644 --- a/contrib/cmake/cmake/msvc_legacy_quirks.cmake +++ b/contrib/cmake/cmake/msvc_legacy_quirks.cmake @@ -110,3 +110,34 @@ endif() # I don't know why. Duplicate this behaviour for now. # See https://msdn.microsoft.com/en-us/library/ms173498.aspx z3_add_cxx_flag("/analyze-" REQUIRED) + +################################################################################ +# Linker flags +################################################################################ + +# By default CMake enables incremental linking for Debug and RelWithDebInfo +# builds. The old build sytem disables it for all builds so try to do the same +# by changing all configurations if necessary + +string(TOUPPER "${available_build_types}" _build_types_as_upper) +foreach (_build_type ${_build_types_as_upper}) + foreach (t EXE SHARED STATIC) + set(_replacement "/INCREMENTAL:NO") + # Remove any existing incremental flags + string(REGEX REPLACE + "/INCREMENTAL:YES" + "${_replacement}" + _replaced_linker_flags + "${CMAKE_${t}_LINKER_FLAGS_${_build_type}}") + string(REGEX REPLACE + "(/INCREMENTAL$)|(/INCREMENTAL )" + "${_replacement} " + _replaced_linker_flags + "${_replaced_linker_flags}") + if (NOT "${_replaced_linker_flags}" MATCHES "${_replacement}") + # Flag not present. Add it + string(APPEND _replaced_linker_flags " ${_replacement}") + endif() + set(CMAKE_${t}_LINKER_FLAGS_${_build_type} "${_replaced_linker_flags}") + endforeach() +endforeach() From 364bcde6c1daa9efa4db30cad5fc179cc304d287 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 29 Apr 2017 13:28:44 +0100 Subject: [PATCH 34/41] [CMake] When building with MSVC pass the `/STACK:` argument to the linker like the old build system does. --- contrib/cmake/cmake/msvc_legacy_quirks.cmake | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/contrib/cmake/cmake/msvc_legacy_quirks.cmake b/contrib/cmake/cmake/msvc_legacy_quirks.cmake index 9411d112b..d0ca00c83 100644 --- a/contrib/cmake/cmake/msvc_legacy_quirks.cmake +++ b/contrib/cmake/cmake/msvc_legacy_quirks.cmake @@ -118,7 +118,6 @@ z3_add_cxx_flag("/analyze-" REQUIRED) # By default CMake enables incremental linking for Debug and RelWithDebInfo # builds. The old build sytem disables it for all builds so try to do the same # by changing all configurations if necessary - string(TOUPPER "${available_build_types}" _build_types_as_upper) foreach (_build_type ${_build_types_as_upper}) foreach (t EXE SHARED STATIC) @@ -141,3 +140,12 @@ foreach (_build_type ${_build_types_as_upper}) set(CMAKE_${t}_LINKER_FLAGS_${_build_type} "${_replaced_linker_flags}") endforeach() endforeach() + +# The original build system passes `/STACK:` to the linker. +# This size comes from the original build system. +# FIXME: What is the rationale behind this? +set(STACK_SIZE_MSVC_LINKER 8388608) +# MSVC documentation (https://msdn.microsoft.com/en-us/library/35yc2tc3.aspx) +# says this only matters for executables which is why this is not being +# set for CMAKE_SHARED_LINKER_FLAGS or CMAKE_STATIC_LINKER_FLAGS. +string(APPEND CMAKE_EXE_LINKER_FLAGS " /STACK:${STACK_SIZE_MSVC_LINKER}") From d032dbcbb238e9be365d9b8057190d9f3f375def Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 29 Apr 2017 13:49:53 +0100 Subject: [PATCH 35/41] [CMake] When using MSVC set the `/SUBSYSTEM:` argument given to the linker. This mimics the behaviour of the old build system. --- contrib/cmake/cmake/msvc_legacy_quirks.cmake | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/contrib/cmake/cmake/msvc_legacy_quirks.cmake b/contrib/cmake/cmake/msvc_legacy_quirks.cmake index d0ca00c83..f36a5bfb0 100644 --- a/contrib/cmake/cmake/msvc_legacy_quirks.cmake +++ b/contrib/cmake/cmake/msvc_legacy_quirks.cmake @@ -149,3 +149,13 @@ set(STACK_SIZE_MSVC_LINKER 8388608) # says this only matters for executables which is why this is not being # set for CMAKE_SHARED_LINKER_FLAGS or CMAKE_STATIC_LINKER_FLAGS. string(APPEND CMAKE_EXE_LINKER_FLAGS " /STACK:${STACK_SIZE_MSVC_LINKER}") + +# The original build system passes `/SUBSYSTEM:` to the linker where `` +# depends on what is being linked. Where `` is `CONSOLE` for executables +# and `WINDOWS` for shard libraries. +# We don't need to pass `/SUBSYSTEM:CONSOLE` because CMake will do this for +# us when building executables because we don't pass the `WIN32` argument to +# `add_executable()`. +# FIXME: We probably don't need this. https://msdn.microsoft.com/en-us/library/fcc1zstk.aspx +# suggests that `/SUBSYSTEM:` only matters for executables. +string(APPEND CMAKE_SHARED_LINKER_FLAGS " /SUBSYSTEM:WINDOWS") From 2a919cf16e7d6807a76fa2806d37486c7e7e04e5 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 29 Apr 2017 15:02:01 +0100 Subject: [PATCH 36/41] [CMake] Duplicate the remaining linker flags from the old build system. --- contrib/cmake/cmake/msvc_legacy_quirks.cmake | 33 ++++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/contrib/cmake/cmake/msvc_legacy_quirks.cmake b/contrib/cmake/cmake/msvc_legacy_quirks.cmake index f36a5bfb0..2ca20277c 100644 --- a/contrib/cmake/cmake/msvc_legacy_quirks.cmake +++ b/contrib/cmake/cmake/msvc_legacy_quirks.cmake @@ -159,3 +159,36 @@ string(APPEND CMAKE_EXE_LINKER_FLAGS " /STACK:${STACK_SIZE_MSVC_LINKER}") # FIXME: We probably don't need this. https://msdn.microsoft.com/en-us/library/fcc1zstk.aspx # suggests that `/SUBSYSTEM:` only matters for executables. string(APPEND CMAKE_SHARED_LINKER_FLAGS " /SUBSYSTEM:WINDOWS") + +# FIXME: The following linker flags are weird. They are set in all configurations +# in the old build system except release x86_64. We try to emulate this here but +# this is likely the wrong thing to do. +foreach (_build_type ${_build_types_as_upper}) + if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64" AND + ("${_build_type}" STREQUAL "RELEASE" OR + "${_build_type}" STREQUAL "RELWITHDEBINFO") + ) + message(AUTHOR_WARNING "Skipping legacy linker MSVC options for x86_64 ${_build_type}") + else() + # Linker optimizations. + # See https://msdn.microsoft.com/en-us/library/bxwfs976.aspx + string(APPEND CMAKE_EXE_LINKER_FLAGS_${_build_type} " /OPT:REF /OPT:ICF") + string(APPEND CMAKE_SHARED_LINKER_FLAGS_${_build_type} " /OPT:REF /OPT:ICF") + + # FIXME: This is not necessary. This is MSVC's default. + # See https://msdn.microsoft.com/en-us/library/b1kw34cb.aspx + string(APPEND CMAKE_EXE_LINKER_FLAGS_${_build_type} " /TLBID:1") + string(APPEND CMAKE_SHARED_LINKER_FLAGS_${_build_type} " /TLBID:1") + + # FIXME: This is not necessary. This is MSVC's default. + # Address space layout randomization + # See https://msdn.microsoft.com/en-us/library/bb384887.aspx + string(APPEND CMAKE_EXE_LINKER_FLAGS_${_build_type} " /DYNAMICBASE") + string(APPEND CMAKE_SHARED_LINKER_FLAGS_${_build_type} " /DYNAMICBASE:NO") + + # FIXME: This is not necessary. This is MSVC's default. + # Indicate that the executable is compatible with DEP + # See https://msdn.microsoft.com/en-us/library/ms235442.aspx + string(APPEND CMAKE_EXE_LINKER_FLAGS_${_build_type} " /NXCOMPAT") + endif() +endforeach() From 6e07d6dd2d11c7c779640f7cdb9c234875454e88 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 29 Apr 2017 17:45:02 +0100 Subject: [PATCH 37/41] [CMake] Override CMake's default flags for GCC/Clang as we were doing before 4cc2b292c0cc8759da7a525e63dbfefdb06d6a01. It's useful to be able to control the defaults and CMake's internal logic for GCC/Clang is simple enough that doing this makes sense. It would be nice to do the same for MSVC but CMake's internal logic is more complicated so for now it's better that we just use CMake's default. --- CMakeLists.txt | 1 + .../cmake/cmake/cxx_compiler_flags_overrides.cmake | 14 ++++++++++++++ 2 files changed, 15 insertions(+) create mode 100644 contrib/cmake/cmake/cxx_compiler_flags_overrides.cmake diff --git a/CMakeLists.txt b/CMakeLists.txt index aa347ae66..19c56a413 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -24,6 +24,7 @@ if (NOT (EXISTS "${CMAKE_SOURCE_DIR}/src/CMakeLists.txt")) "``python contrib/cmake/bootstrap.py create``") endif() +set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake") project(Z3 CXX) ################################################################################ diff --git a/contrib/cmake/cmake/cxx_compiler_flags_overrides.cmake b/contrib/cmake/cmake/cxx_compiler_flags_overrides.cmake new file mode 100644 index 000000000..59966f424 --- /dev/null +++ b/contrib/cmake/cmake/cxx_compiler_flags_overrides.cmake @@ -0,0 +1,14 @@ +# This file overrides the default compiler flags for CMake's built-in +# configurations (CMAKE_BUILD_TYPE). Most compiler flags should not be set here. +# The main purpose is to have very fine grained control of the compiler flags. + +# We only override the defaults for Clang and GCC right now. +# CMake's MSVC logic is complicated so for now it's better to just inherit CMake's defaults. +if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")) + # Taken from Modules/Compiler/GNU.cmake + set(CMAKE_CXX_FLAGS_INIT "") + set(CMAKE_CXX_FLAGS_DEBUG_INIT "-g -O0") + set(CMAKE_CXX_FLAGS_MINSIZEREL_INIT "-Os -DNDEBUG") + set(CMAKE_CXX_FLAGS_RELEASE_INIT "-O3 -DNDEBUG") + set(CMAKE_CXX_FLAGS_RELWITHDEBINFO_INIT "-O2 -g -DNDEBUG") +endif() From fa868e058efa853cceff50e4ae925a8381a91cfc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 29 Apr 2017 17:39:02 -0700 Subject: [PATCH 38/41] fix bound bug #991 Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver.cpp | 100 ++++++++++++++++++++++++++++++++++++- src/smt/theory_arith.h | 1 + src/smt/theory_arith_nl.h | 38 +++++++++++--- src/test/cnf_backbones.cpp | 81 ++++++++++++++++++++++++++---- src/test/main.cpp | 14 +++++- 5 files changed, 215 insertions(+), 19 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 739a591e7..bc28221a9 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -3141,6 +3141,101 @@ namespace sat { // // ----------------------- +static void prune_unfixed(sat::literal_vector& lambda, sat::model const& m) { + for (unsigned i = 0; i < lambda.size(); ++i) { + if ((m[lambda[i].var()] == l_false) != lambda[i].sign()) { + lambda[i] = lambda.back(); + lambda.pop_back(); + --i; + } + } +} + +// Algorithm 7: Corebased Algorithm with Chunking + +static void back_remove(sat::literal_vector& lits, sat::literal l) { + for (unsigned i = lits.size(); i > 0; ) { + --i; + if (lits[i] == l) { + lits[i] = lits.back(); + lits.pop_back(); + return; + } + } + std::cout << "UNREACHABLE\n"; +} + + static void brute_force_consequences(sat::solver& s, sat::literal_vector const& asms, sat::literal_vector const& gamma, vector& conseq) { + for (unsigned i = 0; i < gamma.size(); ++i) { + sat::literal nlit = ~gamma[i]; + sat::literal_vector asms1(asms); + asms1.push_back(nlit); + lbool r = s.check(asms1.size(), asms1.c_ptr()); + if (r == l_false) { + conseq.push_back(s.get_core()); + } + } +} + + static lbool core_chunking(sat::solver& s, model const& m, sat::bool_var_vector const& vars, sat::literal_vector const& asms, vector& conseq, unsigned K) { + sat::literal_vector lambda; + for (unsigned i = 0; i < vars.size(); i++) { + lambda.push_back(sat::literal(i, m[vars[i]] == l_false)); + } + while (!lambda.empty()) { + IF_VERBOSE(1, verbose_stream() << "(sat-backbone-core " << lambda.size() << " " << conseq.size() << ")\n";); + unsigned k = std::min(K, lambda.size()); + sat::literal_vector gamma, omegaN; + for (unsigned i = 0; i < k; ++i) { + sat::literal l = lambda[lambda.size() - i - 1]; + gamma.push_back(l); + omegaN.push_back(~l); + } + while (true) { + sat::literal_vector asms1(asms); + asms1.append(omegaN); + lbool r = s.check(asms1.size(), asms1.c_ptr()); + if (r == l_true) { + IF_VERBOSE(1, verbose_stream() << "(sat) " << omegaN << "\n";); + prune_unfixed(lambda, s.get_model()); + break; + } + sat::literal_vector const& core = s.get_core(); + sat::literal_vector occurs; + IF_VERBOSE(1, verbose_stream() << "(core " << core.size() << ")\n";); + for (unsigned i = 0; i < omegaN.size(); ++i) { + if (core.contains(omegaN[i])) { + occurs.push_back(omegaN[i]); + } + } + if (occurs.size() == 1) { + sat::literal lit = occurs.back(); + sat::literal nlit = ~lit; + conseq.push_back(core); + back_remove(lambda, ~lit); + back_remove(gamma, ~lit); + s.mk_clause(1, &nlit); + } + for (unsigned i = 0; i < omegaN.size(); ++i) { + if (occurs.contains(omegaN[i])) { + omegaN[i] = omegaN.back(); + omegaN.pop_back(); + --i; + } + } + if (omegaN.empty() && occurs.size() > 1) { + brute_force_consequences(s, asms, gamma, conseq); + for (unsigned i = 0; i < gamma.size(); ++i) { + back_remove(lambda, gamma[i]); + } + break; + } + } + } + return l_true; + } + + lbool solver::get_consequences(literal_vector const& asms, bool_var_vector const& vars, vector& conseq) { literal_vector lits; lbool is_sat = l_true; @@ -3163,6 +3258,9 @@ namespace sat { default: break; } } + + // is_sat = core_chunking(*this, mdl, vars, asms, conseq, 100); + is_sat = get_consequences(asms, lits, conseq); set_model(mdl); return is_sat; @@ -3307,7 +3405,7 @@ namespace sat { propagate(false); ++num_resolves; } - if (scope_lvl() == 1) { + if (false && scope_lvl() == 1) { break; } } diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 77882f186..439adbdff 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -552,6 +552,7 @@ namespace smt { bool is_int(theory_var v) const { return m_data[v].m_is_int; } bool is_int_src(theory_var v) const { return m_util.is_int(var2expr(v)); } bool is_real(theory_var v) const { return !is_int(v); } + bool is_real_src(theory_var v) const { return !is_int_src(v); } bool get_implied_old_value(theory_var v, inf_numeral & r) const; inf_numeral const & get_implied_value(theory_var v) const; inf_numeral const & get_quasi_base_value(theory_var v) const { return get_implied_value(v); } diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index c8729ea36..8a632cf48 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -444,7 +444,7 @@ namespace smt { m_asserted_bounds.push_back(new_bound); // copy justification to new bound dependency2new_bound(dep, *new_bound); - TRACE("buggy_bound", new_bound->display(*this, tout); tout << "\n";); + TRACE("non_linear", new_bound->display(*this, tout); tout << "\n";); } /** @@ -457,8 +457,19 @@ namespace smt { bool r = false; if (!i.minus_infinity()) { inf_numeral new_lower(i.get_lower_value()); - if (i.is_lower_open()) - new_lower += get_epsilon(v); + if (i.is_lower_open()) { + if (is_int(v)) { + if (new_lower.is_int()) { + new_lower += rational::one(); + } + else { + new_lower = ceil(new_lower.get_rational()); + } + } + else { + new_lower += get_epsilon(v); + } + } bound * old_lower = lower(v); if (old_lower == 0 || new_lower > old_lower->get_value()) { TRACE("non_linear", tout << "NEW lower bound for v" << v << " " << new_lower << "\n"; @@ -469,8 +480,19 @@ namespace smt { } if (!i.plus_infinity()) { inf_numeral new_upper(i.get_upper_value()); - if (i.is_upper_open()) - new_upper -= get_epsilon(v); + if (i.is_upper_open()) { + if (is_int(v)) { + if (new_upper.is_int()) { + new_upper -= rational::one(); + } + else { + new_upper = floor(new_upper.get_rational()); + } + } + else { + new_upper -= get_epsilon(v); + } + } bound * old_upper = upper(v); if (old_upper == 0 || new_upper < old_upper->get_value()) { TRACE("non_linear", tout << "NEW upper bound for v" << v << " " << new_upper << "\n"; @@ -819,6 +841,7 @@ namespace smt { if (is_fixed(_var)) r *= lower_bound(_var).get_rational(); } + TRACE("arith", tout << mk_pp(m, get_manager()) << " " << r << "\n";); return r; } @@ -896,7 +919,7 @@ namespace smt { // Assert the equality // (= (* x_1 ... x_n) k) - TRACE("non_linear", tout << "all variables are fixed.\n";); + TRACE("non_linear", tout << "all variables are fixed, and bound is: " << k << "\n";); new_lower = alloc(derived_bound, v, inf_numeral(k), B_LOWER); new_upper = alloc(derived_bound, v, inf_numeral(k), B_UPPER); } @@ -953,7 +976,8 @@ namespace smt { new_upper->m_eqs.append(new_lower->m_eqs); TRACE("non_linear", - tout << "lower: " << new_lower << " upper: " << new_upper << "\n"; + new_lower->display(*this, tout << "lower: "); tout << "\n"; + new_upper->display(*this, tout << "upper: "); tout << "\n"; for (unsigned j = 0; j < new_upper->m_lits.size(); ++j) { ctx.display_detailed_literal(tout, new_upper->m_lits[j]); tout << " "; diff --git a/src/test/cnf_backbones.cpp b/src/test/cnf_backbones.cpp index a4eaa4222..3387e1a8e 100644 --- a/src/test/cnf_backbones.cpp +++ b/src/test/cnf_backbones.cpp @@ -64,6 +64,56 @@ static void display_status(lbool r) { } } +static void track_clause(sat::solver& dst, + sat::literal_vector& lits, + sat::literal_vector& assumptions, + vector& tracking_clauses) { + sat::literal lit = sat::literal(dst.mk_var(true, false), false); + tracking_clauses.set(lit.var(), lits); + lits.push_back(~lit); + dst.mk_clause(lits.size(), lits.c_ptr()); + assumptions.push_back(lit); +} + + +static void track_clauses(sat::solver const& src, + sat::solver& dst, + sat::literal_vector& assumptions, + vector& tracking_clauses) { + for (sat::bool_var v = 0; v < src.num_vars(); ++v) { + dst.mk_var(false, true); + } + sat::literal_vector lits; + sat::literal lit; + sat::clause * const * it = src.begin_clauses(); + sat::clause * const * end = src.end_clauses(); + svector bin_clauses; + src.collect_bin_clauses(bin_clauses, false); + tracking_clauses.reserve(2*src.num_vars() + static_cast(end - it) + bin_clauses.size()); + + for (sat::bool_var v = 1; v < src.num_vars(); ++v) { + if (src.value(v) != l_undef) { + bool sign = src.value(v) == l_false; + lits.reset(); + lits.push_back(sat::literal(v, sign)); + track_clause(dst, lits, assumptions, tracking_clauses); + } + } + for (; it != end; ++it) { + lits.reset(); + sat::clause& cls = *(*it); + lits.append(static_cast(cls.end()-cls.begin()), cls.begin()); + track_clause(dst, lits, assumptions, tracking_clauses); + } + for (unsigned i = 0; i < bin_clauses.size(); ++i) { + lits.reset(); + lits.push_back(bin_clauses[i].first); + lits.push_back(bin_clauses[i].second); + track_clause(dst, lits, assumptions, tracking_clauses); + } +} + + static void prune_unfixed(sat::literal_vector& lambda, sat::model const& m) { for (unsigned i = 0; i < lambda.size(); ++i) { if ((m[lambda[i].var()] == l_false) != lambda[i].sign()) { @@ -88,18 +138,20 @@ static void back_remove(sat::literal_vector& lits, sat::literal l) { std::cout << "UNREACHABLE\n"; } -static void brute_force_consequences(sat::solver& s, sat::literal_vector const& gamma, sat::literal_vector& backbones) { +static void brute_force_consequences(sat::solver& s, sat::literal_vector const& asms, sat::literal_vector const& gamma, sat::literal_vector& backbones) { for (unsigned i = 0; i < gamma.size(); ++i) { sat::literal nlit = ~gamma[i]; - lbool r = s.check(1, &nlit); + sat::literal_vector asms1(asms); + asms1.push_back(nlit); + lbool r = s.check(asms1.size(), asms1.c_ptr()); if (r == l_false) { backbones.push_back(gamma[i]); } } } -static lbool core_chunking(sat::solver& s, sat::bool_var_vector& vars, vector& conseq, unsigned K) { - lbool r = s.check(); +static lbool core_chunking(sat::solver& s, sat::bool_var_vector& vars, sat::literal_vector const& asms, vector& conseq, unsigned K) { + lbool r = s.check(asms.size(), asms.c_ptr()); display_status(r); if (r != l_true) { return r; @@ -119,7 +171,9 @@ static lbool core_chunking(sat::solver& s, sat::bool_var_vector& vars, vector 1) { - brute_force_consequences(s, gamma, backbones); + brute_force_consequences(s, asms, gamma, backbones); for (unsigned i = 0; i < gamma.size(); ++i) { back_remove(lambda, gamma[i]); } @@ -174,6 +228,7 @@ static void cnf_backbones(bool use_chunk, char const* file_name) { p.set_bool("produce_models", true); reslimit limit; sat::solver solver(p, limit, 0); + sat::solver solver2(p, limit, 0); g_solver = &solver; if (file_name) { @@ -192,16 +247,22 @@ static void cnf_backbones(bool use_chunk, char const* file_name) { vector conseq; sat::bool_var_vector vars; sat::literal_vector assumptions; - for (unsigned i = 1; i < solver.num_vars(); ++i) { + if (p.get_bool("dimacs.core", false)) { + g_solver = &solver2; + vector tracking_clauses; + track_clauses(solver, solver2, assumptions, tracking_clauses); + } + + for (unsigned i = 1; i < g_solver->num_vars(); ++i) { vars.push_back(i); - solver.set_external(i); + g_solver->set_external(i); } lbool r; if (use_chunk) { - r = core_chunking(solver, vars, conseq, 100); + r = core_chunking(*g_solver, vars, assumptions, conseq, 100); } else { - r = solver.get_consequences(assumptions, vars, conseq); + r = g_solver->get_consequences(assumptions, vars, conseq); } std::cout << vars.size() << " " << conseq.size() << "\n"; display_status(r); diff --git a/src/test/main.cpp b/src/test/main.cpp index 4a54797ac..15f92b2f7 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -8,6 +8,7 @@ #include"timeit.h" #include"warning.h" #include "memory_manager.h" +#include"gparams.h" // // Unit tests fail by asserting. @@ -75,7 +76,7 @@ void display_usage() { void parse_cmd_line_args(int argc, char ** argv, bool& do_display_usage, bool& test_all) { int i = 1; while (i < argc) { - char * arg = argv[i]; + char * arg = argv[i], *eq_pos = 0; if (arg[0] == '-' || arg[0] == '/') { char * opt_name = arg + 1; @@ -118,6 +119,17 @@ void parse_cmd_line_args(int argc, char ** argv, bool& do_display_usage, bool& t } #endif } + else if (arg[0] != '"' && (eq_pos = strchr(arg, '='))) { + char * key = arg; + *eq_pos = 0; + char * value = eq_pos+1; + try { + gparams::set(key, value); + } + catch (z3_exception& ex) { + std::cerr << ex.msg() << "\n"; + } + } i++; } } From 3152833893ece622174d1b8e6fab443da1e409cf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 29 Apr 2017 18:55:47 -0700 Subject: [PATCH 39/41] fix unused variables Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 9dd082de0..7a9369fd3 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3874,8 +3874,8 @@ void theory_seq::new_eq_eh(dependency* deps, enode* n1, enode* n2) { } else if (n1 != n2 && m_util.is_re(n1->get_owner())) { warning_msg("equality between regular expressions is not yet supported"); - eautomaton* a1 = get_automaton(n1->get_owner()); - eautomaton* a2 = get_automaton(n2->get_owner()); + // eautomaton* a1 = get_automaton(n1->get_owner()); + // eautomaton* a2 = get_automaton(n2->get_owner()); // eautomaton* b1 = mk_difference(*a1, *a2); // eautomaton* b2 = mk_difference(*a2, *a1); // eautomaton* c = mk_union(*b1, *b2); From b3f720c2bf0ba2326f5c1513c27c3e142683d068 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 29 Apr 2017 18:58:34 -0700 Subject: [PATCH 40/41] fix unused variables Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_core.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 785e0120f..5c652414a 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -465,7 +465,7 @@ namespace smt { TRACE("arith_axiom", tout << mk_pp(ante, m) << "\n" << mk_pp(conseq, m) << "\n"; tout << s_ante << "\n" << s_conseq << "\n";); - literal lits[2] = {l_ante, l_conseq}; + // literal lits[2] = {l_ante, l_conseq}; mk_clause(l_ante, l_conseq, 0, 0); if (ctx.relevancy()) { if (l_ante == false_literal) { From 4468816d3223ff8efa604388c5967e34cf7fe354 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 29 Apr 2017 19:00:15 -0700 Subject: [PATCH 41/41] fix unused variables Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context_inv.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/smt/smt_context_inv.cpp b/src/smt/smt_context_inv.cpp index f63e07b57..e6551b8da 100644 --- a/src/smt/smt_context_inv.cpp +++ b/src/smt/smt_context_inv.cpp @@ -405,7 +405,6 @@ namespace smt { bool context::validate_justification(bool_var v, bool_var_data const& d, b_justification const& j) { if (j.get_kind() == b_justification::CLAUSE && v != true_bool_var) { clause* cls = j.get_clause(); - unsigned num_lits = cls->get_num_literals(); literal l = cls->get_literal(0); if (l.var() != v) { l = cls->get_literal(1);