diff --git a/.gitignore b/.gitignore index 8424ea64b..505601597 100644 --- a/.gitignore +++ b/.gitignore @@ -48,4 +48,6 @@ src/api/dotnet/Native.cs src/api/python/z3consts.py src/api/python/z3core.py src/ast/pattern/database.h -src/util/version.h \ No newline at end of file +src/util/version.h +src/api/java/Z3Native.c +src/api/java/Z3Native.java \ No newline at end of file diff --git a/doc/README b/doc/README index 68019ca86..818374808 100644 --- a/doc/README +++ b/doc/README @@ -3,9 +3,20 @@ API documentation To generate the API documentation for the C, .NET and Python APIs, we must execute - python mk_doc.py + python mk_api_doc.py We must have doxygen installed in our system. -The documentation will be stored in the subdirectory './html'. -The main file is './html/index.html' +The documentation will be stored in the subdirectory './api/html'. +The main file is './api/html/index.html' + +Code documentation +------------------ + +To generate documentation for the Z3 code, we must execute + + doxygen z3code.dox + +The documentation will be store in the subdirectory './code/html'. +The main file is './code/html/index.html' + diff --git a/doc/mk_doc.py b/doc/mk_api_doc.py similarity index 88% rename from doc/mk_doc.py rename to doc/mk_api_doc.py index b6ca4ae0b..cb90748ff 100644 --- a/doc/mk_doc.py +++ b/doc/mk_api_doc.py @@ -21,7 +21,7 @@ def cleanup_API(inf, outf): _outf.write(line) try: - mk_dir('html') + mk_dir('api/html') cleanup_API('../src/api/z3_api.h', 'z3_api.h') print "Removed annotations from z3_api.h." DEVNULL = open(os.devnull, 'wb') @@ -33,15 +33,15 @@ try: print "Generated C and .NET API documentation." os.remove('z3_api.h') print "Removed temporary file z3_api.h." - shutil.copy('z3.css', 'html/z3.css') + shutil.copy('z3.css', 'api/html/z3.css') print "Copied z3.css." - shutil.copy('z3.png', 'html/z3.png') + shutil.copy('z3.png', 'api/html/z3.png') print "Copied z3.png." sys.path.append('../src/api/python') pydoc.writedoc('z3') - shutil.move('z3.html', 'html/z3.html') + shutil.move('z3.html', 'api/html/z3.html') print "Generated Python documentation." - print "Documentation was successfully generated at subdirectory './html'." + print "Documentation was successfully generated at subdirectory './api/html'." except: print "ERROR: failed to generate documentation" exit(1) diff --git a/doc/update_website.cmd b/doc/update_website.cmd index 1b1ede627..106d6a4eb 100644 --- a/doc/update_website.cmd +++ b/doc/update_website.cmd @@ -1,4 +1,4 @@ REM Script for updating the website containing the Z3 API documentation. REM You must be inside the Microsoft network to execute this script, and REM robocopy must be in your PATH. -robocopy /S html \\research\root\web\external\en-us\UM\redmond\projects\z3 \ No newline at end of file +robocopy /S api\html \\research\root\web\external\en-us\UM\redmond\projects\z3 \ No newline at end of file diff --git a/doc/z3.dox b/doc/z3.dox index 0ab3d7656..6b8780352 100644 --- a/doc/z3.dox +++ b/doc/z3.dox @@ -38,7 +38,7 @@ PROJECT_NUMBER = # 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 = api # 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 diff --git a/doc/z3code.dox b/doc/z3code.dox new file mode 100644 index 000000000..7ec57594e --- /dev/null +++ b/doc/z3code.dox @@ -0,0 +1,1081 @@ +# Doxyfile 1.6.3 + +# This file describes the settings to be used by the documentation system +# doxygen (www.doxygen.org) for a project +# +# All text after a hash (#) is considered a comment and will be ignored +# The format is: +# TAG = value [value, ...] +# For lists items can also be appended using: +# TAG += value [value, ...] +# Values that contain spaces should be placed between quotes (" ") + +#--------------------------------------------------------------------------- +# Project related configuration options +#--------------------------------------------------------------------------- + +DOXYFILE_ENCODING = UTF-8 + +# The PROJECT_NAME tag is a single word (or a sequence of words surrounded +# by quotes) that should identify the project. + +PROJECT_NAME = Z3_CODE +PROJECT_NUMBER = +OUTPUT_DIRECTORY = code +CREATE_SUBDIRS = NO +OUTPUT_LANGUAGE = English +BRIEF_MEMBER_DESC = YES +REPEAT_BRIEF = YES +ABBREVIATE_BRIEF = "The $name class " \ + "The $name widget " \ + "The $name file " \ + is \ + provides \ + specifies \ + contains \ + represents \ + a \ + an \ + the + +# If the ALWAYS_DETAILED_SEC and REPEAT_BRIEF tags are both set to YES then +# Doxygen will generate a detailed section even if there is only a brief +# description. + +ALWAYS_DETAILED_SEC = YES +INLINE_INHERITED_MEMB = NO +FULL_PATH_NAMES = YES +STRIP_FROM_PATH = ".." +STRIP_FROM_INC_PATH = +SHORT_NAMES = NO +JAVADOC_AUTOBRIEF = NO +QT_AUTOBRIEF = NO +MULTILINE_CPP_IS_BRIEF = NO +INHERIT_DOCS = YES +SEPARATE_MEMBER_PAGES = NO +TAB_SIZE = 4 + +ALIASES = "beginfaq=" \ + "cmdopt{1}=\arg /\1" \ + "ext{1}=.\1" \ + "ty{1}=\1" \ + "emph{1}=\1" \ + "extdoc{2}=\2" \ + "nicebox{1}=
\1
" \ + "mlonly=\if Ocaml" \ + "endmlonly=\endif" \ + "mlh=\if Ocaml" \ + "endmlh=\endif" \ + "conly=" \ + "ccode{1}=\1" \ + "zframe=" + +OPTIMIZE_OUTPUT_FOR_C = YES +OPTIMIZE_OUTPUT_JAVA = NO +OPTIMIZE_FOR_FORTRAN = NO +OPTIMIZE_OUTPUT_VHDL = NO + +# Doxygen has a built-in mapping, but you can override or extend it using this tag. +# The format is ext=language, where ext is a file extension, and language is one of +# the parsers supported by doxygen: IDL, Java, Javascript, C#, C, C++, D, PHP, +# Objective-C, Python, Fortran, VHDL, C, C++. For instance to make doxygen treat +# .inc files as Fortran files (default is PHP), and .f files as C (default is Fortran), +# use: inc=Fortran f=C. Note that for custom extensions you also need to set FILE_PATTERNS otherwise the files are not read by doxygen. + +EXTENSION_MAPPING = + +BUILTIN_STL_SUPPORT = NO +CPP_CLI_SUPPORT = NO +SIP_SUPPORT = NO +IDL_PROPERTY_SUPPORT = YES +DISTRIBUTE_GROUP_DOC = NO +SUBGROUPING = YES +TYPEDEF_HIDES_STRUCT = NO +SYMBOL_CACHE_SIZE = 0 + +#--------------------------------------------------------------------------- +# Build related configuration options +#--------------------------------------------------------------------------- + +EXTRACT_ALL = YES +EXTRACT_PRIVATE = YES +EXTRACT_STATIC = YES +EXTRACT_LOCAL_CLASSES = YES +EXTRACT_LOCAL_METHODS = YES +EXTRACT_ANON_NSPACES = YES +HIDE_UNDOC_MEMBERS = NO +HIDE_UNDOC_CLASSES = NO +HIDE_FRIEND_COMPOUNDS = NO +HIDE_IN_BODY_DOCS = NO +INTERNAL_DOCS = YES +CASE_SENSE_NAMES = NO + +# If the HIDE_SCOPE_NAMES tag is set to NO (the default) then Doxygen +# will show members with their full class and namespace scopes in the +# documentation. If set to YES the scope will be hidden. + +HIDE_SCOPE_NAMES = YES + +SHOW_INCLUDE_FILES = YES + +FORCE_LOCAL_INCLUDES = NO +INLINE_INFO = YES +SORT_MEMBER_DOCS = YES + +# If the SORT_BRIEF_DOCS tag is set to YES then doxygen will sort the +# brief documentation of file, namespace and class members alphabetically +# by member name. If set to NO (the default) the members will appear in +# declaration order. + +SORT_BRIEF_DOCS = NO + +# If the SORT_MEMBERS_CTORS_1ST tag is set to YES then doxygen will sort the (brief and detailed) documentation of class members so that constructors and destructors are listed first. If set to NO (the default) the constructors will appear in the respective orders defined by SORT_MEMBER_DOCS and SORT_BRIEF_DOCS. This tag will be ignored for brief docs if SORT_BRIEF_DOCS is set to NO and ignored for detailed docs if SORT_MEMBER_DOCS is set to NO. + +SORT_MEMBERS_CTORS_1ST = NO + +# If the SORT_GROUP_NAMES tag is set to YES then doxygen will sort the +# hierarchy of group names into alphabetical order. If set to NO (the default) +# the group names will appear in their defined order. + +SORT_GROUP_NAMES = NO + +# If the SORT_BY_SCOPE_NAME tag is set to YES, the class list will be +# sorted by fully-qualified names, including namespaces. If set to +# NO (the default), the class list will be sorted only by class name, +# not including the namespace part. +# Note: This option is not very useful if HIDE_SCOPE_NAMES is set to YES. +# Note: This option applies only to the class list, not to the +# alphabetical list. + +SORT_BY_SCOPE_NAME = NO + +# The GENERATE_TODOLIST tag can be used to enable (YES) or +# disable (NO) the todo list. This list is created by putting \todo +# commands in the documentation. + +GENERATE_TODOLIST = YES + +# The GENERATE_TESTLIST tag can be used to enable (YES) or +# disable (NO) the test list. This list is created by putting \test +# commands in the documentation. + +GENERATE_TESTLIST = YES + +# The GENERATE_BUGLIST tag can be used to enable (YES) or +# disable (NO) the bug list. This list is created by putting \bug +# commands in the documentation. + +GENERATE_BUGLIST = YES + +# The GENERATE_DEPRECATEDLIST tag can be used to enable (YES) or +# disable (NO) the deprecated list. This list is created by putting +# \deprecated commands in the documentation. + +GENERATE_DEPRECATEDLIST= YES + +# The ENABLED_SECTIONS tag can be used to enable conditional +# documentation sections, marked by \if sectionname ... \endif. + +ENABLED_SECTIONS = + +# The MAX_INITIALIZER_LINES tag determines the maximum number of lines +# the initial value of a variable or define consists of for it to appear in +# the documentation. If the initializer consists of more lines than specified +# here it will be hidden. Use a value of 0 to hide initializers completely. +# The appearance of the initializer of individual variables and defines in the +# documentation can be controlled using \showinitializer or \hideinitializer +# command in the documentation regardless of this setting. + +MAX_INITIALIZER_LINES = 30 + +# Set the SHOW_USED_FILES tag to NO to disable the list of files generated +# at the bottom of the documentation of classes and structs. If set to YES the +# list will mention the files that were used to generate the documentation. + +SHOW_USED_FILES = NO + +# If the sources in your project are distributed over multiple directories +# then setting the SHOW_DIRECTORIES tag to YES will show the directory hierarchy +# in the documentation. The default is NO. + +SHOW_DIRECTORIES = NO + +# Set the SHOW_FILES tag to NO to disable the generation of the Files page. +# This will remove the Files entry from the Quick Index and from the +# Folder Tree View (if specified). The default is YES. + +SHOW_FILES = YES + +# Set the SHOW_NAMESPACES tag to NO to disable the generation of the +# Namespaces page. +# This will remove the Namespaces entry from the Quick Index +# and from the Folder Tree View (if specified). The default is YES. + +SHOW_NAMESPACES = YES + +# The FILE_VERSION_FILTER tag can be used to specify a program or script that +# doxygen should invoke to get the current version for each file (typically from +# the version control system). Doxygen will invoke the program by executing (via +# popen()) the command , where is the value of +# the FILE_VERSION_FILTER tag, and is the name of an input file +# provided by doxygen. Whatever the program writes to standard output +# is used as the file version. See the manual for examples. + +FILE_VERSION_FILTER = + +# The LAYOUT_FILE tag can be used to specify a layout file which will be parsed by +# doxygen. The layout file controls the global structure of the generated output files +# in an output format independent way. The create the layout file that represents +# doxygen's defaults, run doxygen with the -l option. You can optionally specify a +# file name after the option, if omitted DoxygenLayout.xml will be used as the name +# of the layout file. + +LAYOUT_FILE = + +#--------------------------------------------------------------------------- +# configuration options related to warning and progress messages +#--------------------------------------------------------------------------- + +# The QUIET tag can be used to turn on/off the messages that are generated +# by doxygen. Possible values are YES and NO. If left blank NO is used. + +QUIET = NO + +# The WARNINGS tag can be used to turn on/off the warning messages that are +# generated by doxygen. Possible values are YES and NO. If left blank +# NO is used. + +WARNINGS = YES + +# If WARN_IF_UNDOCUMENTED is set to YES, then doxygen will generate warnings +# for undocumented members. If EXTRACT_ALL is set to YES then this flag will +# automatically be disabled. + +WARN_IF_UNDOCUMENTED = YES + +# If WARN_IF_DOC_ERROR is set to YES, doxygen will generate warnings for +# potential errors in the documentation, such as not documenting some +# parameters in a documented function, or documenting parameters that +# don't exist or using markup commands wrongly. + +WARN_IF_DOC_ERROR = YES + +# This WARN_NO_PARAMDOC option can be abled to get warnings for +# functions that are documented, but have no documentation for their parameters +# or return value. If set to NO (the default) doxygen will only warn about +# wrong or incomplete parameter documentation, but not about the absence of +# documentation. + +WARN_NO_PARAMDOC = NO + +# The WARN_FORMAT tag determines the format of the warning messages that +# doxygen can produce. The string should contain the $file, $line, and $text +# tags, which will be replaced by the file and line number from which the +# warning originated and the warning text. Optionally the format may contain +# $version, which will be replaced by the version of the file (if it could +# be obtained via FILE_VERSION_FILTER) + +WARN_FORMAT = "$file:$line: $text " + +# The WARN_LOGFILE tag can be used to specify a file to which warning +# and error messages should be written. If left blank the output is written +# to stderr. + +WARN_LOGFILE = + +#--------------------------------------------------------------------------- +# configuration options related to the input files +#--------------------------------------------------------------------------- + +# The INPUT tag can be used to specify the files and/or directories that contain +# documented source files. You may enter file names like "myfile.cpp" or +# directories like "/usr/src/myproject". Separate the files or directories +# with spaces. + +INPUT = ../src + +# 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 +# also the default input encoding. Doxygen uses libiconv (or the iconv built +# into libc) for the transcoding. See http://www.gnu.org/software/libiconv for +# the list of possible encodings. + +INPUT_ENCODING = UTF-8 + +# If the value of the INPUT tag contains directories, you can use the +# FILE_PATTERNS tag to specify one or more wildcard pattern (like *.cpp +# and *.h) to filter out the source-files in the directories. If left +# blank the following patterns are tested: +# *.c *.cc *.cxx *.cpp *.c++ *.java *.ii *.ixx *.ipp *.i++ *.inl *.h *.hh *.hxx +# *.hpp *.h++ *.idl *.odl *.cs *.php *.php3 *.inc *.m *.mm *.py *.f90 + +FILE_PATTERNS = *.cpp *.h + +# 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. +# If left blank NO is used. + +RECURSIVE = YES + +# The EXCLUDE tag can be used to specify files and/or directories that should +# excluded from the INPUT source files. This way you can easily exclude a +# subdirectory from a directory tree whose root is specified with the INPUT tag. + +EXCLUDE = + +# The EXCLUDE_SYMLINKS tag can be used select whether or not files or +# directories that are symbolic links (a Unix filesystem feature) are excluded +# from the input. + +EXCLUDE_SYMLINKS = NO + +# If the value of the INPUT tag contains directories, you can use the +# EXCLUDE_PATTERNS tag to specify one or more wildcard patterns to exclude +# certain files from those directories. Note that the wildcards are matched +# against the file with absolute path, so to exclude all test directories +# for example use the pattern */test/* + +EXCLUDE_PATTERNS = + +# The EXCLUDE_SYMBOLS tag can be used to specify one or more symbol names +# (namespaces, classes, functions, etc.) that should be excluded from the +# output. The symbol name can be a fully qualified name, a word, or if the +# wildcard * is used, a substring. Examples: ANamespace, AClass, +# AClass::ANamespace, ANamespace::*Test + +EXCLUDE_SYMBOLS = + +# The EXAMPLE_PATH tag can be used to specify one or more files or +# directories that contain example code fragments that are included (see +# the \include command). + +EXAMPLE_PATH = + +# If the value of the EXAMPLE_PATH tag contains directories, you can use the +# EXAMPLE_PATTERNS tag to specify one or more wildcard pattern (like *.cpp +# and *.h) to filter out the source-files in the directories. If left +# blank all files are included. + +EXAMPLE_PATTERNS = * + +# If the EXAMPLE_RECURSIVE tag is set to YES then subdirectories will be +# searched for input files to be used with the \include or \dontinclude +# commands irrespective of the value of the RECURSIVE tag. +# Possible values are YES and NO. If left blank NO is used. + +EXAMPLE_RECURSIVE = NO + +# The IMAGE_PATH tag can be used to specify one or more files or +# directories that contain image that are included in the documentation (see +# the \image command). + +IMAGE_PATH = + +# The INPUT_FILTER tag can be used to specify a program that doxygen should +# invoke to filter for each input file. Doxygen will invoke the filter program +# by executing (via popen()) the command , where +# is the value of the INPUT_FILTER tag, and is the name of an +# input file. Doxygen will then use the output that the filter program writes +# to standard output. +# If FILTER_PATTERNS is specified, this tag will be +# ignored. + +INPUT_FILTER = + +# The FILTER_PATTERNS tag can be used to specify filters on a per file pattern +# basis. +# Doxygen will compare the file name with each pattern and apply the +# filter if there is a match. +# The filters are a list of the form: +# pattern=filter (like *.cpp=my_cpp_filter). See INPUT_FILTER for further +# info on how filters are used. If FILTER_PATTERNS is empty, INPUT_FILTER +# is applied to all files. + +FILTER_PATTERNS = + +# If the FILTER_SOURCE_FILES tag is set to YES, the input filter (if set using +# INPUT_FILTER) will be used to filter the input files when producing source +# files to browse (i.e. when SOURCE_BROWSER is set to YES). + +FILTER_SOURCE_FILES = NO + +#--------------------------------------------------------------------------- +# configuration options related to source browsing +#--------------------------------------------------------------------------- + +# If the SOURCE_BROWSER tag is set to YES then a list of source files will +# be generated. Documented entities will be cross-referenced with these sources. +# Note: To get rid of all source code in the generated output, make sure also +# VERBATIM_HEADERS is set to NO. + +SOURCE_BROWSER = YES + +# Setting the INLINE_SOURCES tag to YES will include the body +# of functions and classes directly in the documentation. + +INLINE_SOURCES = YES + +# Setting the STRIP_CODE_COMMENTS tag to YES (the default) will instruct +# doxygen to hide any special comment blocks from generated source code +# fragments. Normal C and C++ comments will always remain visible. + +STRIP_CODE_COMMENTS = YES + +# If the REFERENCED_BY_RELATION tag is set to YES +# then for each documented function all documented +# functions referencing it will be listed. + +REFERENCED_BY_RELATION = YES + +# If the REFERENCES_RELATION tag is set to YES +# then for each documented function all documented entities +# called/used by that function will be listed. + +REFERENCES_RELATION = YES + +# If the REFERENCES_LINK_SOURCE tag is set to YES (the default) +# and SOURCE_BROWSER tag is set to YES, then the hyperlinks from +# functions in REFERENCES_RELATION and REFERENCED_BY_RELATION lists will +# link to the source code. +# Otherwise they will link to the documentation. + +REFERENCES_LINK_SOURCE = YES + +# If the USE_HTAGS tag is set to YES then the references to source code +# will point to the HTML generated by the htags(1) tool instead of doxygen +# built-in source browser. The htags tool is part of GNU's global source +# tagging system (see http://www.gnu.org/software/global/global.html). You +# will need version 4.8.6 or higher. + +USE_HTAGS = NO + +# If the VERBATIM_HEADERS tag is set to YES (the default) then Doxygen +# will generate a verbatim copy of the header file for each class for +# which an include is specified. Set to NO to disable this. + +VERBATIM_HEADERS = NO + +#--------------------------------------------------------------------------- +# configuration options related to the alphabetical class index +#--------------------------------------------------------------------------- + +# If the ALPHABETICAL_INDEX tag is set to YES, an alphabetical index +# of all compounds will be generated. Enable this if the project +# contains a lot of classes, structs, unions or interfaces. + +ALPHABETICAL_INDEX = NO + +# If the alphabetical index is enabled (see ALPHABETICAL_INDEX) then +# the COLS_IN_ALPHA_INDEX tag can be used to specify the number of columns +# in which this list will be split (can be a number in the range [1..20]) + +COLS_IN_ALPHA_INDEX = 5 + +# In case all classes in a project start with a common prefix, all +# classes will be put under the same header in the alphabetical index. +# The IGNORE_PREFIX tag can be used to specify one or more prefixes that +# should be ignored while generating the index headers. + +IGNORE_PREFIX = + +#--------------------------------------------------------------------------- +# configuration options related to the HTML output +#--------------------------------------------------------------------------- + +# If the GENERATE_HTML tag is set to YES (the default) Doxygen will +# generate HTML output. + +GENERATE_HTML = YES + +# The HTML_OUTPUT tag is used to specify where the HTML docs will be put. +# If a relative path is entered the value of OUTPUT_DIRECTORY will be +# put in front of it. If left blank `html' will be used as the default path. + +HTML_OUTPUT = html + +# The HTML_FILE_EXTENSION tag can be used to specify the file extension for +# each generated HTML page (for example: .htm,.php,.asp). If it is left blank +# doxygen will generate files with .html extension. + +HTML_FILE_EXTENSION = .html + +# The HTML_HEADER tag can be used to specify a personal HTML header for +# each generated HTML page. If it is left blank doxygen will generate a +# standard header. + +HTML_HEADER = + +# The HTML_FOOTER tag can be used to specify a personal HTML footer for +# each generated HTML page. If it is left blank doxygen will generate a +# standard footer. + +HTML_FOOTER = + +# The HTML_STYLESHEET tag can be used to specify a user-defined cascading +# style sheet that is used by each HTML page. It can be used to +# fine-tune the look of the HTML output. If the tag is left blank doxygen +# will generate a default style sheet. Note that doxygen will try to copy +# the style sheet file to the HTML output directory, so don't put your own +# stylesheet in the HTML output directory as well, or it will be erased! + +HTML_STYLESHEET = + +# If the HTML_TIMESTAMP tag is set to YES then the footer of each generated HTML +# page will contain the date and time when the page was generated. Setting +# this to NO can help when comparing the output of multiple runs. + +HTML_TIMESTAMP = YES + +# If the HTML_ALIGN_MEMBERS tag is set to YES, the members of classes, +# files or namespaces will be aligned in HTML using tables. If set to +# NO a bullet list will be used. + +HTML_ALIGN_MEMBERS = YES + +# If the HTML_DYNAMIC_SECTIONS tag is set to YES then the generated HTML +# documentation will contain sections that can be hidden and shown after the +# page has loaded. For this to work a browser that supports +# JavaScript and DHTML is required (for instance Mozilla 1.0+, Firefox +# Netscape 6.0+, Internet explorer 5.0+, Konqueror, or Safari). + +HTML_DYNAMIC_SECTIONS = YES + +# If the GENERATE_DOCSET tag is set to YES, additional index files +# will be generated that can be used as input for Apple's Xcode 3 +# integrated development environment, introduced with OSX 10.5 (Leopard). +# To create a documentation set, doxygen will generate a Makefile in the +# HTML output directory. Running make will produce the docset in that +# directory and running "make install" will install the docset in +# ~/Library/Developer/Shared/Documentation/DocSets so that Xcode will find +# it at startup. +# See http://developer.apple.com/tools/creatingdocsetswithdoxygen.html for more information. + +GENERATE_DOCSET = NO + +# When GENERATE_DOCSET tag is set to YES, this tag determines the name of the +# feed. A documentation feed provides an umbrella under which multiple +# documentation sets from a single provider (such as a company or product suite) +# can be grouped. + +DOCSET_FEEDNAME = "Doxygen generated docs" + +# When GENERATE_DOCSET tag is set to YES, this tag specifies a string that +# should uniquely identify the documentation set bundle. This should be a +# reverse domain-name style string, e.g. com.mycompany.MyDocSet. Doxygen +# will append .docset to the name. + +DOCSET_BUNDLE_ID = org.doxygen.Project + +# If the GENERATE_HTMLHELP tag is set to YES, additional index files +# will be generated that can be used as input for tools like the +# Microsoft HTML help workshop to generate a compiled HTML help file (.chm) +# of the generated HTML documentation. + +GENERATE_HTMLHELP = NO + +# If the GENERATE_HTMLHELP tag is set to YES, the CHM_FILE tag can +# be used to specify the file name of the resulting .chm file. You +# can add a path in front of the file if the result should not be +# written to the html output directory. + +CHM_FILE = + +# If the GENERATE_HTMLHELP tag is set to YES, the HHC_LOCATION tag can +# be used to specify the location (absolute path including file name) of +# the HTML help compiler (hhc.exe). If non-empty doxygen will try to run +# the HTML help compiler on the generated index.hhp. + +HHC_LOCATION = + +# If the GENERATE_HTMLHELP tag is set to YES, the GENERATE_CHI flag +# controls if a separate .chi index file is generated (YES) or that +# it should be included in the master .chm file (NO). + +GENERATE_CHI = NO + +# If the GENERATE_HTMLHELP tag is set to YES, the CHM_INDEX_ENCODING +# is used to encode HtmlHelp index (hhk), content (hhc) and project file +# content. + +CHM_INDEX_ENCODING = + +# If the GENERATE_HTMLHELP tag is set to YES, the BINARY_TOC flag +# controls whether a binary table of contents is generated (YES) or a +# normal table of contents (NO) in the .chm file. + +BINARY_TOC = NO + +# The TOC_EXPAND flag can be set to YES to add extra items for group members +# to the contents of the HTML help documentation and to the tree view. + +TOC_EXPAND = NO + +# If the GENERATE_QHP tag is set to YES and both QHP_NAMESPACE and QHP_VIRTUAL_FOLDER +# are set, an additional index file will be generated that can be used as input for +# Qt's qhelpgenerator to generate a Qt Compressed Help (.qch) of the generated +# HTML documentation. + +GENERATE_QHP = NO + +# If the QHG_LOCATION tag is specified, the QCH_FILE tag can +# be used to specify the file name of the resulting .qch file. +# The path specified is relative to the HTML output folder. + +QCH_FILE = + +# The QHP_NAMESPACE tag specifies the namespace to use when generating +# Qt Help Project output. For more information please see +# http://doc.trolltech.com/qthelpproject.html#namespace + +QHP_NAMESPACE = org.doxygen.Project + +# The QHP_VIRTUAL_FOLDER tag specifies the namespace to use when generating +# Qt Help Project output. For more information please see +# http://doc.trolltech.com/qthelpproject.html#virtual-folders + +QHP_VIRTUAL_FOLDER = doc + +# If QHP_CUST_FILTER_NAME is set, it specifies the name of a custom filter to add. +# For more information please see +# http://doc.trolltech.com/qthelpproject.html#custom-filters + +QHP_CUST_FILTER_NAME = + +# The QHP_CUST_FILT_ATTRS tag specifies the list of the attributes of the custom filter to add.For more information please see +# Qt Help Project / Custom Filters. + +QHP_CUST_FILTER_ATTRS = + +# The QHP_SECT_FILTER_ATTRS tag specifies the list of the attributes this project's +# filter section matches. +# Qt Help Project / Filter Attributes. + +QHP_SECT_FILTER_ATTRS = + +# If the GENERATE_QHP tag is set to YES, the QHG_LOCATION tag can +# be used to specify the location of Qt's qhelpgenerator. +# If non-empty doxygen will try to run qhelpgenerator on the generated +# .qhp file. + +QHG_LOCATION = + +# If the GENERATE_ECLIPSEHELP tag is set to YES, additional index files +# will be generated, which together with the HTML files, form an Eclipse help +# plugin. To install this plugin and make it available under the help contents +# menu in Eclipse, the contents of the directory containing the HTML and XML +# files needs to be copied into the plugins directory of eclipse. The name of +# the directory within the plugins directory should be the same as +# the ECLIPSE_DOC_ID value. After copying Eclipse needs to be restarted before the help appears. + +GENERATE_ECLIPSEHELP = NO + +# A unique identifier for the eclipse help plugin. When installing the plugin +# the directory name containing the HTML and XML files should also have +# this name. + +ECLIPSE_DOC_ID = org.doxygen.Project + +# The DISABLE_INDEX tag can be used to turn on/off the condensed index at +# top of each HTML page. The value NO (the default) enables the index and +# the value YES disables it. + +DISABLE_INDEX = YES + +# This tag can be used to set the number of enum values (range [1..20]) +# that doxygen will group on one line in the generated HTML documentation. + +ENUM_VALUES_PER_LINE = 4 + +# The GENERATE_TREEVIEW tag is used to specify whether a tree-like index +# structure should be generated to display hierarchical information. +# If the tag value is set to YES, a side panel will be generated +# containing a tree-like index structure (just like the one that +# is generated for HTML Help). For this to work a browser that supports +# JavaScript, DHTML, CSS and frames is required (i.e. any modern browser). +# Windows users are probably better off using the HTML help feature. + +GENERATE_TREEVIEW = YES + +# By enabling USE_INLINE_TREES, doxygen will generate the Groups, Directories, +# and Class Hierarchy pages using a tree view instead of an ordered list. + +USE_INLINE_TREES = YES + +# If the treeview is enabled (see GENERATE_TREEVIEW) then this tag can be +# used to set the initial width (in pixels) of the frame in which the tree +# is shown. + +TREEVIEW_WIDTH = 250 + +# Use this tag to change the font size of Latex formulas included +# as images in the HTML documentation. The default is 10. Note that +# when you change the font size after a successful doxygen run you need +# to manually remove any form_*.png images from the HTML output directory +# to force them to be regenerated. + +FORMULA_FONTSIZE = 10 + +# When the SEARCHENGINE tag is enabled doxygen will generate a search box for the HTML output. The underlying search engine uses javascript +# and DHTML and should work on any modern browser. Note that when using HTML help (GENERATE_HTMLHELP), Qt help (GENERATE_QHP), or docsets (GENERATE_DOCSET) there is already a search function so this one should +# typically be disabled. For large projects the javascript based search engine +# can be slow, then enabling SERVER_BASED_SEARCH may provide a better solution. + +SEARCHENGINE = YES + +# When the SERVER_BASED_SEARCH tag is enabled the search engine will be implemented using a PHP enabled web server instead of at the web client using Javascript. Doxygen will generate the search PHP script and index +# file to put on the web server. The advantage of the server based approach is that it scales better to large projects and allows full text search. The disadvances is that it is more difficult to setup +# and does not have live searching capabilities. + +SERVER_BASED_SEARCH = NO + +#--------------------------------------------------------------------------- +# configuration options related to the LaTeX output +#--------------------------------------------------------------------------- + +GENERATE_LATEX = NO +LATEX_OUTPUT = latex +LATEX_CMD_NAME = latex +MAKEINDEX_CMD_NAME = makeindex +COMPACT_LATEX = NO +PAPER_TYPE = a4wide +EXTRA_PACKAGES = +LATEX_HEADER = +PDF_HYPERLINKS = NO +USE_PDFLATEX = YES +LATEX_BATCHMODE = NO +LATEX_HIDE_INDICES = NO +LATEX_SOURCE_CODE = NO + +GENERATE_RTF = NO +RTF_OUTPUT = rtf +COMPACT_RTF = NO +RTF_HYPERLINKS = NO +RTF_STYLESHEET_FILE = +RTF_EXTENSIONS_FILE = + +GENERATE_MAN = NO +MAN_OUTPUT = man +MAN_EXTENSION = .3 +MAN_LINKS = NO + +GENERATE_XML = NO +XML_OUTPUT = xml +XML_SCHEMA = +XML_DTD = +XML_PROGRAMLISTING = YES + +GENERATE_AUTOGEN_DEF = NO + +GENERATE_PERLMOD = NO +PERLMOD_LATEX = NO +PERLMOD_PRETTY = YES +PERLMOD_MAKEVAR_PREFIX = + +#--------------------------------------------------------------------------- +# Configuration options related to the preprocessor +#--------------------------------------------------------------------------- + +# If the ENABLE_PREPROCESSING tag is set to YES (the default) Doxygen will +# evaluate all C-preprocessor directives found in the sources and include +# files. + +ENABLE_PREPROCESSING = YES + +# If the MACRO_EXPANSION tag is set to YES Doxygen will expand all macro +# names in the source code. If set to NO (the default) only conditional +# compilation will be performed. Macro expansion can be done in a controlled +# way by setting EXPAND_ONLY_PREDEF to YES. + +MACRO_EXPANSION = YES + +# If the EXPAND_ONLY_PREDEF and MACRO_EXPANSION tags are both set to YES +# then the macro expansion is limited to the macros specified with the +# PREDEFINED and EXPAND_AS_DEFINED tags. + +EXPAND_ONLY_PREDEF = YES + +# If the SEARCH_INCLUDES tag is set to YES (the default) the includes files +# in the INCLUDE_PATH (see below) will be search if a #include is found. + +SEARCH_INCLUDES = YES + +# The INCLUDE_PATH tag can be used to specify one or more directories that +# contain include files that are not input files but should be processed by +# the preprocessor. + +INCLUDE_PATH = + +# You can use the INCLUDE_FILE_PATTERNS tag to specify one or more wildcard +# patterns (like *.h and *.hpp) to filter out the header-files in the +# directories. If left blank, the patterns specified with FILE_PATTERNS will +# be used. + +INCLUDE_FILE_PATTERNS = + +# The PREDEFINED tag can be used to specify one or more macro names that +# are defined before the preprocessor is started (similar to the -D option of +# gcc). The argument of the tag is a list of macros of the form: name +# or name=definition (no spaces). If the definition and the = are +# omitted =1 is assumed. To prevent a macro definition from being +# undefined via #undef or recursively expanded use the := operator +# instead of the = operator. + +PREDEFINED =Z3_ast_opt:=Z3_ast Z3_bool_opt:=Z3_bool Z3_func_interp_opt:=Z3_func_interp Z3_model_opt:=Z3_model __out_opt:=__out + +# If the MACRO_EXPANSION and EXPAND_ONLY_PREDEF tags are set to YES then +# this tag can be used to specify a list of macro names that should be expanded. +# The macro definition that is found in the sources will be used. +# Use the PREDEFINED tag if you want to use a different macro definition. + +EXPAND_AS_DEFINED = + +# Z3_ast_opt Z3_bool_opt Z3_func_interp_opt Z3_model_opt __out_opt + +# If the SKIP_FUNCTION_MACROS tag is set to YES (the default) then +# doxygen's preprocessor will remove all function-like macros that are alone +# on a line, have an all uppercase name, and do not end with a semicolon. Such +# function macros are typically used for boiler-plate code, and will confuse +# the parser if not removed. + +SKIP_FUNCTION_MACROS = YES + +#--------------------------------------------------------------------------- +# Configuration::additions related to external references +#--------------------------------------------------------------------------- + +# The TAGFILES option can be used to specify one or more tagfiles. +# Optionally an initial location of the external documentation +# can be added for each tagfile. The format of a tag file without +# this location is as follows: +# +# TAGFILES = file1 file2 ... +# Adding location for the tag files is done as follows: +# +# TAGFILES = file1=loc1 "file2 = loc2" ... +# where "loc1" and "loc2" can be relative or absolute paths or +# URLs. If a location is present for each tag, the installdox tool +# does not have to be run to correct the links. +# Note that each tag file must have a unique name +# (where the name does NOT include the path) +# If a tag file is not located in the directory in which doxygen +# is run, you must also specify the path to the tagfile here. + +TAGFILES = + +# When a file name is specified after GENERATE_TAGFILE, doxygen will create +# a tag file that is based on the input files it reads. + +GENERATE_TAGFILE = + +# If the ALLEXTERNALS tag is set to YES all external classes will be listed +# in the class index. If set to NO only the inherited external classes +# will be listed. + +ALLEXTERNALS = NO + +# If the EXTERNAL_GROUPS tag is set to YES all external groups will be listed +# in the modules index. If set to NO, only the current project's groups will +# be listed. + +EXTERNAL_GROUPS = YES + +# The PERL_PATH should be the absolute path and name of the perl script +# interpreter (i.e. the result of `which perl'). + +PERL_PATH = /usr/bin/perl + +#--------------------------------------------------------------------------- +# Configuration options related to the dot tool +#--------------------------------------------------------------------------- + +# If the CLASS_DIAGRAMS tag is set to YES (the default) Doxygen will +# generate a inheritance diagram (in HTML, RTF and LaTeX) for classes with base +# or super classes. Setting the tag to NO turns the diagrams off. Note that +# this option is superseded by the HAVE_DOT option below. This is only a +# fallback. It is recommended to install and use dot, since it yields more +# powerful graphs. + +CLASS_DIAGRAMS = YES + +# You can define message sequence charts within doxygen comments using the \msc +# command. Doxygen will then run the mscgen tool (see +# http://www.mcternan.me.uk/mscgen/) to produce the chart and insert it in the +# documentation. The MSCGEN_PATH tag allows you to specify the directory where +# the mscgen tool resides. If left empty the tool is assumed to be found in the +# default search path. + +MSCGEN_PATH = + +# If set to YES, the inheritance and collaboration graphs will hide +# inheritance and usage relations if the target is undocumented +# or is not a class. + +HIDE_UNDOC_RELATIONS = NO + +# If you set the HAVE_DOT tag to YES then doxygen will assume the dot tool is +# available from the path. This tool is part of Graphviz, a graph visualization +# toolkit from AT&T and Lucent Bell Labs. The other options in this section +# have no effect if this option is set to NO (the default) + +HAVE_DOT = YES + +# By default doxygen will write a font called FreeSans.ttf to the output +# directory and reference it in all dot files that doxygen generates. This +# font does not include all possible unicode characters however, so when you need +# these (or just want a differently looking font) you can specify the font name +# using DOT_FONTNAME. You need need to make sure dot is able to find the font, +# which can be done by putting it in a standard location or by setting the +# DOTFONTPATH environment variable or by setting DOT_FONTPATH to the directory +# containing the font. + +DOT_FONTNAME = FreeSans + +# The DOT_FONTSIZE tag can be used to set the size of the font of dot graphs. +# The default size is 10pt. + +DOT_FONTSIZE = 10 + +# By default doxygen will tell dot to use the output directory to look for the +# FreeSans.ttf font (which doxygen will put there itself). If you specify a +# different font using DOT_FONTNAME you can set the path where dot +# can find it using this tag. + +DOT_FONTPATH = + +# If the CLASS_GRAPH and HAVE_DOT tags are set to YES then doxygen +# will generate a graph for each documented class showing the direct and +# indirect inheritance relations. Setting this tag to YES will force the +# the CLASS_DIAGRAMS tag to NO. + +CLASS_GRAPH = YES + +# If the COLLABORATION_GRAPH and HAVE_DOT tags are set to YES then doxygen +# will generate a graph for each documented class showing the direct and +# indirect implementation dependencies (inheritance, containment, and +# class references variables) of the class with other documented classes. + +COLLABORATION_GRAPH = NO + +# If the GROUP_GRAPHS and HAVE_DOT tags are set to YES then doxygen +# will generate a graph for groups, showing the direct groups dependencies + +GROUP_GRAPHS = YES + +# If the UML_LOOK tag is set to YES doxygen will generate inheritance and +# collaboration diagrams in a style similar to the OMG's Unified Modeling +# Language. + +UML_LOOK = YES + +# If set to YES, the inheritance and collaboration graphs will show the +# relations between templates and their instances. + +TEMPLATE_RELATIONS = YES + +# If the ENABLE_PREPROCESSING, SEARCH_INCLUDES, INCLUDE_GRAPH, and HAVE_DOT +# tags are set to YES then doxygen will generate a graph for each documented +# file showing the direct and indirect include dependencies of the file with +# other documented files. + +INCLUDE_GRAPH = YES + +# If the ENABLE_PREPROCESSING, SEARCH_INCLUDES, INCLUDED_BY_GRAPH, and +# HAVE_DOT tags are set to YES then doxygen will generate a graph for each +# documented header file showing the documented files that directly or +# indirectly include this file. + +INCLUDED_BY_GRAPH = YES + +# If the CALL_GRAPH and HAVE_DOT options are set to YES then +# doxygen will generate a call dependency graph for every global function +# or class method. Note that enabling this option will significantly increase +# the time of a run. So in most cases it will be better to enable call graphs +# for selected functions only using the \callgraph command. + +CALL_GRAPH = YES + +# If the CALLER_GRAPH and HAVE_DOT tags are set to YES then +# doxygen will generate a caller dependency graph for every global function +# or class method. Note that enabling this option will significantly increase +# the time of a run. So in most cases it will be better to enable caller +# graphs for selected functions only using the \callergraph command. + +CALLER_GRAPH = YES + +# If the GRAPHICAL_HIERARCHY and HAVE_DOT tags are set to YES then doxygen +# will graphical hierarchy of all classes instead of a textual one. + +GRAPHICAL_HIERARCHY = YES + +# If the DIRECTORY_GRAPH, SHOW_DIRECTORIES and HAVE_DOT tags are set to YES +# then doxygen will show the dependencies a directory has on other directories +# in a graphical way. The dependency relations are determined by the #include +# relations between the files in the directories. + +DIRECTORY_GRAPH = YES + +# The DOT_IMAGE_FORMAT tag can be used to set the image format of the images +# generated by dot. Possible values are png, jpg, or gif +# If left blank png will be used. + +DOT_IMAGE_FORMAT = png + +# The tag DOT_PATH can be used to specify the path where the dot tool can be +# found. If left blank, it is assumed the dot tool can be found in the path. + +DOT_PATH = + +# The DOTFILE_DIRS tag can be used to specify one or more directories that +# contain dot files that are included in the documentation (see the +# \dotfile command). + +DOTFILE_DIRS = + +# The DOT_GRAPH_MAX_NODES tag can be used to set the maximum number of +# nodes that will be shown in the graph. If the number of nodes in a graph +# becomes larger than this value, doxygen will truncate the graph, which is +# visualized by representing a node as a red box. Note that doxygen if the +# number of direct children of the root node in a graph is already larger than +# DOT_GRAPH_MAX_NODES then the graph will not be shown at all. Also note +# that the size of a graph can be further restricted by MAX_DOT_GRAPH_DEPTH. + +DOT_GRAPH_MAX_NODES = 50 + +# The MAX_DOT_GRAPH_DEPTH tag can be used to set the maximum depth of the +# graphs generated by dot. A depth value of 3 means that only nodes reachable +# from the root by following a path via at most 3 edges will be shown. Nodes +# that lay further from the root node will be omitted. Note that setting this +# option to 1 or 2 may greatly reduce the computation time needed for large +# code bases. Also note that the size of a graph can be further restricted by +# DOT_GRAPH_MAX_NODES. Using a depth of 0 means no depth restriction. + +MAX_DOT_GRAPH_DEPTH = 1000 + +# Set the DOT_TRANSPARENT tag to YES to generate images with a transparent +# background. This is disabled by default, because dot on Windows does not +# seem to support this out of the box. Warning: Depending on the platform used, +# enabling this option may lead to badly anti-aliased labels on the edges of +# a graph (i.e. they become hard to read). + +DOT_TRANSPARENT = NO + +# Set the DOT_MULTI_TARGETS tag to YES allow dot to generate multiple output +# files in one run (i.e. multiple -o and -T options on the command line). This +# makes dot run faster, but since only newer versions of dot (>1.8.10) +# support this, this feature is disabled by default. + +DOT_MULTI_TARGETS = NO + +# If the GENERATE_LEGEND tag is set to YES (the default) Doxygen will +# generate a legend page explaining the meaning of the various boxes and +# arrows in the dot generated graphs. + +GENERATE_LEGEND = NO + +# If the DOT_CLEANUP tag is set to YES (the default) Doxygen will +# remove the intermediate dot files that are used to generate +# the various graphs. + +DOT_CLEANUP = YES diff --git a/scripts/mk_project.py b/scripts/mk_project.py index acf964589..6d2b7c70e 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -71,7 +71,7 @@ def init_project_def(): static=build_static_lib(), export_files=API_files) add_dot_net_dll('dotnet', ['api_dll'], 'api/dotnet', dll_name='Microsoft.Z3', assembly_info_dir='Properties') - add_java_dll('java', ['api_dll'], 'api/java', dll_name='libz3j') + add_java_dll('java', 'api/java', dll_name='libz3java') add_hlib('cpp', 'api/c++', includes2install=['z3++.h']) set_z3py_dir('api/python') # Examples diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 20a25908d..35ef7166d 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -22,10 +22,11 @@ from fnmatch import fnmatch import distutils.sysconfig import compileall import subprocess +import string def getenv(name, default): try: - return os.environ[name] + return os.environ[name].strip(' "\'') except: return default @@ -36,7 +37,7 @@ CXXFLAGS=getenv("CXXFLAGS", "") LDFLAGS=getenv("LDFLAGS", "") JAVA=getenv("JAVA", "java") JAVAC=getenv("JAVAC", "javac") -JAVAH=getenv("JAVAH", "javah") +JAVA_HOME=getenv("JAVA_HOME", None) CXX_COMPILERS=['g++', 'clang++'] C_COMPILERS=['gcc', 'clang'] @@ -72,6 +73,12 @@ VER_REVISION=None PREFIX='/usr' GMP=False +def is_windows(): + return IS_WINDOWS + +def unix_path2dos(path): + return string.join(path.split('/'), '\\') + def which(program): import os def is_exe(fpath): @@ -106,20 +113,25 @@ class TempFile: try: os.remove(self.name) except: - raise MKException("Failed to eliminate temporary file '%s'" % self.name) + pass def exec_cmd(cmd): if isinstance(cmd, str): cmd = cmd.split(' ') new_cmd = [] + first = True for e in cmd: - e = e.strip(' ') - if e != "": - se = e.split(' ') - if len(se) > 1: - new_cmd.extend(se) - else: - new_cmd.append(e) + if first: + # Allow spaces in the executable name + first = False + new_cmd.append(e) + else: + if e != "": + se = e.split(' ') + if len(se) > 1: + new_cmd.extend(se) + else: + new_cmd.append(e) cmd = new_cmd null = open(os.devnull, 'wb') try: @@ -177,23 +189,40 @@ def check_java(): rmf('Hello.class') if r != 0: raise MKException('Failed testing Java program. Set environment variable JAVA with the path to the Java virtual machine') - t2 = TempFile('Z3Native.java') - t2.add('public final class Z3Native { public static native long mkConfig(); }\n') - t2.commit() + find_java_home() + +def find_java_home(): + global JAVA_HOME + if JAVA_HOME != None: + if is_verbose(): + print "Checking jni.h..." + if os.path.exists('%s%sinclude%sjni.h' % (JAVA_HOME, os.sep, os.sep)): + return if is_verbose(): - print "Testing %s (for JNI)..." % JAVAC - r = exec_cmd([JAVAC, 'Z3Native.java']) - if r != 0: - raise MKException('Failed testing Java compiler (for source containing JNI bindings). Set environment variable JAVAC with the path to the Java compiler') - if is_verbose(): - print "Testing %s..." % JAVAH - r = exec_cmd([JAVAH, 'Z3Native']) - if not os.path.exists('Z3Native.h'): - r = 1 - rmf('Z3Native.h') - rmf('Z3Native.class') - if r != 0: - raise MKException('Failed testing Java JNI Header file generator. Set environment variable JAVAH with the path to the Java JNI header file generator') + print "Finding JAVA_HOME..." + t = TempFile('output') + null = open(os.devnull, 'wb') + try: + subprocess.call([JAVA, '-verbose'], stdout=t.fname, stderr=null) + t.commit() + except: + raise MKException('Failed to find JAVA_HOME') + open_pat = re.compile("\[Opened (.*)\]") + t = open('output', 'r') + for line in t: + m = open_pat.match(line) + if m: + # Remove last 3 directives from m.group(1) + print m.group(1) + tmp = m.group(1).split(os.sep) + path = string.join(tmp[:len(tmp) - 3], os.sep) + if is_verbose(): + print "Checking jni.h..." + if not os.path.exists('%s%sinclude%sjni.h' % (path, os.sep, os.sep)): + raise MKException("Failed to detect jni.h at '%s%sinclude'" % (path, os.sep)) + JAVA_HOME = path + return + raise MKException('Failed to find JAVA_HOME') def is64(): return sys.maxsize >= 2**32 @@ -311,17 +340,17 @@ def display_help(exit_code): print " --staticlib build Z3 static library." if not IS_WINDOWS: print " -g, --gmp use GMP." + print "" + print "Some influential environment variables:" if not IS_WINDOWS: - print "" - print "Some influential environment variables:" print " CXX C++ compiler" - print " CC C compiler (only used for compiling examples)" + print " CC C compiler" print " LDFLAGS Linker flags, e.g., -L if you have libraries in a non-standard directory" print " CPPFLAGS Preprocessor flags, e.g., -I if you have header files in a non-standard directory" print " CXXFLAGS C++ compiler flags" - print " JAVA Java virtual machine (only relevant if -j or --java option is provided)" - print " JAVAC Java compiler (only relevant if -j or --java option is provided)" - print " JAVAH Java H file generator for JNI bindinds (only relevant if -j or --java option is provided)" + print " JAVA Java virtual machine (only relevant if -j or --java option is provided)" + print " JAVAC Java compiler (only relevant if -j or --java option is provided)" + print " JAVA_HOME JDK installation directory (only relevant if -j or --java option is provided)" exit(exit_code) # Parse configuration option for mk_make script @@ -694,9 +723,9 @@ class ExeComponent(Component): def require_mem_initializer(self): return True - # All executables are included in the all: rule + # All executables (to be installed) are included in the all: rule def main_component(self): - return True + return self.install def mk_install(self, out): if self.install: @@ -892,17 +921,30 @@ class DotNetDLLComponent(Component): class JavaDLLComponent(Component): - def __init__(self, name, dll_name, path, deps): - Component.__init__(self, name, path, deps) + def __init__(self, name, dll_name, path): + Component.__init__(self, name, path, []) if dll_name == None: dll_name = name self.dll_name = dll_name def mk_makefile(self, out): - return + if is_java_enabled(): + dllfile = '%s$(SO_EXT)' % self.dll_name + out.write('%s: %s/Z3Native.java %s$(SO_EXT)\n' % (dllfile, self.to_src_dir, get_component('api_dll').dll_name)) + if IS_WINDOWS: + out.write('\tcd %s && %s Z3Native.java\n' % (unix_path2dos(self.to_src_dir), JAVAC)) + out.write('\tmove %s\\*.class .\n' % unix_path2dos(self.to_src_dir)) + out.write('\t$(CXX) $(CXXFLAGS) $(CXX_OUT_FLAG)Z3Native$(OBJ_EXT) -I"%s/include" -I"%s/include/win32" -I%s %s/Z3Native.c\n' % (JAVA_HOME, JAVA_HOME, get_component('api').to_src_dir, self.to_src_dir)) + out.write('\t$(SLINK) $(SLINK_OUT_FLAG)%s $(SLINK_FLAGS) Z3Native$(OBJ_EXT) libz3.lib\n' % dllfile) + else: + out.write('\tcd %s; %s Z3Native.java\n' % (self.to_src_dir, JAVAC)) + out.write('\tmv %s/*.class .\n' % self.to_src_dir) + out.write('\t$(CXX) $(CXXFLAGS) $(CXX_OUT_FLAG)Z3Native$(OBJ_EXT) -I"%s/include" -I%s %s/Z3Native.c\n' % (JAVA_HOME, get_component('api').to_src_dir, self.to_src_dir)) + out.write('\t$(SLINK) $(SLINK_OUT_FLAG)%s $(SLINK_FLAGS) -L. Z3Native$(OBJ_EXT) -lz3\n' % dllfile) + out.write('%s: %s\n\n' % (self.name, dllfile)) def main_component(self): - return JAVA_ENABLED + return is_java_enabled() class ExampleComponent(Component): @@ -1038,8 +1080,8 @@ def add_dot_net_dll(name, deps=[], path=None, dll_name=None, assembly_info_dir=N c = DotNetDLLComponent(name, dll_name, path, deps, assembly_info_dir) reg_component(name, c) -def add_java_dll(name, deps=[], path=None, dll_name=None): - c = JavaDLLComponent(name, dll_name, path, deps) +def add_java_dll(name, path=None, dll_name=None): + c = JavaDLLComponent(name, dll_name, path) reg_component(name, c) def add_cpp_example(name, path=None): @@ -1114,6 +1156,12 @@ def mk_config(): 'SLINK_EXTRA_FLAGS=/link /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608\n') # End of Windows VS config.mk + if is_verbose(): + print '64-bit: %s' % is64() + if is_java_enabled(): + print 'Java Home: %s' % JAVA_HOME + print 'Java Compiler: %s' % JAVAC + print 'Java VM: %s' % JAVA else: global CXX, CC, GMP, CPPFLAGS, CXXFLAGS, LDFLAGS ARITH = "internal" @@ -1202,9 +1250,9 @@ def mk_config(): print 'Prefix: %s' % PREFIX print '64-bit: %s' % is64() if is_java_enabled(): + print 'Java Home: %s' % JAVA_HOME print 'Java Compiler: %s' % JAVAC print 'Java VM: %s' % JAVA - print 'Java H gen.: %s' % JAVAH def mk_install(out): out.write('install:\n') diff --git a/scripts/update_api.py b/scripts/update_api.py index 89c7ab74d..b43c07ea5 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -137,6 +137,11 @@ Type2Java = { VOID : 'void', VOID_PTR : 'long', INT : 'int', UINT : 'int', INT64 STRING : 'String', STRING_PTR : 'StringPtr', BOOL : 'boolean', SYMBOL : 'long', PRINT_MODE : 'int', ERROR_CODE : 'int' } +Type2JavaW = { VOID : 'void', VOID_PTR : 'jlong', INT : 'jint', UINT : 'jint', INT64 : 'jlong', UINT64 : 'jlong', DOUBLE : 'jdouble', + STRING : 'jstring', STRING_PTR : 'jobject', + BOOL : 'jboolean', SYMBOL : 'jlong', PRINT_MODE : 'jint', ERROR_CODE : 'jint' } + + next_type_id = FIRST_OBJ_ID def def_Type(var, c_type, py_type): @@ -177,6 +182,13 @@ def type2java(ty): else: return Type2Java[ty] +def type2javaw(ty): + global Type2JavaW + if (ty >= FIRST_OBJ_ID): + return 'jlong' + else: + return Type2JavaW[ty] + def _in(ty): return (IN, ty); @@ -241,15 +253,31 @@ def param2java(p): if k == OUT: if param_type(p) == INT or param_type(p) == UINT: return "IntPtr" - elif param_type(p) == INT64 or param_type(p) == UINT64: + elif param_type(p) == INT64 or param_type(p) == UINT64 or param_type(p) >= FIRST_OBJ_ID: return "LongPtr" + elif param_type(p) == STRING: + return "StringPtr" else: - return "long" # ? + print "ERROR: unreachable code" + assert(False) + exit(1) if k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY: return "%s[]" % type2java(param_type(p)) else: return type2java(param_type(p)) +def param2javaw(p): + k = param_kind(p) + if k == OUT: + return "jobject" + if k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY: + if param_type(p) == INT or param_type(p) == UINT: + return "jintArray" + else: + return "jlongArray" + else: + return type2javaw(param_type(p)) + def param2pystr(p): if param_kind(p) == IN_ARRAY or param_kind(p) == OUT_ARRAY or param_kind(p) == IN_ARRAY or param_kind(p) == INOUT_ARRAY or param_kind(p) == OUT: return "ctypes.POINTER(%s)" % type2pystr(param_type(p)) @@ -440,6 +468,30 @@ def java_method_name(name): i = i + 1 return result +# Return the Java method name used to retrieve the elements of the given parameter +def java_get_array_elements(p): + if param_type(p) == INT or param_type(p) == UINT: + return 'GetIntArrayElements' + else: + return 'GetLongArrayElements' +# Return the Java method name used to release the elements of the given parameter +def java_release_array_elements(p): + if param_type(p) == INT or param_type(p) == UINT: + return 'ReleaseIntArrayElements' + else: + return 'ReleaseLongArrayElements' +# Return the type of the java array elements +def java_array_element_type(p): + if param_type(p) == INT or param_type(p) == UINT: + return 'jint' + else: + return 'jlong' +def java_set_array_region(p): + if param_type(p) == INT or param_type(p) == UINT: + return 'SetIntArrayRegion' + else: + return 'SetLongArrayRegion' + def mk_java(): if not is_java_enabled(): return @@ -447,12 +499,17 @@ def mk_java(): java_nativef = '%s/Z3Native.java' % java_dir java_wrapperf = '%s/Z3Native.c' % java_dir java_native = open(java_nativef, 'w') + java_native.write('// Automatically generated file\n') java_native.write('public final class Z3Native {\n') - java_native.write('public static class IntPtr { public int value; }\n') - java_native.write('public static class LongPtr { public long value; }\n') - java_native.write('public static class StringPtr { public String value; }\n') + java_native.write(' public static class IntPtr { public int value; }\n') + java_native.write(' public static class LongPtr { public long value; }\n') + java_native.write(' public static class StringPtr { public String value; }\n') + if is_windows(): + java_native.write(' static { System.loadLibrary("%s"); }\n' % get_component('java')) + else: + java_native.write(' static { System.loadLibrary("%s"); }\n' % get_component('java').dll_name[3:]) # We need 3: to extract the prexi 'lib' form the dll_name for name, result, params in _dotnet_decls: - java_native.write(' public static native %s %s(' % (type2java(result), java_method_name(name))) + java_native.write(' public static native %s %s(' % (type2java(result), java_method_name(name))) first = True i = 0; for param in params: @@ -463,7 +520,111 @@ def mk_java(): java_native.write('%s a%d' % (param2java(param), i)) i = i + 1 java_native.write(');\n') + java_native.write(' public static void main(String[] args) {\n') + java_native.write(' IntPtr major = new IntPtr(), minor = new IntPtr(), build = new IntPtr(), revision = new IntPtr();\n') + java_native.write(' getVersion(major, minor, build, revision);\n') + java_native.write(' System.out.format("Z3 (for Java) %d.%d.%d%n", major.value, minor.value, build.value);\n') + java_native.write(' }\n') java_native.write('}\n'); + java_wrapper = open(java_wrapperf, 'w') + java_wrapper.write('// Automatically generated file\n') + java_wrapper.write('#include\n') + java_wrapper.write('#include\n') + java_wrapper.write('#include"z3.h"\n') + java_wrapper.write('#ifdef __cplusplus\n') + java_wrapper.write('extern "C" {\n') + java_wrapper.write('#endif\n') + for name, result, params in _dotnet_decls: + java_wrapper.write('JNIEXPORT %s JNICALL Java_Z3Native_%s(JNIEnv * jenv, jclass cls' % (type2javaw(result), java_method_name(name))) + i = 0; + for param in params: + java_wrapper.write(', ') + java_wrapper.write('%s a%d' % (param2javaw(param), i)) + i = i + 1 + java_wrapper.write(') {\n') + # preprocess arrays, strings, in/out arguments + i = 0 + for param in params: + k = param_kind(param) + if k == OUT or k == INOUT: + java_wrapper.write(' %s _a%s;\n' % (type2str(param_type(param)), i)) + elif k == IN_ARRAY or k == INOUT_ARRAY: + java_wrapper.write(' %s * _a%s = (%s *) jenv->%s(a%s, NULL);\n' % (type2str(param_type(param)), + i, + type2str(param_type(param)), + java_get_array_elements(param), + i)) + elif k == OUT_ARRAY: + java_wrapper.write(' %s * _a%s = (%s *) malloc(((unsigned)a%s) * sizeof(%s));\n' % (type2str(param_type(param)), + i, + type2str(param_type(param)), + param_array_capacity_pos(param), + type2str(param_type(param)))) + elif k == IN and param_type(param) == STRING: + java_wrapper.write(' Z3_string _a%s = (Z3_string) jenv->GetStringUTFChars(a%s, NULL);\n' % (i, i)) + i = i + 1 + # invoke procedure + java_wrapper.write(' ') + if result != VOID: + java_wrapper.write('%s result = ' % type2str(result)) + java_wrapper.write('%s(' % name) + i = 0 + first = True + for param in params: + if first: + first = False + else: + java_wrapper.write(', ') + k = param_kind(param) + if k == OUT or k == INOUT: + java_wrapper.write('&_a%s' % i) + elif k == OUT_ARRAY or k == IN_ARRAY or k == INOUT_ARRAY: + java_wrapper.write('_a%s' % i) + elif k == IN and param_type(param) == STRING: + java_wrapper.write('_a%s' % i) + else: + java_wrapper.write('(%s)a%i' % (param2str(param), i)) + i = i + 1 + java_wrapper.write(');\n') + # cleanup + i = 0 + for param in params: + k = param_kind(param) + if k == OUT_ARRAY: + java_wrapper.write(' jenv->%s(a%s, 0, (jsize)a%s, (%s *) _a%s);\n' % (java_set_array_region(param), + i, + param_array_capacity_pos(param), + java_array_element_type(param), + i)) + java_wrapper.write(' free(_a%s);\n' % i) + elif k == IN_ARRAY or k == OUT_ARRAY: + java_wrapper.write(' jenv->%s(a%s, (%s *) _a%s, JNI_ABORT);\n' % (java_release_array_elements(param), + i, + java_array_element_type(param), + i)) + elif k == OUT or k == INOUT: + if param_type(param) == INT or param_type(param) == UINT: + java_wrapper.write(' {\n') + java_wrapper.write(' jclass mc = jenv->GetObjectClass(a%s);\n' % i) + java_wrapper.write(' jfieldID fid = jenv->GetFieldID(mc, "value", "I");\n') + java_wrapper.write(' jenv->SetIntField(a%s, fid, (jint) _a%s);\n' % (i, i)) + java_wrapper.write(' }\n') + else: + java_wrapper.write(' {\n') + java_wrapper.write(' jclass mc = jenv->GetObjectClass(a%s);\n' % i) + java_wrapper.write(' jfieldID fid = jenv->GetFieldID(mc, "value", "J");\n') + java_wrapper.write(' jenv->SetLongField(a%s, fid, (jlong) _a%s);\n' % (i, i)) + java_wrapper.write(' }\n') + i = i + 1 + # return + if result == STRING: + java_wrapper.write(' return jenv->NewStringUTF(result);\n') + elif result != VOID: + java_wrapper.write(' return (%s) result;\n' % type2javaw(result)) + java_wrapper.write('}\n') + java_wrapper.write('#ifdef __cplusplus\n') + java_wrapper.write('}\n') + java_wrapper.write('#endif\n') if is_verbose(): print "Generated '%s'" % java_nativef diff --git a/src/api/api_arith.cpp b/src/api/api_arith.cpp index e4d687d47..55aef4868 100644 --- a/src/api/api_arith.cpp +++ b/src/api/api_arith.cpp @@ -101,27 +101,14 @@ extern "C" { SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); } - if (mk_c(c)->fparams().m_pre_simplify_expr) { - // Do not use logging here... the function is implemented using API primitives - Z3_ast m1 = Z3_mk_int(c, -1, Z3_get_sort(c, args[0])); - Z3_ast args1[2] = { args[0], 0 }; - for (unsigned i = 1; i < num_args; ++i) { - Z3_ast args2[3] = { m1, args[i] }; - args1[1] = Z3_mk_mul(c, 2, args2); - args1[0] = Z3_mk_add(c, 2, args1); - } - RETURN_Z3(args1[0]); - } - else { - expr* r = to_expr(args[0]); - for (unsigned i = 1; i < num_args; ++i) { - expr* args1[2] = { r, to_expr(args[i]) }; - r = mk_c(c)->m().mk_app(mk_c(c)->get_arith_fid(), OP_SUB, 0, 0, 2, args1); - check_sorts(c, r); - } - mk_c(c)->save_ast_trail(r); - RETURN_Z3(of_expr(r)); + expr* r = to_expr(args[0]); + for (unsigned i = 1; i < num_args; ++i) { + expr* args1[2] = { r, to_expr(args[i]) }; + r = mk_c(c)->m().mk_app(mk_c(c)->get_arith_fid(), OP_SUB, 0, 0, 2, args1); + check_sorts(c, r); } + mk_c(c)->save_ast_trail(r); + RETURN_Z3(of_expr(r)); Z3_CATCH_RETURN(0); } @@ -129,12 +116,6 @@ extern "C" { Z3_TRY; LOG_Z3_mk_unary_minus(c, n); RESET_ERROR_CODE(); - if (mk_c(c)->fparams().m_pre_simplify_expr) { - Z3_ast m1 = Z3_mk_int(c, -1, Z3_get_sort(c, n)); - Z3_ast args[2] = { m1, n }; - Z3_ast r = Z3_mk_mul(c, 2, args); - RETURN_Z3(r); - } MK_UNARY_BODY(Z3_mk_unary_minus, mk_c(c)->get_arith_fid(), OP_UMINUS, SKIP); Z3_CATCH_RETURN(0); } diff --git a/src/api/api_bv.cpp b/src/api/api_bv.cpp index 32df30a64..8126c8e2a 100644 --- a/src/api/api_bv.cpp +++ b/src/api/api_bv.cpp @@ -280,12 +280,6 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ Z3_TRY; LOG_Z3_mk_bvsub(c, n1, n2); RESET_ERROR_CODE(); - // TODO: Do we really need this pre_simplifier hack? - if (mk_c(c)->fparams().m_pre_simplify_expr) { - Z3_ast m1 = Z3_mk_int(c, -1, Z3_get_sort(c, n2)); - Z3_ast r = Z3_mk_bvadd(c, n1, Z3_mk_bvmul(c, m1, n2)); - RETURN_Z3(r); - } MK_BINARY_BODY(Z3_mk_bvsub, mk_c(c)->get_bv_fid(), OP_BSUB, SKIP); Z3_CATCH_RETURN(0); } @@ -294,12 +288,6 @@ Z3_ast Z3_API NAME(Z3_context c, unsigned i, Z3_ast n) { \ Z3_TRY; LOG_Z3_mk_bvneg(c, n); RESET_ERROR_CODE(); - // TODO: Do we really need this pre_simplifier hack? - if (mk_c(c)->fparams().m_pre_simplify_expr) { - Z3_ast m1 = Z3_mk_int(c, -1, Z3_get_sort(c, n)); - Z3_ast r = Z3_mk_bvmul(c, m1, n); - RETURN_Z3(r); - } MK_UNARY_BODY(Z3_mk_bvneg, mk_c(c)->get_bv_fid(), OP_BNEG, SKIP); Z3_CATCH_RETURN(0); } diff --git a/src/api/java/README b/src/api/java/README new file mode 100644 index 000000000..0591eec88 --- /dev/null +++ b/src/api/java/README @@ -0,0 +1,4 @@ +Java bindings +------------- + +This is currently "working in progress". \ No newline at end of file diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 7c9247459..9570af43b 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1860,7 +1860,7 @@ BEGIN_MLAPI_EXCLUDE \param c logical context. \param num_sorts number of datatype sorts. \param sort_names names of datatype sorts. - \param sorts array of datattype sorts. + \param sorts array of datatype sorts. \param constructor_lists list of constructors, one list per sort. def_API('Z3_mk_datatypes', VOID, (_in(CONTEXT), _in(UINT), _in_array(1, SYMBOL), _out_array(1, SORT), _inout_array(1, CONSTRUCTOR_LIST))) diff --git a/src/ast/rewriter/bit_blaster/eager_bit_blaster.cpp b/src/ast/rewriter/bit_blaster/eager_bit_blaster.cpp deleted file mode 100644 index 2c7cab462..000000000 --- a/src/ast/rewriter/bit_blaster/eager_bit_blaster.cpp +++ /dev/null @@ -1,436 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - eager_bit_blaster.cpp - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2008-10-02. - -Revision History: - ---*/ - -#include"ast_ll_pp.h" -#include"eager_bit_blaster.h" - -eager_bit_blaster::basic_plugin::basic_plugin(ast_manager & m, eager_bit_blaster::bv_plugin & p, basic_simplifier_plugin & s): - simplifier_plugin(symbol("basic"), m), - m_main(p), - m_s(s) { -} - -eager_bit_blaster::basic_plugin::~basic_plugin() { -} - -bool eager_bit_blaster::basic_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { - if (f->get_decl_kind() == OP_ITE) { - SASSERT(num_args == 3); - return m_main.reduce_ite(args[0], args[1], args[2], result); - } - else if (f->get_decl_kind() == OP_NOT) { - // the internalizer assumes there is not double negation (not (not x)) - SASSERT(num_args == 1); - m_s.mk_not(args[0], result); - return true; - } - return false; -} - -eager_bit_blaster::bv_plugin::bv_plugin(ast_manager & m, bit_blaster_params const & p): - simplifier_plugin(symbol("bv"), m), - m_util(m), - m_bb(m, p), - m_s(m) { -} - -eager_bit_blaster::bv_plugin::~bv_plugin() { -} - -void eager_bit_blaster::bv_plugin::get_bits(expr * n, expr_ref_vector & out_bits) { - rational val; - unsigned bv_size; - if (m_util.is_numeral(n, val, bv_size)) { - TRACE("eager_bb_bug", tout << "bv_size: " << bv_size << "\n";); - m_bb.num2bits(val, bv_size, out_bits); - SASSERT(out_bits.size() == bv_size); - } - else if (m_util.is_mkbv(n)) { - out_bits.append(to_app(n)->get_num_args(), to_app(n)->get_args()); - } - else { - unsigned bv_size = m_util.get_bv_size(n); - for (unsigned i = 0; i < bv_size; i++) { - parameter p(i); - out_bits.push_back(m_manager.mk_app(get_family_id(), OP_BIT2BOOL, 1, &p, 1, &n)); - } - SASSERT(bv_size == out_bits.size()); - } -} - -inline app * eager_bit_blaster::bv_plugin::mk_mkbv(expr_ref_vector const & bits) { -#ifdef Z3DEBUG - for (unsigned i = 0; i < bits.size(); i++) { - expr * b = bits.get(i); - SASSERT(!m_manager.is_not(b) || !m_manager.is_not(to_app(b)->get_arg(0))); - } -#endif - return m_manager.mk_app(get_family_id(), OP_MKBV, bits.size(), bits.c_ptr()); -} - -#define MK_UNARY_REDUCE(OP, BB_OP) \ -void eager_bit_blaster::bv_plugin::OP(expr * arg, expr_ref & result) { \ - expr_ref_vector bits(m_manager); \ - get_bits(arg, bits); \ - expr_ref_vector out_bits(m_manager); \ - m_bb.BB_OP(bits.size(), bits.c_ptr(), out_bits); \ - result = mk_mkbv(out_bits); \ -} - -#define MK_BIN_REDUCE(OP, BB_OP) \ -void eager_bit_blaster::bv_plugin::OP(expr * arg1, expr * arg2, expr_ref & result) { \ - expr_ref_vector bits1(m_manager); \ - expr_ref_vector bits2(m_manager); \ - get_bits(arg1, bits1); \ - get_bits(arg2, bits2); \ - expr_ref_vector out_bits(m_manager); \ - m_bb.BB_OP(bits1.size(), bits1.c_ptr(), bits2.c_ptr(), out_bits); \ - result = mk_mkbv(out_bits); \ -} - -#define MK_BIN_AC_FLAT_REDUCE(OP, BIN_OP, S_OP, BB_OP) \ -MK_BIN_REDUCE(BIN_OP, BB_OP); \ -void eager_bit_blaster::bv_plugin::OP(unsigned num_args, expr * const * args, expr_ref & result) { \ - SASSERT(num_args > 0); \ - if (num_args == 2) { \ - BIN_OP(args[0], args[1], result); \ - return; \ - } \ - \ - ptr_buffer args_bits; \ - for (unsigned i = 0; i < num_args; i++) { \ - expr_ref_vector * bits = alloc(expr_ref_vector, m_manager); \ - get_bits(args[i], *bits); \ - args_bits.push_back(bits); \ - } \ - \ - unsigned bv_size = m_util.get_bv_size(args[0]); \ - expr_ref_vector new_bits(m_manager); \ - for (unsigned i = 0; i < bv_size; i++) { \ - expr_ref_vector arg_bits(m_manager); \ - for (unsigned j = 0; j < num_args; j++) \ - arg_bits.push_back(args_bits[j]->get(i)); \ - expr_ref new_bit(m_manager); \ - m_s.S_OP(arg_bits.size(), arg_bits.c_ptr(), new_bit); \ - new_bits.push_back(new_bit); \ - } \ - result = mk_mkbv(new_bits); \ - std::for_each(args_bits.begin(), args_bits.end(), delete_proc()); \ -} - -#define MK_BIN_AC_REDUCE(OP, BIN_OP, BB_OP) \ -MK_BIN_REDUCE(BIN_OP, BB_OP); \ -void eager_bit_blaster::bv_plugin::OP(unsigned num_args, expr * const * args, expr_ref & result) { \ - SASSERT(num_args > 0); \ - result = args[0]; \ - for (unsigned i = 1; i < num_args; i++) { \ - expr_ref new_result(m_manager); \ - BIN_OP(result.get(), args[i], new_result); \ - result = new_result; \ - } \ -} - -#define MK_BIN_PRED_REDUCE(OP, BB_OP) \ -void eager_bit_blaster::bv_plugin::OP(expr * arg1, expr * arg2, expr_ref & result) { \ - expr_ref_vector bits1(m_manager); \ - expr_ref_vector bits2(m_manager); \ - get_bits(arg1, bits1); \ - get_bits(arg2, bits2); \ - m_bb.BB_OP(bits1.size(), bits1.c_ptr(), bits2.c_ptr(), result); \ -} - -#define MK_PARAMETRIC_UNARY_REDUCE(OP, BB_OP) \ -void eager_bit_blaster::bv_plugin::OP(expr * arg, unsigned n, expr_ref & result) { \ - expr_ref_vector bits(m_manager); \ - get_bits(arg, bits); \ - expr_ref_vector out_bits(m_manager); \ - m_bb.BB_OP(bits.size(), bits.c_ptr(), n, out_bits); \ - result = mk_mkbv(out_bits); \ -} - -MK_UNARY_REDUCE(reduce_not, mk_not); -MK_BIN_AC_FLAT_REDUCE(reduce_or, reduce_bin_or, mk_or, mk_or); -MK_BIN_AC_FLAT_REDUCE(reduce_and, reduce_bin_and, mk_and, mk_and); -MK_BIN_AC_FLAT_REDUCE(reduce_nor, reduce_bin_nor, mk_nor, mk_nor); -MK_BIN_AC_FLAT_REDUCE(reduce_nand, reduce_bin_nand, mk_nand, mk_nand); -MK_BIN_REDUCE(reduce_xor, mk_xor); -MK_BIN_REDUCE(reduce_xnor, mk_xnor); -MK_UNARY_REDUCE(reduce_neg, mk_neg); -MK_BIN_AC_REDUCE(reduce_add, reduce_bin_add, mk_adder); -MK_BIN_AC_REDUCE(reduce_mul, reduce_bin_mul, mk_multiplier); -MK_BIN_PRED_REDUCE(reduce_sle, mk_sle); -MK_BIN_PRED_REDUCE(reduce_ule, mk_ule); -MK_PARAMETRIC_UNARY_REDUCE(reduce_rotate_left, mk_rotate_left); -MK_PARAMETRIC_UNARY_REDUCE(reduce_rotate_right, mk_rotate_right); -MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend); -MK_PARAMETRIC_UNARY_REDUCE(reduce_zero_extend, mk_zero_extend); -MK_UNARY_REDUCE(reduce_redor, mk_redor); -MK_UNARY_REDUCE(reduce_redand, mk_redand); -MK_BIN_REDUCE(reduce_shl, mk_shl); -MK_BIN_REDUCE(reduce_ashr, mk_ashr); -MK_BIN_REDUCE(reduce_lshr, mk_lshr); -MK_BIN_REDUCE(reduce_comp, mk_comp); -MK_BIN_REDUCE(reduce_udiv, mk_udiv); -MK_BIN_REDUCE(reduce_urem, mk_urem); -MK_BIN_REDUCE(reduce_sdiv, mk_sdiv); -MK_BIN_REDUCE(reduce_srem, mk_srem); -MK_BIN_REDUCE(reduce_smod, mk_smod); - -void eager_bit_blaster::bv_plugin::reduce_extract(unsigned start, unsigned end, expr * arg, expr_ref & result) { - expr_ref_vector bits(m_manager); - get_bits(arg, bits); - expr_ref_vector out_bits(m_manager); - for (unsigned i = start; i <= end; ++i) - out_bits.push_back(bits.get(i)); - result = mk_mkbv(out_bits); -} - -void eager_bit_blaster::bv_plugin::reduce_concat(unsigned num_args, expr * const * args, expr_ref & result) { - expr_ref_vector out_bits(m_manager); - unsigned i = num_args; - while (i > 0) { - i--; - expr_ref_vector bits(m_manager); - get_bits(args[i], bits); - out_bits.append(bits.size(), bits.c_ptr()); - } - result = mk_mkbv(out_bits); -} - -bool eager_bit_blaster::bv_plugin::reduce_ite(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { - sort * s = m_manager.get_sort(arg2); - if (!m_util.is_bv_sort(s)) - return false; - expr_ref_vector bits1(m_manager); - expr_ref_vector bits2(m_manager); - get_bits(arg2, bits1); - get_bits(arg3, bits2); - SASSERT(bits1.size() == bits2.size()); - expr_ref_vector out_bits(m_manager); - unsigned bv_size = bits1.size(); - for (unsigned i = 0; i < bv_size; i++) { - expr_ref new_bit(m_manager); - m_s.mk_ite(arg1, bits1.get(i), bits2.get(i), new_bit); - out_bits.push_back(new_bit); - } - result = mk_mkbv(out_bits); - return true; -} - -bool eager_bit_blaster::bv_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { - bv_op_kind k = static_cast(f->get_decl_kind()); - switch (k) { - case OP_BNOT: - SASSERT(num_args == 1); - reduce_not(args[0], result); - return true; - case OP_BOR: - reduce_or(num_args, args, result); - return true; - case OP_BAND: - reduce_and(num_args, args, result); - return true; - case OP_BNOR: - reduce_nor(num_args, args, result); - return true; - case OP_BNAND: - reduce_nand(num_args, args, result); - return true; - case OP_BXOR: - SASSERT(num_args == 2); - reduce_xor(args[0], args[1], result); - return true; - case OP_BXNOR: - SASSERT(num_args == 2); - reduce_xnor(args[0], args[1], result); - return true; - case OP_BNEG: - SASSERT(num_args == 1); - reduce_neg(args[0], result); - return true; - case OP_BADD: - reduce_add(num_args, args, result); - return true; - case OP_BMUL: - reduce_mul(num_args, args, result); - return true; - case OP_BIT1: - case OP_BIT0: - case OP_BSUB: - // I'm assuming the expressions were simplified before invoking this method. - UNREACHABLE(); - return false; - case OP_BSDIV: - case OP_BUDIV: - case OP_BSREM: - case OP_BUREM: - case OP_BSMOD: - // I'm assuming the expressions were simplified before invoking this method. - UNREACHABLE(); - return false; - case OP_BSDIV0: - case OP_BUDIV0: - case OP_BSREM0: - case OP_BUREM0: - case OP_BSMOD0: - // do nothing... these are uninterpreted - return true; - case OP_BSDIV_I: - SASSERT(num_args == 2); - reduce_sdiv(args[0], args[1], result); - return true; - case OP_BUDIV_I: - SASSERT(num_args == 2); - reduce_udiv(args[0], args[1], result); - return true; - case OP_BSREM_I: - SASSERT(num_args == 2); - reduce_srem(args[0], args[1], result); - return true; - case OP_BUREM_I: - SASSERT(num_args == 2); - reduce_urem(args[0], args[1], result); - return true; - case OP_BSMOD_I: - SASSERT(num_args == 2); - reduce_smod(args[0], args[1], result); - return true; - case OP_ULEQ: - SASSERT(num_args == 2); - reduce_ule(args[0], args[1], result); - return true; - case OP_SLEQ: - SASSERT(num_args == 2); - reduce_sle(args[0], args[1], result); - return true; - case OP_UGEQ: - case OP_SGEQ: - case OP_ULT: - case OP_SLT: - case OP_UGT: - case OP_SGT: - // I'm assuming the expressions were simplified before invoking this method. - UNREACHABLE(); - return false; - case OP_EXTRACT: - SASSERT(num_args == 1); - reduce_extract(f->get_parameter(1).get_int(), f->get_parameter(0).get_int(), args[0], result); - return true; - case OP_CONCAT: - reduce_concat(num_args, args, result); - return true; - case OP_SIGN_EXT: - SASSERT(num_args == 1); - reduce_sign_extend(args[0], f->get_parameter(0).get_int(), result); - return true; - case OP_ZERO_EXT: - SASSERT(num_args == 1); - reduce_zero_extend(args[0], f->get_parameter(0).get_int(), result); - return true; - case OP_REPEAT: - UNREACHABLE(); - return false; - case OP_BREDOR: - SASSERT(num_args == 1); - reduce_redor(args[0], result); - return true; - case OP_BREDAND: - SASSERT(num_args == 1); - reduce_redand(args[0], result); - return true; - case OP_BCOMP: - SASSERT(num_args == 2); - reduce_comp(args[0], args[1], result); - return true; - case OP_BSHL: - SASSERT(num_args == 2); - reduce_shl(args[0], args[1], result); - return true; - case OP_BLSHR: - SASSERT(num_args == 2); - reduce_lshr(args[0], args[1], result); - return true; - case OP_BASHR: - SASSERT(num_args == 2); - reduce_ashr(args[0], args[1], result); - return true; - case OP_ROTATE_LEFT: - SASSERT(num_args == 1); - reduce_rotate_left(args[0], f->get_parameter(0).get_int(), result); - return true; - case OP_ROTATE_RIGHT: - SASSERT(num_args == 1); - reduce_rotate_right(args[0], f->get_parameter(0).get_int(), result); - return true; - default: - return false; - } -} - -bool eager_bit_blaster::bv_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & result) { - TRACE("eager_bb_eq", tout << mk_ll_pp(lhs, m_manager) << "\n" << mk_ll_pp(rhs, m_manager) << "\n";); - SASSERT(m_util.get_bv_size(lhs) == m_util.get_bv_size(rhs)); - expr_ref_vector bits1(m_manager); - expr_ref_vector bits2(m_manager); - get_bits(lhs, bits1); - get_bits(rhs, bits2); - SASSERT(bits1.size() == bits2.size()); - m_bb.mk_eq(bits1.size(), bits1.c_ptr(), bits2.c_ptr(), result); - return true; -} - -bool eager_bit_blaster::bv_plugin::reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result) { - if (num_args <= 1) { - result = m_manager.mk_true(); - } - if (num_args == 2) { - expr_ref tmp(m_manager); - reduce_eq(args[0], args[1], tmp); - m_s.mk_not(tmp, result); - } - else { - expr_ref_vector new_args(m_manager); - for (unsigned i = 0; i < num_args - 1; i++) { - expr * a1 = args[i]; - for (unsigned j = i + 1; j < num_args; j++) { - expr * a2 = args[j]; - expr_ref tmp1(m_manager); - reduce_eq(a1, a2, tmp1); - expr_ref tmp2(m_manager); - m_s.mk_not(tmp1, tmp2); - new_args.push_back(tmp2); - } - } - m_s.mk_and(new_args.size(), new_args.c_ptr(), result); - } - return true; -} - -eager_bit_blaster::eager_bit_blaster(ast_manager & m, bit_blaster_params const & p): - m_simplifier(m) { - m_simplifier.enable_ac_support(false); - bv_plugin * bv_p = alloc(bv_plugin, m, p); - m_simplifier.register_plugin(bv_p); - m_simplifier.register_plugin(alloc(basic_plugin, m, *bv_p, bv_p->get_basic_simplifier())); -} - -void eager_bit_blaster::operator()(expr * s, expr_ref & r, proof_ref & p) { - m_simplifier.operator()(s, r, p); -} - diff --git a/src/ast/rewriter/bit_blaster/eager_bit_blaster.h b/src/ast/rewriter/bit_blaster/eager_bit_blaster.h deleted file mode 100644 index d3d0284d1..000000000 --- a/src/ast/rewriter/bit_blaster/eager_bit_blaster.h +++ /dev/null @@ -1,107 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - eager_bit_blaster.h - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2008-10-02. - -Revision History: - ---*/ -#ifndef _EAGER_BIT_BLASTER_H_ -#define _EAGER_BIT_BLASTER_H_ - -#include"bv_decl_plugin.h" -#include"bit_blaster.h" -#include"simplifier.h" -#include"basic_simplifier_plugin.h" - -class eager_bit_blaster { - - class bv_plugin : public simplifier_plugin { - bv_util m_util; - bit_blaster m_bb; - basic_simplifier_plugin m_s; - - void get_bits(expr * n, expr_ref_vector & out_bits); - app * mk_mkbv(expr_ref_vector const & bits); - - void reduce_not(expr * arg, expr_ref & result); - void reduce_bin_or(expr * arg1, expr * arg2, expr_ref & result); - void reduce_or(unsigned num_args, expr * const * args, expr_ref & result); - void reduce_bin_and(expr * arg1, expr * arg2, expr_ref & result); - void reduce_and(unsigned num_args, expr * const * args, expr_ref & result); - void reduce_bin_nor(expr * arg1, expr * arg2, expr_ref & result); - void reduce_nor(unsigned num_args, expr * const * args, expr_ref & result); - void reduce_bin_nand(expr * arg1, expr * arg2, expr_ref & result); - void reduce_nand(unsigned num_args, expr * const * args, expr_ref & result); - void reduce_xor(expr * arg1, expr * arg2, expr_ref & result); - void reduce_xnor(expr * arg1, expr * arg2, expr_ref & result); - - void reduce_neg(expr * arg, expr_ref & result); - void reduce_bin_add(expr * arg1, expr * arg2, expr_ref & result); - void reduce_add(unsigned num_args, expr * const * args, expr_ref & result); - void reduce_bin_mul(expr * arg1, expr * arg2, expr_ref & result); - void reduce_mul(unsigned num_args, expr * const * args, expr_ref & result); - void reduce_sdiv(expr * arg1, expr * arg2, expr_ref & result); - void reduce_udiv(expr * arg1, expr * arg2, expr_ref & result); - void reduce_srem(expr * arg1, expr * arg2, expr_ref & result); - void reduce_urem(expr * arg1, expr * arg2, expr_ref & result); - void reduce_smod(expr * arg1, expr * arg2, expr_ref & result); - void reduce_sle(expr * arg1, expr * arg2, expr_ref & result); - void reduce_ule(expr * arg1, expr * arg2, expr_ref & result); - - void reduce_concat(unsigned num_args, expr * const * args, expr_ref & result); - void reduce_extract(unsigned start, unsigned end, expr * arg, expr_ref & result); - - void reduce_redor(expr * arg, expr_ref & result); - void reduce_redand(expr * arg, expr_ref & result); - - void reduce_comp(expr * arg1, expr * arg2, expr_ref & result); - void reduce_shl(expr * arg1, expr * arg2, expr_ref & result); - void reduce_ashr(expr * arg1, expr * arg2, expr_ref & result); - void reduce_lshr(expr * arg1, expr * arg2, expr_ref & result); - - void reduce_rotate_left(expr * arg, unsigned n, expr_ref & result); - void reduce_rotate_right(expr * arg, unsigned n, expr_ref & result); - void reduce_sign_extend(expr * arg, unsigned n, expr_ref & result); - void reduce_zero_extend(expr * arg, unsigned n, expr_ref & result); - - public: - bv_plugin(ast_manager & m, bit_blaster_params const & p); - virtual ~bv_plugin(); - virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); - virtual bool reduce_eq(expr * lhs, expr * rhs, expr_ref & result); - virtual bool reduce_distinct(unsigned num_args, expr * const * args, expr_ref & result); - basic_simplifier_plugin & get_basic_simplifier() { return m_s; } - bool reduce_ite(expr * arg1, expr * arg2, expr * arg3, expr_ref & result); - }; - - /** - \brief Plugin for handling the term-ite. - */ - class basic_plugin : public simplifier_plugin { - bv_plugin & m_main; - basic_simplifier_plugin & m_s; - public: - basic_plugin(ast_manager & m, bv_plugin & p, basic_simplifier_plugin & s); - virtual ~basic_plugin(); - virtual bool reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); - }; - - simplifier m_simplifier; -public: - eager_bit_blaster(ast_manager & m, bit_blaster_params const & p); - void operator()(expr * s, expr_ref & r, proof_ref & p); -}; - -#endif /* _EAGER_BIT_BLASTER_H_ */ - diff --git a/src/front_end_params/bit_blaster_params.h b/src/front_end_params/bit_blaster_params.h index b56be35db..8196774ca 100644 --- a/src/front_end_params/bit_blaster_params.h +++ b/src/front_end_params/bit_blaster_params.h @@ -22,16 +22,13 @@ Revision History: #include"ini_file.h" struct bit_blaster_params { - bool m_bb_eager; bool m_bb_ext_gates; bool m_bb_quantifiers; bit_blaster_params(): - m_bb_eager(false), m_bb_ext_gates(false), m_bb_quantifiers(false) { } void register_params(ini_params & p) { - p.register_bool_param("BB_EAGER", m_bb_eager, "eager bit blasting"); p.register_bool_param("BB_EXT_GATES", m_bb_ext_gates, "use extended gates during bit-blasting"); p.register_bool_param("BB_QUANTIFIERS", m_bb_quantifiers, "convert bit-vectors to Booleans in quantifiers"); } diff --git a/src/front_end_params/front_end_params.cpp b/src/front_end_params/front_end_params.cpp index a30e1dfd3..7aea7e7ee 100644 --- a/src/front_end_params/front_end_params.cpp +++ b/src/front_end_params/front_end_params.cpp @@ -21,12 +21,9 @@ Revision History: void front_end_params::register_params(ini_params & p) { p.register_param_vector(m_param_vector.get()); preprocessor_params::register_params(p); - spc_params::register_params(p); smt_params::register_params(p); parser_params::register_params(p); arith_simplifier_params::register_params(p); - p.register_int_param("ENGINE", 0, 2, reinterpret_cast(m_engine), "0: SMT solver, 1: Superposition prover, 2: EPR solver, true"); - z3_solver_params::register_params(p); model_params::register_params(p); p.register_bool_param("AT_LABELS_CEX", m_at_labels_cex, "only use labels that contain '@' when building multiple counterexamples"); @@ -43,7 +40,6 @@ void front_end_params::register_params(ini_params & p) { p.register_int_param("PROOF_MODE", 0, 2, reinterpret_cast(m_proof_mode), "select proof generation mode: 0 - disabled, 1 - coarse grain, 2 - fine grain"); p.register_bool_param("TRACE", m_trace, "enable tracing for the Axiom Profiler tool"); p.register_string_param("TRACE_FILE_NAME", m_trace_file_name, "tracing file name"); - p.register_bool_param("IGNORE_SETPARAMETER", m_ignore_setparameter, "ignore (SETPARAMETER ...) commands in Simplify format input"); p.register_bool_param("ASYNC_COMMANDS", m_async_commands, "enable/disable support for asynchronous commands in the Simplify front-end."); p.register_bool_param("DISPLAY_CONFIG", m_display_config, "display configuration used by Z3"); diff --git a/src/front_end_params/front_end_params.h b/src/front_end_params/front_end_params.h index cd582e28a..7a9b4e8e8 100644 --- a/src/front_end_params/front_end_params.h +++ b/src/front_end_params/front_end_params.h @@ -22,25 +22,16 @@ Revision History: #include"ini_file.h" #include"ast.h" #include"preprocessor_params.h" -#include"spc_params.h" #include"smt_params.h" #include"pp_params.h" #include"parser_params.h" #include"arith_simplifier_params.h" -#include"z3_solver_params.h" #include"model_params.h" -enum engine { - ENG_SMT, - ENG_SPC, - ENG_EPR -}; - -struct front_end_params : public preprocessor_params, public spc_params, public smt_params, public parser_params, - public arith_simplifier_params, public z3_solver_params, public model_params +struct front_end_params : public preprocessor_params, public smt_params, public parser_params, + public arith_simplifier_params, public model_params { ref m_param_vector; - engine m_engine; bool m_at_labels_cex; // only use labels which contains the @ symbol when building multiple counterexamples. bool m_check_at_labels; // check that @ labels are inserted to generate unique counter-examples. bool m_default_qid; @@ -65,7 +56,6 @@ struct front_end_params : public preprocessor_params, public spc_params, public bool m_trace; std::string m_trace_file_name; std::fstream* m_trace_stream; - bool m_ignore_setparameter; bool m_async_commands; bool m_display_config; bool m_user_theory_preprocess_axioms; @@ -74,7 +64,6 @@ struct front_end_params : public preprocessor_params, public spc_params, public front_end_params(): m_param_vector(alloc(param_vector, this)), - m_engine(ENG_SMT), m_at_labels_cex(false), m_check_at_labels(false), m_default_qid(false), @@ -107,7 +96,6 @@ struct front_end_params : public preprocessor_params, public spc_params, public m_trace(false), m_trace_file_name("z3.log"), m_trace_stream(NULL), - m_ignore_setparameter(false), m_async_commands(true), m_display_config(false), m_user_theory_preprocess_axioms(false), diff --git a/src/front_end_params/order_params.cpp b/src/front_end_params/order_params.cpp deleted file mode 100644 index 47fee103d..000000000 --- a/src/front_end_params/order_params.cpp +++ /dev/null @@ -1,27 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - order_params.cpp - -Abstract: - - Term ordering parameters. - -Author: - - Leonardo de Moura (leonardo) 2008-01-28. - -Revision History: - ---*/ -#include"order_params.h" - -void order_params::register_params(ini_params & p) { - p.register_symbol_list_param("PRECEDENCE", m_order_precedence, "describe a (partial) precedence for the term ordering used in the Superposition Calculus module. The precedence is lists of function symbols. Example: PRECEDENCE=\"(f, g, h)\""); - p.register_symbol_list_param("PRECEDENCE_GEN", m_order_precedence_gen, "describe how a total precedence order is generated. The generator is a sequence of simple (partial) orders with an optional '-' (indicating the next (partial) order should be inverted). The available simple (partial) orders are: user (the order specified by precedence); arity; interpreted (interpreted function symbols are considered smaller); definition (defined function symbols are considered bigger); frequency; arbitrary (total arbitrary order generated by Z3). Example: PRECEDENCE_GEN=\"user interpreted - arity arbitraty\""); - p.register_symbol_nat_list_param("ORDER_WEIGHTS", m_order_weights, "describe a (partial) assignment of weights to function symbols for term orderings (e.g., KBO). The assigment is a list of pairs of the form f:n where f is a string and n is a natural. Example: WEIGHTS=\"(f:1, g:2, h:3)\""); - p.register_unsigned_param("ORDER_VAR_WEIGHT", m_order_var_weight, "weight of variables in term orderings (e.g., KBO)"); - p.register_int_param("ORDER", 0, 1, reinterpret_cast(m_order_kind), "Term ordering: 0 - KBO, 1 - LPO"); -} diff --git a/src/front_end_params/order_params.h b/src/front_end_params/order_params.h deleted file mode 100644 index 17b7fa238..000000000 --- a/src/front_end_params/order_params.h +++ /dev/null @@ -1,44 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - order_params.h - -Abstract: - - Term ordering parameters. - -Author: - - Leonardo de Moura (leonardo) 2008-01-28. - -Revision History: - ---*/ -#ifndef _ORDER_PARAMS_H_ -#define _ORDER_PARAMS_H_ - -#include"ini_file.h" - -enum order_kind { - ORD_KBO, - ORD_LPO -}; - -struct order_params { - svector m_order_precedence; - svector m_order_precedence_gen; - svector m_order_weights; - unsigned m_order_var_weight; - order_kind m_order_kind; - - order_params(): - m_order_var_weight(1), - m_order_kind(ORD_KBO) { - } - - void register_params(ini_params & p); -}; - -#endif /* _ORDER_PARAMS_H_ */ diff --git a/src/front_end_params/spc_params.cpp b/src/front_end_params/spc_params.cpp deleted file mode 100644 index 248b73962..000000000 --- a/src/front_end_params/spc_params.cpp +++ /dev/null @@ -1,37 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - spc_params.cpp - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2008-02-08. - -Revision History: - ---*/ -#include"spc_params.h" - -void spc_params::register_params(ini_params & p) { - order_params::register_params(p); - p.register_unsigned_param("SPC_MIN_FUNC_FREQ_SUBSUMPTION_INDEX",m_min_func_freq_subsumption_index, - "minimal number of occurrences (in clauses) for a function symbol to be considered for subsumption indexing."); - p.register_unsigned_param("SPC_MAX_SUBSUMPTION_INDEX_FEATURES", m_max_subsumption_index_features, - "maximum number of features to be used for subsumption index."); - p.register_unsigned_param("SPC_INITIAL_SUBSUMPTION_INDEX_OPT", m_initial_subsumption_index_opt, - "after how many processed clauses the subsumption index is optimized."); - p.register_double_param("SPC_FACTOR_SUBSUMPTION_INDEX_OPT", m_factor_subsumption_index_opt, - "after each optimization the threshold for optimization is increased by this factor. See INITIAL_SUBSUMPTION_INDEX_OPT."); - p.register_bool_param("SPC_BS", m_backward_subsumption, "Enable/disable backward subsumption in the superposition engine"); - p.register_bool_param("SPC_ES", m_equality_subsumption, "Enable/disable equality resolution in the superposition engine"); - p.register_unsigned_param("SPC_NUM_ITERATIONS", m_spc_num_iterations); - p.register_bool_param("SPC_TRACE", m_spc_trace); -} - - diff --git a/src/front_end_params/spc_params.h b/src/front_end_params/spc_params.h deleted file mode 100644 index bb5232ef4..000000000 --- a/src/front_end_params/spc_params.h +++ /dev/null @@ -1,49 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - spc_params.h - -Abstract: - - Parameters for the Superposition Calculus Engine - -Author: - - Leonardo de Moura (leonardo) 2008-02-08. - -Revision History: - ---*/ -#ifndef _SPC_PARAMS_H_ -#define _SPC_PARAMS_H_ - -#include"order_params.h" - -struct spc_params : public order_params { - unsigned m_min_func_freq_subsumption_index; - unsigned m_max_subsumption_index_features; - unsigned m_initial_subsumption_index_opt; - double m_factor_subsumption_index_opt; - bool m_backward_subsumption; - bool m_equality_subsumption; - unsigned m_spc_num_iterations; - bool m_spc_trace; - - spc_params(): - m_min_func_freq_subsumption_index(100), - m_max_subsumption_index_features(32), - m_initial_subsumption_index_opt(1000), - m_factor_subsumption_index_opt(1.5), - m_backward_subsumption(true), - m_equality_subsumption(true), - m_spc_num_iterations(1000), - m_spc_trace(false) { - } - - void register_params(ini_params & p); -}; - -#endif /* _SPC_PARAMS_H_ */ - diff --git a/src/front_end_params/z3_solver_params.cpp b/src/front_end_params/z3_solver_params.cpp deleted file mode 100644 index cdc3fa23b..000000000 --- a/src/front_end_params/z3_solver_params.cpp +++ /dev/null @@ -1,30 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - z3_solver_params.cpp - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2007-06-11. - -Revision History: - ---*/ - -#include"z3_solver_params.h" - -void z3_solver_params::register_params(ini_params & p) { - p.register_bool_param("Z3_SOLVER_LL_PP", m_ast_ll_pp, "pretty print asserted constraints using low-level printer (Z3 input format specific)"); - p.register_bool_param("Z3_SOLVER_SMT_PP", m_ast_smt_pp, "pretty print asserted constraints using SMT printer (Z3 input format specific)"); - p.register_bool_param("PRE_SIMPLIFY_EXPR", m_pre_simplify_expr, "pre-simplify expressions when created over the API (example: -x -> (* -1 x))"); - p.register_string_param("SMTLIB_TRACE_PATH", m_smtlib_trace_path, "path for converting Z3 formulas to SMTLIB benchmarks"); - p.register_string_param("SMTLIB_SOURCE_INFO", m_smtlib_source_info, "additional source info to add to SMTLIB benchmark"); - p.register_string_param("SMTLIB_CATEGORY", m_smtlib_category, "additional category info to add to SMTLIB benchmark"); -} - diff --git a/src/front_end_params/z3_solver_params.h b/src/front_end_params/z3_solver_params.h deleted file mode 100644 index 5ff211387..000000000 --- a/src/front_end_params/z3_solver_params.h +++ /dev/null @@ -1,44 +0,0 @@ -/*++ -Copyright (c) 2006 Microsoft Corporation - -Module Name: - - z3_solver_params.h - -Abstract: - - - -Author: - - Leonardo de Moura (leonardo) 2007-06-11. - -Revision History: - ---*/ -#ifndef _Z3_SOLVER_PARAMS_H_ -#define _Z3_SOLVER_PARAMS_H_ - -#include"ini_file.h" - -struct z3_solver_params { - bool m_ast_ll_pp; - bool m_ast_smt_pp; - bool m_pre_simplify_expr; - std::string m_smtlib_trace_path; - std::string m_smtlib_source_info; - std::string m_smtlib_category; - - z3_solver_params(): - m_ast_ll_pp(false), - m_ast_smt_pp(false), - m_pre_simplify_expr(false), - m_smtlib_trace_path(""), - m_smtlib_source_info(""), - m_smtlib_category("") - {} - void register_params(ini_params & p); -}; - -#endif /* _Z3_SOLVER_PARAMS_H_ */ - diff --git a/src/muz_qe/dl_mk_extract_quantifiers.cpp b/src/muz_qe/dl_mk_extract_quantifiers.cpp new file mode 100644 index 000000000..614e9dbc8 --- /dev/null +++ b/src/muz_qe/dl_mk_extract_quantifiers.cpp @@ -0,0 +1,97 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + dl_mk_extract_quantifiers.cpp + +Abstract: + + Remove universal quantifiers over interpreted predicates in the body. + +Author: + + Nikolaj Bjorner (nbjorner) 2012-11-21 + +Revision History: + +--*/ + +#include"dl_mk_extract_quantifiers.h" +#include"ast_pp.h" + +namespace datalog { + + + mk_extract_quantifiers::mk_extract_quantifiers(context & ctx) : + rule_transformer::plugin(101, false), + m_ctx(ctx), + m(ctx.get_manager()), + rm(ctx.get_rule_manager()) + {} + + mk_extract_quantifiers::~mk_extract_quantifiers() { + for (unsigned i = 0; i < m_refs.size(); ++i) { + dealloc(m_refs[i]); + } + m_quantifiers.reset(); + m_refs.reset(); + } + + + void mk_extract_quantifiers::extract(rule& r, rule_set& new_rules) { + app_ref_vector tail(m); + svector neg_tail; + quantifier_ref_vector quantifiers(m); + unsigned utsz = r.get_uninterpreted_tail_size(); + unsigned tsz = r.get_tail_size(); + for (unsigned i = 0; i < utsz; ++i) { + tail.push_back(r.get_tail(i)); + neg_tail.push_back(r.is_neg_tail(i)); + } + for (unsigned i = utsz; i < tsz; ++i) { + SASSERT(!r.is_neg_tail(i)); + app* t = r.get_tail(i); + expr_ref_vector conjs(m); + datalog::flatten_and(t, conjs); + for (unsigned j = 0; j < conjs.size(); ++j) { + expr* e = conjs[j].get(); + quantifier* q = 0; + if (rule_manager::is_forall(m, e, q)) { + quantifiers.push_back(q); + } + else { + tail.push_back(is_app(e)?to_app(e):m.mk_eq(e, m.mk_true())); + neg_tail.push_back(false); + } + } + } + if (quantifiers.empty()) { + new_rules.add_rule(&r); + } + else { + rule* new_rule = rm.mk(r.get_head(), tail.size(), tail.c_ptr(), neg_tail.c_ptr(), r.name(), false); + new_rules.add_rule(new_rule); + quantifier_ref_vector* qs = alloc(quantifier_ref_vector, quantifiers); + m_quantifiers.insert(new_rule, qs); + m_refs.push_back(qs); + } + } + + rule_set * mk_extract_quantifiers::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { + m_quantifiers.reset(); + rule_set* rules = alloc(rule_set, m_ctx); + rule_set::iterator it = source.begin(), end = source.end(); + for (; it != end; ++it) { + extract(**it, *rules); + } + if (m_quantifiers.empty()) { + dealloc(rules); + rules = 0; + } + return rules; + } + +}; + + diff --git a/src/muz_qe/dl_mk_extract_quantifiers.h b/src/muz_qe/dl_mk_extract_quantifiers.h new file mode 100644 index 000000000..512e386cd --- /dev/null +++ b/src/muz_qe/dl_mk_extract_quantifiers.h @@ -0,0 +1,59 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + dl_mk_extract_quantifiers.h + +Abstract: + + Remove universal quantifiers over interpreted predicates in the body. + +Author: + + Nikolaj Bjorner (nbjorner) 2012-11-21 + +Revision History: + +--*/ +#ifndef _DL_MK_EXTRACT_QUANTIFIERS_H_ +#define _DL_MK_EXTRACT_QUANTIFIERS_H_ + +#include"dl_context.h" +#include"dl_rule_set.h" +#include"dl_rule_transformer.h" + +namespace datalog { + + /** + \brief Extract universal quantifiers from rules. + */ + class mk_extract_quantifiers : public rule_transformer::plugin { + context& m_ctx; + ast_manager& m; + rule_manager& rm; + ptr_vector m_refs; + obj_map m_quantifiers; + + void extract(rule& r, rule_set& new_rules); + + public: + /** + \brief Create rule transformer that extracts universal quantifiers (over recursive predicates). + */ + mk_extract_quantifiers(context & ctx); + + virtual ~mk_extract_quantifiers(); + + rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); + + obj_map& quantifiers() { return m_quantifiers; } + + bool has_quantifiers() const { return !m_quantifiers.empty(); } + + }; + +}; + +#endif /* _DL_MK_EXTRACT_QUANTIFIERS_H_ */ + diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index 451ec2e7d..404e81c24 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -65,10 +65,6 @@ namespace pdr { m_reachable(pm, pm.get_params()) {} pred_transformer::~pred_transformer() { - qinst_map::iterator it = m_rule2qinst.begin(), end = m_rule2qinst.end(); - for (; it != end; ++it) { - dealloc(it->m_value); - } rule2inst::iterator it2 = m_rule2inst.begin(), end2 = m_rule2inst.end(); for (; it2 != end2; ++it2) { dealloc(it2->m_value); @@ -556,7 +552,6 @@ namespace pdr { // positions the variables occur are made equivalent with these. expr_ref_vector conj(m); app_ref_vector& var_reprs = *(alloc(app_ref_vector, m)); - qinst* qi = 0; ptr_vector aux_vars; unsigned ut_size = rule.get_uninterpreted_tail_size(); @@ -581,19 +576,6 @@ namespace pdr { for (unsigned i = 0; i < tail.size(); ++i) { expr_ref tmp(m); var_subst(m, false)(tail[i].get(), var_reprs.size(), (expr*const*)var_reprs.c_ptr(), tmp); - quantifier* q; - if (datalog::rule_manager::is_forall(m, tmp, q)) { - - if (!qi) { - qi = alloc(qinst, m); - } - // - // The contract is to instantiate q with - // sufficient witnesses to validate body. - // - qi->quantifiers.push_back(q); - tmp = m.mk_true(); - } conj.push_back(tmp); TRACE("pdr", tout << mk_pp(tail[i].get(), m) << "\n" << mk_pp(tmp, m) << "\n";); SASSERT(is_ground(tmp)); @@ -607,12 +589,10 @@ namespace pdr { TRACE("pdr", tout << mk_pp(fml, m) << "\n";); SASSERT(is_ground(fml)); if (m.is_false(fml)) { - dealloc(qi); - qi = 0; // no-op. } else { - if (ut_size == 0 && !qi) { + if (ut_size == 0) { init = m.mk_or(init, fml); } transitions.push_back(fml); @@ -620,9 +600,6 @@ namespace pdr { m_rule2transition.insert(&rule, fml.get()); rules.push_back(&rule); } - if (qi) { - m_rule2qinst.insert(&rule, qi); - } m_rule2inst.insert(&rule,&var_reprs); m_rule2vars.insert(&rule, aux_vars); } @@ -1119,7 +1096,6 @@ namespace pdr { m_params(params), m(m), m_context(0), - m_quantifier_inst(*this, m), m_pm(m_fparams, m_params, m), m_query_pred(m), m_query(0), @@ -1491,7 +1467,6 @@ namespace pdr { UNREACHABLE(); } catch (model_exception) { - check_quantifiers(); IF_VERBOSE(1, verbose_stream() << "\n"; m_search.display(verbose_stream());); m_last_result = l_true; validate(); @@ -1605,24 +1580,6 @@ namespace pdr { } } - // - // Check that quantifiers are satisfied in the produced model. - // - void context::check_quantifiers() { - if (has_quantifiers()) { - m_quantifier_inst.model_check(m_search.get_root()); - } - } - - bool context::has_quantifiers() const { - decl2rel const& dr = get_pred_transformers(); - decl2rel::iterator it = dr.begin(), end = dr.end(); - for (; it != end; ++it) { - pred_transformer* pt = it->m_value; - if (pt->has_quantifiers()) return true; - } - return false; - } // // Pick a potential counter example state. @@ -1832,8 +1789,7 @@ namespace pdr { for (unsigned i = 0; i < sig_size; ++i) { vars.push_back(m.mk_const(m_pm.o2n(pt.sig(i), 0))); } - ptr_vector aux_vars; - pt.get_aux_vars(r, aux_vars); + ptr_vector& aux_vars = pt.get_aux_vars(r); vars.append(aux_vars.size(), aux_vars.c_ptr()); scoped_ptr rep; diff --git a/src/muz_qe/pdr_context.h b/src/muz_qe/pdr_context.h index 14be82dae..4b578a188 100644 --- a/src/muz_qe/pdr_context.h +++ b/src/muz_qe/pdr_context.h @@ -29,7 +29,6 @@ Revision History: #include "dl_base.h" #include "pdr_prop_solver.h" #include "pdr_reachable_cache.h" -#include "pdr_quantifiers.h" namespace datalog { class rule_set; @@ -42,7 +41,6 @@ namespace pdr { class model_node; class context; - typedef obj_map qinst_map; typedef obj_map rule2inst; typedef obj_map decl2rel; @@ -78,7 +76,6 @@ namespace pdr { obj_map m_prop2level; // map property to level where it occurs. obj_map m_tag2rule; // map tag predicate to rule. rule2expr m_rule2tag; // map rule to predicate tag. - qinst_map m_rule2qinst; // map tag to quantifier instantiation. rule2inst m_rule2inst; // map rules to instantiations of indices rule2expr m_rule2transition; // map rules to transition rule2apps m_rule2vars; // map rule to auxiliary variables @@ -99,7 +96,6 @@ namespace pdr { void init_rule(decl2rel const& pts, datalog::rule const& rule, expr_ref& init, ptr_vector& rules, expr_ref_vector& transition); void init_atom(decl2rel const& pts, app * atom, app_ref_vector& var_reprs, expr_ref_vector& conj, unsigned tail_idx); - void ground_free_vars(expr* e, app_ref_vector& vars, ptr_vector& aux_vars); void simplify_formulas(tactic& tac, expr_ref_vector& fmls); @@ -122,8 +118,6 @@ namespace pdr { func_decl* const* sig() { init_sig(); return m_sig.c_ptr(); } expr* transition() const { return m_transition; } expr* initial_state() const { return m_initial_state; } - bool has_quantifiers() const { return !m_rule2qinst.empty(); } - qinst* get_quantifiers(datalog::rule const* r) const { qinst* q = 0; m_rule2qinst.find(r, q); return q; } expr* rule2tag(datalog::rule const* r) { return m_rule2tag.find(r); } unsigned get_num_levels() { return m_levels.size(); } expr_ref get_cover_delta(func_decl* p_orig, int level); @@ -140,7 +134,7 @@ namespace pdr { void find_predecessors(model_core const& model, ptr_vector& preds) const; datalog::rule const& find_rule(model_core const& model) const; expr* get_transition(datalog::rule const& r) { return m_rule2transition.find(&r); } - void get_aux_vars(datalog::rule const& r, ptr_vector& vs) { m_rule2vars.find(&r, vs); } + ptr_vector& get_aux_vars(datalog::rule const& r) { return m_rule2vars.find(&r); } bool propagate_to_next_level(unsigned level); void add_property(expr * lemma, unsigned lvl); // add property 'p' to state at level. @@ -166,6 +160,8 @@ namespace pdr { void inherit_properties(pred_transformer& other); + void ground_free_vars(expr* e, app_ref_vector& vars, ptr_vector& aux_vars); + }; @@ -292,7 +288,6 @@ namespace pdr { params_ref const& m_params; ast_manager& m; datalog::context* m_context; - quantifier_model_checker m_quantifier_inst; manager m_pm; decl2rel m_rels; // Map from relation predicate to fp-operator. func_decl_ref m_query_pred; @@ -309,8 +304,6 @@ namespace pdr { // Functions used by search. void solve_impl(); bool check_reachability(unsigned level); - void check_quantifiers(); - bool has_quantifiers() const; void propagate(unsigned max_prop_lvl); void close_node(model_node& n); void check_pre_closed(model_node& n); @@ -396,8 +389,6 @@ namespace pdr { void set_axioms(expr* axioms) { m_pm.set_background(axioms); } - void refine(qi& q, datalog::rule_set& rules) { m_quantifier_inst.refine(q, rules); } - unsigned get_num_levels(func_decl* p); expr_ref get_cover_delta(int level, func_decl* p_orig, func_decl* p); @@ -408,6 +399,8 @@ namespace pdr { proof_ref get_proof() const; + model_node& get_root() const { return m_search.get_root(); } + }; }; diff --git a/src/muz_qe/pdr_dl_interface.cpp b/src/muz_qe/pdr_dl_interface.cpp index 532019025..cae84d3ff 100644 --- a/src/muz_qe/pdr_dl_interface.cpp +++ b/src/muz_qe/pdr_dl_interface.cpp @@ -25,6 +25,7 @@ Revision History: #include "dl_mk_rule_inliner.h" #include "dl_rule.h" #include "dl_rule_transformer.h" +#include "dl_mk_extract_quantifiers.h" #include "smt2parser.h" #include "pdr_context.h" #include "pdr_dl_interface.h" @@ -32,6 +33,7 @@ Revision History: #include "dl_mk_slice.h" #include "dl_mk_unfold.h" #include "dl_mk_coalesce.h" +#include "pdr_quantifiers.h" using namespace pdr; @@ -144,6 +146,12 @@ lbool dl_interface::query(expr * query) { --num_unfolds; } } + // remove universal quantifiers from body. + datalog::mk_extract_quantifiers* extract_quantifiers = alloc(datalog::mk_extract_quantifiers, m_ctx); + datalog::rule_transformer extract_q_tr(m_ctx); + extract_q_tr.register_plugin(extract_quantifiers); + m_ctx.transform_rules(extract_q_tr, mc, pc); + IF_VERBOSE(2, m_ctx.display_rules(verbose_stream());); m_pdr_rules.add_rules(m_ctx.get_rules()); @@ -151,6 +159,7 @@ lbool dl_interface::query(expr * query) { m_ctx.reopen(); m_ctx.replace_rules(old_rules); + quantifier_model_checker quantifier_mc(*m_context, m, extract_quantifiers->quantifiers(), m_pdr_rules); m_context->set_proof_converter(pc); m_context->set_model_converter(mc); @@ -163,14 +172,20 @@ lbool dl_interface::query(expr * query) { return l_false; } + lbool result; while (true) { - try { - return m_context->solve(); + result = m_context->solve(); + if (result == l_true && extract_quantifiers->has_quantifiers()) { + if (quantifier_mc.check()) { + return l_true; + } + // else continue } - catch (pdr::qi& q) { - m_context->refine(q, m_pdr_rules); + else { + return result; } } + } expr_ref dl_interface::get_cover_delta(int level, func_decl* pred_orig) { diff --git a/src/muz_qe/pdr_quantifiers.cpp b/src/muz_qe/pdr_quantifiers.cpp index 362575a8b..d52a0bf07 100644 --- a/src/muz_qe/pdr_quantifiers.cpp +++ b/src/muz_qe/pdr_quantifiers.cpp @@ -115,166 +115,21 @@ namespace pdr { var_subst vs(m, false); vs(q->get_expr(), binding.size(), binding.c_ptr(), e); (*rep)(e); - m_rules.push_back(m_current_rule); - m_apps.push_back(to_app(e)); + m_instantiated_rules.push_back(m_current_rule); + m_instantiations.push_back(to_app(e)); TRACE("pdr", tout << mk_pp(e, m) << "\n";); } - void quantifier_model_checker::model_check(model_node& root) { - m_apps.reset(); - m_rules.reset(); - ptr_vector nodes; - get_nodes(root, nodes); - for (unsigned i = nodes.size(); i > 0; ) { - --i; - model_check_node(*nodes[i]); - } - if (m_apps.empty()) { - return; - } - qi q(m); - for (unsigned i = 0; i < m_apps.size(); ++i) { - q.add(m_rules[i], m_apps[i].get()); - } - throw q; - } // As & not Body_i is satisfiable // then instantiate with model for parameters to Body_i - bool quantifier_model_checker::find_instantiations(qinst& qi, unsigned level) { + bool quantifier_model_checker::find_instantiations(quantifier_ref_vector const& qs, unsigned level) { return - find_instantiations_proof_based(qi, level); // || - // find_instantiations_qe_based(qi, level); + find_instantiations_proof_based(qs, level); // || + // find_instantiations_qe_based(qs, level); } - bool quantifier_model_checker::find_instantiations_model_based(qinst& qi, unsigned level) { - bool found_instance = false; - expr_ref C(m); - front_end_params fparams; - smt::kernel solver(m, fparams); - solver.assert_expr(m_A); - for (unsigned i = 0; i < m_Bs.size(); ++i) { - expr_ref_vector fresh_vars(m); - quantifier* q = qi.quantifiers[i].get(); - for (unsigned j = 0; j < q->get_num_decls(); ++j) { - fresh_vars.push_back(m.mk_fresh_const("V",q->get_decl_sort(j))); - } - var_subst varsubst(m, false); - varsubst(m_Bs[i].get(), fresh_vars.size(), fresh_vars.c_ptr(), C); - TRACE("pdr", tout << "updated propagation formula: " << mk_pp(C,m) << "\n";); - - solver.push(); - // TBD: what to do with the different tags when unfolding the same predicate twice? - solver.assert_expr(m.mk_not(C)); - lbool result = solver.check(); - if (result == l_true) { - found_instance = true; - model_ref mr; - solver.get_model(mr); - TRACE("pdr", model_smt2_pp(tout, m, *mr, 0);); - - expr_ref_vector insts(m); - for (unsigned j = 0; j < fresh_vars.size(); ++j) { - expr* interp = mr->get_const_interp(to_app(fresh_vars[j].get())->get_decl()); - if (interp) { - insts.push_back(interp); - } - else { - insts.push_back(fresh_vars[j].get()); - } - TRACE("pdr", tout << mk_pp(insts.back(), m) << "\n";); - } - add_binding(q, insts); - } - solver.pop(1); - } - return found_instance; - } - - // - // Build: - // - // A & forall x . B1 & forall y . B2 & ... - // = - // not exists x y . (!A or !B1 or !B2 or ...) - // - // Find an instance that satisfies formula. - // (or find all instances?) - // - bool quantifier_model_checker::find_instantiations_qe_based(qinst& qi, unsigned level) { - expr_ref_vector fmls(m), conjs(m), fresh_vars(m); - app_ref_vector all_vars(m); - expr_ref C(m); - qe::def_vector defs(m); - front_end_params fparams; - qe::expr_quant_elim qe(m, fparams); - for (unsigned i = 0; i < m_Bs.size(); ++i) { - quantifier* q = qi.quantifiers[i].get(); - unsigned num_decls = q->get_num_decls(); - unsigned offset = all_vars.size(); - for (unsigned j = 0; j < num_decls; ++j) { - all_vars.push_back(m.mk_fresh_const("V",q->get_decl_sort(j))); - } - var_subst varsubst(m, false); - varsubst(m_Bs[i].get(), num_decls, (expr**)(all_vars.c_ptr() + offset), C); - fmls.push_back(C); - } - conjs.push_back(m_A); - conjs.push_back(m.mk_not(m.mk_and(fmls.size(), fmls.c_ptr()))); - // add previous instances. - expr* r = m.mk_and(m_Bs.size(), m_Bs.c_ptr()); - m_trail.push_back(r); - expr* inst; - if (!m_bound.find(m_current_rule, r, inst)) { - TRACE("pdr", tout << "did not find: " << mk_pp(r, m) << "\n";); - m_trail.push_back(r); - inst = m.mk_true(); - m_bound.insert(m_current_rule, r, inst); - } - else { - TRACE("pdr", tout << "blocking: " << mk_pp(inst, m) << "\n";); - conjs.push_back(inst); - } - C = m.mk_and(conjs.size(), conjs.c_ptr()); - lbool result = qe.first_elim(all_vars.size(), all_vars.c_ptr(), C, defs); - TRACE("pdr", tout << mk_pp(C.get(), m) << "\n" << result << "\n";); - if (result != l_true) { - return false; - } - inst = m.mk_and(inst, m.mk_not(C)); - m_trail.push_back(inst); - m_bound.insert(m_current_rule, r, inst); - TRACE("pdr", - tout << "Instantiating\n"; - for (unsigned i = 0; i < defs.size(); ++i) { - tout << defs.var(i)->get_name() << " " << mk_pp(defs.def(i), m) << "\n"; - } - ); - expr_substitution sub(m); - for (unsigned i = 0; i < defs.size(); ++i) { - sub.insert(m.mk_const(defs.var(i)), defs.def(i)); - } - scoped_ptr rep = mk_default_expr_replacer(m); - rep->set_substitution(&sub); - for (unsigned i = 0; i < all_vars.size(); ++i) { - expr_ref tmp(all_vars[i].get(), m); - (*rep)(tmp); - all_vars[i] = to_app(tmp); - } - unsigned offset = 0; - for (unsigned i = 0; i < m_Bs.size(); ++i) { - quantifier* q = qi.quantifiers[i].get(); - unsigned num_decls = q->get_num_decls(); - expr_ref_vector new_binding(m); - for (unsigned j = 0; j < num_decls; ++j) { - new_binding.push_back(all_vars[offset+j].get()); - } - offset += num_decls; - add_binding(q, new_binding); - } - return true; - } class collect_insts { ast_manager& m; @@ -322,7 +177,7 @@ namespace pdr { }; - bool quantifier_model_checker::find_instantiations_proof_based(qinst& qi, unsigned level) { + bool quantifier_model_checker::find_instantiations_proof_based(quantifier_ref_vector const& qs, unsigned level) { bool found_instance = false; TRACE("pdr", tout << mk_pp(m_A,m) << "\n";); @@ -336,7 +191,7 @@ namespace pdr { expr_ref C(m); fmls.push_back(tr(m_A.get())); for (unsigned i = 0; i < m_Bs.size(); ++i) { - C = m.update_quantifier(qi.quantifiers[i].get(), m_Bs[i].get()); + C = m.update_quantifier(qs[i], m_Bs[i].get()); fmls.push_back(tr(C.get())); } TRACE("pdr", @@ -355,8 +210,8 @@ namespace pdr { } map qid_map; quantifier* q; - for (unsigned i = 0; i < qi.quantifiers.size(); ++i) { - q = qi.quantifiers[i].get(); + for (unsigned i = 0; i < qs.size(); ++i) { + q = qs[i]; qid_map.insert(q->get_qid(), q); } @@ -391,7 +246,7 @@ namespace pdr { if (collector.size() == 0) { // Try to create dummy instances. for (unsigned i = 0; i < m_Bs.size(); ++i) { - q = qi.quantifiers[i].get(); + q = qs[i]; expr_ref_vector binding(m); for (unsigned j = 0; j < q->get_num_decls(); ++j) { binding.push_back(m.mk_fresh_const("B", q->get_decl_sort(j))); @@ -403,7 +258,6 @@ namespace pdr { return found_instance; } - void quantifier_model_checker::model_check_node(model_node& node) { TRACE("pdr", node.display(tout, 0);); pred_transformer& pt = node.pt(); @@ -411,9 +265,6 @@ namespace pdr { expr_ref A(m), B(m), C(m); expr_ref_vector As(m); m_Bs.reset(); - if (!pt.has_quantifiers()) { - return; - } // // nodes from leaves that are repeated // inside the search tree don't have models. @@ -427,10 +278,12 @@ namespace pdr { if (!m_current_rule) { return; } - qinst* qi = pt.get_quantifiers(m_current_rule); - if (!qi) { + + quantifier_ref_vector* qis = 0; + m_quantifiers.find(m_current_rule, qis); + if (!qis) { return; - } + } unsigned level = node.level(); unsigned previous_level = (level == 0)?0:(level-1); @@ -440,42 +293,69 @@ namespace pdr { m_A = pm.mk_and(As); // Add quantifiers: - scoped_ptr rep = mk_default_expr_replacer(m); - for (unsigned j = 0; j < qi->quantifiers.size(); ++j) { - quantifier* q = qi->quantifiers[j].get(); - app* a = to_app(q->get_expr()); - func_decl* f = a->get_decl(); - pred_transformer& pt2 = m_ctx.get_pred_transformer(f); - B = pt2.get_formulas(previous_level, true); - TRACE("pdr", tout << mk_pp(B, m) << "\n";); - - expr_substitution sub(m); - for (unsigned i = 0; i < a->get_num_args(); ++i) { - expr* v = m.mk_const(pm.o2n(pt2.sig(i),0)); - sub.insert(v, a->get_arg(i)); + + { + datalog::scoped_no_proof _no_proof(m); + scoped_ptr rep = mk_default_expr_replacer(m); + for (unsigned j = 0; j < qis->size(); ++j) { + quantifier* q = (*qis)[j].get(); + app* a = to_app(q->get_expr()); + func_decl* f = a->get_decl(); + pred_transformer& pt2 = m_ctx.get_pred_transformer(f); + B = pt2.get_formulas(previous_level, true); + + expr_substitution sub(m); + expr_ref_vector refs(m); + for (unsigned i = 0; i < a->get_num_args(); ++i) { + expr* v = m.mk_const(pm.o2n(pt2.sig(i),0)); + sub.insert(v, a->get_arg(i)); + refs.push_back(v); + } + rep->set_substitution(&sub); + (*rep)(B); + app_ref_vector& inst = pt.get_inst(m_current_rule); + ptr_vector& aux_vars = pt.get_aux_vars(*m_current_rule); + pt.ground_free_vars(B, inst, aux_vars); + var_subst vs(m, false); + vs(B, inst.size(), (expr*const*)inst.c_ptr(), B); + m_Bs.push_back(B); } - rep->set_substitution(&sub); - // TBD: exclude previous bindings here. - (*rep)(B); - m_Bs.push_back(B); - TRACE("pdr", - tout << mk_pp(q, m) << "\n"; - tout << "propagation formula: " << mk_pp(B, m) << "\n";); } - find_instantiations(*qi, level); + + TRACE("pdr", + tout << "A:\n" << mk_pp(m_A, m) << "\n"; + tout << "B:\n"; + for (unsigned i = 0; i < m_Bs.size(); ++i) { + tout << mk_pp((*qis)[i].get(), m) << "\n" << mk_pp(m_Bs[i].get(), m) << "\n"; + } + ); + + find_instantiations(*qis, level); } - void quantifier_model_checker::refine(qi& q, datalog::rule_set& rules) { + bool quantifier_model_checker::model_check(model_node& root) { + m_instantiations.reset(); + m_instantiated_rules.reset(); + ptr_vector nodes; + get_nodes(root, nodes); + for (unsigned i = nodes.size(); i > 0; ) { + --i; + model_check_node(*nodes[i]); + } + return m_instantiations.empty(); + } + + void quantifier_model_checker::refine() { IF_VERBOSE(1, verbose_stream() << "instantiating quantifiers\n";); - datalog::rule_manager& rule_m = rules.get_rule_manager(); - datalog::rule_set new_rules(rules.get_context()); - datalog::rule_set::iterator it = rules.begin(), end = rules.end(); + datalog::rule_manager& rule_m = m_rules.get_rule_manager(); + datalog::rule_set new_rules(m_rules.get_context()); + datalog::rule_set::iterator it = m_rules.begin(), end = m_rules.end(); for (; it != end; ++it) { datalog::rule* r = *it; - app_ref_vector body(m); - for (unsigned i = 0; i < q.size(); ++i) { - if (r == q.get_rule(i)) { - body.push_back(q.get_app(i)); + expr_ref_vector body(m); + for (unsigned i = 0; i < m_instantiations.size(); ++i) { + if (r == m_instantiated_rules[i]) { + body.push_back(m_instantiations[i].get()); } } if (body.empty()) { @@ -485,19 +365,165 @@ namespace pdr { for (unsigned i = 0; i < r->get_tail_size(); ++i) { body.push_back(r->get_tail(i)); } + quantifier_ref_vector* qs = 0; + m_quantifiers.find(r, qs); + m_quantifiers.remove(r); datalog::rule_ref_vector rules(rule_m); - expr_ref rule(m.mk_implies(m.mk_and(body.size(), (expr*const*)body.c_ptr()), r->get_head()), m); + expr_ref rule(m.mk_implies(m.mk_and(body.size(), body.c_ptr()), r->get_head()), m); rule_m.mk_rule(rule, rules, r->name()); for (unsigned i = 0; i < rules.size(); ++i) { new_rules.add_rule(rules[i].get()); + m_quantifiers.insert(rules[i].get(), qs); } } } new_rules.close(); - rules.reset(); - rules.add_rules(new_rules); - rules.close(); - m_ctx.update_rules(rules); - TRACE("pdr", rules.display(tout);); + m_rules.reset(); + m_rules.add_rules(new_rules); + m_rules.close(); + m_ctx.update_rules(m_rules); + TRACE("pdr", m_rules.display(tout);); + } + + bool quantifier_model_checker::check() { + if (model_check(m_ctx.get_root())) { + return true; + } + refine(); + return false; } }; + + +#if 0 + // + // Build: + // + // A & forall x . B1 & forall y . B2 & ... + // = + // not exists x y . (!A or !B1 or !B2 or ...) + // + // Find an instance that satisfies formula. + // (or find all instances?) + // + bool quantifier_model_checker::find_instantiations_qe_based(quantifier_ref_vector const& qs, unsigned level) { + expr_ref_vector fmls(m), conjs(m), fresh_vars(m); + app_ref_vector all_vars(m); + expr_ref C(m); + qe::def_vector defs(m); + front_end_params fparams; + qe::expr_quant_elim qe(m, fparams); + for (unsigned i = 0; i < m_Bs.size(); ++i) { + quantifier* q = qs[i]; + unsigned num_decls = q->get_num_decls(); + unsigned offset = all_vars.size(); + for (unsigned j = 0; j < num_decls; ++j) { + all_vars.push_back(m.mk_fresh_const("V",q->get_decl_sort(j))); + } + var_subst varsubst(m, false); + varsubst(m_Bs[i].get(), num_decls, (expr**)(all_vars.c_ptr() + offset), C); + fmls.push_back(C); + } + conjs.push_back(m_A); + conjs.push_back(m.mk_not(m.mk_and(fmls.size(), fmls.c_ptr()))); + // add previous instances. + expr* r = m.mk_and(m_Bs.size(), m_Bs.c_ptr()); + m_trail.push_back(r); + expr* inst; + if (!m_bound.find(m_current_rule, r, inst)) { + TRACE("pdr", tout << "did not find: " << mk_pp(r, m) << "\n";); + m_trail.push_back(r);Newton Sanches + inst = m.mk_true(); + m_bound.insert(m_current_rule, r, inst); + } + else { + TRACE("pdr", tout << "blocking: " << mk_pp(inst, m) << "\n";); + conjs.push_back(inst); + } + C = m.mk_and(conjs.size(), conjs.c_ptr()); + lbool result = qe.first_elim(all_vars.size(), all_vars.c_ptr(), C, defs); + TRACE("pdr", tout << mk_pp(C.get(), m) << "\n" << result << "\n";); + if (result != l_true) { + return false; + } + inst = m.mk_and(inst, m.mk_not(C)); + m_trail.push_back(inst); + m_bound.insert(m_current_rule, r, inst); + TRACE("pdr", + tout << "Instantiating\n"; + for (unsigned i = 0; i < defs.size(); ++i) { + tout << defs.var(i)->get_name() << " " << mk_pp(defs.def(i), m) << "\n"; + } + ); + expr_substitution sub(m); + for (unsigned i = 0; i < defs.size(); ++i) { + sub.insert(m.mk_const(defs.var(i)), defs.def(i)); + } + scoped_ptr rep = mk_default_expr_replacer(m); + rep->set_substitution(&sub); + for (unsigned i = 0; i < all_vars.size(); ++i) { + expr_ref tmp(all_vars[i].get(), m); + (*rep)(tmp); + all_vars[i] = to_app(tmp); + } + unsigned offset = 0; + for (unsigned i = 0; i < m_Bs.size(); ++i) { + quantifier* q = qs[i]; + unsigned num_decls = q->get_num_decls(); + expr_ref_vector new_binding(m); + for (unsigned j = 0; j < num_decls; ++j) { + new_binding.push_back(all_vars[offset+j].get()); + } + offset += num_decls; + add_binding(q, new_binding); + } + return true; + } + + bool quantifier_model_checker::find_instantiations_model_based(quantifier_ref_vector const& qs, unsigned level) { + bool found_instance = false; + expr_ref C(m); + front_end_params fparams; + smt::kernel solver(m, fparams); + solver.assert_expr(m_A); + for (unsigned i = 0; i < m_Bs.size(); ++i) { + expr_ref_vector fresh_vars(m); + quantifier* q = qs[i]; + for (unsigned j = 0; j < q->get_num_decls(); ++j) { + fresh_vars.push_back(m.mk_fresh_const("V",q->get_decl_sort(j))); + } + var_subst varsubst(m, false); + varsubst(m_Bs[i].get(), fresh_vars.size(), fresh_vars.c_ptr(), C); + TRACE("pdr", tout << "updated propagation formula: " << mk_pp(C,m) << "\n";); + + solver.push(); + // TBD: what to do with the different tags when unfolding the same predicate twice? + solver.assert_expr(m.mk_not(C)); + lbool result = solver.check(); + if (result == l_true) { + found_instance = true; + model_ref mr; + solver.get_model(mr); + TRACE("pdr", model_smt2_pp(tout, m, *mr, 0);); + + expr_ref_vector insts(m); + for (unsigned j = 0; j < fresh_vars.size(); ++j) { + expr* interp = mr->get_const_interp(to_app(fresh_vars[j].get())->get_decl()); + if (interp) { + insts.push_back(interp); + } + else { + insts.push_back(fresh_vars[j].get()); + } + TRACE("pdr", tout << mk_pp(insts.back(), m) << "\n";); + } + add_binding(q, insts); + } + solver.pop(1); + } + return found_instance; + } + + +#endif + diff --git a/src/muz_qe/pdr_quantifiers.h b/src/muz_qe/pdr_quantifiers.h index 45e8640e4..bae323cf8 100644 --- a/src/muz_qe/pdr_quantifiers.h +++ b/src/muz_qe/pdr_quantifiers.h @@ -33,52 +33,31 @@ namespace pdr { class model_node; class pred_transformer; class context; - - struct qinst { - quantifier_ref_vector quantifiers; // quantifiers in rule body. - func_decl_ref_vector predicates; // predicates in order of bindings. - expr_ref_vector bindings; // the actual instantiations of the predicates - qinst(ast_manager& m): quantifiers(m), predicates(m), bindings(m) {} - }; - - class qi { - ptr_vector m_rules; - app_ref_vector m_apps; - public: - qi(ast_manager& m) : m_apps(m) {} - void add(datalog::rule const* r, app* a) { - m_rules.push_back(r); - m_apps.push_back(a); - } - unsigned size() const { return m_rules.size(); } - datalog::rule const* get_rule(unsigned i) const { return m_rules[i]; } - app* get_app(unsigned i) const { return m_apps[i]; } - }; class quantifier_model_checker { context& m_ctx; ast_manager& m; - obj_pair_map m_bound; + obj_map& m_quantifiers; + datalog::rule_set& m_rules; expr_ref_vector m_trail; expr_ref m_A; expr_ref_vector m_Bs; pred_transformer* m_current_pt; datalog::rule const* m_current_rule; model_node* m_current_node; - - ptr_vector m_rules; - app_ref_vector m_apps; + app_ref_vector m_instantiations; + ptr_vector m_instantiated_rules; void model_check_node(model_node& node); - bool find_instantiations(qinst& qi, unsigned level); + bool find_instantiations(quantifier_ref_vector const& qs, unsigned level); - bool find_instantiations_model_based(qinst& qi, unsigned level); + bool find_instantiations_model_based(quantifier_ref_vector const& qs, unsigned level); - bool find_instantiations_proof_based(qinst& qi, unsigned level); + bool find_instantiations_proof_based(quantifier_ref_vector const& qs, unsigned level); - bool find_instantiations_qe_based(qinst& qi, unsigned level); + bool find_instantiations_qe_based(quantifier_ref_vector const& qs, unsigned level); void add_binding(quantifier* q, expr_ref_vector& binding); @@ -88,12 +67,8 @@ namespace pdr { void generalize_binding(expr_ref_vector const& binding, unsigned idx, expr_ref_vector& new_binding, vector& bindings); - public: - quantifier_model_checker(context& ctx, ast_manager& m): - m_ctx(ctx), - m(m), m_trail(m), m_A(m), m_Bs(m), - m_current_pt(0), m_current_rule(0), - m_current_node(0), m_apps(m) {} + void refine(); + /** \brief model check a potential model against quantifiers in bodies of rules. @@ -102,9 +77,23 @@ namespace pdr { 'false' and a set of instantiations that contradict the current model. */ - void model_check(model_node& root); + bool model_check(model_node& root); - void refine(qi& q, datalog::rule_set& rules); + public: + quantifier_model_checker( + context& ctx, + ast_manager& m, + obj_map& quantifiers, + datalog::rule_set& rules) : + m_ctx(ctx), + m(m), + m_quantifiers(quantifiers), + m_rules(rules), + m_trail(m), m_A(m), m_Bs(m), + m_current_pt(0), m_current_rule(0), + m_current_node(0), m_instantiations(m) {} + + bool check(); }; }; diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 4a6cfd85d..6fdfc0488 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -40,7 +40,6 @@ Revision History: #include"der.h" #include"elim_bounds.h" #include"warning.h" -#include"eager_bit_blaster.h" #include"bit2int.h" #include"distribute_forall.h" #include"quasi_macros.h" @@ -340,13 +339,9 @@ void asserted_formulas::reduce() { INVOKE(m_params.m_quasi_macros && has_quantifiers(), apply_quasi_macros()); INVOKE(m_params.m_simplify_bit2int, apply_bit2int()); INVOKE(m_params.m_eliminate_bounds && has_quantifiers(), cheap_quant_fourier_motzkin()); - INVOKE(!m_params.m_bb_eager && has_quantifiers() && m_params.m_ematching, infer_patterns()); INVOKE(m_params.m_max_bv_sharing && has_bv(), max_bv_sharing()); INVOKE(m_params.m_bb_quantifiers, elim_bvs_from_quantifiers()); - INVOKE(m_params.m_bb_eager, apply_eager_bit_blaster()); - INVOKE(m_params.m_bb_eager && m_params.m_nnf_cnf, nnf_cnf()); // bit-blaster destroys CNF INVOKE(m_params.m_bb_quantifiers && m_params.m_der && has_quantifiers(), apply_der()); // bit-vector elimination + bit-blasting creates new opportunities for der. - INVOKE(m_params.m_bb_eager && has_quantifiers() && m_params.m_ematching, infer_patterns()); // temporary HACK: make sure that arith & bv are list-assoc // this may destroy some simplification steps such as max_bv_sharing reduce_asserted_formulas(); @@ -1434,8 +1429,6 @@ bool asserted_formulas::quant_elim() { return false; } -MK_SIMPLIFIER(apply_eager_bit_blaster, eager_bit_blaster functor(m_manager, m_params), "eager_bb", "eager bit blasting", false); - MK_SIMPLIFIER(elim_bvs_from_quantifiers, bv_elim_star functor(m_manager), "bv_elim", "eliminate bit-vectors from quantifiers", true); #define LIFT_ITE(NAME, FUNCTOR, MSG) \ diff --git a/src/smt/asserted_formulas.h b/src/smt/asserted_formulas.h index 94bb41682..6689e8235 100644 --- a/src/smt/asserted_formulas.h +++ b/src/smt/asserted_formulas.h @@ -94,7 +94,6 @@ class asserted_formulas { void apply_demodulators(); void apply_quasi_macros(); void nnf_cnf(); - bool apply_eager_bit_blaster(); void infer_patterns(); void eliminate_term_ite(); void reduce_and_solve();