mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-04 20:05:40 +00:00
Code Activity
7879 commits 40 branches 51 tags 168 MiB
Commit graph

1206 commits

Author SHA1 Message Date
Bruce Mitchener
7bf80c66d0 Remove redundant void arg. 
While this was needed in ANSI C, it isn't in C++ and triggers a warning
in clang-tidy when `modernize-redundant-void-arg` is enabled.
 2018-02-13 18:51:52 +07:00
Bruce Mitchener
76eb7b9ede Use nullptr. 2018-02-12 14:05:55 +07:00
Bruce Mitchener
7167fda1dc Use override rather than virtual. 2018-02-10 09:56:33 +07:00
Bruce Mitchener
b7d1753843 Use override rather than virtual. 2018-02-09 21:19:27 +07:00
Nikolaj Bjorner
2b847478a2
Merge pull request #1478 from waywardmonkeys/unnecessary-value-param-fixes 
Remove unnecessary value parameter copies.
 2018-02-09 02:20:47 -08:00
Bruce Mitchener
757b7c66ef Remove unnecessary value parameter copies. 2018-02-09 16:35:34 +07:00
Bruce Mitchener
50f3e9c3c0 Fix typos. 2018-02-09 16:35:26 +07:00
Nikolaj Bjorner
3f7453f5c5 fixing build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-07 20:23:31 -08:00
Nikolaj Bjorner
61934d8106 align semantics of re.allchar with string proposal. #1475 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-07 20:08:15 -08:00
Nikolaj Bjorner
9d37257059
Merge pull request #1465 from waywardmonkeys/fix-typos 
thanks
 2018-02-05 18:31:09 -08:00
Nikolaj Bjorner
3e810d6c54 remove static from format (not thread safe), remove std::move #1466 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-02-05 16:46:49 -08:00
Nikolaj Bjorner
2853558bc2
Merge pull request #1466 from waywardmonkeys/reduce-copying 
Use const refs to reduce copying.
 2018-02-05 16:37:44 -08:00
Christoph M. Wintersteiger
333374229d Fixed UFs for unspecified cases of FP conversion operators. Thanks for Youcheng Sun for reporting this bug. 2018-02-03 16:48:05 +00:00
Christoph M. Wintersteiger
c3ed986031 Fixed RNA FP rounding mode semantics. Fixes #1190 and bugs reported by Youcheng Sun. 2018-02-03 16:46:21 +00:00
Christoph M. Wintersteiger
8689921e9c Fixed missing bit of precision in fp.to_ubv/fp.to_sbv. Thanks to Youcheng Sun for reporting this bug. 2018-02-03 15:16:23 +00:00
Christoph M. Wintersteiger
ad3b0ecad0 Fixed pattern rewriting to produce only valid patterns (which led to a segfault). Bug reported by Youcheng Sun. 2018-02-02 19:27:36 +00:00
Bruce Mitchener
ae8027e594 Fix typos. 2018-02-01 19:39:43 +07:00
Bruce Mitchener
177414c0ee Use const refs to reduce copying. 
These are things that have been found by `clang-tidy`.
 2018-01-30 21:43:56 +07: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
Bruce Mitchener
b06f413585 raise_exception: Annotate that this doesn't return. 2018-01-02 23:20:00 +07:00
Bruce Mitchener
73b3da37d8 Typo fixes. 2018-01-02 22:48:06 +07: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
79a9dfd8fd adding pre-processing to nlsat for equations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-30 20:35:33 -08:00
Christoph M. Wintersteiger
2e186633ee Turned assertion failure into proper error message. 2017-12-11 14:59:25 +00:00
Nikolaj Bjorner
a5d5dfdf86 fix setup for non-linear real arithmetic per QF_UFNRA regresssions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-12-08 09:23:57 +05:30
Nikolaj Bjorner
2749e547cf fix c example, remove more smtlib1 printing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-28 18:14:24 -08:00
Nikolaj Bjorner
b8e5fc9f43 remove SMTLIB1 printing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-28 15:08:28 -08:00
Nikolaj Bjorner
5a35d00766 remove std::cout 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-28 08:55:45 -08:00
Nikolaj Bjorner
103ce78c29 save model from level 0, fix #1380 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-28 08:53:06 -08:00
Nikolaj Bjorner
81ec5bae95 fix #1377 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-27 11:02:48 -08:00
Nikolaj Bjorner
36e5d4dec9 fix #1377 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-27 11:01:44 -08:00
Nikolaj Bjorner
1c5f798cbe expose extra symbols for logic ALL, requested in #1364 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-25 12:03:47 -08:00
Christoph M. Wintersteiger
0194df611c Merge branch 'master' of https://github.com/Z3Prover/z3 2017-11-17 21:15:36 +00:00
Christoph M. Wintersteiger
f5ff9fae34 Fixed bug check in bv2fpa converter. Fixes #1291. 2017-11-17 21:15:30 +00:00
Nikolaj Bjorner
7f13cf13f2 clean up bv_numeral code and fix bug in how they are initialized 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-15 15:00:11 -08:00
Nikolaj Bjorner
795e0c641a add method to create bit-vectors directly from an array of Booleans 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-15 14:44:59 -08:00
Nikolaj Bjorner
195d81ebef fix rewriter loop reported in #1354 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-13 13:49:03 -08:00
Christoph M. Wintersteiger
2d221155b3 Fixed bug in fp.to_ieee_bv with rewriter.hi_fp_unspecified=true. Reported in #1349. 2017-11-08 20:52:48 +00:00
Nikolaj Bjorner
9d3518736b fix #889 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-06 15:25:10 -08:00
Nikolaj Bjorner
0f2b1ae7c8 fix proof mode related segfaults #1241 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-06 02:35:10 -08:00
Nikolaj Bjorner
16bab71df2 remove asserts for proof generation to enable mode switch in spacer virtual solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-11-06 02:18:55 -08:00
Nikolaj Bjorner
e4b595d490 add solver pool abstraction for Spacer 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-28 16:10:20 -07:00
Nikolaj Bjorner
8acc924c21 ifndef/define match 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 16:34:49 -07:00
Nikolaj Bjorner
6300a78b82 more build errors in debug mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 12:57:30 -07:00
Nikolaj Bjorner
48d144a6dd missing file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 12:51:47 -07:00
Nikolaj Bjorner
db65cc007a move more proof utils 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 10:27:48 -07:00
Nikolaj Bjorner
fc822af707 move proof utils under ast 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-24 09:59:55 -07:00
Nikolaj Bjorner
2c3b56315d Merge branch 'master' of https://github.com/z3prover/z3 2017-10-24 08:49:56 -07:00