mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity
7825 commits 23 branches 48 tags 157 MiB
Commit graph

7825 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
450f3c9b45 Merge branch 'master' of https://github.com/z3prover/z3 2018-01-12 19:29:56 -08:00
Nikolaj Bjorner
5159291d57 add missing interpreted tail during bottom-up simplification #1452 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-12 19:29:42 -08:00
Christoph M. Wintersteiger
cfdde2f4d1 Added apply_result::as_expr to the C++ API. Requested here: https://stackoverflow.com/questions/48071840/get-result-of-tactics-application-as-an-expression-in-z3 2018-01-08 13:24:52 +00:00
Nikolaj Bjorner
1992749e78 to ascii or not to ascii #1447 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-07 18:52:00 -08:00
Nikolaj Bjorner
e7851a0637 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-07 18:32:31 -08:00
Nikolaj Bjorner
482738bc8a avoid reset_error in dec_ref in bv_val #1443. Add BSD required template instance #1444 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-07 15:51:45 -08:00
Nikolaj Bjorner
711023d557
Merge pull request #1440 from mtrberzi/develop 
Make linear search the default for theory_str
 2018-01-03 13:22:39 -08:00
Murphy Berzish
a5180edc76 make linear search the default for theory_str 2018-01-03 16:05:34 -05:00
Murphy Berzish
83230f944a Merge remote-tracking branch 'upstream/master' into develop 2018-01-03 13:56:18 -05:00
Nikolaj Bjorner
6a4f269563
Merge pull request #1438 from delcypher/cmake_old_glibc_librt 
[CMake] Fix #1437
 2018-01-03 08:41:15 -08:00
Dan Liew
e9be339d9d [CMake] Fix #1437. 
The `clock_gettime()` function in glibc < 2.17 required linking against
librt. Until #1437 nobody had tried using the CMake build system with
a really old version of glibc (in this case 2.12).

The python build system always linked against librt but the CMake build
system never tried to link against it leading to link failures.

This patch teaches the CMake build system to detect if librt is required
when linking against `clock_gettime()` and adds `rt` as a link
dependency if necessary.
 2018-01-03 12:50:42 +00:00
Nikolaj Bjorner
ad15b75dc4
Merge pull request #1436 from waywardmonkeys/noreturn-attribute 
Use noreturn attribute and __declspec version.
 2018-01-02 10:38:59 -08:00
Bruce Mitchener
11f5fdccdf Use noreturn attribute and __declspec version. 2018-01-03 01:02:07 +07:00
Nikolaj Bjorner
16044c74bf revert use of [[noreturn]]. It's not fully supported on compilers #1435 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-02 09:29:14 -08:00
Nikolaj Bjorner
7457fa77cb add noreturn attribute #1435 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-02 08:46:17 -08:00
Nikolaj Bjorner
19e12bbc62
Merge pull request #1435 from waywardmonkeys/raise_exception_doesnt_return 
raise_exception: Annotate that this doesn't return.
 2018-01-02 08:26:44 -08:00
Bruce Mitchener
b06f413585 raise_exception: Annotate that this doesn't return. 2018-01-02 23:20:00 +07:00
Nikolaj Bjorner
b363aa3e35
Merge pull request #1433 from waywardmonkeys/remove-ignored-qualifiers 
Remove ignored const qualifiers.
 2018-01-02 08:18:15 -08:00
Nikolaj Bjorner
8eecafaf05
Merge pull request #1434 from waywardmonkeys/formatting-fix 
Fix code formatting: Incorrect indentation.
 2018-01-02 08:16:35 -08:00
Nikolaj Bjorner
714b086ced
Merge pull request #1432 from waywardmonkeys/remove-copy-of-coeff 
Remove unnecessary copy of coeff in iteration.
 2018-01-02 08:16:01 -08:00
Bruce Mitchener
5a0f5a778f Remove unnecessary copy of coeff in iteration. 2018-01-02 23:14:29 +07:00
Bruce Mitchener
11db778442 Remove ignored const qualifiers. 
The `const` qualifier on a scalar value is ignored in return types.
 2018-01-02 23:12:34 +07:00
