mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity
13684 commits 49 branches 53 tags 182 MiB
Commit graph

1875 commits

Author SHA1 Message Date
Christoph M. Wintersteiger
3626d9f69f Bugfix for floating-point API. 
Fixes #358.
 2015-12-07 19:24:09 +00:00
Christoph M. Wintersteiger
2a0bbad524 Bugfix for ML API 2015-12-07 14:42:40 +00:00
Christoph M. Wintersteiger
cfc25b5094 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-07 13:14:00 +00:00
Nikolaj Bjorner
4550b7ed91 Merge branch 'master' of https://github.com/NikolajBjorner/z3 2015-12-07 03:27:04 +00:00
Andres Notzli
ced9ba17e9 Fix misc issues in Python API docstrings 2015-12-06 19:00:17 -08:00
Nikolaj Bjorner
b5fcbd7099 Merge branch 'mono_dotnet_bindings' of https://github.com/delcypher/z3-1 2015-12-06 13:51:43 -08:00
Dan Liew
c8a2b6645a Teach the build system to generate and install a pkg-config file for the 
".NET" bindings. This file is required for Monodevelop to find the
bindings because Monodevelop uses pkg-config to find packages
(it doesn't use the GAC).

For lack of a better name the GAC (and pkg-config) package name is now
``Microsoft.Z3.Sharp``. I don't want to call it ``Microsoft.Z3`` because
someone may want to create a ``Microsoft.Z3.pc`` file in the future for
the native Z3 library (i.e. C++ or C bindings).

In addition there is a new utility function ``configure_file()``
which reads a template file, applies some substitutions and writes
the result to another file. This very similar to what CMake does.

There is a new environment variable ``Z3_INSTALL_PKGCONFIG_DIR``
which allows pkgconfig directory to be controlled for the install.
 2015-12-05 07:52:31 +00:00
Dan Liew
61d1cd524e Teach the build system to build and install the ".NET bindings" 
under non Windows systems (i.e. Using mono).

Building these bindings is unfortunately on by default because
I didn't want to change the command line interface (i.e. ``--nodotnet``)
which people might be relying on. This should really be changed to
match the other binding flags (e.g. ``--java``) but I will leave
this for now.

To perform the build a C# compiler and the GAC utility are required.
The script will try to automatically detect them but the user can
override this by setting the ``CSC`` and ``GACUTIL`` environment
variables.

In order for the ".NET bindings" to be installed the assembly
(``Microsoft.Z3.dll``) needs to have a strong name which means
we need a Strong name key file which is what the
``Microsoft.Z3.mono.snk`` is for. This is the public and private
key so this key **must never** be used for checking integrity. Instead its
only purpose is to avoid any name clashes in the GAC.

It is also worth noting that slightly different flags needs to
be passed to the C# compiler on non Windows platforms. I don't
understand why some of the flags are being used on Windows but I left
a comment there that hopefully someone can fix...
 2015-12-05 07:52:31 +00:00
Christoph M. Wintersteiger
36a4828526 Whitespace 2015-12-03 17:55:31 +00:00
Christoph M. Wintersteiger
00271e5531 C API cleanup. Mainly removal of ML-specific macros that are not used anymore and inline documentation fixes. 2015-12-03 17:33:25 +00:00
Christoph M. Wintersteiger
d23dce4f7b Bugfix for finite domains in Python API. 2015-12-02 22:34:09 +00:00
Christoph M. Wintersteiger
b77f20fb0c Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-02 17:06:42 +00:00
Christoph M. Wintersteiger
2f86ab98a8 Added finite-domain expressions to the Python pretty printer 2015-12-02 17:04:06 +00:00
Christoph M. Wintersteiger
5510e0ddef Added finite-domain constant to Z3_decl_kind 2015-12-02 17:03:37 +00:00
Christoph M. Wintersteiger
5a43d8a469 Whitespace 2015-12-02 17:02:39 +00:00
Christoph M. Wintersteiger
cbda38ee80 Added finite domain expressions and numerals to the .NET, Java, and Python APIs. 
Relates to #318
 2015-12-02 17:01:52 +00:00
Nikolaj Bjorner
6580f1daf3 expose main interpolation routines in C++ API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-02 07:40:06 -08:00
Christoph M. Wintersteiger
9e756fb6db Warning fix for Comparable<T> in Java API 2015-12-02 14:42:36 +00:00
Christoph M. Wintersteiger
00ce124db3 Bugfix for Z3_is_numeral for finite-domain numerals. 
Relates to #318
 2015-12-02 14:41:46 +00:00
Christoph M. Wintersteiger
52bbd67cd3 Whitespace 2015-12-02 14:40:47 +00:00
Dan Liew
b0bc50a75c Fixed stray UTF-8 Byte order mark in `InterpolationContext.cs`. 
Old versions of the mono compiler don't like it.
 2015-11-30 15:02:02 +00:00
Christoph M. Wintersteiger
5e37cf9bbf Removed potentially unnecessary string decoding in Python API. 2015-11-23 18:41:31 +00:00
Nikolaj Bjorner
665af3d8b9 remove deprecated user-theory plugins and other unused functionality from API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-20 08:43:27 -08:00
Nikolaj Bjorner
fd8fd40669 fix tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-20 08:00:01 -08:00
Nikolaj Bjorner
1d4b996765 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-18 16:39:51 -08:00
Nikolaj Bjorner
9cba63c31f remove deprecated iz3 example. Remove deprecated process control 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-18 12:32:15 -08:00
Yan
4e9b76365d pass the correct context into And() when doing Tactic.as_expr() 2015-11-16 15:41:12 -08:00
Christoph M. Wintersteiger
e8d37dba9c Added comments for quantifier constructors. Fixes #319. 2015-11-16 21:58:17 +01:00
Christoph M. Wintersteiger
706a037bf4 Python 3.x string decoding fix 2015-11-16 15:16:50 +01:00
Nikolaj Bjorner
ab4033133f remove solver_old 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-14 18:46:49 -08:00
Nikolaj Bjorner
bea68cd194 remove deprecated API functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-14 17:05:15 -08:00
Nikolaj Bjorner
0f602d652a remove deprecated API functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-14 13:47:41 -08:00
Christoph M. Wintersteiger
15c48eeaf9 Fix for timeout/rlimit in deprecated solver API. 
Partially fixes #307.
 2015-11-13 16:42:46 +00:00
Christoph M. Wintersteiger
954400cfa2 whitespace 2015-11-13 16:35:08 +00:00
Nikolaj Bjorner
84f935ae85 initialize solver prior to translate. fixes build break 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-09 06:38:06 -08:00
Christoph M. Wintersteiger
689ed9fa12 Added Z3_mk_array_ext to ML API. 
Relates to #292
 2015-11-09 13:49:37 +00:00
Christoph M. Wintersteiger
cffff18373 -whitespace 2015-11-09 13:22:33 +00:00
Christoph M. Wintersteiger
6625f7a749 Added Z3_solver_translate to ML API. 2015-11-09 13:19:10 +00:00
Nikolaj Bjorner
e9315af0d9 remove tabs from z3.py to fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-08 04:22:44 -08:00
Nikolaj Bjorner
4685a5f8ba add array-ext to externally exposed functions to enable interpolants with arrays to be usable in feedback loops with Z3. Addresses one issue raised in #292 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-07 16:42:13 -08:00
Nikolaj Bjorner
13b19eb351 add translate facility to Java/C# APIs, request #209 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-07 10:10:21 -08:00
Nikolaj Bjorner
b4cb51cdb3 working on Forking/Serializing a z3 Solver #209 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-11-06 17:29:24 -08:00
Nikolaj Bjorner
63ea2c4d8f Merge pull request #295 from pazz/AstRef-hash 
add __hash__ to AstRef
 2015-11-05 16:20:10 -08:00
Patrick Totzke
d4242e16c5 add __hash__ to AstRef 
AstRef objects needs to be hashable in order
to be used as keys in python dictionaries
 2015-11-05 16:28:02 +00:00
Christoph M. Wintersteiger
715050da0b Java API comments fix. 2015-11-04 13:34:50 +00:00
Nikolaj Bjorner
b75780ce2b Merge pull request #280 from NikolajBjorner/master 
Add PB operators to Python API
 2015-10-30 14:15:24 -07:00
Nikolaj Bjorner
d83f8d08f3 Merge pull request #276 from kenmcmil/issue260 
issue #260 -- support timeout in Z3_compute_interpolant
 2015-10-28 20:30:15 -07:00
Ken McMillan
d4dff70f39 issue #260 -- support timeout in Z3_compute_interpolant 2015-10-28 18:02:14 -07:00
Nikolaj Bjorner
559f373588 adding PB operators to Python API. remove tabs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-28 17:13:24 -07:00
Nikolaj Bjorner
7f5495b134 adding PB operators to Python API 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-10-28 17:09:42 -07:00