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

3770 commits

Author SHA1 Message Date
Margus Veanes 146f4621c5
Updated regex derivative engine (#5567) 
* updated derivative engine

* some edit

* further improvements in derivative code

* more deriv code edits and re::to_str update

* optimized mk_deriv_accept

* fixed PR comments

* small syntax fix

* updated some simplifications

* bugfix:forgot to_re before reverse

* fixed PR comments

* more PR comment fixes

* more PR comment fixes

* forgot to delete

* deleting unused definition

* fixes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fixes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-10-08 13:04:49 -07:00
Nikolaj Bjorner 8a85cfdb12 fix #5579 - 
It is only possible to reach this case when new assertions are created.
 2021-09-30 09:32:34 -07:00
Nikolaj Bjorner 9aad331699 #5546 
try dampening
 2021-09-14 10:32:53 +02:00
Nikolaj Bjorner f13ccf8969 bv2char and char2bv with Clemens 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-13 16:09:03 +02:00
Nikolaj Bjorner 3e6ff768a5 fix regression bug in mam reported by Aseem 2021-09-10 07:09:22 +02:00
Nikolaj Bjorner 18e4546404 modernize parameter defaults 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-03 17:42:36 -07:00
Nikolaj Bjorner cdcfbeb6d8 #5532 
remove "reflect" parameter from exposed options. It should be internal only.
 2021-09-03 16:01:59 -07:00
Nikolaj Bjorner e9a4a9a390 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-02 09:23:59 -07:00
Nikolaj Bjorner edb26e7be7 Merge branch 'master' of https://github.com/z3prover/z3 2021-09-02 08:53:56 -07:00
Nikolaj Bjorner 02acc38c28 add extra checks that user-supplied assumptions are asserted 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-02 08:53:47 -07:00
Nikolaj Bjorner 9e306e3b6e more useful diagnostics 2021-09-01 20:50:35 -07:00
Nikolaj Bjorner 968717a532 follow on fix from #5528 
the same bug is also undetected in the main solver
 2021-09-01 20:49:39 -07:00
Nikolaj Bjorner 535f442655 #5518 
regression from adding lambdas in model
 2021-08-31 12:13:27 -07:00
Nikolaj Bjorner 09696e989e add missing lambda defs per #5509 
the result is now unknown because the nested expression contains exists, which doesn't get replaced by universal quantifier which is assumed by the legacy core.
The legacy core should not depend on universal quantifiers only, but fixing this is a risk. Workaround is to rewrite goals using forall only (replace exists by de-Morgan dual).
 2021-08-27 11:57:26 -07:00
Nikolaj Bjorner 9790a8aa43 #5507 
can't use auto-config if there are no assertions. Auto-config only works properly for one-shot mode since theories aren't loaded on demand in this solver.
 2021-08-27 09:42:40 -07:00
Nikolaj Bjorner e75b5e9513 don't copy "true" 2021-08-25 05:59:42 -07:00
Nikolaj Bjorner aa05298950 fix #5491 2021-08-19 21:12:27 -07:00
Nikolaj Bjorner 749d1ab305 remove dependencies on stale component 2021-08-16 17:52:36 -07:00
Nikolaj Bjorner 6a3ba64afe #5454 
@wintersteiger: added code review comment to theory_fpa. The bug seen in #5454 doesn't surface with theory_fpa, though.
 2021-08-15 16:48:28 -07:00
Nikolaj Bjorner eefde76bd4 na 2021-07-31 17:16:59 -07:00
Nikolaj Bjorner b723e1093b misc warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-31 17:16:59 -07:00
Nikolaj Bjorner 7de8c72246 cleanups 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-31 11:32:47 -07:00
Nikolaj Bjorner 5652d2a157 #5429 #5431 2021-07-25 11:59:42 -07:00
Nikolaj Bjorner 0ba518b0c0 avoid perf abyss for macros 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-20 20:07:06 -07:00
Nikolaj Bjorner 284d599788 #5323 
https://github.com/Z3Prover/z3/issues/5323#issuecomment-866503616
 2021-07-18 05:14:14 -07:00
Nikolaj Bjorner 9e5dcf3ecb bound length of ubv2s 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-16 16:17:59 +02:00
Margus Veanes 8e9bc86c23
fixed bug #5343 and did some related optimizations (#5411) 2021-07-15 22:28:59 +02:00
Nikolaj Bjorner 0752b1385c add length axioms 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-13 14:22:58 +02:00
Nikolaj Bjorner f74adb1ebd ubv2s step3 2021-07-12 17:15:08 +02:00
Nikolaj Bjorner b6a3891ac4 str.from_ubv step2 2021-07-12 15:00:36 +02:00
Nikolaj Bjorner 805bb58289 fix #5404 2021-07-12 12:35:24 +02:00
Nikolaj Bjorner e05f5ef6d1 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-11 06:15:27 +02:00
Nikolaj Bjorner 5fac396c2f simplify some verbose trace-stream 2021-07-11 06:15:27 +02:00
Nikolaj Bjorner 66fc980154 add helper axioms for int2bv #5396 2021-07-10 17:13:16 +02:00
Nikolaj Bjorner 2973d3bdc1 fix #5392 2021-07-07 23:43:30 +02:00
Nikolaj Bjorner 897cbf347b fix #5381 2021-07-07 16:51:06 +02:00
Nikolaj Bjorner 4f184b6aa9 fix #5376 2021-07-06 19:20:35 +02:00
Nikolaj Bjorner af5b2a4179 #5376 2021-07-06 16:44:44 +02:00
Nikolaj Bjorner ca05c66847 #5376 2021-07-06 14:20:23 +02:00
Nikolaj Bjorner 2a8d00d815 fix #5378 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-06 00:04:16 +02:00
Nikolaj Bjorner f95d0b7216 #5349 #5338 2021-06-16 16:01:42 -05:00
Nikolaj Bjorner 2156c74d51 #4702 
initial gcd test implementation for accumulated parity constraints
 2021-06-01 15:26:36 -07:00
Nikolaj Bjorner 4d75281841 fix #5315 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-30 10:38:04 -07:00
Nikolaj Bjorner b1606487f0 fix #5289 2021-05-30 10:32:30 -07:00
Nikolaj Bjorner 3024fe7baf fix #5312 2021-05-29 08:17:33 -07:00
Nikolaj Bjorner 15916091d1 fix #5307 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-28 14:38:41 -07:00
Nuno Lopes f1e0d5dc8a remove a hundred implicit constructors/destructors 2021-05-23 14:25:01 +01:00
Nikolaj Bjorner 20a67e47ca remove symbol -> zstring -> symbol round-trips 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-22 13:12:49 -07:00
Nikolaj Bjorner 8ba0fb5b58 rounding mode sort removed for incompatibility 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-21 16:18:43 -07:00
Nikolaj Bjorner 00deb12238 signed 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-21 15:51:27 -07:00