3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Commit graph

4466 commits

Author SHA1 Message Date
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
Nikolaj Bjorner a4d9642cf2 parsing of SMT 2.5 style string literals
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-03 09:46:18 -08: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 2c6645ef2d Python 3.x issues 2015-12-03 13:57:29 +00:00
Nikolaj Bjorner b6b5065571 Merge pull request #351 from NikolajBjorner/master
adding SMT2.5 features
2015-12-02 19:24:50 -08:00
Nikolaj Bjorner 5d61c871b0 add some of the SMT2.5 features
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-02 19:14:47 -08:00
Nikolaj Bjorner e9a2b7f9f0 Merge branch 'master' of https://github.com/Z3Prover/z3 2015-12-02 18:41:22 -08:00
Nikolaj Bjorner e2565d8d82 add some of the SMT2.5 features
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-02 18:41:10 -08: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
Nikolaj Bjorner 216c1b2989 Merge pull request #349 from NikolajBjorner/master
add macro for converting std::vectors to pointers (leaking abstraction)
2015-12-01 18:36:16 -08:00
Nikolaj Bjorner 485ac9c39d add macro for converting std::vectors to pointers (leaking abstraction)
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-01 16:35:03 -08:00
Nikolaj Bjorner 2916f14b40 Merge pull request #347 from NikolajBjorner/master
bind variables in queries generated from Horn tactic to enforce that …
2015-12-01 14:49:08 -08:00
Nikolaj Bjorner b3e8020c88 bind variables in queries generated from Horn tactic to enforce that rule formulas don't contain free variables. Issue #328
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-01 14:47:33 -08:00
Nikolaj Bjorner 388b4b6eb7 Merge pull request #346 from NikolajBjorner/master
bugfix for #343
2015-12-01 13:46:08 -08:00
Nikolaj Bjorner aa777bd5c6 Fix for #343. Optimizations introduced on 8-10-2015 were too agressive. Remove unreferened variable
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-01 13:43:47 -08:00
Nikolaj Bjorner 9fa4bf2f8f Fix for #343. Optimizations introduced on 8-10-2015 were too agressive
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2015-12-01 13:41:57 -08:00
Nikolaj Bjorner f68c1d755f Merge pull request #344 from delcypher/fix_stray_uft8_bom
Fixed stray UTF-8 Byte order mark in ``InterpolationContext.cs``.
2015-12-01 05:21:00 +13: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
Nuno Lopes 5d289a8da5 fix leak in asserted_formulas::propagate_values() for proof generation mode
continuation of issue #342

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
2015-11-29 10:49:52 +00:00
Dan Liew d2ba6f0ebf Provide a way to customise the install directories via environment
variables:

Z3_INSTALL_BIN_DIR - defaults to "bin"
Z3_INSTALL_LIB_DIR - defaults to "lib"
Z3_INSTALL_INCLUDE_DIR - defaults to "include"

This has two advantages

* We no longer hard code strings like "bin" all over the place
* Packagers can easily control where things get installed.
2015-11-28 19:11:03 +00:00
Dan Liew d205b176e8 Bug fix for `MakeRuleCmd.create_relative_symbolic_link()`.
create_relative_symbolic_link(out, '/usr/lib64/libz3.so',
'/usr/lib/python3.5/site-package/libz3.so') would create an incorrect relative
path because it would consider ``/usr/lib`` to a be a path prefix of
``/usr/lib64``.
2015-11-28 19:03:05 +00:00
Dan Liew f1d4f36ddf Refactor the use of `$(DESTDIR)$(PREFIX) in MakeRuleCmd`
class so that it is exposed via a public method (``install_root()``)
so that is can be used externally. Also refactor the existing methods
to use it.
2015-11-28 19:03:05 +00:00
Dan Liew 32c4384d48 Fix dead comment and expand on the reasons for making a symbolic link
slightly.
2015-11-28 19:03:05 +00:00
Dan Liew 684318149b Remove dead code that I accidently left behind. 2015-11-28 19:03:05 +00:00
Dan Liew 6984070b3a Fix typo (missing argument) that I missed that didn't fire because
I did not test on Windows.
2015-11-28 19:03:05 +00:00
Dan Liew d6fa0583ab Fix bug in `ExeComponent.mk_uninstall()` in the build system
which would try to uninstall components that were never installed.

This bug would cause the following line to be emitted in the
``Makefile`` under the ``uninstall`` rule even though there was
no corresponding rule to install the file under the ``install`` rule.

```
@rm -f $(DESTDIR)$(PREFIX)/bin/test-z3$(EXE_EXT)
```
2015-11-28 19:03:05 +00:00
Dan Liew 041c02feb7 Finish addressing @wintersteiger comments on `$(DESTDIR)` being
duplicated in too many places by refactoring the installation and
removal of the Python bindings to use the ``MakeRuleCmd`` class.

In order to make this change:

* ``PYTHON_PACKAGE_DIR`` no longer contains the text ``$(PREFIX)``
* ``PYTHON_PACKAGE_DIR`` **MUST BE** inside the installation prefix
2015-11-28 19:03:05 +00:00
Dan Liew 23cf7e86a9 Start to address @wintersteiger 's comments aboug `$(DESTDIR)` being
duplicated in too many places and being worried that someone might
forget to use it when installing additional components.

To acheive this the new ``MakeRuleCmd`` class provides
several class methods to generate commonly needed commands used in
make file rules.

Most of the build system has been changed to use these helper methods
apart from stuff related to the Python bindings. This can't be changed
until we fix how PYTHON_PACKAGE_DIR is handled. Right it not guaranteed
to live under the install prefix but this is a requirement when using
the ``MakeRuleCmd`` methods.
2015-11-28 19:03:05 +00:00