Bruce Mitchener
a5a31fc23c Fix code formatting: Incorrect indentation. 2018-01-02 23:11:36 +07:00
Nikolaj Bjorner
f5bba63674
Merge pull request #1431 from waywardmonkeys/typo-fixes 
Typo fixes.
 2018-01-02 07:56:31 -08:00
Nikolaj Bjorner
a302832917
Merge pull request #1430 from waywardmonkeys/double-promotion-fix 
print_stat_f: Remove implicit conversion of float to double.
 2018-01-02 07:55:13 -08:00
Nikolaj Bjorner
a875d3e491 fix #1429 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-02 07:54:31 -08:00
Bruce Mitchener
a3ad0aff8b print_stat_f: Remove implicit conversion of float to double. 2018-01-02 22:50:50 +07:00
Bruce Mitchener
73b3da37d8 Typo fixes. 2018-01-02 22:48:06 +07:00
Nikolaj Bjorner
e8a9e1a58b set default rewriter behavior in incremental mode to distribute multiplication over addition #1373 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-01 20:04:55 -08:00
Nikolaj Bjorner
c1c1b7378c removing axiom exposing unsoundness, replace by weaker axiom 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-01 19:44:16 -08:00
Nikolaj Bjorner
f0a30ded7d add shorthand for translating models #1407 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-01 19:25:09 -08:00
Nikolaj Bjorner
8dadd30db5 add __copy__, __deepcopy__ as alias to translate on same context #1427. Add generalized Gaussian elimination as an option to first-pass NL solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-01-01 17:11:43 -08:00
Nikolaj Bjorner
b78c538e02 fix build of test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-30 22:58:41 -08:00
Nikolaj Bjorner
c7d534160e Merge branch 'master' of https://github.com/z3prover/z3 2017-12-30 20:35:48 -08:00
Nikolaj Bjorner
79a9dfd8fd adding pre-processing to nlsat for equations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-30 20:35:33 -08:00
Nikolaj Bjorner
4c949cdbac Merge branch 'master' of https://github.com/z3prover/z3 2017-12-27 10:10:26 -08:00
Nikolaj Bjorner
d86e8f02d7 fix get-objectives error #1419 message (get-objectives) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-27 10:09:22 -08:00
Nikolaj Bjorner
5bc4c9809e initialize additional assumptions after setup_context is called the first time 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-25 12:50:11 -08:00
Nikolaj Bjorner
36204fafa0 alternate strategies for QF_NIA 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-19 20:27:08 -08:00
Nikolaj Bjorner
517b081202 remove custom exception, perhaps this handles exception issue 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-18 21:13:03 -08:00
Nikolaj Bjorner
d80c4307a6
Merge pull request #1410 from bannsec/assertion_slices 
Allowing slices and negative index in assertions
 2017-12-18 17:07:09 -08:00
Nikolaj Bjorner
13ee8da659 add virtual destructor to see if this helps ASan error 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-18 15:57:16 -08:00
bannsec
d695767f61 Allowing slices and negative index in assertions 2017-12-18 21:48:54 +00:00
Nikolaj Bjorner
94d1695b01 Merge branch 'master' of https://github.com/z3prover/z3 2017-12-18 12:20:53 -08:00
Nikolaj Bjorner
399b27fda3 add Python facility for int2bv, fix #1398 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-18 12:20:44 -08:00
Christoph M. Wintersteiger
c3c06d756c Documentation fixes. 2017-12-18 20:12:19 +00:00
Christoph M. Wintersteiger
63951b815d Bumped version number. 2017-12-18 18:58:21 +00:00
Christoph M. Wintersteiger
b0aaa4c6d7 Updated release notes 2017-12-18 14:18:30 +00:00
Nikolaj Bjorner
c3add4eeda add back missing initialization of lo 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-15 06:56:36 -08:00
Nikolaj Bjorner
21f685fa5a fix nlsat regression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-15 06:54:02 -08:00