3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Commit graph

5334 commits

Author SHA1 Message Date
Christoph M. Wintersteiger efd923b826 Merge pull request #552 from MikolasJanota/bug_fix
Avoiding adding spurious +0 in poly_rewriter::cancel_monomials.
2016-04-05 19:06:19 +01:00
mikolas 05ce886afe Avoiding adding spurious +0 in poly_rewriter::cancel_monomials. 2016-04-05 17:26:48 +01:00
Christoph M. Wintersteiger 991eae8767 Merge pull request #2 from martin-neuhaeusser/ml_api_patch2
Correct reference counting and handling of NULL pointers in new OCaml bindings.
2016-04-05 13:01:04 +01:00
martin-neuhaeusser 71f991c5df Avoid using physical equality checks in OCaml bindings (z3.ml)
This patch avoids the use of physical equality wherever possible
and improves some details of the OCaml implementation.
2016-04-05 12:51:03 +02:00
Nikolaj Bjorner c454b81b2c special case branching
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-04-05 11:57:49 +02:00
Nikolaj Bjorner ed1a5797fb check that a clause was not removed to fix issue #551
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-04-04 20:15:49 +02:00
martin-neuhaeusser f133f478c8 Translate correctly between OCaml option values and NULL pointers
This patch refactors the update_api script and the z3.ml implementation
to properly translate between OCaml options and NULL pointers. Some
unifications and simplifications (avoidance of unnecessary value allocation)
in the script that creates the native bindings.
2016-04-04 17:16:15 +02:00
Nikolaj Bjorner ec5a4ba63d add documentation comment for evaluation, Issue #536
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-04-04 12:59:18 +02:00
Nikolaj Bjorner 9667185af0 issue #549, replace BoolVal by False, otherwise creates regression
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-04-03 12:53:50 +02:00
Nikolaj Bjorner 11e8f06272 issue #549, replace False by BoolVal
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-04-03 12:52:15 +02:00
Nikolaj Bjorner 33e7640645 disable mb branching pending unit test analysis
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-04-03 10:53:37 +02:00
martin-neuhaeusser b85516c271 Fix reference counting in the C layer of the OCaml bindings
The Z3 context and its reference counters are stored in a structure which is allocated
by the C layer outside the OCaml heap, whenever a Z3 context is created. The structure
and its Z3 context are disposed, once the last reference counter reaches zero. Reference
counters are decremented by C-level finalizers.

