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

7581 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Murphy Berzish
e010e7c0d6 add trace message to indicate which free variables are giving us trouble 
I think I'm onto the issue though
 2015-12-02 23:35:26 -05:00
Nikolaj Bjorner
b6b5065571 Merge pull request #351 from NikolajBjorner/master 
adding SMT2.5 features
 2015-12-02 19:24:50 -08:00
Murphy Berzish
f5e94af784 check that both simplified expressions are concats in simplify_concat_equality() 
this seems to fix all the crashes but the solver takes forever to solve a really simple instance
with easy model generation, so I think something is still wrong
probably next I will go through and change std::map to obj_map, etc.
 2015-12-02 22:15:04 -05: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
Murphy Berzish
1a15b3937d in_same_eqc() now checks to ensure both terms are internalized before doing anything else 2015-12-02 22:09:30 -05:00
Murphy Berzish
23150d3b5e never ever ever reuse constants in mk_string(). this gets us MUCH farther 2015-12-02 22:03:12 -05: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
Murphy Berzish
953a4c5437 add temporary variables to m_trail 2015-12-02 20:48:15 -05: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
Murphy Berzish
52f0277c99 attempt to clean up out-of-scope variables more, still crashing 2015-12-01 19:19:00 -05: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
Murphy Berzish
c44d49b625 keep track of search level ourselves 2015-12-01 14:41:11 -05:00
Murphy Berzish
dd0bc13be7 attempt to track popped variables, still segfaults, WIP 2015-11-30 19:22:01 -05: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
Murphy Berzish
07626a1e03 remove expr_ref stuff, start tracking variables more closely 2015-11-28 23:56:30 -05: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
Dan Liew
53f0addb6b Avoid making a copy of libz3 on non Windows platforms for the 
Python bindings (provided they both exist within the same install
prefix) by creating a relative symbolic link. This saves
space when packaging Z3.
 2015-11-28 19:03:05 +00:00
Dan Liew
e8822b1806 Add a note about using DESTDIR when building Z3 completes. 2015-11-28 19:03:05 +00:00