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

4713 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 3ef6d91038 fix #434: repeat documentation remarks about reference counting for disambiguation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-07 14:46:53 +00:00
Nikolaj Bjorner 677b4bf4fe fix #436, adding more length-based propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-07 14:43:53 +00:00
Nikolaj Bjorner fc1f37efc9 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-06 16:14:07 +00:00
Nikolaj Bjorner 5b50d98b89 ensure that seq rewriter gets invoked during pre-processing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-06 16:13:31 +00:00
Christoph M. Wintersteiger b61376e8c2 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-05 15:22:42 +00:00
Christoph M. Wintersteiger 7ddd2856c8 Added is_considered_uninterpreted() to decl_plugins. 2016-02-05 15:22:37 +00:00
Christoph M. Wintersteiger 3d37c25bcc whitespace 2016-02-05 15:16:54 +00:00
Christoph M. Wintersteiger c11b6d90ce whitespace 2016-02-05 15:16:19 +00:00
Christoph M. Wintersteiger 757585d96f Merge pull request #427 from jwakely/patch-1 
Convert stream to bool explicitly
 2016-02-05 15:08:33 +00:00
Christoph M. Wintersteiger 394b66bc92 Merge pull request #437 from delcypher/fix_custom_build_dir 
Fix the behaviour of  ``--build``
 2016-02-05 15:07:44 +00:00
Dan Liew 508d2e32c8 Fix a bug in Python build scripts where an extra ending slash in the 
build directory would cause REV_BUILD_DIR to be set incorrectly and
would lead to a broken Makefile being generated.

What would happen before:

```
$ python scripts/mk_make.py --build FOO_1
...
REV_BUILD_DIR='..'
```

```
$ python scripts/mk_make.py --build FOO_1/
...
REV_BUILD_DIR='../..'
```
^^^^^ that's wrong. It should be REV_BUILD_DIR='..'

To fix this the ``reverse_path()`` function has been taught to ignore empty
components in ``p.split(os.sep)``.
 2016-02-05 14:51:15 +00:00
Dan Liew 33f676ef6b Do not hardcode default build directory name. 2016-02-05 14:39:27 +00:00
Dan Liew 6112ea2ec7 Fix typo 2016-02-05 14:38:41 +00:00
Christoph M. Wintersteiger ac19bfb032 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-05 13:53:41 +00:00
Christoph M. Wintersteiger bb5118acbb Bugfix for bv*div0 model construction. 2016-02-05 13:53:35 +00:00
Christoph M. Wintersteiger 88f007e9da whitespace 2016-02-05 13:48:47 +00:00
Christoph M. Wintersteiger b87f4ca677 whitespace 2016-02-05 13:48:05 +00:00
Christoph M. Wintersteiger 21b85c27e1 whitespace 2016-02-05 13:47:14 +00:00
Nikolaj Bjorner eae17a43a2 Fix #430: disable rewriting of concatentations with constants because it breaks equality propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-05 11:00:17 +00:00
Nikolaj Bjorner cf970fd76a Fix #430: disable rewriting of concatentations with constants because it breaks equality propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-05 10:59:24 +00:00
Nikolaj Bjorner 2a65503235 fix #425 and report from Patrick Trentin of same bug in preprocessing soft constraints that are simplified to true/false 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-04 22:35:02 +00:00
Nikolaj Bjorner 768bb84798 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-04 08:12:56 -08:00
Nikolaj Bjorner 9c7e5c37d1 add equality propagation based on partial length information to sequence theory. Fix issue #429 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-04 08:12:46 -08:00
Christoph M. Wintersteiger 4e37821dde "canceled" -> Z3_CANCELED_MSG 
Relates to #431
 2016-02-04 13:52:43 +00:00
Jonathan Wakely f02d273ee3 Convert stream to bool explicitly 
In C++11 there is no implicit conversion from iostream classes to `void*`, just an explicit conversion to bool.
 2016-02-02 23:39:11 +00:00
Nikolaj Bjorner 9b979b6e1e more string optimizations based on Chris' examples 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-01 17:08:11 -08:00
Nuno Lopes 16a69e750a fix break in configure 2016-02-01 17:38:14 +00:00
Nuno Lopes ea55bd495f add new API function Z3_get_estimated_alloc_size() that returns *estimated* allocated memory size by Z3 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2016-02-01 17:19:55 +00:00
Nuno Lopes b9c0578eea fix build on C++98 compilers 2016-02-01 17:12:22 +00:00
Nikolaj Bjorner fe6799699c Merge branch 'master' of https://github.com/Z3Prover/z3 2016-02-01 07:51:26 -08:00
Nikolaj Bjorner 995a2e1a29 perf tuning based on Chris's examples 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-02-01 07:51:05 -08:00
Nuno Lopes cc6769c866 improve bit-blasting for the case (bvsrem var power-of-two) 
We will now transform bvsrem into an extract + zero extend
Gives ~40% speedup in selected benchmarks

Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2016-02-01 13:46:55 +00:00
Nikolaj Bjorner 2115111dac update display method for datalog to use predicates, throttle use of extensionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-28 20:23:06 -08:00
Nikolaj Bjorner 847607bda7 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-28 08:51:40 -08:00
Nikolaj Bjorner 30f8110488 fix bugs exposed by Chris' sequence unit tests. Improve diagnostics for reason-unknown in combined solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-28 08:51:04 -08:00
Nikolaj Bjorner b352d43e50 fix bugs exposed by Chris' sequence unit tests. Improve diagnostics for reason-unknown in combined solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-28 08:50:13 -08:00
Christoph M. Wintersteiger 20df9e1cd1 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-28 11:14:11 +00:00
Christoph M. Wintersteiger 5f0ea74e89 Made ufbv-rewriter tactic public 2016-01-28 11:14:01 +00:00
Nikolaj Bjorner 512aa0e8d3 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-27 14:47:24 -08:00
Nikolaj Bjorner 87228b6a9d add a little more verbiage to description of simplify. Issue #424 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-27 14:47:15 -08:00
Nuno Lopes ac2e8f8b57 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-27 18:09:36 +00:00
Nuno Lopes ee2bae898a remove unused exceeded_memory_allocations class 2016-01-27 18:09:24 +00:00
Nikolaj Bjorner 6529d43fb1 fix bugs exposed by unit tests from Pierre 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-26 09:50:14 -08:00
Nikolaj Bjorner 8e378062e2 add get-some-value to seq API, expose quantifier tactics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-26 08:05:44 -08:00
Nikolaj Bjorner 345f6e87bd seq bug fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-26 07:21:31 -08:00
Nikolaj Bjorner 924f03c6de fixing bugs in seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-23 10:38:49 -05:00
Nikolaj Bjorner 993a0434b4 fix warning message for unused variable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-19 23:47:35 -05:00
Nikolaj Bjorner 099e572a26 Merge branch 'master' of https://github.com/Z3Prover/z3 2016-01-19 19:10:08 +01:00
Nikolaj Bjorner a021e51a9c make parse error a bit more informative 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2016-01-19 19:09:41 +01:00
Nuno Lopes 23cc8258fe remove m_ast_lim from API context since that one isn't used either 
Signed-off-by: Nuno Lopes <nlopes@microsoft.com>
 2016-01-19 15:37:58 +00:00