The OCaml representations for a Z3 context wrap only a pointer to the corresponding structure.
2016-04-03 09:41:06 +02:00
Nikolaj Bjorner 03336ab9f2 add evaluation of array equalities to model evaluator
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-04-02 15:07:01 +02:00
Nikolaj Bjorner f6aaa5cc8d Merge pull request #550 from seahorn/farkas
typo: gt -> ge
2016-04-02 11:13:30 +02:00
Arie Gurfinkel 44d4902bb4 typo: gt -> ge 2016-04-02 10:13:14 +02:00
Christoph M. Wintersteiger ccd18283e7 Moved extension_converter func_interp entry compression to func_interp.
Relates to #547
2016-04-01 15:38:38 +01:00
Christoph M. Wintersteiger 3b82604590 whitespace 2016-04-01 15:37:40 +01:00
Christoph M. Wintersteiger d55a6725c9 Compressed func_interps in extension_model_converter.
Fixes #547.
2016-04-01 15:17:38 +01:00
Christoph M. Wintersteiger eb9c5b7cdb Disabled bogus assertions.
Fixes #489
2016-04-01 13:25:37 +01:00
Christoph M. Wintersteiger 852dc6d190 whitespace 2016-04-01 13:22:16 +01:00
Christoph M. Wintersteiger 405650c183 bugfix for ackr_model_converter (refcounts were off due to func_interps not being copied properly). 2016-04-01 13:17:48 +01:00
Christoph M. Wintersteiger dafda681b2 Bugfix for zero-extend.
Fixes #548
2016-04-01 12:48:06 +01:00
Christoph M. Wintersteiger dcca3a9bb1 whitespace 2016-04-01 12:46:49 +01:00
Christoph M. Wintersteiger b178420797 Merge branch 'master' of https://github.com/Z3Prover/z3 into new-ml-api 2016-03-31 18:11:30 +01:00
Christoph M. Wintersteiger f4c330ba5c Merge pull request #1 from martin-neuhaeusser/my-ml-api
Use a custom block for storing a Z3_config in the ML bindings.
2016-03-31 18:10:43 +01:00
Martin R. Neuhaeusser feae0e8277 Use a custom block for storing a Z3_config in the ML bindings. 2016-03-31 18:31:59 +02:00
Christoph M. Wintersteiger bf92e53688 Annotation fix for pattern/quantifier probes 2016-03-30 18:35:49 +01:00
Christoph M. Wintersteiger 1724811e1b qffp tactic cleaned up to be in line with the default behavior of other tactics. 2016-03-30 15:23:46 +01:00
Christoph M. Wintersteiger cb2bf48254 Added has_quantifier probe 2016-03-30 15:22:53 +01:00
Christoph M. Wintersteiger d746b410cf whitespace 2016-03-30 15:22:21 +01:00
Christoph M. Wintersteiger 264bb6321a Merge pull request #545 from MikolasJanota/lackr
Lackr, should fix #544
2016-03-29 19:50:02 +01:00
Mikolas Janota 217c0419a1 Avoiding adding a superfluous unary AND in lackr. 2016-03-29 19:34:30 +01:00
Mikolas Janota 363f57a2f4 Silently bailing out on quantifiers in lackr. 2016-03-29 19:19:07 +01:00
Christoph M. Wintersteiger 1a65153872 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-03-29 16:37:36 +01:00
Christoph M. Wintersteiger 6be24b3201 Bugfix for FPA in solver.to_smt2
Fixes #541
2016-03-29 16:37:24 +01:00
Christoph M. Wintersteiger 19e73fb2ad whitespace 2016-03-29 16:13:31 +01:00
Christoph M. Wintersteiger 2eced4676f Merge pull request #539 from delcypher/cmake_dotnet_bindings
[CMake] Teach CMake to build .NET bindings
2016-03-29 13:56:35 +01:00
Christoph M. Wintersteiger 8709df27c5 Merge pull request #540 from martin-neuhaeusser/ocaml-install
Include *.cmx files during installation of OCaml bindings.
2016-03-29 13:27:10 +01:00
Dan Liew cc12b1ebce [CMake] The bug in mono that causes the `gacutil` utility to crash if
the assembly was compiled with ``/platform:x64`` has now been reported
so update the comments to reflect this.
2016-03-28 23:10:23 +01:00
Nikolaj Bjorner 7eec68c954 add handling for distinct to bit-blaster
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-28 11:22:54 -07:00
martin-neuhaeusser 28f9c61d76 Include *.cmx files during installation of OCaml bindings.
The *.cmx files are now installed using ocamlfind. They contain information from the
compiler that can be used during optimization (the upcoming OCaml 4.03.0 issues
warning 58 if those files are missing from a package).
2016-03-28 17:08:22 +02:00
Dan Liew c52c999393 [CMake] Document the `PYTHON_EXECUTABLE` CMake cache variable.
User's can use this to pick a different version of Python to use
for the build.
2016-03-27 15:04:22 +01:00
Dan Liew 20d3bf4d0c [CMake] Implement support for building the .NET bindings.
When using Mono support for installing/uninstalling the bindings
is also implemented. For Windows install/uninstall is not implemented
because the python build system does not implement it and Microsoft's
documentation (https://msdn.microsoft.com/en-us/library/dkkx7f79.aspx)
says that the gacutil should only be used for development and not for
production.

For now a warning is just emitted if ``INSTALL_DOTNET_BINDINGS``
is enabled and the .NET toolchain is native Windows. Someone with
better knowledge of how to correctly install assemblies under Windows
should implement this or remove this message.

A notable difference from the Python build system is the
``/linkresource:`` flag is not passed to the C# compiler. This means
a user of the .NET bindings will have to copy the Z3 library (i.e.
``libz3.dll``) to their application directory manually. The reason
for this difference is that using this flag requires the working
directory to be the directory containing the Z3 library (i.e.
``libz3.dll``) but setting this up with multi-configuration generators
doesn't currently seem possible.
2016-03-27 15:04:04 +01:00
Dan Liew 6a2a8e06d7 [CMake] Declare uninstall rule before the components so that they
can add dependencies to the rule for their own custom uninstall
logic.
2016-03-26 17:59:11 +00:00
Dan Liew 23ac66ef42 Fix inconsistent emission of `Enumerations.cs`. The ordering of emitted
enum values is not consistent between python 2 or 3. The root cause
of the problem was a dictionary's keys being iterated over which has
no defined order.

This has been fixed by iterating over the dictionary's items and
ordering by values.  We could order by key rather than the values but
seeing as these represent an enum, ordering by value makes more sense.
2016-03-26 17:59:11 +00:00
Dan Liew d3f87e44a2 Refactor `mk_z3consts_dotnet() code into mk_z3consts_dotnet_internal()`
and move that into ``mk_genfile_common.py``. Then adapt ``mk_util.py`` and
``mk_consts_files.py`` to call into the code at its new location.

The purpose of this change is to have Python code common to the Python
and CMake build systems separate from Python code that is only used for
the Python build system.
2016-03-26 17:59:11 +00:00
Nikolaj Bjorner 0870b4a5a0 add length coherence check for length = 0
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-25 17:17:34 -07:00
Nikolaj Bjorner f34a54fea0 fix stats collection over exceptions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-24 17:08:13 -07:00
Nikolaj Bjorner 808855ce6b add internalization for auxiliary division functions
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-24 16:20:42 -07:00
Nikolaj Bjorner 709a5d9524 fix bug: & -> &&
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2016-03-24 16:09:12 -07:00