mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity
5165 commits 23 branches 48 tags 157 MiB
Commit graph

5165 commits

This branch
This branch
All branches
Author SHA1 Message Date
Mikolas Janota 7ad9dec6c2 Adding cpp files for bv_trailing to CMakeLists. 2016-04-06 11:04:17 +01:00
Mikolas Janota dbffc15b98 Improvements in caching of bv_trailing. 2016-04-06 11:04:15 +01:00
mikolas 9ba5bbfd33 Re-factoring and comments in bv_trailing. 2016-04-06 11:04:13 +01:00
Mikolas Janota 248feace34 fixing the behavior in bv_trailing 2016-04-06 11:04:11 +01:00
mikolas fced47386e More work on trailing 0 analysis. 2016-04-06 11:04:09 +01:00
mikolas ddb6ae4eab More work on trailing 0 analysis. 2016-04-06 11:04:07 +01:00
mikolas 78cb1e3c7b More work on trailing 0 analysis. 2016-04-06 11:04:05 +01:00
mikolas c7f1746321 Starting to work on trailing 0 analysis. 2016-04-06 11:04:03 +01:00
Nikolaj Bjorner 493b86eca7 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-04-05 22:27:11 +02:00
Nikolaj Bjorner b97d694e5e undo model evaluation to BR_FULL pending regression in assertion violation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-04-05 22:26:57 +02:00
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
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
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
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 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 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