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

7840 commits

This branch
This branch
All branches
Author SHA1 Message Date
Murphy Berzish a9fda81d03 check polarity 2018-01-18 17:53:42 -05:00
Murphy Berzish 5727950a3c zero-length automaton solution fix 2018-01-18 17:52:55 -05:00
Murphy Berzish dbb15f65b5 correct generation of linear length constraints for regex star terms 2018-01-17 19:26:42 -05:00
Murphy Berzish c2b268c645 short path for length-0 regex terms 2018-01-17 18:26:31 -05:00
Murphy Berzish c0ed683882 disable regex length constraint generation as it currently makes unsound axioms 2018-01-17 13:32:44 -05:00
Murphy Berzish 26ab91a448 check duplicate bounds info for regex terms 2018-01-17 13:02:32 -05:00
Murphy Berzish e5585ecf4c regex fail count and automaton fallback 2018-01-16 18:15:29 -05:00
Murphy Berzish 153701eabe regex length term assertion WIP 2018-01-16 13:56:01 -05:00
Murphy Berzish 6c4c9a10e4 regex length linearity check WIP 2018-01-16 13:16:31 -05:00
Murphy Berzish 191cc30e2a intersection of regex constraints produces a conflict clause 2018-01-15 15:30:12 -05:00
Murphy Berzish 058d24fd09 reuse regex character constraints for the same string 2018-01-15 14:30:12 -05:00
Murphy Berzish 6f889ab699 intersection WIP; fix polarity of generated path constraint LHS 2018-01-15 14:08:15 -05:00
Murphy Berzish ca3784449f regex failsafe and intersect WIP 2018-01-12 13:53:02 -05:00
Murphy Berzish 6b799706b5 add path constraint generation for regex terms 2018-01-10 17:24:47 -05:00
Murphy Berzish bac5a648d9 regex path constraint generation (WIP) 2018-01-09 20:20:04 -05:00
Murphy Berzish 98691a2c49 lower bound refinement 2018-01-08 15:56:21 -05:00
Murphy Berzish 09dc5cd0f8 Merge branch 'develop' into regex-develop 2018-01-03 16:12:33 -05: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
Murphy Berzish 0f20944aeb regex lower bound (WIP) 2018-01-03 13:54:18 -05:00
Murphy Berzish 0917af7c56 full upper bound refinement 2018-01-03 12:02:11 -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