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

4352 commits

This branch
This branch
All branches
Author SHA1 Message Date
Dan Liew 0a8cd3ae19 Refactor the install and uninstall commands for the python bindings 
out of ``DLLComponent`` and into ``PythonInstallComponent`` where they
belong.
 2015-12-08 23:10:48 +00:00
Dan Liew 38b45919b5 Unbreak running `make install. The python site-package` directory 
was not created before trying to create files in it.

The ``install_deps()`` method was also dead. It looks like that
should have been named ``mk_install_deps()`` but even if we give it
the right name it does the wrong thing. That method is supposed
emit target names (i.e. dependencies) not commands.
 2015-12-08 23:10:48 +00:00
Dan Liew e2546d2b95 Refactor references to `pythonPkgDirWithoutPrefix` to a object 
attribute.
 2015-12-08 23:08:23 +00:00
Christoph M. Wintersteiger 83db19654f refactored ocamlfind_install target 2015-12-08 18:57:17 +00:00
Nuno Lopes 4b0f2cae0d fix compiler warning in scoped_timer.cpp on linux 
2 secs in nanosec representation still fit in 31 bits, so no need for ULL

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2015-12-08 17:03:18 +00:00
Christoph M. Wintersteiger ea79d0eacd Bugfix for Python installation on linuxes 2015-12-08 13:45:55 +00:00
Nikolaj Bjorner ca96fea2c0 add seq methods 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-07 16:28:20 -08:00
Nikolaj Bjorner d9fee9af1e Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-07 15:01:56 -08:00
Nikolaj Bjorner a9f5c2f864 seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-07 15:01:46 -08:00
Christoph M. Wintersteiger f6a10b0b82 tabs 2015-12-07 19:28:04 +00:00
Christoph M. Wintersteiger 3626d9f69f Bugfix for floating-point API. 
Fixes #358.
 2015-12-07 19:24:09 +00:00
Nikolaj Bjorner 34a0d7dfed remove python_install target from all 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-07 09:59:46 -08: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 03d1391ded merge seq and string operators 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-06 23:37:37 -08:00
Nikolaj Bjorner 8bb73c8eae merge seq and string operators 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-06 23:34:28 -08:00
Nikolaj Bjorner 70b10d53cf fix build break - remove tabs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-06 22:17:36 -08:00
Nikolaj Bjorner 4944035c0a Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-06 22:16:50 -08:00
Nikolaj Bjorner 08bfd08412 merging seq and string 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-06 22:15:56 -08:00
Nikolaj Bjorner 64b9a301ed add python visitor example in response to Stackoverflow question 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-06 20:09:13 -08:00
Nikolaj Bjorner 90a7f5a4a1 Merge pull request #356 from NikolajBjorner/master 
facilities for proper python installation thanks to delcypher
 2015-12-06 19:37:30 -08:00
Nikolaj Bjorner e1ab2370e1 fix python w.o. proper intallation, #338, #340 
Signed-off-by: Nikolaj Bjorner <nbjorner@z3-mac.local>
 2015-12-07 03:32:58 +00:00
Nikolaj Bjorner 78f44c30a7 Merge branch 'master' of https://github.com/NikolajBjorner/z3 2015-12-07 03:28:53 +00:00
Nikolaj Bjorner 92a4ac9eb7 make dotnet optional and recover from python installation mismatch. Pull requests #338, #340 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-06 19:28:39 -08:00
Nikolaj Bjorner 4550b7ed91 Merge branch 'master' of https://github.com/NikolajBjorner/z3 2015-12-07 03:27:04 +00:00
Nikolaj Bjorner febd83912e make dotnet optional and recover from python installation mismatch. Pull requests #338, #340 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-06 19:25:18 -08:00
Nikolaj Bjorner a940230301 make dotnet optional and recover from python installation mismatch. Pull requests #338, #340 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-06 19:14:53 -08:00
Nikolaj Bjorner aead45a252 make dotnet optional and recover from python installation mismatch. Pull requests #338, #340 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-06 19:14:31 -08:00
Nikolaj Bjorner 6c73c176b3 make dotnet optional and recover from python installation mismatch. Pull requests #338, #340 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-06 19:10:11 -08:00
Nikolaj Bjorner 63429cc862 Merge pull request #355 from 4tXJ7f/master 
Fix misc issues in Python API docstrings
 2015-12-06 19:02:30 -08: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
Nikolaj Bjorner 4ec6bc0825 Merge branch 'better_packaging' of https://github.com/delcypher/z3-1 2015-12-06 12:31:55 -08:00
Nikolaj Bjorner 89fe24342d fix size_t mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-06 11:06:58 -08:00
Nikolaj Bjorner 40e9e4c7f8 more rewrites 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-06 10:44:19 -08:00
Nikolaj Bjorner 4fe0e07080 indexof 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-05 16:36:11 -08:00
Nikolaj Bjorner 5296009f46 ground string rewriting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-05 15:38:54 -08:00
Nikolaj Bjorner 75359c580e add basic rewriting to strings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-05 12:02:33 -08:00
Nikolaj Bjorner c04f75cdbb fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-05 10:30:08 -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
Dan Liew 6884d3a245 Fix references to non existent function and variable due to a refactor 
in 041c02feb7. Spotted by @NikolajBjorner
 2015-12-05 07:50:33 +00:00
Nikolaj Bjorner b77e387265 value 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-04 15:26:53 -08:00
Nikolaj Bjorner a8e366aa24 add basic string factory 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-04 15:24:29 -08:00
Nikolaj Bjorner 75c935a4cb add tokens to parse strings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-04 12:09:15 -08:00
Christoph M. Wintersteiger 4c22a66094 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-04 17:52:59 +00:00
Nikolaj Bjorner 4bbe1d4674 remove unused min-aggregate 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-04 09:23:36 -08:00
Nikolaj Bjorner 3f02beb820 reset-assertions resets everything (also declarations, and we take scopes) when global-declarations is false. v2.5 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2015-12-03 10:18:40 -08:00
Nikolaj Bjorner 8e5dec882b Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-03 10:01:41 -08:00
Christoph M. Wintersteiger 36a4828526 Whitespace 2015-12-03 17:55:31 +00:00