diff --git a/.gitignore b/.gitignore index cc1c2a754..b7e4a0186 100644 --- a/.gitignore +++ b/.gitignore @@ -75,14 +75,3 @@ src/api/ml/z3.mllib *.bak doc/api doc/code - -# CMake files copied over by the ``contrib/cmake/boostrap.py`` script -# See #461 -examples/CMakeLists.txt -examples/*/CMakeLists.txt -src/CMakeLists.txt -src/*/CMakeLists.txt -src/*/*/CMakeLists.txt -src/*/*/*/CMakeLists.txt -src/api/dotnet/cmake_install_gac.cmake.in -src/api/dotnet/cmake_uninstall_gac.cmake.in diff --git a/CMakeLists.txt b/CMakeLists.txt index 7400f67e2..5ed7ee06a 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -14,16 +14,6 @@ if (POLICY CMP0054) cmake_policy(SET CMP0054 OLD) endif() -# Provide a friendly message if the user hasn't run the bootstrap script -# to copy all the CMake files into their correct location. -# It is unfortunate that we have to do this, see #461 for the discussion -# on this. -if (NOT (EXISTS "${CMAKE_SOURCE_DIR}/src/CMakeLists.txt")) - message(FATAL_ERROR "Cannot find \"${CMAKE_SOURCE_DIR}/src/CMakeLists.txt\"" - ". This probably means you need to run" - "``python contrib/cmake/bootstrap.py create``") -endif() - set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake") project(Z3 CXX) diff --git a/README-CMake.md b/README-CMake.md index 1b7d89542..7550808fc 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -33,34 +33,6 @@ git clean -fx src which will remove the generated source files. -### Bootstrapping - -Most of Z3's CMake files do not live in their correct location. Instead those -files live in the ``contrib/cmake`` folder and a script is provided that will -copy (or hard link) the files into their correct location. - -To copy the files run - -``` -python contrib/cmake/bootstrap.py create -``` - -in the root of the repository. Once you have done this you can now build Z3 using CMake. -Make sure you remember to rerun this command if you pull down new code/rebase/change branch so -that the copied CMake files are up to date. - -To remove the copied files run - -``` -python contrib/cmake/bootstrap.py remove -``` - -Note if you plan to do development on Z3 you should read the developer -notes on bootstrapping in this document. - -What follows is a brief walk through of how to build Z3 using some -of the more commonly used CMake generators. - ### Unix Makefiles Run the following in the top level directory of the Z3 repository. @@ -328,44 +300,6 @@ link is not created when building under Windows. These notes are help developers and packagers of Z3. -### Boostrapping the CMake build - -Z3's CMake system is experimental and not officially supported. Consequently -Z3's developers have decided that they do not want the CMake files in the -``src/`` and ``examples/`` folders. Instead the ``contrib/cmake/bootstrap.py`` -script copies or hard links them into the correct locations. For context -on this decision see https://github.com/Z3Prover/z3/pull/461 . - -The ``contrib/cmake/bootstrap.py create`` command just copies over files which makes -development harder because you have to copy your modifications over to the -files in ``contrib/cmake`` for your changes to committed to git. If you are on a UNIX like -platform you can create hard links instead by running - -``` -contrib/cmake/boostrap.py create --hard-link -``` - -Using hard links means that modifying any of the "copied" files also modifies the -file under version control. Using hard links also means that the file modification time -will appear correct (i.e. the hard-linked "copies" have the same file modification time -as the corresponding file under version control) which means CMake will correctly reconfigure -when invoked. This is why using symbolic links is not an option because the file modification -time of a symbolic link is not the same as the file modification of the file being pointed to. - -Unfortunately a downside to using hard links (or just plain copies) is that if -you pull down new code (i.e. ``git pull``) then some of the CMake files under -version control may change but the corresponding hard-linked "copies" will not. - -This mean that (regardless of whether or not you use hard links) every time you -pull down new code or change branch or do an interactive rebase you must run -(with or without ``--hard-link``): - -``` -contrb/cmake/boostrap.py create -``` - -in order to be sure that the copied CMake files are not out of date. - ### Install/Uninstall Install and uninstall targets are supported. Use ``CMAKE_INSTALL_PREFIX`` to diff --git a/contrib/cmake/cmake/Z3Config.cmake.in b/cmake/Z3Config.cmake.in similarity index 100% rename from contrib/cmake/cmake/Z3Config.cmake.in rename to cmake/Z3Config.cmake.in diff --git a/contrib/cmake/cmake/cmake_uninstall.cmake.in b/cmake/cmake_uninstall.cmake.in similarity index 100% rename from contrib/cmake/cmake/cmake_uninstall.cmake.in rename to cmake/cmake_uninstall.cmake.in diff --git a/contrib/cmake/cmake/compiler_lto.cmake b/cmake/compiler_lto.cmake similarity index 100% rename from contrib/cmake/cmake/compiler_lto.cmake rename to cmake/compiler_lto.cmake diff --git a/contrib/cmake/cmake/compiler_warnings.cmake b/cmake/compiler_warnings.cmake similarity index 100% rename from contrib/cmake/cmake/compiler_warnings.cmake rename to cmake/compiler_warnings.cmake diff --git a/contrib/cmake/cmake/cxx_compiler_flags_overrides.cmake b/cmake/cxx_compiler_flags_overrides.cmake similarity index 100% rename from contrib/cmake/cmake/cxx_compiler_flags_overrides.cmake rename to cmake/cxx_compiler_flags_overrides.cmake diff --git a/contrib/cmake/cmake/git_utils.cmake b/cmake/git_utils.cmake similarity index 100% rename from contrib/cmake/cmake/git_utils.cmake rename to cmake/git_utils.cmake diff --git a/contrib/cmake/cmake/modules/FindDotNetToolchain.cmake b/cmake/modules/FindDotNetToolchain.cmake similarity index 100% rename from contrib/cmake/cmake/modules/FindDotNetToolchain.cmake rename to cmake/modules/FindDotNetToolchain.cmake diff --git a/contrib/cmake/cmake/modules/FindGMP.cmake b/cmake/modules/FindGMP.cmake similarity index 100% rename from contrib/cmake/cmake/modules/FindGMP.cmake rename to cmake/modules/FindGMP.cmake diff --git a/contrib/cmake/cmake/msvc_legacy_quirks.cmake b/cmake/msvc_legacy_quirks.cmake similarity index 100% rename from contrib/cmake/cmake/msvc_legacy_quirks.cmake rename to cmake/msvc_legacy_quirks.cmake diff --git a/contrib/cmake/cmake/target_arch_detect.cmake b/cmake/target_arch_detect.cmake similarity index 100% rename from contrib/cmake/cmake/target_arch_detect.cmake rename to cmake/target_arch_detect.cmake diff --git a/contrib/cmake/cmake/target_arch_detect.cpp b/cmake/target_arch_detect.cpp similarity index 100% rename from contrib/cmake/cmake/target_arch_detect.cpp rename to cmake/target_arch_detect.cpp diff --git a/contrib/cmake/cmake/z3_add_component.cmake b/cmake/z3_add_component.cmake similarity index 100% rename from contrib/cmake/cmake/z3_add_component.cmake rename to cmake/z3_add_component.cmake diff --git a/contrib/cmake/cmake/z3_add_cxx_flag.cmake b/cmake/z3_add_cxx_flag.cmake similarity index 100% rename from contrib/cmake/cmake/z3_add_cxx_flag.cmake rename to cmake/z3_add_cxx_flag.cmake diff --git a/contrib/cmake/cmake/z3_append_linker_flag_list_to_target.cmake b/cmake/z3_append_linker_flag_list_to_target.cmake similarity index 100% rename from contrib/cmake/cmake/z3_append_linker_flag_list_to_target.cmake rename to cmake/z3_append_linker_flag_list_to_target.cmake diff --git a/contrib/cmake/bootstrap.py b/contrib/cmake/bootstrap.py index a3c81fb25..dac08b383 100755 --- a/contrib/cmake/bootstrap.py +++ b/contrib/cmake/bootstrap.py @@ -1,25 +1,13 @@ #!/usr/bin/env python """ -This script is used to copy or delete the -CMake build system files from the contrib/cmake -folder into the their correct location in the Z3 -repository. +This script is an artifact of compromise that was +made when the CMake build system was first introduced +(see #461). -It offers two modes - -* create - This will symlink the ``cmake`` directory and copy (or hard link) -the appropriate files into their correct locations in the repository. - -* remove - This will remove the symlinked ``cmake`` -directory and remove the files added by the above -methods. - -This has the advantage -that editing the hard link edits the underlying file -(making development easier because copying files is -not neccessary) and CMake will regenerate correctly -because the modification time stamps will be correct. +This script now does nothing. It remains only to not +break out-of-tree scripts that build Z3 using CMake. +Eventually this script will be removed. """ import argparse import logging @@ -28,189 +16,6 @@ import pprint import shutil import sys -def get_full_path_to_script(): - return os.path.abspath(__file__) - -def get_cmake_contrib_dir(): - return os.path.dirname(get_full_path_to_script()) - -def get_repo_root_dir(): - r = os.path.dirname(os.path.dirname(get_cmake_contrib_dir())) - assert os.path.isdir(r) - return r - -# These are paths that should be ignored when checking if a folder -# in the ``contrib/cmake`` exists in the root of the repository -verificationExceptions = { - os.path.join(get_repo_root_dir(), 'cmake'), - os.path.join(get_repo_root_dir(), 'cmake', 'modules') -} - -def contribPathToRepoPath(path): - assert path.startswith(get_cmake_contrib_dir()) - stripped = path[len(get_cmake_contrib_dir()) + 1:] # Plus one is to remove leading slash - assert not os.path.isabs(stripped) - logging.debug('stripped:{}'.format(stripped)) - r = os.path.join(get_repo_root_dir(), stripped) - assert os.path.isabs(r) - logging.debug('Converted contrib path "{}" to repo path "{}"'.format(path, r)) - return r - -def verify_mirrored_directory_struture(): - """ - Check that the directories contained in ``contrib/cmake`` exist - in the root of the repo. - """ - for (dirpath, _, _) in os.walk(get_cmake_contrib_dir()): - expectedDir = contribPathToRepoPath(dirpath) - logging.debug('expectedDir:{}'.format(expectedDir)) - if (not (os.path.exists(expectedDir) and os.path.isdir(expectedDir)) and - expectedDir not in verificationExceptions): - logging.error(('Expected to find directory "{}" but it does not exist' - ' or is not a directory').format(expectedDir)) - return 1 - - return 0 - -def mk_sym_link(target, linkName): - logging.info('Making symbolic link target="{}", linkName="{}"'.format(target, linkName)) - if os.path.exists(linkName): - logging.info('Removing existing link "{}"'.format(linkName)) - if not os.path.islink(linkName): - logging.warning('"{}" overwriting file that is not a symlink'.format(linkName)) - delete_path(linkName) - if os.name == 'posix': - os.symlink(target, linkName) - else: - # TODO: Windows does support symlinks but the implementation to do that - # from python is a little complicated so for now lets just copy everyting - logging.warning('Creating symbolic links is not supported. Just making a copy instead') - if os.path.isdir(target): - # Recursively copy directory - shutil.copytree(src=target, dst=linkName, symlinks=False) - else: - # Copy file - assert os.path.isfile(target) - shutil.copy2(src=target, dst=linkName) - -def delete_path(path): - logging.info('Removing "{}"'.format(path)) - if not os.path.exists(path): - logging.warning('"{}" does not exist'.format(path)) - return - if os.path.isdir(path) and not os.path.islink(path): - # FIXME: If we can get symbolic link support on Windows we - # can disallow this completely. - assert os.name == 'nt' - shutil.rmtree(path) - else: - os.remove(path) - -def shouldSkipFile(path): - # Skip this script - if path == get_full_path_to_script(): - return True - # Skip the maintainers file - if path == os.path.join(get_cmake_contrib_dir(), 'maintainers.txt'): - return True - # Skip Vim temporary files - if os.path.basename(path).startswith('.') and path.endswith('.swp'): - return True - return False - - -def create(useHardLinks): - """ - Copy or hard link files in the CMake contrib directory - into the repository where they are intended to live. - - Note that symbolic links for the CMakeLists.txt files - are not appropriate because they won't have the right - file modification time when the files they point to - are modified. This would prevent CMake from correctly - reconfiguring when it detects this is required. - """ - - # Make the ``cmake`` directory a symbolic link. - # We treat this one specially as it is the only directory - # that doesn't already exist in the repository root so - # we can just use a symlink here - linkName = os.path.join(get_repo_root_dir(), 'cmake') - target = os.path.join(get_cmake_contrib_dir(), 'cmake') - specialDir = target - mk_sym_link(target, linkName) - - for (dirPath,_ , fileNames) in os.walk(get_cmake_contrib_dir()): - # Skip the special directory and its children - if dirPath.startswith(specialDir): - logging.info('Skipping directory "{}"'.format(dirPath)) - continue - - for fileName in fileNames: - fileInContrib = os.path.join(dirPath, fileName) - # Skip files - if shouldSkipFile(fileInContrib): - logging.info('Skipping "{}"'.format(fileInContrib)) - continue - fileInRepo = contribPathToRepoPath(fileInContrib) - logging.info('"{}" => "{}"'.format(fileInContrib, fileInRepo)) - if useHardLinks: - if not os.name == 'posix': - logging.error('Hard links are not supported on your platform') - return False - if os.path.exists(fileInRepo): - delete_path(fileInRepo) - os.link(fileInContrib, fileInRepo) - else: - try: - shutil.copy2(src=fileInContrib, dst=fileInRepo) - except shutil.Error as e: - # Can hit this if used created hard links first and then run again without - # wanting hard links - if sys.version_info.major <= 2: - logging.error(e.message) - else: - # Python >= 3 - if isinstance(e, shutil.SameFileError): - logging.error('Trying to copy "{}" to "{}" but they are the same file'.format( - fileInContrib, fileInRepo)) - else: - logging.error(e) - logging.error('You should remove the files using the "remove" mode ' - 'and try to create again. You probably are mixing the ' - 'hard-link and non-hard-link create modes') - return False - return True - -def remove(): - """ - Remove the CMake files from their intended location in - the repository. This is used to remove - the files created by the ``create()`` function. - """ - # This directory is treated specially as it is normally - # a symlink. - linkName = os.path.join(get_repo_root_dir(), 'cmake') - delete_path(linkName) - specialDir = os.path.join(get_cmake_contrib_dir(), 'cmake') - - for (dirPath,_ , fileNames) in os.walk(get_cmake_contrib_dir()): - # Skip the special directory and its children - if dirPath.startswith(specialDir): - logging.info('Skipping directory "{}"'.format(dirPath)) - continue - for fileName in fileNames: - fileInContrib = os.path.join(dirPath, fileName) - # Skip files - if shouldSkipFile(fileInContrib): - logging.info('Skipping "{}"'.format(fileInContrib)) - continue - fileInRepo = contribPathToRepoPath(fileInContrib) - if os.path.exists(fileInRepo): - logging.info('Removing "{}"'.format(fileInRepo)) - delete_path(fileInRepo) - return True - def main(args): logging.basicConfig(level=logging.INFO) parser = argparse.ArgumentParser(description=__doc__) @@ -233,28 +38,10 @@ def main(args): logLevel = getattr(logging, pargs.log_level.upper(),None) logging.basicConfig(level=logLevel) - - # Before we start make sure we can transplant the CMake files on to - # repository - if verify_mirrored_directory_struture() != 0: - logging.error('"{}" does not mirror "{}"'.format(get_cmake_contrib_dir(), get_repo_root_dir())) - return 1 - - if pargs.mode == "create": - if not create(useHardLinks=pargs.hard_link): - logging.error("Failed to create") - return 1 - elif pargs.mode == "create_hard_link": - if not create(useHardLinks=True): - logging.error("Failed to create_hard_link") - return 1 - elif pargs.mode == "remove": - if not remove(): - logging.error("Failed to remove") - return 1 - else: - logging.error('Unknown mode "{}"'.format(pargs.mode)) - + logging.warning('Use of this script is deprecated. The script will be removed in the future') + logging.warning('Action "{}" ignored'.format(pargs.mode)) + if pargs.hard_link: + logging.warning('Hard link option ignored') return 0 if __name__ == '__main__': diff --git a/contrib/cmake/doc/CMakeLists.txt b/doc/CMakeLists.txt similarity index 100% rename from contrib/cmake/doc/CMakeLists.txt rename to doc/CMakeLists.txt diff --git a/doc/z3api.cfg.in b/doc/z3api.cfg.in index 9e946aa7f..9c4b464c2 100644 --- a/doc/z3api.cfg.in +++ b/doc/z3api.cfg.in @@ -704,10 +704,13 @@ INPUT_ENCODING = UTF-8 FILE_PATTERNS = website.dox \ z3_api.h \ z3_algebraic.h \ + z3_ast_containers.h \ + z3_fixedpoint.h \ + z3_fpa.h \ + z3_interp.h \ + z3_optimization.h \ z3_polynomial.h \ z3_rcf.h \ - z3_interp.h \ - z3_fpa.h \ z3++.h \ @PYTHON_API_FILES@ @DOTNET_API_FILES@ @JAVA_API_FILES@ diff --git a/contrib/cmake/examples/CMakeLists.txt b/examples/CMakeLists.txt similarity index 100% rename from contrib/cmake/examples/CMakeLists.txt rename to examples/CMakeLists.txt diff --git a/contrib/cmake/examples/c++/CMakeLists.txt b/examples/c++/CMakeLists.txt similarity index 100% rename from contrib/cmake/examples/c++/CMakeLists.txt rename to examples/c++/CMakeLists.txt diff --git a/contrib/cmake/examples/c/CMakeLists.txt b/examples/c/CMakeLists.txt similarity index 100% rename from contrib/cmake/examples/c/CMakeLists.txt rename to examples/c/CMakeLists.txt diff --git a/examples/dotnet/Program.cs b/examples/dotnet/Program.cs index 20bb012b1..64149a553 100644 --- a/examples/dotnet/Program.cs +++ b/examples/dotnet/Program.cs @@ -2152,6 +2152,31 @@ namespace test_mapi Console.WriteLine("OK, model: {0}", s.Model.ToString()); } + public static void TranslationExample() + { + Context ctx1 = new Context(); + Context ctx2 = new Context(); + + Sort s1 = ctx1.IntSort; + Sort s2 = ctx2.IntSort; + Sort s3 = s1.Translate(ctx2); + + Console.WriteLine(s1 == s2); + Console.WriteLine(s1.Equals(s2)); + Console.WriteLine(s2.Equals(s3)); + Console.WriteLine(s1.Equals(s3)); + + Expr e1 = ctx1.MkIntConst("e1"); + Expr e2 = ctx2.MkIntConst("e1"); + Expr e3 = e1.Translate(ctx2); + + Console.WriteLine(e1 == e2); + Console.WriteLine(e1.Equals(e2)); + Console.WriteLine(e2.Equals(e3)); + Console.WriteLine(e1.Equals(e3)); + } + + static void Main(string[] args) { try @@ -2225,6 +2250,8 @@ namespace test_mapi QuantifierExample4(ctx); } + TranslationExample(); + Log.Close(); if (Log.isOpen()) Console.WriteLine("Log is still open!"); diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java index 5810dab37..25076e27c 100644 --- a/examples/java/JavaExample.java +++ b/examples/java/JavaExample.java @@ -281,7 +281,7 @@ class JavaExample } void disprove(Context ctx, BoolExpr f, boolean useMBQI) - throws TestFailedException + throws TestFailedException { BoolExpr[] a = {}; disprove(ctx, f, useMBQI, a); @@ -2279,6 +2279,29 @@ class JavaExample System.out.println(my); } + public void translationExample() { + Context ctx1 = new Context(); + Context ctx2 = new Context(); + + Sort s1 = ctx1.getIntSort(); + Sort s2 = ctx2.getIntSort(); + Sort s3 = s1.translate(ctx2); + + System.out.println(s1 == s2); + System.out.println(s1.equals(s2)); + System.out.println(s2.equals(s3)); + System.out.println(s1.equals(s3)); + + Expr e1 = ctx1.mkIntConst("e1"); + Expr e2 = ctx2.mkIntConst("e1"); + Expr e3 = e1.translate(ctx2); + + System.out.println(e1 == e2); + System.out.println(e1.equals(e2)); + System.out.println(e2.equals(e3)); + System.out.println(e1.equals(e3)); + } + public static void main(String[] args) { JavaExample p = new JavaExample(); @@ -2300,8 +2323,8 @@ class JavaExample HashMap cfg = new HashMap(); cfg.put("model", "true"); Context ctx = new Context(cfg); - - p.optimizeExample(ctx); + + p.optimizeExample(ctx); p.basicTests(ctx); p.castingTest(ctx); p.sudokuExample(ctx); @@ -2355,7 +2378,9 @@ class JavaExample Context ctx = new Context(cfg); p.quantifierExample3(ctx); p.quantifierExample4(ctx); - } + } + + p.translationExample(); Log.close(); if (Log.isOpen()) diff --git a/contrib/cmake/examples/python/CMakeLists.txt b/examples/python/CMakeLists.txt similarity index 100% rename from contrib/cmake/examples/python/CMakeLists.txt rename to examples/python/CMakeLists.txt diff --git a/contrib/cmake/examples/tptp/CMakeLists.txt b/examples/tptp/CMakeLists.txt similarity index 100% rename from contrib/cmake/examples/tptp/CMakeLists.txt rename to examples/tptp/CMakeLists.txt diff --git a/contrib/cmake/src/CMakeLists.txt b/src/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/CMakeLists.txt rename to src/CMakeLists.txt diff --git a/contrib/cmake/src/ackermannization/CMakeLists.txt b/src/ackermannization/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/ackermannization/CMakeLists.txt rename to src/ackermannization/CMakeLists.txt diff --git a/contrib/cmake/src/api/CMakeLists.txt b/src/api/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/api/CMakeLists.txt rename to src/api/CMakeLists.txt diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index c9cdc6ab3..d34cad2f4 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -558,6 +558,7 @@ extern "C" { Z3_TRY; LOG_Z3_get_sort(c, a); RESET_ERROR_CODE(); + CHECK_IS_EXPR(a, 0); Z3_sort r = of_sort(mk_c(c)->m().get_sort(to_expr(a))); RETURN_Z3(r); Z3_CATCH_RETURN(0); @@ -821,9 +822,13 @@ extern "C" { RESET_ERROR_CODE(); std::ostringstream buffer; switch (mk_c(c)->get_print_mode()) { - case Z3_PRINT_SMTLIB_FULL: - buffer << mk_pp(to_ast(a), mk_c(c)->m()); + case Z3_PRINT_SMTLIB_FULL: { + params_ref p; + p.set_uint("max_depth", 4294967295u); + p.set_uint("min_alias_size", 4294967295u); + buffer << mk_pp(to_ast(a), mk_c(c)->m(), p); break; + } case Z3_PRINT_LOW_LEVEL: buffer << mk_ll_pp(to_ast(a), mk_c(c)->m()); break; @@ -1066,7 +1071,7 @@ extern "C" { case OP_BIT2BOOL: return Z3_OP_BIT2BOOL; case OP_BSMUL_NO_OVFL: return Z3_OP_BSMUL_NO_OVFL; case OP_BUMUL_NO_OVFL: return Z3_OP_BUMUL_NO_OVFL; - case OP_BSMUL_NO_UDFL: return Z3_OP_BSMUL_NO_UDFL; + case OP_BSMUL_NO_UDFL: return Z3_OP_BSMUL_NO_UDFL; case OP_BSDIV_I: return Z3_OP_BSDIV_I; case OP_BUDIV_I: return Z3_OP_BUDIV_I; case OP_BSREM_I: return Z3_OP_BSREM_I; @@ -1124,6 +1129,20 @@ extern "C" { case OP_SEQ_TO_RE: return Z3_OP_SEQ_TO_RE; case OP_SEQ_IN_RE: return Z3_OP_SEQ_IN_RE; + case _OP_STRING_STRREPL: return Z3_OP_SEQ_REPLACE; + case _OP_STRING_CONCAT: return Z3_OP_SEQ_CONCAT; + case _OP_STRING_LENGTH: return Z3_OP_SEQ_LENGTH; + case _OP_STRING_STRCTN: return Z3_OP_SEQ_CONTAINS; + case _OP_STRING_PREFIX: return Z3_OP_SEQ_PREFIX; + case _OP_STRING_SUFFIX: return Z3_OP_SEQ_SUFFIX; + case _OP_STRING_IN_REGEXP: return Z3_OP_SEQ_IN_RE; + case _OP_STRING_TO_REGEXP: return Z3_OP_SEQ_TO_RE; + case _OP_STRING_CHARAT: return Z3_OP_SEQ_AT; + case _OP_STRING_SUBSTR: return Z3_OP_SEQ_EXTRACT; + case _OP_STRING_STRIDOF: return Z3_OP_SEQ_INDEX; + case _OP_REGEXP_EMPTY: return Z3_OP_RE_EMPTY_SET; + case _OP_REGEXP_FULL: return Z3_OP_RE_FULL_SET; + case OP_STRING_STOI: return Z3_OP_STR_TO_INT; case OP_STRING_ITOS: return Z3_OP_INT_TO_STR; diff --git a/contrib/cmake/src/api/dll/CMakeLists.txt b/src/api/dll/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/api/dll/CMakeLists.txt rename to src/api/dll/CMakeLists.txt diff --git a/src/api/dotnet/AST.cs b/src/api/dotnet/AST.cs index 2ffaaa661..c7ca1851e 100644 --- a/src/api/dotnet/AST.cs +++ b/src/api/dotnet/AST.cs @@ -14,7 +14,7 @@ Author: Christoph Wintersteiger (cwinter) 2012-03-16 Notes: - + --*/ using System; @@ -25,7 +25,7 @@ using System.Diagnostics.Contracts; namespace Microsoft.Z3 { /// - /// The abstract syntax tree (AST) class. + /// The abstract syntax tree (AST) class. /// [ContractVerification(true)] public class AST : Z3Object, IComparable @@ -35,7 +35,7 @@ namespace Microsoft.Z3 /// /// An AST /// An AST - /// True if and are from the same context + /// True if and are from the same context /// and represent the same sort; false otherwise. public static bool operator ==(AST a, AST b) { @@ -51,7 +51,7 @@ namespace Microsoft.Z3 /// /// An AST /// An AST - /// True if and are not from the same context + /// True if and are not from the same context /// or represent different sorts; false otherwise. public static bool operator !=(AST a, AST b) { @@ -120,12 +120,12 @@ namespace Microsoft.Z3 if (ReferenceEquals(Context, ctx)) return this; else - return new AST(ctx, Native.Z3_translate(Context.nCtx, NativeObject, ctx.nCtx)); + return Create(ctx, Native.Z3_translate(Context.nCtx, NativeObject, ctx.nCtx)); } /// /// The kind of the AST. - /// + /// public Z3_ast_kind ASTKind { get { return (Z3_ast_kind)Native.Z3_get_ast_kind(Context.nCtx, NativeObject); } @@ -224,10 +224,10 @@ namespace Microsoft.Z3 { Native.Z3_dec_ref(ctx.nCtx, obj); } - }; + }; internal override void IncRef(IntPtr o) - { + { // Console.WriteLine("AST IncRef()"); if (Context == null || o == IntPtr.Zero) return; diff --git a/contrib/cmake/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/api/dotnet/CMakeLists.txt rename to src/api/dotnet/CMakeLists.txt diff --git a/src/api/dotnet/Expr.cs b/src/api/dotnet/Expr.cs index cac62d2f0..6c52b83c8 100644 --- a/src/api/dotnet/Expr.cs +++ b/src/api/dotnet/Expr.cs @@ -163,13 +163,7 @@ namespace Microsoft.Z3 /// A copy of the term which is associated with new public Expr Translate(Context ctx) { - Contract.Requires(ctx != null); - Contract.Ensures(Contract.Result() != null); - - if (ReferenceEquals(Context, ctx)) - return this; - else - return Expr.Create(ctx, Native.Z3_translate(Context.nCtx, NativeObject, ctx.nCtx)); + return (Expr)base.Translate(ctx); } /// @@ -797,6 +791,77 @@ namespace Microsoft.Z3 public bool IsLabelLit { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL_LIT; } } #endregion + #region Sequences and Strings + + /// + /// Check whether expression is a string constant. + /// + /// a Boolean + public bool IsString { get { return IsApp && 0 != Native.Z3_is_string(Context.nCtx, NativeObject); } } + + /// + /// Retrieve string corresponding to string constant. + /// + /// the expression should be a string constant, (IsString should be true). + public string String { get { return Native.Z3_get_string(Context.nCtx, NativeObject); } } + + /// + /// Check whether expression is a concatentation. + /// + /// a Boolean + public bool IsConcat { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_CONCAT; } } + + /// + /// Check whether expression is a prefix. + /// + /// a Boolean + public bool IsPrefix { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_PREFIX; } } + + /// + /// Check whether expression is a suffix. + /// + /// a Boolean + public bool IsSuffix { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_SUFFIX; } } + + /// + /// Check whether expression is a contains. + /// + /// a Boolean + public bool IsContains { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_CONTAINS; } } + + /// + /// Check whether expression is an extract. + /// + /// a Boolean + public bool IsExtract { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_EXTRACT; } } + + /// + /// Check whether expression is a replace. + /// + /// a Boolean + public bool IsReplace { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_REPLACE; } } + + /// + /// Check whether expression is an at. + /// + /// a Boolean + public bool IsAt { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_AT; } } + + /// + /// Check whether expression is a sequence length. + /// + /// a Boolean + public bool IsLength { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_LENGTH; } } + + /// + /// Check whether expression is a sequence index. + /// + /// a Boolean + public bool IsIndex { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_SEQ_INDEX; } } + + + #endregion + #region Proof Terms /// /// Indicates whether the term is a binary equivalence modulo namings. diff --git a/src/api/dotnet/FuncDecl.cs b/src/api/dotnet/FuncDecl.cs index 2f5cd0ce8..0587a2276 100644 --- a/src/api/dotnet/FuncDecl.cs +++ b/src/api/dotnet/FuncDecl.cs @@ -14,7 +14,7 @@ Author: Christoph Wintersteiger (cwinter) 2012-03-16 Notes: - + --*/ using System; @@ -23,7 +23,7 @@ using System.Diagnostics.Contracts; namespace Microsoft.Z3 { /// - /// Function declarations. + /// Function declarations. /// [ContractVerification(true)] public class FuncDecl : AST @@ -62,7 +62,7 @@ namespace Microsoft.Z3 /// /// A hash code. - /// + /// public override int GetHashCode() { return base.GetHashCode(); @@ -205,7 +205,7 @@ namespace Microsoft.Z3 } /// - /// Function declarations can have Parameters associated with them. + /// Function declarations can have Parameters associated with them. /// public class Parameter { @@ -315,6 +315,17 @@ namespace Microsoft.Z3 #endif #endregion + /// + /// Translates (copies) the function declaration to the Context . + /// + /// A context + /// A copy of the function declaration which is associated with + new public FuncDecl Translate(Context ctx) + { + return (FuncDecl) base.Translate(ctx); + } + + /// /// Create expression that applies function to arguments. /// @@ -342,6 +353,5 @@ namespace Microsoft.Z3 Context.CheckContextMatch(args); return Expr.Create(Context, this, args); } - } } diff --git a/src/api/dotnet/Model.cs b/src/api/dotnet/Model.cs index a7f62e6e8..12992fa8a 100644 --- a/src/api/dotnet/Model.cs +++ b/src/api/dotnet/Model.cs @@ -19,6 +19,7 @@ Notes: using System; using System.Diagnostics.Contracts; +using System.Collections.Generic; namespace Microsoft.Z3 { @@ -131,6 +132,24 @@ namespace Microsoft.Z3 } } + /// + /// Enumerate constants in model. + /// + public IEnumerable> Consts + { + get + { + uint nc = NumConsts; + for (uint i = 0; i < nc; ++i) + { + var f = new FuncDecl(Context, Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i)); + IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f.NativeObject); + if (n == IntPtr.Zero) continue; + yield return new KeyValuePair(f, Expr.Create(Context, n)); + } + } + } + /// /// The number of function interpretations in the model. /// diff --git a/src/api/dotnet/Quantifier.cs b/src/api/dotnet/Quantifier.cs index eb21ed2b9..eca4e3c7e 100644 --- a/src/api/dotnet/Quantifier.cs +++ b/src/api/dotnet/Quantifier.cs @@ -14,7 +14,7 @@ Author: Christoph Wintersteiger (cwinter) 2012-03-19 Notes: - + --*/ using System; @@ -157,6 +157,16 @@ namespace Microsoft.Z3 } } + /// + /// Translates (copies) the quantifier to the Context . + /// + /// A context + /// A copy of the quantifier which is associated with + new public Quantifier Translate(Context ctx) + { + return (Quantifier)base.Translate(ctx); + } + #region Internal [ContractVerification(false)] // F: Clousot ForAll decompilation gets confused below. Setting verification off until I fixed the bug internal Quantifier(Context ctx, bool isForall, Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null) diff --git a/src/api/dotnet/Sort.cs b/src/api/dotnet/Sort.cs index e1b8ca1b7..e6f195434 100644 --- a/src/api/dotnet/Sort.cs +++ b/src/api/dotnet/Sort.cs @@ -14,7 +14,7 @@ Author: Christoph Wintersteiger (cwinter) 2012-03-15 Notes: - + --*/ using System; @@ -33,7 +33,7 @@ namespace Microsoft.Z3 /// /// A Sort /// A Sort - /// True if and are from the same context + /// True if and are from the same context /// and represent the same sort; false otherwise. public static bool operator ==(Sort a, Sort b) { @@ -49,7 +49,7 @@ namespace Microsoft.Z3 /// /// A Sort /// A Sort - /// True if and are not from the same context + /// True if and are not from the same context /// or represent different sorts; false otherwise. public static bool operator !=(Sort a, Sort b) { @@ -113,10 +113,20 @@ namespace Microsoft.Z3 return Native.Z3_sort_to_string(Context.nCtx, NativeObject); } + /// + /// Translates (copies) the sort to the Context . + /// + /// A context + /// A copy of the sort which is associated with + new public Sort Translate(Context ctx) + { + return (Sort)base.Translate(ctx); + } + #region Internal /// /// Sort constructor - /// + /// internal Sort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); } #if DEBUG @@ -154,5 +164,5 @@ namespace Microsoft.Z3 } } #endregion - } + } } diff --git a/contrib/cmake/src/api/dotnet/cmake_install_gac.cmake.in b/src/api/dotnet/cmake_install_gac.cmake.in similarity index 100% rename from contrib/cmake/src/api/dotnet/cmake_install_gac.cmake.in rename to src/api/dotnet/cmake_install_gac.cmake.in diff --git a/contrib/cmake/src/api/dotnet/cmake_uninstall_gac.cmake.in b/src/api/dotnet/cmake_uninstall_gac.cmake.in similarity index 100% rename from contrib/cmake/src/api/dotnet/cmake_uninstall_gac.cmake.in rename to src/api/dotnet/cmake_uninstall_gac.cmake.in diff --git a/src/api/java/AST.java b/src/api/java/AST.java index e1cde837f..350830443 100644 --- a/src/api/java/AST.java +++ b/src/api/java/AST.java @@ -87,12 +87,10 @@ public class AST extends Z3Object implements Comparable **/ public AST translate(Context ctx) { - if (getContext() == ctx) { return this; } else { - return new AST(ctx, Native.translate(getContext().nCtx(), - getNativeObject(), ctx.nCtx())); + return create(ctx, Native.translate(getContext().nCtx(), getNativeObject(), ctx.nCtx())); } } diff --git a/contrib/cmake/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/api/java/CMakeLists.txt rename to src/api/java/CMakeLists.txt diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index ef86f510a..6cabbb1b8 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -194,14 +194,7 @@ public class Expr extends AST **/ public Expr translate(Context ctx) { - if (getContext() == ctx) { - return this; - } else { - return Expr.create( - ctx, - Native.translate(getContext().nCtx(), getNativeObject(), - ctx.nCtx())); - } + return (Expr) super.translate(ctx); } /** @@ -1277,6 +1270,35 @@ public class Expr extends AST return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LABEL_LIT; } + /** + * Check whether expression is a string constant. + * @return a boolean + */ + public boolean isString() + { + return isApp() && Native.isString(getContext().nCtx(), getNativeObject()); + } + + /** + * Retrieve string corresponding to string constant. + * Remark: the expression should be a string constant, (isString() should return true). + * @throws Z3Exception on error + * @return a string + */ + public String getString() + { + return Native.getString(getContext().nCtx(), getNativeObject()); + } + + /** + * Check whether expression is a concatenation + * @return a boolean + */ + public boolean isConcat() + { + return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_SEQ_CONCAT; + } + /** * Indicates whether the term is a binary equivalence modulo namings. * Remarks: This binary predicate is used in proof terms. It captures diff --git a/src/api/java/FuncDecl.java b/src/api/java/FuncDecl.java index 273e853c0..255bc2c4a 100644 --- a/src/api/java/FuncDecl.java +++ b/src/api/java/FuncDecl.java @@ -1,6 +1,6 @@ /** Copyright (c) 2012-2014 Microsoft Corporation - + Module Name: FuncDecl.java @@ -12,8 +12,8 @@ Author: @author Christoph Wintersteiger (cwinter) 2012-03-15 Notes: - -**/ + +**/ package com.microsoft.z3; @@ -59,6 +59,18 @@ public class FuncDecl extends AST return Native.getFuncDeclId(getContext().nCtx(), getNativeObject()); } + /** + * Translates (copies) the function declaration to the Context {@code ctx}. + * @param ctx A context + * + * @return A copy of the function declaration which is associated with {@code ctx} + * @throws Z3Exception on error + **/ + public FuncDecl translate(Context ctx) + { + return (FuncDecl) super.translate(ctx); + } + /** * The arity of the function declaration **/ @@ -68,7 +80,7 @@ public class FuncDecl extends AST } /** - * The size of the domain of the function declaration + * The size of the domain of the function declaration * @see #getArity **/ public int getDomainSize() @@ -324,7 +336,7 @@ public class FuncDecl extends AST } FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range) - + { super(ctx, Native.mkFuncDecl(ctx.nCtx(), name.getNativeObject(), AST.arrayLength(domain), AST.arrayToNative(domain), @@ -333,7 +345,7 @@ public class FuncDecl extends AST } FuncDecl(Context ctx, String prefix, Sort[] domain, Sort range) - + { super(ctx, Native.mkFreshFuncDecl(ctx.nCtx(), prefix, AST.arrayLength(domain), AST.arrayToNative(domain), @@ -351,7 +363,7 @@ public class FuncDecl extends AST } /** - * Create expression that applies function to arguments. + * Create expression that applies function to arguments. **/ public Expr apply(Expr ... args) { diff --git a/src/api/java/Quantifier.java b/src/api/java/Quantifier.java index bc2537107..ce2adce21 100644 --- a/src/api/java/Quantifier.java +++ b/src/api/java/Quantifier.java @@ -145,6 +145,19 @@ public class Quantifier extends BoolExpr .nCtx(), getNativeObject())); } + /** + * Translates (copies) the quantifier to the Context {@code ctx}. + * + * @param ctx A context + * + * @return A copy of the quantifier which is associated with {@code ctx} + * @throws Z3Exception on error + **/ + public Quantifier translate(Context ctx) + { + return (Quantifier) super.translate(ctx); + } + /** * Create a quantified expression. * diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java index 0763a69a3..e7a186ad2 100644 --- a/src/api/java/Sort.java +++ b/src/api/java/Sort.java @@ -87,6 +87,19 @@ public class Sort extends AST return Native.sortToString(getContext().nCtx(), getNativeObject()); } + /** + * Translates (copies) the sort to the Context {@code ctx}. + * + * @param ctx A context + * + * @return A copy of the sort which is associated with {@code ctx} + * @throws Z3Exception on error + **/ + public Sort translate(Context ctx) + { + return (Sort) super.translate(ctx); + } + /** * Sort constructor **/ diff --git a/contrib/cmake/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/api/python/CMakeLists.txt rename to src/api/python/CMakeLists.txt diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 84a80ddf7..52cc2e858 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -50,6 +50,7 @@ from fractions import Fraction import sys import io import math +import copy if sys.version < '3': def _is_int(v): @@ -288,6 +289,9 @@ class AstRef(Z3PPObject): if self.ctx.ref() is not None: Z3_dec_ref(self.ctx.ref(), self.as_ast()) + def __deepcopy__(self, memo={}): + return _to_ast_ref(self.ast, self.ctx) + def __str__(self): return obj_to_string(self) @@ -314,7 +318,7 @@ class AstRef(Z3PPObject): raise Z3Exception("Symbolic expressions cannot be cast to concrete Boolean values.") def sexpr(self): - """Return an string representing the AST node in s-expression notation. + """Return a string representing the AST node in s-expression notation. >>> x = Int('x') >>> ((x + 1)*x).sexpr() @@ -4357,6 +4361,11 @@ class Datatype: self.name = name self.constructors = [] + def __deepcopy__(self, memo={}): + r = Datatype(self.name, self.ctx) + r.constructors = copy.deepcopy(self.constructors) + return r + def declare_core(self, name, rec_name, *args): if __debug__: _z3_assert(isinstance(name, str), "String expected") @@ -4647,11 +4656,17 @@ class ParamsRef: Consider using the function `args2params` to create instances of this object. """ - def __init__(self, ctx=None): + def __init__(self, ctx=None, params=None): self.ctx = _get_ctx(ctx) - self.params = Z3_mk_params(self.ctx.ref()) + if params is None: + self.params = Z3_mk_params(self.ctx.ref()) + else: + self.params = params Z3_params_inc_ref(self.ctx.ref(), self.params) + def __deepcopy__(self, memo={}): + return ParamsRef(self.ctx, self.params) + def __del__(self): if self.ctx.ref() is not None: Z3_params_dec_ref(self.ctx.ref(), self.params) @@ -4711,6 +4726,9 @@ class ParamDescrsRef: self.descr = descr Z3_param_descrs_inc_ref(self.ctx.ref(), self.descr) + def __deepcopy__(self, memo={}): + return ParamsDescrsRef(self.descr, self.ctx) + def __del__(self): if self.ctx.ref() is not None: Z3_param_descrs_dec_ref(self.ctx.ref(), self.descr) @@ -4772,6 +4790,9 @@ class Goal(Z3PPObject): self.goal = Z3_mk_goal(self.ctx.ref(), models, unsat_cores, proofs) Z3_goal_inc_ref(self.ctx.ref(), self.goal) + def __deepcopy__(self, memo={}): + return Goal(False, False, False, self.ctx, self.goal) + def __del__(self): if self.goal is not None and self.ctx.ref() is not None: Z3_goal_dec_ref(self.ctx.ref(), self.goal) @@ -5034,6 +5055,9 @@ class AstVector(Z3PPObject): self.ctx = ctx Z3_ast_vector_inc_ref(self.ctx.ref(), self.vector) + def __deepcopy__(self, memo={}): + return AstVector(self.vector, self.ctx) + def __del__(self): if self.vector is not None and self.ctx.ref() is not None: Z3_ast_vector_dec_ref(self.ctx.ref(), self.vector) @@ -5169,6 +5193,9 @@ class AstMap: self.ctx = ctx Z3_ast_map_inc_ref(self.ctx.ref(), self.map) + def __deepcopy__(self, memo={}): + return AstMap(self.map, self.ctx) + def __del__(self): if self.map is not None and self.ctx.ref() is not None: Z3_ast_map_dec_ref(self.ctx.ref(), self.map) @@ -5284,6 +5311,9 @@ class FuncEntry: self.ctx = ctx Z3_func_entry_inc_ref(self.ctx.ref(), self.entry) + def __deepcopy__(self, memo={}): + return FuncEntry(self.entry, self.ctx) + def __del__(self): if self.ctx.ref() is not None: Z3_func_entry_dec_ref(self.ctx.ref(), self.entry) @@ -5390,6 +5420,9 @@ class FuncInterp(Z3PPObject): if self.f is not None: Z3_func_interp_inc_ref(self.ctx.ref(), self.f) + def __deepcopy__(self, memo={}): + return FuncInterp(self.f, self.ctx) + def __del__(self): if self.f is not None and self.ctx.ref() is not None: Z3_func_interp_dec_ref(self.ctx.ref(), self.f) @@ -5500,6 +5533,9 @@ class ModelRef(Z3PPObject): self.ctx = ctx Z3_model_inc_ref(self.ctx.ref(), self.model) + def __deepcopy__(self, memo={}): + return ModelRef(self.m, self.ctx) + def __del__(self): if self.ctx.ref() is not None: Z3_model_dec_ref(self.ctx.ref(), self.model) @@ -5776,6 +5812,9 @@ class Statistics: self.ctx = ctx Z3_stats_inc_ref(self.ctx.ref(), self.stats) + def __deepcopy__(self, memo={}): + return Statistics(self.stats, self.ctx) + def __del__(self): if self.ctx.ref() is not None: Z3_stats_dec_ref(self.ctx.ref(), self.stats) @@ -5910,6 +5949,9 @@ class CheckSatResult: def __init__(self, r): self.r = r + def __deepcopy__(self, memo={}): + return CheckSatResult(self.r) + def __eq__(self, other): return isinstance(other, CheckSatResult) and self.r == other.r @@ -5949,6 +5991,9 @@ class Solver(Z3PPObject): self.solver = solver Z3_solver_inc_ref(self.ctx.ref(), self.solver) + def __deepcopy__(self, memo={}): + return Solver(self.solver, self.ctx) + def __del__(self): if self.solver is not None and self.ctx.ref() is not None: Z3_solver_dec_ref(self.ctx.ref(), self.solver) @@ -6369,6 +6414,9 @@ class Fixedpoint(Z3PPObject): Z3_fixedpoint_inc_ref(self.ctx.ref(), self.fixedpoint) self.vars = [] + def __deepcopy__(self, memo={}): + return FixedPoint(self.fixedpoint, self.ctx) + def __del__(self): if self.fixedpoint is not None and self.ctx.ref() is not None: Z3_fixedpoint_dec_ref(self.ctx.ref(), self.fixedpoint) @@ -6743,6 +6791,9 @@ class Optimize(Z3PPObject): self.optimize = Z3_mk_optimize(self.ctx.ref()) Z3_optimize_inc_ref(self.ctx.ref(), self.optimize) + def __deepcopy__(self, memo={}): + return Optimize(self.optimize, self.ctx) + def __del__(self): if self.optimize is not None and self.ctx.ref() is not None: Z3_optimize_dec_ref(self.ctx.ref(), self.optimize) @@ -6895,6 +6946,9 @@ class ApplyResult(Z3PPObject): self.ctx = ctx Z3_apply_result_inc_ref(self.ctx.ref(), self.result) + def __deepcopy__(self, memo={}): + return ApplyResult(self.result, self.ctx) + def __del__(self): if self.ctx.ref() is not None: Z3_apply_result_dec_ref(self.ctx.ref(), self.result) @@ -7023,6 +7077,9 @@ class Tactic: raise Z3Exception("unknown tactic '%s'" % tactic) Z3_tactic_inc_ref(self.ctx.ref(), self.tactic) + def __deepcopy__(self, memo={}): + return Tactic(self.tactic, self.ctx) + def __del__(self): if self.tactic is not None and self.ctx.ref() is not None: Z3_tactic_dec_ref(self.ctx.ref(), self.tactic) @@ -7295,6 +7352,9 @@ class Probe: raise Z3Exception("unknown probe '%s'" % probe) Z3_probe_inc_ref(self.ctx.ref(), self.probe) + def __deepcopy__(self, memo={}): + return Probe(self.probe, self.ctx) + def __del__(self): if self.probe is not None and self.ctx.ref() is not None: Z3_probe_dec_ref(self.ctx.ref(), self.probe) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 45065f856..63f1d15ff 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -48,6 +48,7 @@ DEFINE_TYPE(Z3_rcf_num); /*@{*/ /** @name Types + @{ Most of the types in the C API are opaque pointers. @@ -5238,7 +5239,6 @@ extern "C" { def_API('Z3_get_error_msg', STRING, (_in(CONTEXT), _in(ERROR_CODE))) */ Z3_string Z3_API Z3_get_error_msg(Z3_context c, Z3_error_code err); - /*@}*/ /** \brief Return a string describing the given error code. @@ -5349,6 +5349,10 @@ extern "C" { /** \brief Add a new formula \c a to the given goal. + Conjunctions are split into separate formulas. + If the goal is \c false, adding new formulas is a no-op. + If the formula \c a is \c true, then nothing is added. + If the formula \c a is \c false, then the entire goal is replaced by the formula \c false. def_API('Z3_goal_assert', VOID, (_in(CONTEXT), _in(GOAL), _in(AST))) */ @@ -5791,9 +5795,35 @@ extern "C" { /** @name Solvers*/ /*@{*/ /** - \brief Create a new (incremental) solver. This solver also uses a - set of builtin tactics for handling the first check-sat command, and - check-sat commands that take more than a given number of milliseconds to be solved. + \brief Create a new solver. This solver is a "combined solver" (see + combined_solver module) that internally uses a non-incremental (solver1) and an + incremental solver (solver2). This combined solver changes its behaviour based + on how it is used and how its parameters are set. + + If the solver is used in a non incremental way (i.e. no calls to + `Z3_solver_push()` or `Z3_solver_pop()`, and no calls to + `Z3_solver_assert()` or `Z3_solver_assert_and_track()` after checking + satisfiability without an intervening `Z3_solver_reset()`) then solver1 + will be used. This solver will apply Z3's "default" tactic. + + The "default" tactic will attempt to probe the logic used by the + assertions and will apply a specialized tactic if one is supported. + Otherwise the general `(and-then simplify smt)` tactic will be used. + + If the solver is used in an incremental way then the combined solver + will switch to using solver2 (which behaves similarly to the general + "smt" tactic). + + Note however it is possible to set the `solver2_timeout`, + `solver2_unknown`, and `ignore_solver1` parameters of the combined + solver to change its behaviour. + + The function #Z3_solver_get_model retrieves a model if the + assertions is satisfiable (i.e., the result is \c + Z3_L_TRUE) and model construction is enabled. + The function #Z3_solver_get_model can also be used even + if the result is \c Z3_L_UNDEF, but the returned model + is not guaranteed to satisfy quantified assertions. \remark User must use #Z3_solver_inc_ref and #Z3_solver_dec_ref to manage solver objects. Even if the context was created using #Z3_mk_context instead of #Z3_mk_context_rc. @@ -5803,7 +5833,17 @@ extern "C" { Z3_solver Z3_API Z3_mk_solver(Z3_context c); /** - \brief Create a new (incremental) solver. + \brief Create a new incremental solver. + + This is equivalent to applying the "smt" tactic. + + Unlike `Z3_mk_solver()` this solver + - Does not attempt to apply any logic specific tactics. + - Does not change its behaviour based on whether it used + incrementally/non-incrementally. + + Note that these differences can result in very different performance + compared to `Z3_mk_solver()`. The function #Z3_solver_get_model retrieves a model if the assertions is satisfiable (i.e., the result is \c diff --git a/src/api/z3_optimization.h b/src/api/z3_optimization.h index 795b4b8fd..f49e1b9ce 100644 --- a/src/api/z3_optimization.h +++ b/src/api/z3_optimization.h @@ -75,7 +75,7 @@ extern "C" { \brief Add a maximization constraint. \param c - context \param o - optimization context - \param a - arithmetical term + \param t - arithmetical term def_API('Z3_optimize_maximize', UINT, (_in(CONTEXT), _in(OPTIMIZE), _in(AST))) */ unsigned Z3_API Z3_optimize_maximize(Z3_context c, Z3_optimize o, Z3_ast t); @@ -84,7 +84,7 @@ extern "C" { \brief Add a minimization constraint. \param c - context \param o - optimization context - \param a - arithmetical term + \param t - arithmetical term def_API('Z3_optimize_minimize', UINT, (_in(CONTEXT), _in(OPTIMIZE), _in(AST))) */ diff --git a/contrib/cmake/src/ast/CMakeLists.txt b/src/ast/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/ast/CMakeLists.txt rename to src/ast/CMakeLists.txt diff --git a/src/ast/ast.h b/src/ast/ast.h index 6bb3b01c9..475e58ac7 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -2082,6 +2082,7 @@ public: bool is_undef_proof(expr const * e) const { return e == m_undef_proof; } bool is_asserted(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_ASSERTED); } + bool is_hypothesis (expr const *e) const {return is_app_of (e, m_basic_family_id, PR_HYPOTHESIS);} bool is_goal(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_GOAL); } bool is_modus_ponens(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_MODUS_PONENS); } bool is_reflexivity(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_REFLEXIVITY); } @@ -2112,6 +2113,7 @@ public: bool is_skolemize(expr const * e) const { return is_app_of(e, m_basic_family_id, PR_SKOLEMIZE); } MATCH_UNARY(is_asserted); + MATCH_UNARY(is_hypothesis); MATCH_UNARY(is_lemma); bool has_fact(proof const * p) const { diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index 89af8bd3e..d5e46548a 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -557,7 +557,14 @@ class smt2_printer { format * f; if (v->get_idx() < m_var_names.size()) { symbol s = m_var_names[m_var_names.size() - v->get_idx() - 1]; - f = mk_string(m(), s.str().c_str()); + std::string vname; + if (is_smt2_quoted_symbol (s)) { + vname = mk_smt2_quoted_symbol (s); + } + else { + vname = s.str(); + } + f = mk_string(m(), vname.c_str ()); } else { // fallback... it is not supposed to happen when the printer is correctly used. @@ -884,7 +891,14 @@ class smt2_printer { symbol * it = m_var_names.end() - num_decls; for (unsigned i = 0; i < num_decls; i++, it++) { format * fs[1] = { m_env.pp_sort(q->get_decl_sort(i)) }; - buf.push_back(mk_seq1(m(), fs, fs+1, f2f(), it->str().c_str())); + std::string var_name; + if (is_smt2_quoted_symbol (*it)) { + var_name = mk_smt2_quoted_symbol (*it); + } + else { + var_name = it->str ();\ + } + buf.push_back(mk_seq1(m(), fs, fs+1, f2f(), var_name.c_str ())); } return mk_seq5(m(), buf.begin(), buf.end(), f2f()); } diff --git a/src/ast/expr_map.h b/src/ast/expr_map.h index ddd94ea13..2b49a4a30 100644 --- a/src/ast/expr_map.h +++ b/src/ast/expr_map.h @@ -35,6 +35,13 @@ class expr_map { obj_map m_expr2expr; obj_map m_expr2pr; public: + typedef obj_map Map; + typedef Map::iterator iterator; + typedef Map::key key; + typedef Map::value value; + typedef Map::data data; + typedef Map::entry entry; + expr_map(ast_manager & m); expr_map(ast_manager & m, bool store_proofs); ~expr_map(); @@ -44,6 +51,8 @@ public: void erase(expr * k); void reset(); void flush(); + iterator begin () const { return m_expr2expr.begin (); } + iterator end () const {return m_expr2expr.end (); } void set_store_proofs(bool f) { if (m_store_proofs != f) flush(); m_store_proofs = f; diff --git a/contrib/cmake/src/ast/fpa/CMakeLists.txt b/src/ast/fpa/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/ast/fpa/CMakeLists.txt rename to src/ast/fpa/CMakeLists.txt diff --git a/contrib/cmake/src/ast/macros/CMakeLists.txt b/src/ast/macros/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/ast/macros/CMakeLists.txt rename to src/ast/macros/CMakeLists.txt diff --git a/contrib/cmake/src/ast/normal_forms/CMakeLists.txt b/src/ast/normal_forms/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/ast/normal_forms/CMakeLists.txt rename to src/ast/normal_forms/CMakeLists.txt diff --git a/contrib/cmake/src/ast/pattern/CMakeLists.txt b/src/ast/pattern/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/ast/pattern/CMakeLists.txt rename to src/ast/pattern/CMakeLists.txt diff --git a/contrib/cmake/src/ast/proof_checker/CMakeLists.txt b/src/ast/proof_checker/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/ast/proof_checker/CMakeLists.txt rename to src/ast/proof_checker/CMakeLists.txt diff --git a/contrib/cmake/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/ast/rewriter/CMakeLists.txt rename to src/ast/rewriter/CMakeLists.txt diff --git a/contrib/cmake/src/ast/rewriter/bit_blaster/CMakeLists.txt b/src/ast/rewriter/bit_blaster/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/ast/rewriter/bit_blaster/CMakeLists.txt rename to src/ast/rewriter/bit_blaster/CMakeLists.txt diff --git a/contrib/cmake/src/ast/simplifier/CMakeLists.txt b/src/ast/simplifier/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/ast/simplifier/CMakeLists.txt rename to src/ast/simplifier/CMakeLists.txt diff --git a/contrib/cmake/src/ast/substitution/CMakeLists.txt b/src/ast/substitution/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/ast/substitution/CMakeLists.txt rename to src/ast/substitution/CMakeLists.txt diff --git a/contrib/cmake/src/cmd_context/CMakeLists.txt b/src/cmd_context/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/cmd_context/CMakeLists.txt rename to src/cmd_context/CMakeLists.txt diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 26cd0628e..ea6d1c232 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -39,7 +39,7 @@ class help_cmd : public cmd { ctx.regular_stream() << " (" << s; if (usage) ctx.regular_stream() << " " << escaped(usage, true) << ")\n"; - else + else ctx.regular_stream() << ")\n"; if (descr) { ctx.regular_stream() << " " << escaped(descr, true, 4) << "\n"; @@ -62,7 +62,7 @@ public: } m_cmds.push_back(s); } - + typedef std::pair named_cmd; struct named_cmd_lt { bool operator()(named_cmd const & c1, named_cmd const & c2) const { return c1.first.str() < c2.first.str(); } @@ -104,14 +104,14 @@ class get_model_cmd : public cmd { unsigned m_index; public: get_model_cmd(): cmd("get-model"), m_index(0) {} - virtual char const * get_usage() const { return "[]"; } - virtual char const * get_descr(cmd_context & ctx) const { - return "retrieve model for the last check-sat command.\nSupply optional index if retrieving a model corresponding to a box optimization objective"; + virtual char const * get_usage() const { return "[]"; } + virtual char const * get_descr(cmd_context & ctx) const { + return "retrieve model for the last check-sat command.\nSupply optional index if retrieving a model corresponding to a box optimization objective"; } - virtual unsigned get_arity() const { return VAR_ARITY; } + virtual unsigned get_arity() const { return VAR_ARITY; } virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_UINT; } - virtual void set_next_arg(cmd_context & ctx, unsigned index) { m_index = index; } - virtual void execute(cmd_context & ctx) { + virtual void set_next_arg(cmd_context & ctx, unsigned index) { m_index = index; } + virtual void execute(cmd_context & ctx) { if (!ctx.is_model_available() || ctx.get_check_sat_result() == 0) throw cmd_exception("model is not available"); model_ref m; @@ -122,7 +122,7 @@ public: ctx.get_check_sat_result()->get_model(m); } ctx.display_model(m); - } + } virtual void reset(cmd_context& ctx) { m_index = 0; } @@ -149,7 +149,14 @@ ATOMIC_CMD(get_assignment_cmd, "get-assignment", "retrieve assignment", { first = false; else ctx.regular_stream() << " "; - ctx.regular_stream() << "(" << name << " " << (ctx.m().is_true(val) ? "true" : "false") << ")"; + ctx.regular_stream() << "("; + if (is_smt2_quoted_symbol(name)) { + ctx.regular_stream() << mk_smt2_quoted_symbol(name); + } + else { + ctx.regular_stream() << name; + } + ctx.regular_stream() << " " << (ctx.m().is_true(val) ? "true" : "false") << ")"; } } } @@ -160,11 +167,11 @@ class cmd_is_declared : public ast_smt_pp::is_declared { cmd_context& m_ctx; public: cmd_is_declared(cmd_context& ctx): m_ctx(ctx) {} - - virtual bool operator()(func_decl* d) const { + + virtual bool operator()(func_decl* d) const { return m_ctx.is_func_decl(d->get_name()); } - virtual bool operator()(sort* s) const { + virtual bool operator()(sort* s) const { return m_ctx.is_sort_decl(s->get_name()); } }; @@ -182,13 +189,13 @@ ATOMIC_CMD(get_proof_cmd, "get-proof", "retrieve proof", { if (ctx.well_sorted_check_enabled() && !is_well_sorted(ctx.m(), pr)) { throw cmd_exception("proof is not well sorted"); } - + pp_params params; if (params.pretty_proof()) { ctx.regular_stream() << mk_pp(pr, ctx.m()) << std::endl; } else { - // TODO: reimplement a new SMT2 pretty printer + // TODO: reimplement a new SMT2 pretty printer ast_smt_pp pp(ctx.m()); cmd_is_declared isd(ctx); pp.set_is_declared(&isd); @@ -198,20 +205,21 @@ ATOMIC_CMD(get_proof_cmd, "get-proof", "retrieve proof", { } }); -#define PRINT_CORE() \ - ptr_vector core; \ - ctx.get_check_sat_result()->get_unsat_core(core); \ - ctx.regular_stream() << "("; \ - ptr_vector::const_iterator it = core.begin(); \ - ptr_vector::const_iterator end = core.end(); \ - for (bool first = true; it != end; ++it) { \ - if (first) \ - first = false; \ - else \ - ctx.regular_stream() << " "; \ - ctx.regular_stream() << mk_ismt2_pp(*it, ctx.m()); \ - } \ - ctx.regular_stream() << ")" << std::endl; \ +static void print_core(cmd_context& ctx) { + ptr_vector core; + ctx.get_check_sat_result()->get_unsat_core(core); + ctx.regular_stream() << "("; + ptr_vector::const_iterator it = core.begin(); + ptr_vector::const_iterator end = core.end(); + for (bool first = true; it != end; ++it) { + if (first) + first = false; + else + ctx.regular_stream() << " "; + ctx.regular_stream() << mk_ismt2_pp(*it, ctx.m()); + } + ctx.regular_stream() << ")" << std::endl; +} ATOMIC_CMD(get_unsat_core_cmd, "get-unsat-core", "retrieve unsat core", { if (!ctx.produce_unsat_cores()) @@ -219,7 +227,7 @@ ATOMIC_CMD(get_unsat_core_cmd, "get-unsat-core", "retrieve unsat core", { if (!ctx.has_manager() || ctx.cs_state() != cmd_context::css_unsat) throw cmd_exception("unsat core is not available"); - PRINT_CORE(); + print_core(ctx); }); ATOMIC_CMD(get_unsat_assumptions_cmd, "get-unsat-assumptions", "retrieve subset of assumptions sufficient for unsatisfiability", { @@ -228,7 +236,7 @@ ATOMIC_CMD(get_unsat_assumptions_cmd, "get-unsat-assumptions", "retrieve subset if (!ctx.has_manager() || ctx.cs_state() != cmd_context::css_unsat) { throw cmd_exception("unsat assumptions is not available"); } - PRINT_CORE(); + print_core(ctx); }); @@ -250,9 +258,9 @@ ATOMIC_CMD(get_assertions_cmd, "get-assertions", "retrieve asserted terms when i -ATOMIC_CMD(reset_assertions_cmd, "reset-assertions", "reset all asserted formulas (but retain definitions and declarations)", ctx.reset_assertions();); +ATOMIC_CMD(reset_assertions_cmd, "reset-assertions", "reset all asserted formulas (but retain definitions and declarations)", ctx.reset_assertions(); ctx.print_success();); -UNARY_CMD(set_logic_cmd, "set-logic", "", "set the background logic.", CPK_SYMBOL, symbol const &, +UNARY_CMD(set_logic_cmd, "set-logic", "", "set the background logic.", CPK_SYMBOL, symbol const &, if (ctx.set_logic(arg)) ctx.print_success(); else { @@ -261,12 +269,14 @@ UNARY_CMD(set_logic_cmd, "set-logic", "", "set the background logic.", C } ); -UNARY_CMD(pp_cmd, "display", "", "display the given term.", CPK_EXPR, expr *, { +UNARY_CMD(pp_cmd, "display", "", "display the given term.", CPK_EXPR, expr *, { ctx.display(ctx.regular_stream(), arg); - ctx.regular_stream() << std::endl; + ctx.regular_stream() << std::endl; }); -UNARY_CMD(echo_cmd, "echo", "", "display the given string", CPK_STRING, char const *, ctx.regular_stream() << arg << std::endl;); +UNARY_CMD(echo_cmd, "echo", "", "display the given string", CPK_STRING, char const *, + bool smt2c = ctx.params().m_smtlib2_compliant; + ctx.regular_stream() << (smt2c ? "\"" : "") << arg << (smt2c ? "\"" : "") << std::endl;); class set_get_option_cmd : public cmd { @@ -297,18 +307,18 @@ protected: symbol m_reproducible_resource_limit; bool is_builtin_option(symbol const & s) const { - return - s == m_print_success || s == m_print_warning || s == m_expand_definitions || + return + s == m_print_success || s == m_print_warning || s == m_expand_definitions || s == m_interactive_mode || s == m_produce_proofs || s == m_produce_unsat_cores || s == m_produce_unsat_assumptions || s == m_produce_models || s == m_produce_assignments || s == m_produce_interpolants || - s == m_regular_output_channel || s == m_diagnostic_output_channel || + s == m_regular_output_channel || s == m_diagnostic_output_channel || s == m_random_seed || s == m_verbosity || s == m_global_decls || s == m_global_declarations || s == m_produce_assertions || s == m_reproducible_resource_limit; } public: set_get_option_cmd(char const * name): - cmd(name), + cmd(name), m_true("true"), m_false("false"), m_print_success(":print-success"), @@ -340,7 +350,7 @@ public: class set_option_cmd : public set_get_option_cmd { bool m_unsupported; symbol m_option; - + bool to_bool(symbol const & value) const { if (value != m_true && value != m_false) throw cmd_exception("invalid option value, true/false expected"); @@ -361,7 +371,7 @@ class set_option_cmd : public set_get_option_cmd { throw cmd_exception(msg); } } - + void set_param(cmd_context & ctx, char const * value) { try { gparams::set(m_option, value); @@ -458,11 +468,11 @@ public: virtual void prepare(cmd_context & ctx) { m_unsupported = false; m_option = symbol::null; } - virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { + virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return m_option == symbol::null ? CPK_KEYWORD : CPK_OPTION_VALUE; } - virtual void set_next_arg(cmd_context & ctx, symbol const & opt) { + virtual void set_next_arg(cmd_context & ctx, symbol const & opt) { if (m_option == symbol::null) { m_option = opt; } @@ -517,7 +527,7 @@ class get_option_cmd : public set_get_option_cmd { static void print_bool(cmd_context & ctx, bool b) { ctx.regular_stream() << (b ? "true" : "false") << std::endl; } - + static void print_unsigned(cmd_context & ctx, unsigned v) { ctx.regular_stream() << v << std::endl; } @@ -534,11 +544,11 @@ public: virtual char const * get_descr(cmd_context & ctx) const { return "get configuration option."; } virtual unsigned get_arity() const { return 1; } virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_KEYWORD; } - virtual void set_next_arg(cmd_context & ctx, symbol const & opt) { + virtual void set_next_arg(cmd_context & ctx, symbol const & opt) { if (opt == m_print_success) { - print_bool(ctx, ctx.print_success_enabled()); + print_bool(ctx, ctx.print_success_enabled()); } - // TODO: + // TODO: // else if (opt == m_print_warning) { // print_bool(ctx, ); // } @@ -628,7 +638,7 @@ public: virtual char const * get_descr(cmd_context & ctx) const { return "get information."; } virtual unsigned get_arity() const { return 1; } virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_KEYWORD; } - virtual void set_next_arg(cmd_context & ctx, symbol const & opt) { + virtual void set_next_arg(cmd_context & ctx, symbol const & opt) { if (opt == m_error_behavior) { if (ctx.exit_on_error()) ctx.regular_stream() << "(:error-behavior immediate-exit)" << std::endl; @@ -684,12 +694,12 @@ public: virtual char const * get_descr(cmd_context & ctx) const { return "set information."; } virtual unsigned get_arity() const { return 2; } virtual void prepare(cmd_context & ctx) { m_info = symbol::null; } - virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { - return m_info == symbol::null ? CPK_KEYWORD : CPK_OPTION_VALUE; + virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { + return m_info == symbol::null ? CPK_KEYWORD : CPK_OPTION_VALUE; } virtual void set_next_arg(cmd_context & ctx, rational const & val) {} virtual void set_next_arg(cmd_context & ctx, char const * val) {} - virtual void set_next_arg(cmd_context & ctx, symbol const & s) { + virtual void set_next_arg(cmd_context & ctx, symbol const & s) { if (m_info == symbol::null) { m_info = s; } @@ -737,7 +747,7 @@ public: virtual char const * get_descr(cmd_context & ctx) const { return "declare a new array map operator with name using the given function declaration.\n ::= \n | ( (*) )\n | ((_ +) (*) )\nThe last two cases are used to disumbiguate between declarations with the same name and/or select (indexed) builtin declarations.\nFor more details about the the array map operator, see 'Generalized and Efficient Array Decision Procedures' (FMCAD 2009).\nExample: (declare-map set-union (Int) (or (Bool Bool) Bool))\nDeclares a new function (declare-fun set-union ((Array Int Bool) (Array Int Bool)) (Array Int Bool)).\nThe instance of the map axiom for this new declaration is:\n(forall ((a1 (Array Int Bool)) (a2 (Array Int Bool)) (i Int)) (= (select (set-union a1 a2) i) (or (select a1 i) (select a2 i))))"; } virtual unsigned get_arity() const { return 3; } virtual void prepare(cmd_context & ctx) { m_name = symbol::null; m_domain.reset(); } - virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { + virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { if (m_name == symbol::null) return CPK_SYMBOL; if (m_domain.empty()) return CPK_SORT_LIST; return CPK_FUNC_DECL; @@ -748,10 +758,10 @@ public: throw cmd_exception("invalid map declaration, empty sort list"); m_domain.append(num, slist); } - virtual void set_next_arg(cmd_context & ctx, func_decl * f) { - m_f = f; - if (m_f->get_arity() == 0) - throw cmd_exception("invalid map declaration, function declaration must have arity > 0"); + virtual void set_next_arg(cmd_context & ctx, func_decl * f) { + m_f = f; + if (m_f->get_arity() == 0) + throw cmd_exception("invalid map declaration, function declaration must have arity > 0"); } virtual void reset(cmd_context & ctx) { m_array_fid = null_family_id; @@ -790,7 +800,7 @@ public: virtual char const * get_descr(cmd_context & ctx) const { return "retrieve consequences that fix values for supplied variables"; } virtual unsigned get_arity() const { return 2; } virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_EXPR_LIST; } - virtual void set_next_arg(cmd_context & ctx, unsigned num, expr * const * tlist) { + virtual void set_next_arg(cmd_context & ctx, unsigned num, expr * const * tlist) { if (m_count == 0) { m_assumptions.append(num, tlist); ++m_count; @@ -850,7 +860,7 @@ void install_basic_cmds(cmd_context & ctx) { ctx.insert(alloc(builtin_cmd, "declare-fun", " (*) ", "declare a new function/constant.")); ctx.insert(alloc(builtin_cmd, "declare-const", " ", "declare a new constant.")); ctx.insert(alloc(builtin_cmd, "declare-datatypes", "(*) (+)", "declare mutually recursive datatypes.\n ::= ( +)\n ::= ( *)\n ::= ( )\nexample: (declare-datatypes (T) ((BinTree (leaf (value T)) (node (left BinTree) (right BinTree)))))")); - ctx.insert(alloc(builtin_cmd, "check-sat-asuming", "( hprop_literali* )", "check sat assuming a collection of literals")); + ctx.insert(alloc(builtin_cmd, "check-sat-assuming", "( hprop_literali* )", "check sat assuming a collection of literals")); ctx.insert(alloc(get_unsat_assumptions_cmd)); ctx.insert(alloc(reset_assertions_cmd)); diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index d4273d42d..af16f5796 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -15,6 +15,7 @@ Author: Notes: --*/ + #include #include"tptr.h" #include"cmd_context.h" @@ -325,8 +326,8 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l): m_status(UNKNOWN), m_numeral_as_real(false), m_ignore_check(false), - m_exit_on_error(false), m_processing_pareto(false), + m_exit_on_error(false), m_manager(m), m_own_manager(m == 0), m_manager_initialized(false), diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index ed92ab909..b231e3c82 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -159,7 +159,7 @@ protected: bool m_produce_assignments; status m_status; bool m_numeral_as_real; - bool m_ignore_check; // used by the API to disable check-sat() commands when parsing SMT 2.0 files. + bool m_ignore_check; // used by the API to disable check-sat() commands when parsing SMT 2.0 files. bool m_processing_pareto; // used when re-entering check-sat for pareto front. bool m_exit_on_error; diff --git a/contrib/cmake/src/cmd_context/extra_cmds/CMakeLists.txt b/src/cmd_context/extra_cmds/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/cmd_context/extra_cmds/CMakeLists.txt rename to src/cmd_context/extra_cmds/CMakeLists.txt diff --git a/contrib/cmake/src/duality/CMakeLists.txt b/src/duality/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/duality/CMakeLists.txt rename to src/duality/CMakeLists.txt diff --git a/contrib/cmake/src/interp/CMakeLists.txt b/src/interp/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/interp/CMakeLists.txt rename to src/interp/CMakeLists.txt diff --git a/contrib/cmake/src/math/automata/CMakeLists.txt b/src/math/automata/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/math/automata/CMakeLists.txt rename to src/math/automata/CMakeLists.txt diff --git a/contrib/cmake/src/math/euclid/CMakeLists.txt b/src/math/euclid/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/math/euclid/CMakeLists.txt rename to src/math/euclid/CMakeLists.txt diff --git a/contrib/cmake/src/math/grobner/CMakeLists.txt b/src/math/grobner/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/math/grobner/CMakeLists.txt rename to src/math/grobner/CMakeLists.txt diff --git a/contrib/cmake/src/math/hilbert/CMakeLists.txt b/src/math/hilbert/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/math/hilbert/CMakeLists.txt rename to src/math/hilbert/CMakeLists.txt diff --git a/contrib/cmake/src/math/interval/CMakeLists.txt b/src/math/interval/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/math/interval/CMakeLists.txt rename to src/math/interval/CMakeLists.txt diff --git a/contrib/cmake/src/math/polynomial/CMakeLists.txt b/src/math/polynomial/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/math/polynomial/CMakeLists.txt rename to src/math/polynomial/CMakeLists.txt diff --git a/contrib/cmake/src/math/realclosure/CMakeLists.txt b/src/math/realclosure/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/math/realclosure/CMakeLists.txt rename to src/math/realclosure/CMakeLists.txt diff --git a/contrib/cmake/src/math/simplex/CMakeLists.txt b/src/math/simplex/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/math/simplex/CMakeLists.txt rename to src/math/simplex/CMakeLists.txt diff --git a/contrib/cmake/src/math/subpaving/CMakeLists.txt b/src/math/subpaving/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/math/subpaving/CMakeLists.txt rename to src/math/subpaving/CMakeLists.txt diff --git a/contrib/cmake/src/math/subpaving/tactic/CMakeLists.txt b/src/math/subpaving/tactic/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/math/subpaving/tactic/CMakeLists.txt rename to src/math/subpaving/tactic/CMakeLists.txt diff --git a/contrib/cmake/src/model/CMakeLists.txt b/src/model/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/model/CMakeLists.txt rename to src/model/CMakeLists.txt diff --git a/contrib/cmake/src/muz/base/CMakeLists.txt b/src/muz/base/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/muz/base/CMakeLists.txt rename to src/muz/base/CMakeLists.txt diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp index ffb964f47..27d62538e 100644 --- a/src/muz/base/dl_rule.cpp +++ b/src/muz/base/dl_rule.cpp @@ -784,7 +784,7 @@ namespace datalog { SASSERT(tail.size()==tail_neg.size()); rule_ref old_r = r; - r = mk(head, tail.size(), tail.c_ptr(), tail_neg.c_ptr()); + r = mk(head, tail.size(), tail.c_ptr(), tail_neg.c_ptr(), old_r->name()); r->set_accounting_parent_object(m_ctx, old_r); } @@ -1003,6 +1003,7 @@ namespace datalog { void rule::display(context & ctx, std::ostream & out) const { ast_manager & m = ctx.get_manager(); + out << m_name.str () << ":\n"; //out << mk_pp(m_head, m); output_predicate(ctx, m_head, out); if (m_tail_size == 0) { diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h index f7dc18b5e..856814531 100644 --- a/src/muz/base/dl_rule.h +++ b/src/muz/base/dl_rule.h @@ -298,7 +298,7 @@ namespace datalog { static unsigned get_obj_size(unsigned n) { return sizeof(rule) + n * sizeof(app *); } - rule() : m_ref_cnt(0) {} + rule() : m_ref_cnt(0), m_name(symbol::null) {} ~rule() {} void deallocate(ast_manager & m); @@ -355,7 +355,12 @@ namespace datalog { void display(context & ctx, std::ostream & out) const; - symbol const& name() const { return m_name; } + /** + \brief Return the name(s) associated with this rule. Plural for preprocessed (e.g. obtained by inlining) rules. + + This possibly returns a ";"-separated list of names. + */ + symbol const& name() const { return m_name; } ; unsigned hash() const; diff --git a/contrib/cmake/src/muz/bmc/CMakeLists.txt b/src/muz/bmc/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/muz/bmc/CMakeLists.txt rename to src/muz/bmc/CMakeLists.txt diff --git a/contrib/cmake/src/muz/clp/CMakeLists.txt b/src/muz/clp/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/muz/clp/CMakeLists.txt rename to src/muz/clp/CMakeLists.txt diff --git a/contrib/cmake/src/muz/dataflow/CMakeLists.txt b/src/muz/dataflow/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/muz/dataflow/CMakeLists.txt rename to src/muz/dataflow/CMakeLists.txt diff --git a/contrib/cmake/src/muz/ddnf/CMakeLists.txt b/src/muz/ddnf/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/muz/ddnf/CMakeLists.txt rename to src/muz/ddnf/CMakeLists.txt diff --git a/contrib/cmake/src/muz/duality/CMakeLists.txt b/src/muz/duality/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/muz/duality/CMakeLists.txt rename to src/muz/duality/CMakeLists.txt diff --git a/contrib/cmake/src/muz/fp/CMakeLists.txt b/src/muz/fp/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/muz/fp/CMakeLists.txt rename to src/muz/fp/CMakeLists.txt diff --git a/contrib/cmake/src/muz/pdr/CMakeLists.txt b/src/muz/pdr/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/muz/pdr/CMakeLists.txt rename to src/muz/pdr/CMakeLists.txt diff --git a/contrib/cmake/src/muz/rel/CMakeLists.txt b/src/muz/rel/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/muz/rel/CMakeLists.txt rename to src/muz/rel/CMakeLists.txt diff --git a/contrib/cmake/src/muz/tab/CMakeLists.txt b/src/muz/tab/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/muz/tab/CMakeLists.txt rename to src/muz/tab/CMakeLists.txt diff --git a/contrib/cmake/src/muz/transforms/CMakeLists.txt b/src/muz/transforms/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/muz/transforms/CMakeLists.txt rename to src/muz/transforms/CMakeLists.txt diff --git a/src/muz/transforms/dl_mk_filter_rules.cpp b/src/muz/transforms/dl_mk_filter_rules.cpp index b112f4c99..0d118a589 100644 --- a/src/muz/transforms/dl_mk_filter_rules.cpp +++ b/src/muz/transforms/dl_mk_filter_rules.cpp @@ -140,7 +140,7 @@ namespace datalog { if (rule_modified) { remove_duplicate_tails(new_tail, new_is_negated); SASSERT(new_tail.size() == new_is_negated.size()); - rule * new_rule = m_context.get_rule_manager().mk(new_head, new_tail.size(), new_tail.c_ptr(), new_is_negated.c_ptr()); + rule * new_rule = m_context.get_rule_manager().mk(new_head, new_tail.size(), new_tail.c_ptr(), new_is_negated.c_ptr(), r->name()); new_rule->set_accounting_parent_object(m_context, m_current); m_result->add_rule(new_rule); m_context.get_rule_manager().mk_rule_rewrite_proof(*r, *new_rule); diff --git a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp index 455b06d3d..3c1d1b924 100644 --- a/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp +++ b/src/muz/transforms/dl_mk_interp_tail_simplifier.cpp @@ -84,7 +84,7 @@ namespace datalog { mk_rule_inliner::remove_duplicate_tails(m_tail, m_neg); SASSERT(m_tail.size() == m_neg.size()); - res = m_context.get_rule_manager().mk(m_head, m_tail.size(), m_tail.c_ptr(), m_neg.c_ptr()); + res = m_context.get_rule_manager().mk(m_head, m_tail.size(), m_tail.c_ptr(), m_neg.c_ptr(),m_rule->name()); res->set_accounting_parent_object(m_context, m_rule); res->norm_vars(res.get_manager()); } @@ -557,7 +557,7 @@ namespace datalog { } SASSERT(m_tail.size() == m_tail_neg.size()); - res = m_context.get_rule_manager().mk(head, m_tail.size(), m_tail.c_ptr(), m_tail_neg.c_ptr()); + res = m_context.get_rule_manager().mk(head, m_tail.size(), m_tail.c_ptr(), m_tail_neg.c_ptr(), r->name()); res->set_accounting_parent_object(m_context, r); } else { diff --git a/src/muz/transforms/dl_mk_magic_sets.cpp b/src/muz/transforms/dl_mk_magic_sets.cpp index 048decaf9..19dccf417 100644 --- a/src/muz/transforms/dl_mk_magic_sets.cpp +++ b/src/muz/transforms/dl_mk_magic_sets.cpp @@ -280,7 +280,7 @@ namespace datalog { new_tail.push_back(create_magic_literal(new_head)); negations.push_back(false); - rule * nr = m_context.get_rule_manager().mk(new_head, new_tail.size(), new_tail.c_ptr(), negations.c_ptr()); + rule * nr = m_context.get_rule_manager().mk(new_head, new_tail.size(), new_tail.c_ptr(), negations.c_ptr(), r->name()); result.add_rule(nr); nr->set_accounting_parent_object(m_context, r); } diff --git a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp index caff79d2e..5c0d442df 100644 --- a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp +++ b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp @@ -341,7 +341,7 @@ namespace datalog { head = mk_head(source, *result, r.get_head(), cnt); fml = m.mk_implies(m.mk_and(tail.size(), tail.c_ptr()), head); proof_ref pr(m); - rm.mk_rule(fml, pr, *result); + rm.mk_rule(fml, pr, *result, r.name()); TRACE("dl", result->last()->display(m_ctx, tout);); } diff --git a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp index 5d36d26cc..586c52cd6 100644 --- a/src/muz/transforms/dl_mk_quantifier_instantiation.cpp +++ b/src/muz/transforms/dl_mk_quantifier_instantiation.cpp @@ -232,7 +232,7 @@ namespace datalog { rule_set added_rules(m_ctx); proof_ref pr(m); - rm.mk_rule(fml, pr, added_rules); + rm.mk_rule(fml, pr, added_rules, r.name()); if (r.get_proof()) { // use def-axiom to encode that new rule is a weakening of the original. proof* p1 = r.get_proof(); diff --git a/src/muz/transforms/dl_mk_rule_inliner.cpp b/src/muz/transforms/dl_mk_rule_inliner.cpp index 7dabece2f..c6b3e8be7 100644 --- a/src/muz/transforms/dl_mk_rule_inliner.cpp +++ b/src/muz/transforms/dl_mk_rule_inliner.cpp @@ -114,7 +114,10 @@ namespace datalog { apply(src, false, UINT_MAX, tail, tail_neg); mk_rule_inliner::remove_duplicate_tails(tail, tail_neg); SASSERT(tail.size()==tail_neg.size()); - res = m_rm.mk(new_head, tail.size(), tail.c_ptr(), tail_neg.c_ptr(), tgt.name(), m_normalize); + std::ostringstream comb_name; + comb_name << tgt.name().str() << ";" << src.name().str(); + symbol combined_rule_name = symbol(comb_name.str().c_str()); + res = m_rm.mk(new_head, tail.size(), tail.c_ptr(), tail_neg.c_ptr(), combined_rule_name, m_normalize); res->set_accounting_parent_object(m_context, const_cast(&tgt)); TRACE("dl", tgt.display(m_context, tout << "tgt (" << tail_index << "): \n"); diff --git a/src/muz/transforms/dl_mk_slice.cpp b/src/muz/transforms/dl_mk_slice.cpp index 2f7d0d475..aa910002d 100644 --- a/src/muz/transforms/dl_mk_slice.cpp +++ b/src/muz/transforms/dl_mk_slice.cpp @@ -22,7 +22,7 @@ Revision History: input: x, z output: x, y - Let x_i, y_i, z_i be incides into the vectors x, y, z. + Let x_i, y_i, z_i be indices into the vectors x, y, z. Suppose that positions in P and R are annotated with what is slicable. diff --git a/src/muz/transforms/dl_mk_subsumption_checker.cpp b/src/muz/transforms/dl_mk_subsumption_checker.cpp index 1967fdc93..8fae4ee35 100644 --- a/src/muz/transforms/dl_mk_subsumption_checker.cpp +++ b/src/muz/transforms/dl_mk_subsumption_checker.cpp @@ -159,7 +159,7 @@ namespace datalog { } SASSERT(tail.size()==tail_neg.size()); - res = m_context.get_rule_manager().mk(head, tail.size(), tail.c_ptr(), tail_neg.c_ptr()); + res = m_context.get_rule_manager().mk(head, tail.size(), tail.c_ptr(), tail_neg.c_ptr(), r->name()); res->set_accounting_parent_object(m_context, r); m_context.get_rule_manager().fix_unbound_vars(res, true); m_context.get_rule_manager().mk_rule_rewrite_proof(*r, *res.get()); diff --git a/contrib/cmake/src/nlsat/CMakeLists.txt b/src/nlsat/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/nlsat/CMakeLists.txt rename to src/nlsat/CMakeLists.txt diff --git a/contrib/cmake/src/nlsat/tactic/CMakeLists.txt b/src/nlsat/tactic/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/nlsat/tactic/CMakeLists.txt rename to src/nlsat/tactic/CMakeLists.txt diff --git a/contrib/cmake/src/opt/CMakeLists.txt b/src/opt/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/opt/CMakeLists.txt rename to src/opt/CMakeLists.txt diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp index 571c26e2d..a5c163562 100644 --- a/src/opt/opt_cmds.cpp +++ b/src/opt/opt_cmds.cpp @@ -100,6 +100,7 @@ public: rational weight = ps().get_rat(symbol("weight"), rational::one()); symbol id = ps().get_sym(symbol("id"), symbol::null); get_opt(ctx, m_opt).add_soft_constraint(m_formula, weight, id); + ctx.print_success(); reset(ctx); } @@ -131,6 +132,7 @@ public: throw cmd_exception("malformed objective term: it cannot be a quantifier or bound variable"); } get_opt(ctx, m_opt).add_objective(to_app(t), m_is_max); + ctx.print_success(); } virtual void failure_cleanup(cmd_context & ctx) { diff --git a/contrib/cmake/src/parsers/smt/CMakeLists.txt b/src/parsers/smt/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/parsers/smt/CMakeLists.txt rename to src/parsers/smt/CMakeLists.txt diff --git a/contrib/cmake/src/parsers/smt2/CMakeLists.txt b/src/parsers/smt2/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/parsers/smt2/CMakeLists.txt rename to src/parsers/smt2/CMakeLists.txt diff --git a/src/parsers/smt2/smt2scanner.cpp b/src/parsers/smt2/smt2scanner.cpp index fb2f9f34a..1763a4fa5 100644 --- a/src/parsers/smt2/smt2scanner.cpp +++ b/src/parsers/smt2/smt2scanner.cpp @@ -23,7 +23,7 @@ namespace smt2 { void scanner::next() { if (m_cache_input) - m_cache.push_back(m_curr); + m_cache.push_back(m_curr); SASSERT(!m_at_eof); if (m_interactive) { m_curr = m_stream.get(); @@ -293,11 +293,11 @@ namespace smt2 { } scanner::token scanner::scan() { - while (true) { + while (true) { signed char c = curr(); m_pos = m_spos; - if (m_at_eof) + if (m_at_eof) return EOF_TOKEN; switch (m_normalized[(unsigned char) c]) { diff --git a/contrib/cmake/src/parsers/util/CMakeLists.txt b/src/parsers/util/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/parsers/util/CMakeLists.txt rename to src/parsers/util/CMakeLists.txt diff --git a/contrib/cmake/src/qe/CMakeLists.txt b/src/qe/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/qe/CMakeLists.txt rename to src/qe/CMakeLists.txt diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index eccc2d0c7..ce182a97b 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -36,44 +36,7 @@ Revision History: #include "cooperate.h" #include "datatype_decl_plugin.h" -class is_variable_proc { -public: - virtual bool operator()(expr* e) const = 0; -}; - -class is_variable_test : public is_variable_proc { - enum is_var_kind { BY_VAR_SET, BY_VAR_SET_COMPLEMENT, BY_NUM_DECLS }; - uint_set m_var_set; - unsigned m_num_decls; - is_var_kind m_var_kind; -public: - is_variable_test(uint_set const& vars, bool index_of_bound) : - m_var_set(vars), - m_num_decls(0), - m_var_kind(index_of_bound?BY_VAR_SET:BY_VAR_SET_COMPLEMENT) {} - - is_variable_test(unsigned num_decls) : - m_num_decls(num_decls), - m_var_kind(BY_NUM_DECLS) {} - - virtual bool operator()(expr* e) const { - if (!is_var(e)) { - return false; - } - unsigned idx = to_var(e)->get_idx(); - switch(m_var_kind) { - case BY_VAR_SET: - return m_var_set.contains(idx); - case BY_VAR_SET_COMPLEMENT: - return !m_var_set.contains(idx); - case BY_NUM_DECLS: - return idx < m_num_decls; - } - UNREACHABLE(); - return false; - } -}; - +#include "qe_vartest.h" namespace eq { class der { @@ -86,6 +49,7 @@ namespace eq { ptr_vector m_map; int_vector m_pos2var; + int_vector m_var2pos; ptr_vector m_inx2var; unsigned_vector m_order; expr_ref_vector m_subst_map; @@ -578,6 +542,7 @@ namespace eq { largest_vinx = 0; m_map.reset(); m_pos2var.reset(); + m_var2pos.reset(); m_inx2var.reset(); m_pos2var.reserve(num_args, -1); @@ -597,10 +562,48 @@ namespace eq { m_map[idx] = t; m_inx2var[idx] = v; m_pos2var[i] = idx; + m_var2pos.reserve(idx + 1, -1); + m_var2pos[idx] = i; def_count++; largest_vinx = std::max(idx, largest_vinx); m_new_exprs.push_back(t); } + else if (!m.is_value(m_map[idx])) { + // check if the new definition is simpler + expr *old_def = m_map[idx]; + + // -- prefer values + if (m.is_value(t)) { + m_pos2var[m_var2pos[idx]] = -1; + m_pos2var[i] = idx; + m_var2pos[idx] = i; + m_map[idx] = t; + m_new_exprs.push_back(t); + } + // -- prefer ground + else if (is_app(t) && to_app(t)->is_ground() && + (!is_app(old_def) || + !to_app(old_def)->is_ground())) { + m_pos2var[m_var2pos[idx]] = -1; + m_pos2var[i] = idx; + m_var2pos[idx] = i; + m_map[idx] = t; + m_new_exprs.push_back(t); + } + // -- prefer constants + else if (is_uninterp_const(t) + /* && !is_uninterp_const(old_def) */){ + m_pos2var[m_var2pos[idx]] = -1; + m_pos2var[i] = idx; + m_var2pos[idx] = i; + m_map[idx] = t; + m_new_exprs.push_back(t); + } + TRACE ("qe_def", + tout << "Replacing definition of VAR " << idx << " from " + << mk_pp(old_def, m) << " to " << mk_pp(t, m) + << " inferred from: " << mk_pp(args[i], m) << "\n";); + } } } } @@ -825,12 +828,13 @@ namespace ar { } /** - Ex A. A[x] = t & Phi where x \not\in A, t. A \not\in t, x + Ex A. A[x] = t & Phi[A] where x \not\in A, t. A \not\in t, x => Ex A. Phi[store(A,x,t)] + (Not implemented) Perhaps also: - Ex A. store(A,y,z)[x] = t & Phi where x \not\in A, t, y, z, A \not\in y z, t + Ex A. store(A,y,z)[x] = t & Phi[A] where x \not\in A, t, y, z, A \not\in y z, t => Ex A, v . (x = y => z = t) & Phi[store(store(A,x,t),y,v)] @@ -859,7 +863,8 @@ namespace ar { expr_safe_replace rep(m); rep.insert(A, B); expr_ref tmp(m); - std::cout << mk_pp(e1, m) << " = " << mk_pp(e2, m) << "\n"; + TRACE("qe_lite", + tout << mk_pp(e1, m) << " = " << mk_pp(e2, m) << "\n";); for (unsigned j = 0; j < conjs.size(); ++j) { if (i == j) { conjs[j] = m.mk_true(); @@ -1491,8 +1496,10 @@ namespace fm { unsigned sz = g.size(); for (unsigned i = 0; i < sz; i++) { expr * f = g[i]; - if (is_occ(f)) + if (is_occ(f)) { + TRACE("qe_lite", tout << "OCC: " << mk_ismt2_pp(f, m) << "\n";); continue; + } TRACE("qe_lite", tout << "not OCC:\n" << mk_ismt2_pp(f, m) << "\n";); quick_for_each_expr(proc, visited, f); } @@ -2221,6 +2228,9 @@ namespace fm { void operator()(expr_ref_vector& fmls) { init(fmls); init_use_list(fmls); + for (auto & f : fmls) { + if (has_quantifiers(f)) return; + } if (m_inconsistent) { m_new_fmls.reset(); m_new_fmls.push_back(m.mk_false()); diff --git a/src/qe/qe_vartest.h b/src/qe/qe_vartest.h new file mode 100644 index 000000000..b2b4be649 --- /dev/null +++ b/src/qe/qe_vartest.h @@ -0,0 +1,63 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + qe_vartest.h + +Abstract: + + Utilities for quantifiers. + +Author: + + Nikolaj Bjorner (nbjorner) 2013-08-28 + +Revision History: + +--*/ +#ifndef QE_VARTEST_H_ +#define QE_VARTEST_H_ + +#include "ast.h" +#include "uint_set.h" + +class is_variable_proc { +public: + virtual bool operator()(expr* e) const = 0; +}; + +class is_variable_test : public is_variable_proc { + enum is_var_kind { BY_VAR_SET, BY_VAR_SET_COMPLEMENT, BY_NUM_DECLS }; + uint_set m_var_set; + unsigned m_num_decls; + is_var_kind m_var_kind; +public: + is_variable_test(uint_set const& vars, bool index_of_bound) : + m_var_set(vars), + m_num_decls(0), + m_var_kind(index_of_bound?BY_VAR_SET:BY_VAR_SET_COMPLEMENT) {} + + is_variable_test(unsigned num_decls) : + m_num_decls(num_decls), + m_var_kind(BY_NUM_DECLS) {} + + virtual bool operator()(expr* e) const { + if (!is_var(e)) { + return false; + } + unsigned idx = to_var(e)->get_idx(); + switch(m_var_kind) { + case BY_VAR_SET: + return m_var_set.contains(idx); + case BY_VAR_SET_COMPLEMENT: + return !m_var_set.contains(idx); + case BY_NUM_DECLS: + return idx < m_num_decls; + } + UNREACHABLE(); + return false; + } +}; + +#endif diff --git a/contrib/cmake/src/sat/CMakeLists.txt b/src/sat/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/sat/CMakeLists.txt rename to src/sat/CMakeLists.txt diff --git a/contrib/cmake/src/sat/sat_solver/CMakeLists.txt b/src/sat/sat_solver/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/sat/sat_solver/CMakeLists.txt rename to src/sat/sat_solver/CMakeLists.txt diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 4a4e0af38..b6904ef02 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -326,7 +326,6 @@ public: return l_true; } - virtual std::string reason_unknown() const { return m_unknown; } @@ -598,16 +597,14 @@ private: extract_asm2dep(dep2asm, asm2dep); sat::literal_vector const& core = m_solver.get_core(); TRACE("sat", - dep2asm_t::iterator it2 = dep2asm.begin(); - dep2asm_t::iterator end2 = dep2asm.end(); - for (; it2 != end2; ++it2) { - tout << mk_pp(it2->m_key, m) << " |-> " << sat::literal(it2->m_value) << "\n"; + for (auto kv : dep2asm) { + tout << mk_pp(kv.m_key, m) << " |-> " << sat::literal(kv.m_value) << "\n"; } - tout << "core: "; - for (unsigned i = 0; i < core.size(); ++i) { - tout << core[i] << " "; + tout << "asm2fml: "; + for (auto kv : asm2fml) { + tout << mk_pp(kv.m_key, m) << " |-> " << mk_pp(kv.m_value, m) << "\n"; } - tout << "\n"; + tout << "core: "; for (auto c : core) tout << c << " "; tout << "\n"; ); m_core.reset(); diff --git a/contrib/cmake/src/sat/tactic/CMakeLists.txt b/src/sat/tactic/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/sat/tactic/CMakeLists.txt rename to src/sat/tactic/CMakeLists.txt diff --git a/contrib/cmake/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/shell/CMakeLists.txt rename to src/shell/CMakeLists.txt diff --git a/contrib/cmake/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/smt/CMakeLists.txt rename to src/smt/CMakeLists.txt diff --git a/contrib/cmake/src/smt/params/CMakeLists.txt b/src/smt/params/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/smt/params/CMakeLists.txt rename to src/smt/params/CMakeLists.txt diff --git a/contrib/cmake/src/smt/proto_model/CMakeLists.txt b/src/smt/proto_model/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/smt/proto_model/CMakeLists.txt rename to src/smt/proto_model/CMakeLists.txt diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index 8d90f9583..ade667e34 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -1405,6 +1405,7 @@ namespace smt { switch (js.get_kind()) { case b_justification::CLAUSE: { clause * cls = js.get_clause(); + TRACE("unsat_core_bug", m_ctx.display_clause_detail(tout, cls);); unsigned num_lits = cls->get_num_literals(); unsigned i = 0; if (consequent != false_literal) { @@ -1422,8 +1423,9 @@ namespace smt { process_antecedent_for_unsat_core(~l); } justification * js = cls->get_justification(); - if (js) + if (js) { process_justification_for_unsat_core(js); + } break; } case b_justification::BIN_CLAUSE: diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index f7936eacd..5fbdb2477 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -1034,8 +1034,10 @@ namespace smt { lbool val = get_assignment(curr); switch(val) { case l_false: + TRACE("simplify_aux_clause_literals", display_literal(tout << get_assign_level(curr) << " " << get_scope_level() << " ", curr); tout << "\n"; ); simp_lits.push_back(~curr); - break; // ignore literal + break; // ignore literal + // fall through case l_undef: if (curr == ~prev) return false; // clause is equivalent to true diff --git a/contrib/cmake/src/smt/tactic/CMakeLists.txt b/src/smt/tactic/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/smt/tactic/CMakeLists.txt rename to src/smt/tactic/CMakeLists.txt diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 54b617152..f94de7eba 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -1458,7 +1458,7 @@ namespace smt { normalize_gain(min_gain.get_rational(), max_gain); } - if (is_int(x_i) && !max_gain.is_rational()) { + if (is_int(x_i) && !max_gain.is_int()) { max_gain = inf_numeral(floor(max_gain)); normalize_gain(min_gain.get_rational(), max_gain); } @@ -1483,7 +1483,7 @@ namespace smt { } } TRACE("opt", - tout << "v" << x_i << " a_ij " << a_ij << " " + tout << "v" << x_i << (is_int(x_i)?" int":" real") << " a_ij " << a_ij << " " << "min gain: " << min_gain << " " << "max gain: " << max_gain << " tighter: " << (is_tighter?"true":"false") << "\n";); @@ -1696,6 +1696,7 @@ namespace smt { if (lower(x_j)) tout << "lower x_j: " << lower_bound(x_j) << " "; tout << "value x_j: " << get_value(x_j) << "\n"; ); + pivot(x_i, x_j, a_ij, false); SASSERT(is_non_base(x_i)); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 3f8845546..4dfff21c2 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2176,8 +2176,67 @@ bool theory_seq::simplify_and_solve_eqs() { return m_new_propagation || ctx.inconsistent(); } -void theory_seq::internalize_eq_eh(app * atom, bool_var v) {} +void theory_seq::internalize_eq_eh(app * atom, bool_var v) { +} +bool theory_seq::internalize_atom(app* a, bool) { +#if 1 + return internalize_term(a); +#else + if (is_skolem(m_eq, a)) { + return internalize_term(a); + } + context & ctx = get_context(); + bool_var bv = ctx.mk_bool_var(a); + ctx.set_var_theory(bv, get_id()); + ctx.mark_as_relevant(bv); + + expr* e1, *e2; + if (m_util.str.is_in_re(a, e1, e2)) { + return internalize_term(to_app(e1)) && internalize_re(e2); + } + if (m_util.str.is_contains(a, e1, e2) || + m_util.str.is_prefix(a, e1, e2) || + m_util.str.is_suffix(a, e1, e2)) { + return internalize_term(to_app(e1)) && internalize_term(to_app(e2)); + } + if (is_accept(a) || is_reject(a) || is_step(a) || is_skolem(symbol("seq.is_digit"), a)) { + return true; + } + UNREACHABLE(); + return internalize_term(a); +#endif +} + +bool theory_seq::internalize_re(expr* e) { + expr* e1, *e2; + unsigned lc, uc; + if (m_util.re.is_to_re(e, e1)) { + return internalize_term(to_app(e1)); + } + if (m_util.re.is_star(e, e1) || + m_util.re.is_plus(e, e1) || + m_util.re.is_opt(e, e1) || + m_util.re.is_loop(e, e1, lc) || + m_util.re.is_loop(e, e1, lc, uc) || + m_util.re.is_complement(e, e1)) { + return internalize_re(e1); + } + if (m_util.re.is_union(e, e1, e2) || + m_util.re.is_intersection(e, e1, e2) || + m_util.re.is_concat(e, e1, e2)) { + return internalize_re(e1) && internalize_re(e2); + } + if (m_util.re.is_full(e) || + m_util.re.is_empty(e)) { + return true; + } + if (m_util.re.is_range(e, e1, e2)) { + return internalize_term(to_app(e1)) && internalize_term(to_app(e2)); + } + UNREACHABLE(); + return internalize_term(to_app(e)); +} bool theory_seq::internalize_term(app* term) { context & ctx = get_context(); @@ -2962,6 +3021,7 @@ void theory_seq::deque_axiom(expr* n) { add_length_axiom(n); } else if (m_util.str.is_empty(n) && !has_length(n) && !m_length.empty()) { + ensure_enode(n); enforce_length(get_context().get_enode(n)); } else if (m_util.str.is_index(n)) { @@ -3567,8 +3627,8 @@ void theory_seq::add_at_axiom(expr* e) { add_axiom(~i_ge_0, i_ge_len_s, mk_eq(one, len_e, false)); add_axiom(~i_ge_0, i_ge_len_s, mk_eq(i, len_x, false)); - add_axiom(i_ge_0, mk_eq(s, emp, false)); - add_axiom(~i_ge_len_s, mk_eq(s, emp, false)); + add_axiom(i_ge_0, mk_eq(e, emp, false)); + add_axiom(~i_ge_len_s, mk_eq(e, emp, false)); } /** @@ -3875,7 +3935,7 @@ void theory_seq::new_eq_eh(dependency* deps, enode* n1, enode* n2) { enforce_length_coherence(n1, n2); } else if (n1 != n2 && m_util.is_re(n1->get_owner())) { - warning_msg("equality between regular expressions is not yet supported"); + // ignore // eautomaton* a1 = get_automaton(n1->get_owner()); // eautomaton* a2 = get_automaton(n2->get_owner()); // eautomaton* b1 = mk_difference(*a1, *a2); @@ -3995,7 +4055,7 @@ void theory_seq::relevant_eh(app* n) { } expr* arg; - if (m_util.str.is_length(n, arg) && !has_length(arg)) { + if (m_util.str.is_length(n, arg) && !has_length(arg) && get_context().e_internalized(arg)) { enforce_length(get_context().get_enode(arg)); } } diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index e145d3077..5fd31e2ca 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -341,8 +341,8 @@ namespace smt { virtual void init(context* ctx); virtual final_check_status final_check_eh(); - virtual bool internalize_atom(app* atom, bool) { return internalize_term(atom); } - virtual bool internalize_term(app*); + virtual bool internalize_atom(app* atom, bool); + virtual bool internalize_term(app*); virtual void internalize_eq_eh(app * atom, bool_var v); virtual void new_eq_eh(theory_var, theory_var); virtual void new_diseq_eh(theory_var, theory_var); @@ -387,6 +387,7 @@ namespace smt { vector const& ll, vector const& rl); bool set_empty(expr* x); bool is_complex(eq const& e); + bool internalize_re(expr* e); bool check_extensionality(); bool check_contains(); diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index f9b463b30..523e087f2 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -25,6 +25,7 @@ #include #include"theory_seq_empty.h" #include"theory_arith.h" +#include"ast_util.h" namespace smt { @@ -98,7 +99,7 @@ namespace smt { if (defaultCharset) { // valid C strings can't contain the null byte ('\0') charSetSize = 255; - char_set = alloc_svect(char, charSetSize); + char_set.resize(256, 0); int idx = 0; // small letters for (int i = 97; i < 123; i++) { @@ -157,8 +158,7 @@ namespace smt { } else { const char setset[] = { 'a', 'b', 'c' }; int fSize = sizeof(setset) / sizeof(char); - - char_set = alloc_svect(char, fSize); + char_set.resize(fSize, 0); charSetSize = fSize; for (int i = 0; i < charSetSize; i++) { char_set[i] = setset[i]; @@ -6927,9 +6927,9 @@ namespace smt { ast_manager & m = get_manager(); if (lenTester_fvar_map.contains(lenTester)) { expr * fVar = lenTester_fvar_map[lenTester]; - expr * toAssert = gen_len_val_options_for_free_var(fVar, lenTester, lenTesterValue); + expr_ref toAssert(gen_len_val_options_for_free_var(fVar, lenTester, lenTesterValue), m); TRACE("str", tout << "asserting more length tests for free variable " << mk_ismt2_pp(fVar, m) << std::endl;); - if (toAssert != NULL) { + if (toAssert) { assert_axiom(toAssert); } } @@ -9123,7 +9123,7 @@ namespace smt { zstring theory_str::gen_val_string(int len, int_vector & encoding) { SASSERT(charSetSize > 0); - SASSERT(char_set != NULL); + SASSERT(!char_set.empty()); std::string re(len, char_set[0]); for (int i = 0; i < (int) encoding.size() - 1; i++) { @@ -9173,7 +9173,7 @@ namespace smt { } } - expr * theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr * val_indicator, + expr* theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr * val_indicator, zstring lenStr, int tries) { ast_manager & m = get_manager(); context & ctx = get_context(); @@ -9194,7 +9194,7 @@ namespace smt { // ---------------------------------------------------------------------------------------- int len = atoi(lenStr.encode().c_str()); bool coverAll = false; - vector options; + vector options; int_vector base; TRACE("str", tout @@ -9240,8 +9240,7 @@ namespace smt { // ---------------------------------------------------------------------------------------- - ptr_vector orList; - ptr_vector andList; + expr_ref_vector orList(m), andList(m); for (long long i = l; i < h; i++) { orList.push_back(m.mk_eq(val_indicator, mk_string(longlong_to_string(i).c_str()) )); @@ -9262,7 +9261,7 @@ namespace smt { } else { strAst = mk_string(aStr); } - andList.push_back(m.mk_eq(orList[orList.size() - 1], m.mk_eq(freeVar, strAst))); + andList.push_back(m.mk_eq(orList[orList.size() - 1].get(), m.mk_eq(freeVar, strAst))); } if (!coverAll) { orList.push_back(m.mk_eq(val_indicator, mk_string("more"))); @@ -9273,21 +9272,8 @@ namespace smt { } } - expr ** or_items = alloc_svect(expr*, orList.size()); - expr ** and_items = alloc_svect(expr*, andList.size() + 1); - - for (int i = 0; i < (int) orList.size(); i++) { - or_items[i] = orList[i]; - } - if (orList.size() > 1) - and_items[0] = m.mk_or(orList.size(), or_items); - else - and_items[0] = or_items[0]; - - for (int i = 0; i < (int) andList.size(); i++) { - and_items[i + 1] = andList[i]; - } - expr * valTestAssert = m.mk_and(andList.size() + 1, and_items); + andList.push_back(mk_or(orList)); + expr_ref valTestAssert = mk_and(andList); // --------------------------------------- // If the new value tester is $$_val_x_16_i @@ -9300,20 +9286,9 @@ namespace smt { if (vTester != val_indicator) andList.push_back(m.mk_eq(vTester, mk_string("more"))); } - expr * assertL = NULL; - if (andList.size() == 1) { - assertL = andList[0]; - } else { - expr ** and_items = alloc_svect(expr*, andList.size()); - for (int i = 0; i < (int) andList.size(); i++) { - and_items[i] = andList[i]; - } - assertL = m.mk_and(andList.size(), and_items); - } - + expr_ref assertL = mk_and(andList); // (assertL => valTestAssert) <=> (!assertL OR valTestAssert) - valTestAssert = m.mk_or(m.mk_not(assertL), valTestAssert); - return valTestAssert; + return m.mk_or(m.mk_not(assertL), valTestAssert); } expr * theory_str::gen_free_var_options(expr * freeVar, expr * len_indicator, @@ -9378,7 +9353,7 @@ namespace smt { << " doesn't have an equivalence class value." << std::endl;); refresh_theory_var(aTester); - expr * makeupAssert = gen_val_options(freeVar, len_indicator, aTester, len_valueStr, i); + expr_ref makeupAssert(gen_val_options(freeVar, len_indicator, aTester, len_valueStr, i), m); TRACE("str", tout << "var: " << mk_ismt2_pp(freeVar, m) << std::endl << mk_ismt2_pp(makeupAssert, m) << std::endl;); @@ -9400,8 +9375,7 @@ namespace smt { fvar_valueTester_map[freeVar][len].push_back(std::make_pair(sLevel, valTester)); print_value_tester_list(fvar_valueTester_map[freeVar][len]); } - expr * nextAssert = gen_val_options(freeVar, len_indicator, valTester, len_valueStr, i + 1); - return nextAssert; + return gen_val_options(freeVar, len_indicator, valTester, len_valueStr, i + 1); } return NULL; diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 4752e8a1b..0bbc44ab8 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -330,9 +330,9 @@ protected: std::map regex_nfa_cache; // Regex term --> NFA - char * char_set; - std::map charSetLookupTable; - int charSetSize; + svector char_set; + std::map charSetLookupTable; + int charSetSize; obj_pair_map concat_astNode_map; @@ -553,7 +553,7 @@ protected: expr * gen_len_test_options(expr * freeVar, expr * indicator, int tries); expr * gen_free_var_options(expr * freeVar, expr * len_indicator, zstring len_valueStr, expr * valTesterInCbEq, zstring valTesterValueStr); - expr * gen_val_options(expr * freeVar, expr * len_indicator, expr * val_indicator, + expr* gen_val_options(expr * freeVar, expr * len_indicator, expr * val_indicator, zstring lenStr, int tries); void print_value_tester_list(svector > & testerList); bool get_next_val_encode(int_vector & base, int_vector & next); diff --git a/contrib/cmake/src/solver/CMakeLists.txt b/src/solver/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/solver/CMakeLists.txt rename to src/solver/CMakeLists.txt diff --git a/contrib/cmake/src/tactic/CMakeLists.txt b/src/tactic/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/tactic/CMakeLists.txt rename to src/tactic/CMakeLists.txt diff --git a/contrib/cmake/src/tactic/aig/CMakeLists.txt b/src/tactic/aig/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/tactic/aig/CMakeLists.txt rename to src/tactic/aig/CMakeLists.txt diff --git a/contrib/cmake/src/tactic/arith/CMakeLists.txt b/src/tactic/arith/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/tactic/arith/CMakeLists.txt rename to src/tactic/arith/CMakeLists.txt diff --git a/contrib/cmake/src/tactic/bv/CMakeLists.txt b/src/tactic/bv/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/tactic/bv/CMakeLists.txt rename to src/tactic/bv/CMakeLists.txt diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp index 1b324b2eb..94c9935b9 100644 --- a/src/tactic/bv/bv_bounds_tactic.cpp +++ b/src/tactic/bv/bv_bounds_tactic.cpp @@ -234,6 +234,7 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier { return false; } +#if 0 expr_set* get_expr_vars(expr* t) { unsigned id = t->get_id(); m_expr_vars.reserve(id + 1); @@ -259,7 +260,9 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier { } return set; } +#endif +#if 0 expr_cnt* get_expr_bounds(expr* t) { unsigned id = t->get_id(); m_bound_exprs.reserve(id + 1); @@ -288,6 +291,7 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier { } return set; } +#endif public: bv_bounds_simplifier(ast_manager& m, params_ref const& p) : m(m), m_params(p), m_bv(m) { @@ -392,17 +396,86 @@ public: return result != 0; } + // check if t contains v + ptr_vector todo; + bool contains(expr* t, expr* v) { + ast_fast_mark1 mark; + todo.push_back(t); + while (!todo.empty()) { + t = todo.back(); + todo.pop_back(); + if (mark.is_marked(t)) { + continue; + } + if (t == v) { + todo.reset(); + return true; + } + mark.mark(t); + + if (!is_app(t)) { + continue; + } + app* a = to_app(t); + todo.append(a->get_num_args(), a->get_args()); + } + return false; + } + + bool contains_bound(expr* t) { + ast_fast_mark1 mark1; + ast_fast_mark2 mark2; + + todo.push_back(t); + while (!todo.empty()) { + t = todo.back(); + todo.pop_back(); + if (mark1.is_marked(t)) { + continue; + } + mark1.mark(t); + + if (!is_app(t)) { + continue; + } + interval b; + expr* e; + if (is_bound(t, e, b)) { + if (mark2.is_marked(e)) { + todo.reset(); + return true; + } + mark2.mark(e); + if (m_bound.contains(e)) { + todo.reset(); + return true; + } + } + + app* a = to_app(t); + todo.append(a->get_num_args(), a->get_args()); + } + return false; + } + virtual bool may_simplify(expr* t) { if (m_bv.is_numeral(t)) return false; while (m.is_not(t, t)); + for (auto & v : m_bound) { + if (contains(t, v.m_key)) return true; + } + +#if 0 expr_set* used_exprs = get_expr_vars(t); for (map::iterator I = m_bound.begin(), E = m_bound.end(); I != E; ++I) { + if (contains(t, I->m_key)) return true; if (I->m_value.is_singleton() && used_exprs->contains(I->m_key)) return true; } +#endif expr* t1; interval b; @@ -411,11 +484,16 @@ public: return b.is_full() || m_bound.contains(t1); } + if (contains_bound(t)) { + return true; + } +#if 0 expr_cnt* bounds = get_expr_bounds(t); for (expr_cnt::iterator I = bounds->begin(), E = bounds->end(); I != E; ++I) { if (I->m_value > 1 || m_bound.contains(I->m_key)) return true; } +#endif return false; } diff --git a/contrib/cmake/src/tactic/core/CMakeLists.txt b/src/tactic/core/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/tactic/core/CMakeLists.txt rename to src/tactic/core/CMakeLists.txt diff --git a/src/tactic/core/blast_term_ite_tactic.cpp b/src/tactic/core/blast_term_ite_tactic.cpp index ea59641c9..483b59776 100644 --- a/src/tactic/core/blast_term_ite_tactic.cpp +++ b/src/tactic/core/blast_term_ite_tactic.cpp @@ -62,14 +62,14 @@ class blast_term_ite_tactic : public tactic { for (unsigned i = 0; i < num_args; ++i) { expr* c, *t, *e; if (!m.is_bool(args[i]) && m.is_ite(args[i], c, t, e)) { - enable_trace("blast_term_ite"); + // enable_trace("blast_term_ite"); TRACE("blast_term_ite", result = m.mk_app(f, num_args, args); tout << result << "\n";); expr_ref e1(m), e2(m); ptr_vector args1(num_args, args); args1[i] = t; ++m_num_fresh; e1 = m.mk_app(f, num_args, args1.c_ptr()); - if (t == e) { + if (m.are_equal(t,e)) { result = e1; return BR_REWRITE1; } diff --git a/contrib/cmake/src/tactic/fpa/CMakeLists.txt b/src/tactic/fpa/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/tactic/fpa/CMakeLists.txt rename to src/tactic/fpa/CMakeLists.txt diff --git a/contrib/cmake/src/tactic/nlsat_smt/CMakeLists.txt b/src/tactic/nlsat_smt/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/tactic/nlsat_smt/CMakeLists.txt rename to src/tactic/nlsat_smt/CMakeLists.txt diff --git a/contrib/cmake/src/tactic/portfolio/CMakeLists.txt b/src/tactic/portfolio/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/tactic/portfolio/CMakeLists.txt rename to src/tactic/portfolio/CMakeLists.txt diff --git a/contrib/cmake/src/tactic/sls/CMakeLists.txt b/src/tactic/sls/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/tactic/sls/CMakeLists.txt rename to src/tactic/sls/CMakeLists.txt diff --git a/contrib/cmake/src/tactic/smtlogics/CMakeLists.txt b/src/tactic/smtlogics/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/tactic/smtlogics/CMakeLists.txt rename to src/tactic/smtlogics/CMakeLists.txt diff --git a/contrib/cmake/src/tactic/ufbv/CMakeLists.txt b/src/tactic/ufbv/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/tactic/ufbv/CMakeLists.txt rename to src/tactic/ufbv/CMakeLists.txt diff --git a/contrib/cmake/src/test/CMakeLists.txt b/src/test/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/test/CMakeLists.txt rename to src/test/CMakeLists.txt diff --git a/contrib/cmake/src/test/fuzzing/CMakeLists.txt b/src/test/fuzzing/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/test/fuzzing/CMakeLists.txt rename to src/test/fuzzing/CMakeLists.txt diff --git a/contrib/cmake/src/util/CMakeLists.txt b/src/util/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/util/CMakeLists.txt rename to src/util/CMakeLists.txt diff --git a/contrib/cmake/src/util/lp/CMakeLists.txt b/src/util/lp/CMakeLists.txt similarity index 100% rename from contrib/cmake/src/util/lp/CMakeLists.txt rename to src/util/lp/CMakeLists.txt diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h index 383ecaeb3..2720f1b00 100644 --- a/src/util/obj_hashtable.h +++ b/src/util/obj_hashtable.h @@ -70,6 +70,7 @@ public: m_value(v) { } Value const & get_value() const { return m_value; } + Key & get_key () const { return *m_key; } unsigned hash() const { return m_key->hash(); } bool operator==(key_data const & other) const { return m_key == other.m_key; } }; @@ -100,6 +101,8 @@ public: m_table(DEFAULT_HASHTABLE_INITIAL_CAPACITY) {} typedef typename table::iterator iterator; + typedef typename table::data data; + typedef typename table::entry entry; typedef Key key; typedef Value value; diff --git a/src/util/stopwatch.h b/src/util/stopwatch.h index b1f6bba03..7a9066030 100644 --- a/src/util/stopwatch.h +++ b/src/util/stopwatch.h @@ -43,6 +43,8 @@ public: } ~stopwatch() {}; + + void add (const stopwatch &s) {/* TODO */} void reset() { m_elapsed.QuadPart = 0; } @@ -90,6 +92,8 @@ public: ~stopwatch() {} + void add (const stopwatch &s) {m_time += s.m_time;} + void reset() { m_time = 0ull; } @@ -141,6 +145,8 @@ public: ~stopwatch() {} + void add (const stopwatch &s) {m_time += s.m_time;} + void reset() { m_time = 0ull; }