From 68247aa58f2c736eedc9f5eff62a48d25c601d19 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 12 Dec 2015 10:01:27 +0000 Subject: [PATCH 01/15] Convert README to markdown --- README | 53 ----------------------------------------- README.md | 71 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 71 insertions(+), 53 deletions(-) delete mode 100644 README create mode 100644 README.md diff --git a/README b/README deleted file mode 100644 index 22fc58c7a..000000000 --- a/README +++ /dev/null @@ -1,53 +0,0 @@ -Z3 is a theorem prover from Microsoft Research. -Z3 is licensed under the MIT license. -Z3 can be built using Visual Studio Command Prompt and make/g++. - -1) Building Z3 on Windows using Visual Studio Command Prompt - -32-bit builds, start with: - - python scripts/mk_make.py - -or instead, for a 64-bit build: - - python scripts/mk_make.py -x - -then: - - cd build - nmake - -2) Building Z3 using make/g++ and Python -Execute: - - python scripts/mk_make.py - cd build - make - sudo make install - -By default, it will install z3 executable at PREFIX/bin, libraries at PREFIX/lib, and include files at PREFIX/include, -where PREFIX is the installation prefix used for installing Python in your system. -It is usually /usr for most Linux distros, and /usr/local for FreeBSD. -Use the following commands to install in a different prefix (e.g., /home/leo) - - python scripts/mk_make.py --prefix=/home/leo - cd build - make - make install - -In this example, the Z3 Python bindings will be stored at /home/leo/lib/pythonX.Y/dist-packages, -where X.Y corresponds to the python version in your system. - -To uninstall Z3, use - - sudo make uninstall - -4) Building Z3 using clang and clang++ on Linux/OSX -Remark: clang does not support OpenMP yet. - - CXX=clang++ CC=clang python scripts/mk_make.py - cd build - make - - -To clean Z3 you can delete the build directory and run the mk_make.py script again. diff --git a/README.md b/README.md new file mode 100644 index 000000000..4688e3d01 --- /dev/null +++ b/README.md @@ -0,0 +1,71 @@ +# Z3 + +Z3 is a theorem prover from Microsoft Research. +Z3 is licensed under the MIT license. +Z3 can be built using Visual Studio Command Prompt and make/g++. + +## Building Z3 on Windows using Visual Studio Command Prompt + +32-bit builds, start with: + +```bash + python scripts/mk_make.py +``` + +or instead, for a 64-bit build: + +```bash + python scripts/mk_make.py -x +``` + +then: + +```bash + cd build + nmake +``` + +## Building Z3 using make/g++ and Python + +Execute: + +```bash + python scripts/mk_make.py + cd build + make + sudo make install +``` + +By default, it will install z3 executable at ``PREFIX/bin``, libraries at +``PREFIX/lib``, and include files at ``PREFIX/include``, where ``PREFIX`` +installation prefix used for installing Python in your system. + +It is usually ``/usr`` for most Linux distros, and ``/usr/local`` for FreeBSD. +Use the following commands to install in a different prefix (e.g., /home/leo) + +```bash + python scripts/mk_make.py --prefix=/home/leo + cd build + make + make install +``` + +In this example, the Z3 Python bindings will be stored at ``/home/leo/lib/pythonX.Y/dist-packages``, +where X.Y corresponds to the python version in your system. + +To uninstall Z3, use + +```bash + sudo make uninstall +``` + +## Building Z3 using clang and clang++ on Linux/OSX +Remark: clang does not support OpenMP yet. + +```bash + CXX=clang++ CC=clang python scripts/mk_make.py + cd build + make +``` + +To clean Z3 you can delete the build directory and run the ``mk_make.py`` script again. From 08610ae243804b0ee22237b7ee0ca53b24ec82d5 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 12 Dec 2015 10:06:10 +0000 Subject: [PATCH 02/15] Correct incorrect information on what ``PREFIX`` is in ``README.md``. It isn't always the root of the Python install. --- README.md | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index 4688e3d01..0795c2a40 100644 --- a/README.md +++ b/README.md @@ -38,10 +38,9 @@ Execute: By default, it will install z3 executable at ``PREFIX/bin``, libraries at ``PREFIX/lib``, and include files at ``PREFIX/include``, where ``PREFIX`` -installation prefix used for installing Python in your system. - -It is usually ``/usr`` for most Linux distros, and ``/usr/local`` for FreeBSD. -Use the following commands to install in a different prefix (e.g., /home/leo) +installation prefix if inferred by the ``mk_make.py`` script. It is usually +``/usr`` for most Linux distros, and ``/usr/local`` for FreeBSD and OSX. Use +the ``--prefix=`` command line option to change the install prefix. For example: ```bash python scripts/mk_make.py --prefix=/home/leo From f09fa3c87b1853f26e4dde2bae4b531a204f431b Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 12 Dec 2015 10:22:56 +0000 Subject: [PATCH 03/15] Recent changes to the build system mean that setting a custom ``--prefix=`` is likely to disable installing the Python bindings so the old instructions aren't helpful. Reword them and mention using ``DESTDIR``. --- README.md | 26 ++++++++++++++++++++++++-- 1 file changed, 24 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 0795c2a40..a731a452d 100644 --- a/README.md +++ b/README.md @@ -49,8 +49,30 @@ the ``--prefix=`` command line option to change the install prefix. For example: make install ``` -In this example, the Z3 Python bindings will be stored at ``/home/leo/lib/pythonX.Y/dist-packages``, -where X.Y corresponds to the python version in your system. +Note the above will typically disable the installation of the Python bindings +because the Python ``site-packages`` directory (e.g. +``/usr/lib/python3.5/site-packages/``) is not rooted in the install prefix and +installing outside of the install prefix is dangerous and misleading. + +To avoid this issue you can use the ``DESTDIR`` makefile variable and leave the +install prefix as the default. The ``DESTDIR`` variable is prepended to the +install locations during ``make install`` and ``make uninstall`` and is intended +to allow ["staged installs"](https://www.gnu.org/prep/standards/html_node/DESTDIR.html). +Therefore it must always contain a trailing slash. + +For example: + +```bash + python scripts/mk_make.py + cd build + make + make install DESTDIR=/home/leo/ +``` + +In this example, the Z3 Python bindings will be stored at +``/home/leo/lib/pythonX.Y/site-packages`` +(``/home/leo/lib/pythonX.Y/dist-packages`` on Debian based Linux +distributions) where X.Y corresponds to the python version in your system. To uninstall Z3, use From 2bd9bbafe4eb56f03b67af8918ba371b8453e119 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 12 Dec 2015 10:31:12 +0000 Subject: [PATCH 04/15] Re-organise the discussion of Clang, it is not a second class citizen and so doesn't deserve to be stuck at the end of the README. It also **does** support OpenMP! --- README.md | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/README.md b/README.md index a731a452d..f4153b21d 100644 --- a/README.md +++ b/README.md @@ -25,7 +25,7 @@ then: nmake ``` -## Building Z3 using make/g++ and Python +## Building Z3 using make and GCC/Clang Execute: @@ -36,6 +36,15 @@ Execute: sudo make install ``` +Note by default ``gcc`` is used as the C++ compiler if it is available. If you +would prefer to use Clang change the ``mk_make.py`` line to + +```bash + CXX=clang++ CC=clang python scripts/mk_make.py +``` + +Note that Clang < 3.7 does not support OpenMP. + By default, it will install z3 executable at ``PREFIX/bin``, libraries at ``PREFIX/lib``, and include files at ``PREFIX/include``, where ``PREFIX`` installation prefix if inferred by the ``mk_make.py`` script. It is usually @@ -80,13 +89,4 @@ To uninstall Z3, use sudo make uninstall ``` -## Building Z3 using clang and clang++ on Linux/OSX -Remark: clang does not support OpenMP yet. - -```bash - CXX=clang++ CC=clang python scripts/mk_make.py - cd build - make -``` - To clean Z3 you can delete the build directory and run the ``mk_make.py`` script again. From 2947893e109f903f2e36ec4e6e9e7f90f86cada4 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 12 Dec 2015 11:04:12 +0000 Subject: [PATCH 05/15] Partially document the Z3 bindings in ``README.md`` --- README.md | 61 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 61 insertions(+) diff --git a/README.md b/README.md index f4153b21d..c757dee30 100644 --- a/README.md +++ b/README.md @@ -90,3 +90,64 @@ To uninstall Z3, use ``` To clean Z3 you can delete the build directory and run the ``mk_make.py`` script again. + +## Z3 bindings + +Z3 has bindings for various programming languages. + +### ``.NET`` + +These bindings are enabled by default on Windows and are enabled on other +platforms if [mono](http://www.mono-project.com/) is detected. On these +platforms the location of the C# compiler and gac utility need to be known. You +can set these as follows if they aren't detected automatically. For example: + +```bash + CSC=/usr/bin/csc GACUTIL=/usr/bin/gacutil python scripts/mk_make.py +``` + +To disable building these bindings pass ``--nodotnet`` to ``mk_make.py``. + +Note for very old versions of Mono (e.g. ``2.10``) you may need to set ``CSC`` +to ``/usr/bin/dmcs``. + +Note that when ``make install`` is executed on non-windows platforms the GAC +utility is used to install ``Microsoft.Z3.dll`` into the +[GAC](http://www.mono-project.com/docs/advanced/assemblies-and-the-gac/) as the +``Microsoft.Z3.Sharp`` package. During install a +[pkg-config](http://www.freedesktop.org/wiki/Software/pkg-config/) file +(``Microsoft.Z3.Sharp.pc``) is also installed which allows the +[MonoDevelop](http://www.monodevelop.com/) IDE to find the bindings. Running +``make uninstall`` will remove the dll from the GAC and the pkg-config file. + +See [``examples/dotnet``](examples/dotnet) for examples. + +### ``C`` + +These are always enabled. + +See [``examples/c``](examples/c) for examples. + +### ``C++`` + +These are always enabled. + +See [``examples/c++``](examples/c++) for examples. + +### ``Java`` + +Use the ``--java`` command line flag with ``mk_make.py`` to enable building these. + +See [``examples/java``](examples/java) for examples. + +### ``OCaml`` + +Use the ``--ml`` command line flag with ``mk_make.py`` to enable building these. + +See [``examples/ml``](examples/ml) for examples. + +### ``Python`` + +These bindings are always enabled. + +See [``examples/python``](examples/python) for examples. From 560810ee6778d85792e2ac3ab6cc925d15a0ce0c Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 12 Dec 2015 11:33:32 +0000 Subject: [PATCH 06/15] Fix command line indent in ``README.md`` --- README.md | 38 +++++++++++++++++++------------------- 1 file changed, 19 insertions(+), 19 deletions(-) diff --git a/README.md b/README.md index c757dee30..46a39134b 100644 --- a/README.md +++ b/README.md @@ -9,20 +9,20 @@ Z3 can be built using Visual Studio Command Prompt and make/g++. 32-bit builds, start with: ```bash - python scripts/mk_make.py +python scripts/mk_make.py ``` or instead, for a 64-bit build: ```bash - python scripts/mk_make.py -x +python scripts/mk_make.py -x ``` then: ```bash - cd build - nmake +cd build +nmake ``` ## Building Z3 using make and GCC/Clang @@ -30,17 +30,17 @@ then: Execute: ```bash - python scripts/mk_make.py - cd build - make - sudo make install +python scripts/mk_make.py +cd build +make +sudo make install ``` Note by default ``gcc`` is used as the C++ compiler if it is available. If you would prefer to use Clang change the ``mk_make.py`` line to ```bash - CXX=clang++ CC=clang python scripts/mk_make.py +CXX=clang++ CC=clang python scripts/mk_make.py ``` Note that Clang < 3.7 does not support OpenMP. @@ -52,10 +52,10 @@ installation prefix if inferred by the ``mk_make.py`` script. It is usually the ``--prefix=`` command line option to change the install prefix. For example: ```bash - python scripts/mk_make.py --prefix=/home/leo - cd build - make - make install +python scripts/mk_make.py --prefix=/home/leo +cd build +make +make install ``` Note the above will typically disable the installation of the Python bindings @@ -72,10 +72,10 @@ Therefore it must always contain a trailing slash. For example: ```bash - python scripts/mk_make.py - cd build - make - make install DESTDIR=/home/leo/ +python scripts/mk_make.py +cd build +make +make install DESTDIR=/home/leo/ ``` In this example, the Z3 Python bindings will be stored at @@ -86,7 +86,7 @@ distributions) where X.Y corresponds to the python version in your system. To uninstall Z3, use ```bash - sudo make uninstall +sudo make uninstall ``` To clean Z3 you can delete the build directory and run the ``mk_make.py`` script again. @@ -103,7 +103,7 @@ platforms the location of the C# compiler and gac utility need to be known. You can set these as follows if they aren't detected automatically. For example: ```bash - CSC=/usr/bin/csc GACUTIL=/usr/bin/gacutil python scripts/mk_make.py +CSC=/usr/bin/csc GACUTIL=/usr/bin/gacutil python scripts/mk_make.py ``` To disable building these bindings pass ``--nodotnet`` to ``mk_make.py``. From b4dd5d3d08f309ff2d90a8abbb09bc019af95b7e Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 12 Dec 2015 11:46:02 +0000 Subject: [PATCH 07/15] Rewrite intro text in ``README.md``. --- README.md | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 46a39134b..9ca373f87 100644 --- a/README.md +++ b/README.md @@ -1,8 +1,14 @@ # Z3 -Z3 is a theorem prover from Microsoft Research. -Z3 is licensed under the MIT license. -Z3 can be built using Visual Studio Command Prompt and make/g++. +Z3 is a theorem prover from Microsoft Research. It is licensed +under the [MIT license](LICENSE.txt). + +Z3 can be built using [Visual Studio][1] or a [Makefile][2]. It provides +[bindings for several programming languages][3]. + +[1]: #building-z3-on-windows-using-visual-studio-command-prompt +[2]: #building-z3-using-make-and-gccclang +[3]: #z3-bindings ## Building Z3 on Windows using Visual Studio Command Prompt From f9687e780aa6653e1a0c4eb5521c4c6a1b6f7f18 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 12 Dec 2015 11:50:38 +0000 Subject: [PATCH 08/15] Link to the release notes in ``README.md`` --- README.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/README.md b/README.md index 9ca373f87..7d2fc5a24 100644 --- a/README.md +++ b/README.md @@ -6,6 +6,8 @@ under the [MIT license](LICENSE.txt). Z3 can be built using [Visual Studio][1] or a [Makefile][2]. It provides [bindings for several programming languages][3]. +See the [release notes](RELEASE_NOTES) for notes on various stable releases of Z3. + [1]: #building-z3-on-windows-using-visual-studio-command-prompt [2]: #building-z3-using-make-and-gccclang [3]: #z3-bindings From 3d01246f71ced42b8da55e8ae3866d2820b35a0d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Jan 2016 08:17:18 -0800 Subject: [PATCH 09/15] Skip propagation on bits that have not (yet) been fixed by the SAT core: congruence closure for bits has not necessarily propagated to all bit positions when a bit in a congruence class gets fixed. Signed-off-by: Nikolaj Bjorner --- src/smt/theory_bv.cpp | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index cef8d5fc7..e4f698914 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -1176,31 +1176,37 @@ namespace smt { unsigned idx = entry.second; if (m_wpos[v] == idx) - find_wpos(v); - + find_wpos(v); literal_vector & bits = m_bits[v]; literal bit = bits[idx]; - lbool val = ctx.get_assignment(bit); + lbool val = ctx.get_assignment(bit); + if (val == l_undef) { + continue; + } theory_var v2 = next(v); TRACE("bv_bit_prop", tout << "propagating #" << get_enode(v)->get_owner_id() << "[" << idx << "] = " << val << "\n";); + literal antecedent = bit; + + if (val == l_false) { + antecedent.neg(); + } while (v2 != v) { literal_vector & bits2 = m_bits[v2]; literal bit2 = bits2[idx]; SASSERT(bit != ~bit2); lbool val2 = ctx.get_assignment(bit2); TRACE("bv_bit_prop", tout << "propagating #" << get_enode(v2)->get_owner_id() << "[" << idx << "] = " << val2 << "\n";); + if (val != val2) { - literal antecedent = bit; literal consequent = bit2; if (val == l_false) { - antecedent.neg(); consequent.neg(); } - SASSERT(ctx.get_assignment(antecedent) == l_true); assign_bit(consequent, v, v2, idx, antecedent, false); if (ctx.inconsistent()) { TRACE("bv_bit_prop", tout << "inconsistent " << bit << " " << bit2 << "\n";); + m_prop_queue.reset(); return; } } From e9ea687bb9e4848a6205cf7e0b07f73f349f7c36 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Fri, 8 Jan 2016 04:08:06 +0000 Subject: [PATCH 10/15] Disable the Python bindings by default which partially fixes issue #404. To enable the Python bindings use the newly added ``--python`` option. --- scripts/mk_util.py | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 6a070fe93..ca1b34c17 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -79,7 +79,7 @@ TRACE = False DOTNET_ENABLED=False JAVA_ENABLED=False ML_ENABLED=False -PYTHON_INSTALL_ENABLED=True +PYTHON_INSTALL_ENABLED=False STATIC_LIB=False VER_MAJOR=None VER_MINOR=None @@ -612,6 +612,7 @@ def display_help(exit_code): print(" --dotnet generate .NET bindings.") print(" --java generate Java bindings.") print(" --ml generate OCaml bindings.") + print(" --python generate Python bindings.") print(" --staticlib build Z3 static library.") if not IS_WINDOWS: print(" -g, --gmp use GMP.") @@ -642,14 +643,14 @@ def display_help(exit_code): # Parse configuration option for mk_make script def parse_options(): global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM - global DOTNET_ENABLED, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH + global DOTNET_ENABLED, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, PYTHON_INSTALL_ENABLED global LINUX_X64, SLOW_OPTIMIZE, USE_OMP try: options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:df:sxhmcvtnp:gj', ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj', 'trace', 'dotnet', 'staticlib', 'prefix=', 'gmp', 'foci2=', 'java', 'parallel=', 'gprof', - 'githash=', 'x86', 'ml', 'optimize', 'noomp', 'pypkgdir=']) + 'githash=', 'x86', 'ml', 'optimize', 'noomp', 'pypkgdir=', 'python']) except: print("ERROR: Invalid command line option") display_help(1) @@ -708,6 +709,8 @@ def parse_options(): ML_ENABLED = True elif opt in ('', '--noomp'): USE_OMP = False + elif opt in ('--python'): + PYTHON_INSTALL_ENABLED = True else: print("ERROR: Invalid command line option '%s'" % opt) display_help(1) @@ -1339,6 +1342,9 @@ class PythonInstallComponent(Component): self.in_prefix_install = True self.libz3Component = libz3Component + if not PYTHON_INSTALL_ENABLED: + return + if IS_WINDOWS: # Installing under Windows doesn't make sense as the install prefix is used # but that doesn't make sense under Windows @@ -1365,7 +1371,7 @@ class PythonInstallComponent(Component): assert not os.path.isabs(self.pythonPkgDir) def final_info(self): - if not PYTHON_PACKAGE_DIR.startswith(PREFIX): + if not PYTHON_PACKAGE_DIR.startswith(PREFIX) and PYTHON_INSTALL_ENABLED: print("Warning: The detected Python package directory (%s) is not " "in the installation prefix (%s). This can lead to a broken " "Python API installation. Use --pypkgdir= to change the " From 49a2ed01c8271660f4a323a2aec82a0f82958e9c Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Fri, 8 Jan 2016 04:43:09 +0000 Subject: [PATCH 11/15] Improve error message emitting during configure when the Python bindings are enabled and the set python package directory does not live under the install prefix. This is the other part required to fix issue #404. --- scripts/mk_util.py | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index ca1b34c17..ed5df106b 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1363,7 +1363,15 @@ class PythonInstallComponent(Component): else: # Use path inside the prefix (should be the normal case on Linux) # CMW: Also normal on *BSD? - assert PYTHON_PACKAGE_DIR.startswith(PREFIX) + if not PYTHON_PACKAGE_DIR.startswith(PREFIX): + raise MKException(('The python package directory ({}) must live ' + + 'under the install prefix ({}) to install the python bindings.' + + 'Use --pypkgdir and --prefix to set the python package directory ' + + 'and install prefix respectively. Note that the python package ' + + 'directory does not need to exist and will be created if ' + + 'necessary during install.').format( + PYTHON_PACKAGE_DIR, + PREFIX)) self.pythonPkgDir = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX) self.in_prefix_install = True From 9fb3d36961f9e6368bafe107374e23a6efbc7024 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Jan 2016 13:39:23 -0800 Subject: [PATCH 12/15] pin expressions during substitution. Issue #367 Signed-off-by: Nikolaj Bjorner --- src/api/ml/z3.ml | 266 +++++++++++++++++++---------------------------- 1 file changed, 109 insertions(+), 157 deletions(-) diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index bca0bdd1b..ccf18a024 100644 --- a/src/api/ml/z3.ml +++ b/src/api/ml/z3.ml @@ -789,6 +789,8 @@ sig val apply2 : context -> (Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr) -> expr -> expr -> expr val apply3 : context -> (Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr) -> expr -> expr -> expr -> expr + val apply4 : context -> (Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr -> Z3native.ptr) + -> expr -> expr -> expr -> expr -> expr val compare : expr -> expr -> int end = struct type expr = Expr of AST.ast @@ -797,6 +799,12 @@ end = struct let gnc e = match e with Expr(a) -> (z3obj_gnc a) let gno e = match e with Expr(a) -> (z3obj_gno a) + let inc_elist (es : expr list) = + List.iter (fun e -> match e with Expr(o) -> o.inc_ref (gnc e) o.m_n_obj) es + + let dec_elist (es : expr list) = + List.iter (fun e -> match e with Expr(o) -> o.dec_ref (gnc e) o.m_n_obj) es + let expr_of_ptr : context -> Z3native.ptr -> expr = fun ctx no -> let e = z3_native_object_of_ast_ptr ctx no in if ast_kind_of_int (Z3native.get_ast_kind (context_gno ctx) no) == QUANTIFIER_AST then @@ -850,6 +858,9 @@ end = struct let apply3 ctx f t1 t2 t3 = expr_of_ptr ctx (f (context_gno ctx) (gno t1) (gno t2) (gno t3)) + let apply4 ctx f t1 t2 t3 t4 = + expr_of_ptr ctx (f (context_gno ctx) (gno t1) (gno t2) (gno t3) (gno t4)) + let simplify ( x : expr ) ( p : Params.params option ) = match p with | None -> expr_of_ptr (Expr.gc x) (Z3native.simplify (gnc x) (gno x)) | Some pp -> expr_of_ptr (Expr.gc x) (Z3native.simplify_ex (gnc x) (gno x) (z3obj_gno pp)) @@ -871,19 +882,30 @@ end = struct if ((AST.is_app (ast_of_expr x)) && (List.length args <> (get_num_args x))) then raise (Z3native.Exception "Number of arguments does not match") else - expr_of_ptr (Expr.gc x) (Z3native.update_term (gnc x) (gno x) (List.length args) (expr_lton args)) + (inc_elist args; + let r = expr_of_ptr (Expr.gc x) (Z3native.update_term (gnc x) (gno x) (List.length args) (expr_lton args)) in + dec_elist args; + r) let substitute ( x : expr ) from to_ = if (List.length from) <> (List.length to_) then raise (Z3native.Exception "Argument sizes do not match") else - expr_of_ptr (Expr.gc x) (Z3native.substitute (gnc x) (gno x) (List.length from) (expr_lton from) (expr_lton to_)) + (inc_elist from; + inc_elist to_; + let r = expr_of_ptr (Expr.gc x) (Z3native.substitute (gnc x) (gno x) (List.length from) (expr_lton from) (expr_lton to_)) in + dec_elist from; + dec_elist to_; + r) let substitute_one ( x : expr ) from to_ = substitute ( x : expr ) [ from ] [ to_ ] let substitute_vars ( x : expr ) to_ = - expr_of_ptr (Expr.gc x) (Z3native.substitute_vars (gnc x) (gno x) (List.length to_) (expr_lton to_)) + (inc_elist to_; + let r = expr_of_ptr (Expr.gc x) (Z3native.substitute_vars (gnc x) (gno x) (List.length to_) (expr_lton to_)) in + dec_elist to_; + r) let translate ( x : expr ) to_ctx = if (Expr.gc x) == to_ctx then @@ -1257,22 +1279,21 @@ struct let mk_union ( ctx : context ) ( args : expr list ) = expr_of_ptr ctx (Z3native.mk_set_union (context_gno ctx) (List.length args) (expr_lton args)) - - + let mk_intersection ( ctx : context ) ( args : expr list ) = expr_of_ptr ctx (Z3native.mk_set_intersect (context_gno ctx) (List.length args) (expr_lton args)) let mk_difference ( ctx : context ) ( arg1 : expr ) ( arg2 : expr ) = - expr_of_ptr ctx (Z3native.mk_set_difference (context_gno ctx) (Expr.gno arg1) (Expr.gno arg2)) + apply2 ctx Z3native.mk_set_difference arg1 arg2 let mk_complement ( ctx : context ) ( arg : expr ) = - expr_of_ptr ctx (Z3native.mk_set_complement (context_gno ctx) (Expr.gno arg)) + apply1 ctx Z3native.mk_set_complement arg let mk_membership ( ctx : context ) ( elem : expr ) ( set : expr ) = - expr_of_ptr ctx (Z3native.mk_set_member (context_gno ctx) (Expr.gno elem) (Expr.gno set)) + apply2 ctx Z3native.mk_set_member elem set let mk_subset ( ctx : context ) ( arg1 : expr ) ( arg2 : expr ) = - expr_of_ptr ctx (Z3native.mk_set_subset (context_gno ctx) (Expr.gno arg1) (Expr.gno arg2)) + apply2 ctx Z3native.mk_set_subset arg1 arg2 end @@ -1612,10 +1633,10 @@ struct mk_const ctx (Symbol.mk_string ctx name) let mk_mod ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_mod (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) + apply2 ctx Z3native.mk_mod t1 t2 let mk_rem ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_rem (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) + apply2 ctx Z3native.mk_rem t1 t2 let mk_numeral_s ( ctx : context ) ( v : string ) = expr_of_ptr ctx (Z3native.mk_numeral (context_gno ctx) v (Sort.gno (mk_sort ctx))) @@ -1624,7 +1645,7 @@ struct expr_of_ptr ctx (Z3native.mk_int (context_gno ctx) v (Sort.gno (mk_sort ctx))) let mk_int2real ( ctx : context ) ( t : expr ) = - (Expr.expr_of_ptr ctx (Z3native.mk_int2real (context_gno ctx) (Expr.gno t))) + apply1 ctx Z3native.mk_int2real t let mk_int2bv ( ctx : context ) ( n : int ) ( t : expr ) = (Expr.expr_of_ptr ctx (Z3native.mk_int2bv (context_gno ctx) n (Expr.gno t))) @@ -1636,10 +1657,10 @@ struct Sort.sort_of_ptr ctx (Z3native.mk_real_sort (context_gno ctx)) let get_numerator ( x : expr ) = - expr_of_ptr (Expr.gc x) (Z3native.get_numerator (Expr.gnc x) (Expr.gno x)) + apply1 (Expr.gc x) Z3native.get_numerator x let get_denominator ( x : expr ) = - expr_of_ptr (Expr.gc x) (Z3native.get_denominator (Expr.gnc x) (Expr.gno x)) + apply1 (Expr.gc x) Z3native.get_denominator x let get_ratio ( x : expr ) = if (is_rat_numeral x) then @@ -1671,10 +1692,10 @@ struct expr_of_ptr ctx (Z3native.mk_int (context_gno ctx) v (Sort.gno (mk_sort ctx))) let mk_is_integer ( ctx : context ) ( t : expr ) = - (expr_of_ptr ctx (Z3native.mk_is_int (context_gno ctx) (Expr.gno t))) + apply1 ctx Z3native.mk_is_int t let mk_real2int ( ctx : context ) ( t : expr ) = - (expr_of_ptr ctx (Z3native.mk_real2int (context_gno ctx) (Expr.gno t))) + apply1 ctx Z3native.mk_real2int t module AlgebraicNumber = struct @@ -1703,26 +1724,19 @@ struct let f x = (Expr.gno x) in (expr_of_ptr ctx (Z3native.mk_sub (context_gno ctx) (List.length t) (Array.of_list (List.map f t)))) - let mk_unary_minus ( ctx : context ) ( t : expr ) = - (expr_of_ptr ctx (Z3native.mk_unary_minus (context_gno ctx) (Expr.gno t))) + let mk_unary_minus ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_unary_minus t - let mk_div ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_div (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) + let mk_div ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_div t1 t2 - let mk_power ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_power (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) + let mk_power ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_power t1 t2 - let mk_lt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_lt (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) + let mk_lt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_lt t1 t2 - let mk_le ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_le (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) + let mk_le ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_le t1 t2 - let mk_gt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_gt (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) + let mk_gt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_gt t1 t2 - let mk_ge ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_ge (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) + let mk_ge ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_ge t1 t2 end @@ -1793,100 +1807,63 @@ struct Expr.mk_const ctx name (mk_sort ctx size) let mk_const_s ( ctx : context ) ( name : string ) ( size : int ) = mk_const ctx (Symbol.mk_string ctx name) size - let mk_not ( ctx : context ) ( t : expr ) = - expr_of_ptr ctx (Z3native.mk_bvnot (context_gno ctx) (Expr.gno t)) - let mk_redand ( ctx : context ) ( t : expr ) = - expr_of_ptr ctx (Z3native.mk_bvredand (context_gno ctx) (Expr.gno t)) - let mk_redor ( ctx : context ) ( t : expr ) = - expr_of_ptr ctx (Z3native.mk_bvredor (context_gno ctx) (Expr.gno t)) - let mk_and ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvand (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_or ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvor (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_xor ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvxor (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_nand ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvnand (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_nor ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvnor (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_xnor ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvxnor (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_neg ( ctx : context ) ( t : expr ) = - expr_of_ptr ctx (Z3native.mk_bvneg (context_gno ctx) (Expr.gno t)) - let mk_add ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvadd (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_sub ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvsub (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_mul ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvmul (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_udiv ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvudiv (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_sdiv ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvsdiv (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_urem ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvurem (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_srem ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvsrem (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_smod ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvsmod (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_ult ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_bvult (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) - let mk_slt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_bvslt (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) - let mk_ule ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_bvule (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) - let mk_sle ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_bvsle (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) - let mk_uge ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_bvuge (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) - let mk_sge ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_bvsge (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) - let mk_ugt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_bvugt (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) - let mk_sgt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_bvsgt (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) - let mk_concat ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_concat (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) + let mk_not ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_bvnot t + let mk_redand ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_bvredand t + let mk_redor ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_bvredor t + let mk_and ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvand t1 t2 + let mk_or ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvor t1 t2 + let mk_xor ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvxor t1 t2 + let mk_nand ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvnand t1 t2 + let mk_nor ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvnor t1 t2 + let mk_xnor ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvxnor t1 t2 + let mk_neg ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_bvneg t + let mk_add ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvadd t1 t2 + let mk_sub ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvsub t1 t2 + let mk_mul ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvmul t1 t2 + let mk_udiv ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvudiv t1 t2 + let mk_sdiv ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvsdiv t1 t2 + let mk_urem ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvurem t1 t2 + let mk_srem ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvsrem t1 t2 + let mk_smod ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvsmod t1 t2 + let mk_ult ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvult t1 t2 + let mk_slt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvslt t1 t2 + let mk_ule ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvule t1 t2 + let mk_sle ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvsle t1 t2 + let mk_uge ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvuge t1 t2 + let mk_sge ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvsge t1 t2 + let mk_ugt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvugt t1 t2 + let mk_sgt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvsgt t1 t2 + let mk_concat ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_concat t1 t2 let mk_extract ( ctx : context ) ( high : int ) ( low : int ) ( t : expr ) = expr_of_ptr ctx (Z3native.mk_extract (context_gno ctx) high low (Expr.gno t)) - let mk_sign_ext ( ctx : context ) ( i : int ) ( t : expr ) = + let mk_sign_ext ( ctx : context ) ( i : int ) ( t : expr ) = expr_of_ptr ctx (Z3native.mk_sign_ext (context_gno ctx) i (Expr.gno t)) let mk_zero_ext ( ctx : context ) ( i : int ) ( t : expr ) = expr_of_ptr ctx (Z3native.mk_zero_ext (context_gno ctx) i (Expr.gno t)) let mk_repeat ( ctx : context ) ( i : int ) ( t : expr ) = expr_of_ptr ctx (Z3native.mk_repeat (context_gno ctx) i (Expr.gno t)) - let mk_shl ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvshl (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_lshr ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvlshr (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_ashr ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_bvashr (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_rotate_left ( ctx : context ) ( i : int ) ( t : expr ) = + let mk_shl ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvshl t1 t2 + let mk_lshr ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvlshr t1 t2 + let mk_ashr ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvashr t1 t2 + let mk_rotate_left ( ctx : context ) ( i : int ) ( t : expr ) = expr_of_ptr ctx (Z3native.mk_rotate_left (context_gno ctx) i (Expr.gno t)) let mk_rotate_right ( ctx : context ) ( i : int ) ( t : expr ) = expr_of_ptr ctx (Z3native.mk_rotate_right (context_gno ctx) i (Expr.gno t)) - let mk_ext_rotate_left ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_ext_rotate_left (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_ext_rotate_right ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_ext_rotate_right (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) + let mk_ext_rotate_left ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_ext_rotate_left t1 t2 + let mk_ext_rotate_right ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_ext_rotate_right t1 t2 let mk_bv2int ( ctx : context ) ( t : expr ) ( signed : bool ) = expr_of_ptr ctx (Z3native.mk_bv2int (context_gno ctx) (Expr.gno t) signed) let mk_add_no_overflow ( ctx : context ) ( t1 : expr ) ( t2 : expr ) ( signed : bool) = (expr_of_ptr ctx (Z3native.mk_bvadd_no_overflow (context_gno ctx) (Expr.gno t1) (Expr.gno t2) signed)) - let mk_add_no_underflow ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_bvadd_no_underflow (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) - let mk_sub_no_overflow ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_bvsub_no_overflow (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) + let mk_add_no_underflow ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvadd_no_underflow t1 t2 + let mk_sub_no_overflow ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvsub_no_overflow t1 t2 let mk_sub_no_underflow ( ctx : context ) ( t1 : expr ) ( t2 : expr ) ( signed : bool) = (expr_of_ptr ctx (Z3native.mk_bvsub_no_underflow (context_gno ctx) (Expr.gno t1) (Expr.gno t2) signed)) - let mk_sdiv_no_overflow ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_bvsdiv_no_overflow (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) - let mk_neg_no_overflow ( ctx : context ) ( t : expr ) = - (expr_of_ptr ctx (Z3native.mk_bvneg_no_overflow (context_gno ctx) (Expr.gno t))) + let mk_sdiv_no_overflow ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvsdiv_no_overflow t1 t2 + let mk_neg_no_overflow ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_bvneg_no_overflow t let mk_mul_no_overflow ( ctx : context ) ( t1 : expr ) ( t2 : expr ) ( signed : bool) = (expr_of_ptr ctx (Z3native.mk_bvmul_no_overflow (context_gno ctx) (Expr.gno t1) (Expr.gno t2) signed)) - let mk_mul_no_underflow ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - (expr_of_ptr ctx (Z3native.mk_bvmul_no_underflow (context_gno ctx) (Expr.gno t1) (Expr.gno t2))) + let mk_mul_no_underflow ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_bvmul_no_underflow t1 t2 let mk_numeral ( ctx : context ) ( v : string ) ( size : int ) = expr_of_ptr ctx (Z3native.mk_numeral (context_gno ctx) v (Sort.gno (mk_sort ctx size))) end @@ -1949,7 +1926,7 @@ struct (expr_of_ptr ctx (Z3native.mk_fpa_zero (context_gno ctx) (Sort.gno s) negative)) let mk_fp ( ctx : context ) ( sign : expr ) ( exponent : expr ) ( significand : expr ) = - (expr_of_ptr ctx (Z3native.mk_fpa_fp (context_gno ctx) (Expr.gno sign) (Expr.gno exponent) (Expr.gno significand))) + apply3 ctx Z3native.mk_fpa_fp sign exponent significand let mk_numeral_f ( ctx : context ) ( value : float ) ( s : Sort.sort ) = (expr_of_ptr ctx (Z3native.mk_fpa_numeral_double (context_gno ctx) value (Sort.gno s))) let mk_numeral_i ( ctx : context ) ( value : int ) ( s : Sort.sort ) = @@ -1997,54 +1974,30 @@ struct let mk_const_s ( ctx : context ) ( name : string ) ( s : Sort.sort ) = mk_const ctx (Symbol.mk_string ctx name) s - let mk_abs ( ctx : context ) ( t : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_abs (context_gno ctx) (Expr.gno t)) - let mk_neg ( ctx : context ) ( t : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_neg (context_gno ctx) (Expr.gno t)) - let mk_add ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_add (context_gno ctx) (Expr.gno rm) (Expr.gno t1) (Expr.gno t2)) - let mk_sub ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_sub (context_gno ctx) (Expr.gno rm) (Expr.gno t1) (Expr.gno t2)) - let mk_mul ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_mul (context_gno ctx) (Expr.gno rm) (Expr.gno t1) (Expr.gno t2)) - let mk_div ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_div (context_gno ctx) (Expr.gno rm) (Expr.gno t1) (Expr.gno t2)) - let mk_fma ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) ( t3 : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_fma (context_gno ctx) (Expr.gno rm) (Expr.gno t1) (Expr.gno t2) (Expr.gno t3)) - let mk_sqrt ( ctx : context ) ( rm : expr ) ( t : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_sqrt (context_gno ctx) (Expr.gno rm) (Expr.gno t)) - let mk_rem ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_rem (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_round_to_integral ( ctx : context ) ( rm : expr ) ( t : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_round_to_integral (context_gno ctx) (Expr.gno rm) (Expr.gno t)) - let mk_min ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_min (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_max ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_max (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_leq ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_leq (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_lt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_lt (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_geq ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_geq (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_gt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_gt (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_eq ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_eq (context_gno ctx) (Expr.gno t1) (Expr.gno t2)) - let mk_is_normal ( ctx : context ) ( t : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_is_normal (context_gno ctx) (Expr.gno t)) - let mk_is_subnormal ( ctx : context ) ( t : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_is_subnormal (context_gno ctx) (Expr.gno t)) - let mk_is_zero ( ctx : context ) ( t : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_is_zero (context_gno ctx) (Expr.gno t)) - let mk_is_infinite ( ctx : context ) ( t : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_is_infinite (context_gno ctx) (Expr.gno t)) - let mk_is_nan ( ctx : context ) ( t : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_is_nan (context_gno ctx) (Expr.gno t)) - let mk_is_negative ( ctx : context ) ( t : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_is_negative (context_gno ctx) (Expr.gno t)) - let mk_is_positive ( ctx : context ) ( t : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_is_positive (context_gno ctx) (Expr.gno t)) + let mk_abs ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_fpa_abs t + let mk_neg ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_fpa_neg t + let mk_add ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) = apply3 ctx Z3native.mk_fpa_add rm t1 t2 + let mk_sub ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) = apply3 ctx Z3native.mk_fpa_sub rm t1 t2 + let mk_mul ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) = apply3 ctx Z3native.mk_fpa_mul rm t1 t2 + let mk_div ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) = apply3 ctx Z3native.mk_fpa_div rm t1 t2 + let mk_fma ( ctx : context ) ( rm : expr ) ( t1 : expr ) ( t2 : expr ) ( t3 : expr ) = apply4 ctx Z3native.mk_fpa_fma rm t1 t2 t3 + let mk_sqrt ( ctx : context ) ( rm : expr ) ( t : expr ) = apply2 ctx Z3native.mk_fpa_sqrt rm t + let mk_rem ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_fpa_rem t1 t2 + let mk_round_to_integral ( ctx : context ) ( rm : expr ) ( t : expr ) = apply2 ctx Z3native.mk_fpa_round_to_integral rm t + let mk_min ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_fpa_min t1 t2 + let mk_max ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_fpa_max t1 t2 + let mk_leq ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_fpa_leq t1 t2 + let mk_lt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_fpa_lt t1 t2 + let mk_geq ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_fpa_geq t1 t2 + let mk_gt ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_fpa_gt t1 t2 + let mk_eq ( ctx : context ) ( t1 : expr ) ( t2 : expr ) = apply2 ctx Z3native.mk_fpa_eq t1 t2 + let mk_is_normal ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_fpa_is_normal t + let mk_is_subnormal ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_fpa_is_subnormal t + let mk_is_zero ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_fpa_is_zero t + let mk_is_infinite ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_fpa_is_infinite t + let mk_is_nan ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_fpa_is_nan t + let mk_is_negative ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_fpa_is_negative t + let mk_is_positive ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_fpa_is_positive t let mk_to_fp_bv ( ctx : context ) ( t : expr ) ( s : Sort.sort ) = expr_of_ptr ctx (Z3native.mk_fpa_to_fp_bv (context_gno ctx) (Expr.gno t) (Sort.gno s)) let mk_to_fp_float ( ctx : context ) ( rm : expr) ( t : expr ) ( s : Sort.sort ) = @@ -2059,8 +2012,7 @@ struct expr_of_ptr ctx (Z3native.mk_fpa_to_ubv (context_gno ctx) (Expr.gno rm) (Expr.gno t) size) let mk_to_sbv ( ctx : context ) ( rm : expr) ( t : expr ) ( size : int ) = expr_of_ptr ctx (Z3native.mk_fpa_to_sbv (context_gno ctx) (Expr.gno rm) (Expr.gno t) size) - let mk_to_real ( ctx : context ) ( t : expr ) = - expr_of_ptr ctx (Z3native.mk_fpa_to_real (context_gno ctx) (Expr.gno t)) + let mk_to_real ( ctx : context ) ( t : expr ) = apply1 ctx Z3native.mk_fpa_to_real t let get_ebits ( ctx : context ) ( s : Sort.sort ) = (Z3native.fpa_get_ebits (context_gno ctx) (Sort.gno s)) From 4939957f6ae95521f04472e233c1be60690f3c55 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Jan 2016 16:07:42 -0800 Subject: [PATCH 13/15] check that disequations are solved Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 22 +++++++++++++++++----- 1 file changed, 17 insertions(+), 5 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 4bc867717..f06afce71 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -551,6 +551,9 @@ bool theory_seq::is_solved() { IF_VERBOSE(10, verbose_stream() << "(seq.giveup " << m_eqs[0].ls() << " = " << m_eqs[0].rs() << " is unsolved)\n";); return false; } + if (!m_nqs.empty()) { + return false; + } for (unsigned i = 0; i < m_automata.size(); ++i) { if (!m_automata[i]) { IF_VERBOSE(10, verbose_stream() << "(seq.giveup regular expression did not compile to automaton)\n";); @@ -967,10 +970,10 @@ bool theory_seq::solve_ne(unsigned idx) { } } + bool updated = false; dependency* new_deps = n.dep(); vector new_ls, new_rs; literal_vector new_lits(n.lits()); - bool updated = false; for (unsigned i = 0; i < n.ls().size(); ++i) { expr_ref_vector& ls = m_ls; expr_ref_vector& rs = m_rs; @@ -986,8 +989,7 @@ bool theory_seq::solve_ne(unsigned idx) { return true; } else if (!change) { -// std::cout << n.ls(i) << " " << ls << "\n"; -// std::cout << n.rs(i) << " " << rs << "\n"; + TRACE("seq", tout << "no change " << n.ls(i) << " " << n.rs(i) << "\n";); continue; } else { @@ -1015,7 +1017,7 @@ bool theory_seq::solve_ne(unsigned idx) { expr* nr = rhs[j].get(); if (m_util.is_seq(nl) || m_util.is_re(nl)) { ls.reset(); - rs.reset(); + rs.reset(); SASSERT(!m_util.str.is_concat(nl)); SASSERT(!m_util.str.is_concat(nr)); ls.push_back(nl); rs.push_back(nr); @@ -1041,6 +1043,16 @@ bool theory_seq::solve_ne(unsigned idx) { new_deps = m_dm.mk_join(deps, new_deps); } } + if (!updated && num_undef_lits == 0) { + return false; + } + if (!updated) { + for (unsigned j = 0; j < n.ls().size(); ++j) { + new_ls.push_back(n.ls(j)); + new_rs.push_back(n.rs(j)); + } + } + if (num_undef_lits == 1 && new_ls.empty()) { literal_vector lits; literal undef_lit = null_literal; @@ -1064,7 +1076,7 @@ bool theory_seq::solve_ne(unsigned idx) { propagate_lit(new_deps, lits.size(), lits.c_ptr(), ~undef_lit); return true; } - else if (updated) { + if (updated) { if (num_undef_lits == 0 && new_ls.empty()) { TRACE("seq", tout << "conflict\n";); set_conflict(new_deps, new_lits); From 03cef7b03c6519e452cf9c78a3ee96acc64d0e3d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Jan 2016 16:19:32 -0800 Subject: [PATCH 14/15] add some conveniences for expressing string constraints Signed-off-by: Nikolaj Bjorner --- src/api/python/z3.py | 25 +++++++++++++++++-------- 1 file changed, 17 insertions(+), 8 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index afdca7464..b8ec74d18 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -3572,15 +3572,19 @@ def Concat(*args): if __debug__: _z3_assert(sz >= 2, "At least two arguments expected.") - ctx = args[0].ctx - - if is_seq(args[0]): - if __debug__: - _z3_assert(all([is_seq(a) for a in args]), "All arguments must be sequence expressions.") - v = (Ast * sz)() - for i in range(sz): + ctx = None + for a in args: + if is_expr(a): + ctx = a.ctx + break + if is_seq(args[0]) or isinstance(args[0], str): + args = [_coerce_seq(s, ctx) for s in args] + if __debug__: + _z3_assert(all([is_seq(a) for a in args]), "All arguments must be sequence expressions.") + v = (Ast * sz)() + for i in range(sz): v[i] = args[i].as_ast() - return SeqRef(Z3_mk_seq_concat(ctx.ref(), sz, v), ctx) + return SeqRef(Z3_mk_seq_concat(ctx.ref(), sz, v), ctx) if is_re(args[0]): if __debug__: @@ -9066,7 +9070,12 @@ class SeqRef(ExprRef): def __add__(self, other): return Concat(self, other) + def __radd__(self, other): + return Concat(other, self) + def __getitem__(self, i): + if _is_int(i): + i = IntVal(i, self.ctx) return SeqRef(Z3_mk_seq_at(self.ctx_ref(), self.as_ast(), i.as_ast()), self.ctx) def is_string(self): From fc4260e0183dc35a6bad0e9fd124b18623f65c45 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 9 Jan 2016 10:01:44 -0800 Subject: [PATCH 15/15] enable Horner evaluation also for mixed-integer constraints now that ast-manger inserts coercions on the fly. Avoids loop for issue #399, but with this alone results in unknown status Signed-off-by: Nikolaj Bjorner --- src/muz/pdr/pdr_context.cpp | 1 + src/smt/theory_arith_nl.h | 6 +++++- 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp index b3648f38d..20bf183e0 100644 --- a/src/muz/pdr/pdr_context.cpp +++ b/src/muz/pdr/pdr_context.cpp @@ -1705,6 +1705,7 @@ namespace pdr { void context::validate_search() { expr_ref tr = m_search.get_trace(*this); + TRACE("pdr", tout << tr << "\n";); smt::kernel solver(m, get_fparams()); solver.assert_expr(tr); lbool res = solver.check(); diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index 982aa963f..311a62a38 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -354,6 +354,7 @@ namespace smt { */ template interval theory_arith::evaluate_as_interval(expr * n) { + expr* arg; TRACE("nl_evaluate", tout << "evaluating: " << mk_bounded_pp(n, get_manager(), 10) << "\n";); if (has_var(n)) { TRACE("nl_evaluate", tout << "n has a variable associated with it\n";); @@ -385,6 +386,9 @@ namespace smt { TRACE("cross_nested_eval_bug", display_nested_form(tout, n); tout << "\ninterval: " << r << "\n";); return r; } + else if (m_util.is_to_real(n, arg)) { + return evaluate_as_interval(arg); + } else { rational val; if (m_util.is_numeral(n, val)) { @@ -1660,7 +1664,7 @@ namespace smt { 3) (new non-int coeffs) This only happens in an optional step in the conversion. Now, for int rows, I only apply this optional step only if non-int coeffs are not created. */ - if (is_mixed_real_integer(r)) + if (!get_manager().int_real_coercions() && is_mixed_real_integer(r)) return true; // giving up... see comment above TRACE("cross_nested", tout << "cheking problematic row...\n";);