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

13298 commits

Author SHA1 Message Date
Nikolaj Bjorner f03d756e08 missing rewrite exposed by #5498 2021-08-25 06:34:27 -07:00
Nikolaj Bjorner 17663acf75 #5482 other relevancy tracking 2021-08-25 05:59:42 -07:00
Nikolaj Bjorner e75b5e9513 don't copy "true" 2021-08-25 05:59:42 -07:00
Nikolaj Bjorner 037c93b258 #5482 2021-08-25 05:59:42 -07:00
Nikolaj Bjorner 7bae297297 #5482 
add unit propagation
 2021-08-24 11:24:31 -07:00
Nikolaj Bjorner 26db68bf2c #5482 2021-08-24 11:15:52 -07:00
Nikolaj Bjorner e5b6cd36f0 use datatype name instead of instantiation for cycle detection #5482 2021-08-24 11:14:41 -07:00
Nikolaj Bjorner e90ec457c3 #5482 
non-termination (stack overflow) bug in recursive comparison
 2021-08-24 09:49:36 -07:00
Nikolaj Bjorner 5fa1b0b09f update project description #5503 2021-08-24 09:48:33 -07:00
Nikolaj Bjorner 23b995d3b5 #5499 
throw exception when dividing by a small 0
 2021-08-24 08:52:20 -07:00
Nikolaj Bjorner dd91cfb47e #5482 
update temp variables
 2021-08-23 22:21:52 -07:00
Nikolaj Bjorner 592c53e46d char sort 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-23 20:45:26 -07:00
Nikolaj Bjorner 170ef1dcca add character sort to Python API and allchar function to API for ease. #5500 2021-08-23 20:02:50 -07:00
Nikolaj Bjorner 4b3b4b95d9 missing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-23 10:03:34 -07:00
Nikolaj Bjorner 2a682e4b13 #5482 
tricky one
 2021-08-23 10:01:53 -07:00
Nikolaj Bjorner 1975e486ee finally expose some easier to use basics could be used in cases such as #5496 2021-08-21 21:22:54 -07:00
Nikolaj Bjorner aa05298950 fix #5491 2021-08-19 21:12:27 -07:00
Nikolaj Bjorner 15e3e81cb5 remove likely culprit for #5493 
@zwimer: I had to remove a different move constructor before in the same API due to a different bug that the coverage tool exposed. I was unable to reproduce the bug reported in #5493 in my environment, but the interaction with reference counting and move constructors is sufficiently opaque that I rather not have to fix more bugs introduced with move constructors in the API. I am therefore removing also this use of && and maybe this fixes #5493
 2021-08-19 21:08:20 -07:00
Nikolaj Bjorner d0e210849f #5454 again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-19 03:06:23 -07:00
Nikolaj Bjorner adcdd11afc #5454 again 2021-08-18 13:32:51 -07:00
Nikolaj Bjorner 1db9f9a3b5 try vscode from github integration 2021-08-18 11:02:02 -07:00
Nikolaj Bjorner d980ee0533 fix regression in FPNumRef sign 2021-08-18 10:00:22 -07:00
Nikolaj Bjorner b3db9a1cd5 #5488 2021-08-18 08:30:08 -07:00
Nikolaj Bjorner 5c9f4dc4d7 #5486 - improve type elaboration by epsilon to make common cases parse without type annotation 2021-08-17 16:43:36 -07:00
Nikolaj Bjorner 7f88cfe727 build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-17 10:10:20 -07:00
Nikolaj Bjorner 1884ad5b2f expose method for updating python model for constants 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-17 09:09:04 -07:00
Nikolaj Bjorner 34fc0276e9 Update array_axioms.cpp 2021-08-16 17:52:37 -07:00
Nikolaj Bjorner 749d1ab305 remove dependencies on stale component 2021-08-16 17:52:36 -07:00
Nikolaj Bjorner c8a83749dd #5484 2021-08-16 11:19:22 -07:00
Nikolaj Bjorner 904c6e21b1 modify #5454 2021-08-16 03:29:40 -07:00
Nikolaj Bjorner 429e5ed0cd #5454 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-15 19:07:37 -07:00
Nikolaj Bjorner 3d13c0335f #5454 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-15 18:40:05 -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 fe4c48e14c reorder fields 2021-08-15 12:29:43 -07:00
Nikolaj Bjorner bebf2d6a52 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-15 00:24:43 -07:00
Nikolaj Bjorner b7d4501bc3 widen scope of der #5480 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-15 00:22:34 -07:00
Nikolaj Bjorner 2704fb5fd5 expose n-ary xor 2021-08-14 10:52:09 -07:00
intrigus-lgtm 35698c650d
Add AssertSoft String overload for Java Api (#5475) 
This adds a String overload for AssertSoft.
Previously only integer weights could have been used,
limiting the user. With Strings the user can now use
e.g. Java's BigInteger class converted to a String instead.
 2021-08-12 09:18:18 -07:00
Nikolaj Bjorner b016465ad2 #5454 2021-08-11 20:31:53 -07:00
Nikolaj Bjorner fea14245a0 #5454 2021-08-11 19:43:42 -07:00
Nikolaj Bjorner 46107022f7 #5454 2021-08-11 17:06:42 -07:00
Nikolaj Bjorner fde8808a40 #5454 2021-08-11 16:59:46 -07:00
Nikolaj Bjorner 8faad26c3c #5454 2021-08-11 09:46:35 -07:00
Nikolaj Bjorner 178262fc12 #5454 2021-08-11 09:30:03 -07:00
Nikolaj Bjorner 496ec5f2b4 #5454 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-11 05:00:02 -07:00
Nikolaj Bjorner d1d64bbe59 #5454 2021-08-11 04:55:20 -07:00
Nikolaj Bjorner 4f2211baab fix solver-subsumption again, #5468 (negation was swapped in original wrong subsumption check, then soundness fix removed core subsumption functionality) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-11 04:36:48 -07:00
Nikolaj Bjorner 7ab7b8646b #5454 2021-08-10 14:47:26 -07:00
Nikolaj Bjorner 081cdbd762 fix #5468 2021-08-10 10:46:47 -07:00
Nikolaj Bjorner 391db898d3 lost update from August 3 #5468 2021-08-10 09:45:17 -07:00
Nikolaj Bjorner 2075cb9fa4 remove useless literal found during review #5470 2021-08-10 09:29:39 -07:00
Nikolaj Bjorner 4beb29d45e fix #5469 documentation bug 2021-08-10 09:22:24 -07:00
Margus Veanes 22bb4c2db7
more fixes related to issue #5140 (#5466) 
* instead of u in to_re(s) make u = s

* bug fix: added missing emptiness check
 2021-08-09 17:48:35 -07:00
Nikolaj Bjorner 3eb849ad9e rewrite equality too 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-09 15:32:04 -07:00
Nikolaj Bjorner aa7e9b09f3 fix equality rewrite with itos 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-09 14:22:48 -07:00
Margus Veanes 225204e2f4
updates related to issue #5140 (#5463) 
* updates related to issue #5140

* updated/simplified some cases

* fixing feedback comments

* fixed comments and added missing case for get_re_head_tail_reversed

* two bug fixes and some other code improvements
 2021-08-09 10:48:56 -07:00
Nikolaj Bjorner af5fd1014f #5460 2021-08-08 17:33:49 -07:00
Nikolaj Bjorner 85da7407dc #5460 
NB @nunoplopes - the code path regarding rewrite_uncstr could use some unit tests.
 2021-08-08 17:18:31 -07:00
Nikolaj Bjorner e27a71bbcb #5460 2021-08-08 16:29:41 -07:00
Jamey Sharp 5de5f5a442
report which operator bit-blast failed on (#5459) 2021-08-08 15:53:07 -07:00
Jamey Sharp 1d3ee70af4
support bit-blasting bvand (#5458) 2021-08-08 15:52:54 -07:00
Nikolaj Bjorner dcfd7b76c9 more rewrites based on example in #5457 2021-08-05 11:54:13 -07:00
Nikolaj Bjorner e10850e66a fix #5457 2021-08-05 11:27:03 -07:00
Nikolaj Bjorner ed3f8a52e6 #5454 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-04 14:05:29 -07:00
Nikolaj Bjorner a39d1c6188 fix #5456 2021-08-04 10:07:29 -07:00
Nikolaj Bjorner 939860148f #5452 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-03 20:03:34 -07:00
Nikolaj Bjorner 2891ac7dec merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-03 19:47:38 -07:00
Nikolaj Bjorner 40f5270ae2 fix #5452 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-03 17:23:41 -07:00
Nikolaj Bjorner 7ae4e93e86 Sharon & Neta notes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-03 16:45:25 -07:00
Nikolaj Bjorner da60abd84b #5445 2021-08-03 11:19:42 -07:00
Nikolaj Bjorner 202ed79a24 #5445 2021-08-03 11:17:23 -07:00
Nikolaj Bjorner f333d78f01 #5445 2021-08-02 20:41:34 -07:00
Nikolaj Bjorner 1173c93150 #5140 2021-08-02 17:13:47 -07:00
Nikolaj Bjorner 4aaf026b49 format 2021-08-02 13:45:23 -07:00
Nikolaj Bjorner fc36fb115f format 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-02 13:45:23 -07:00
Nikolaj Bjorner d3194bb8a8 #5445 2021-08-02 11:07:28 -07:00
Nikolaj Bjorner 6c0a790576 #5445 2021-08-02 09:22:54 -07:00
Nikolaj Bjorner da8530e2db #5447 
That the bug went away is a fluke. It wasnt fixed.
It is in pb-preprocess, an essentially unused tactic. The special subsumption resolution rule wasn't accounting for membership of all variables.
 2021-08-02 09:03:15 -07:00
Nikolaj Bjorner e3be25dad6 #5445 2021-08-01 16:48:25 -07:00
Nikolaj Bjorner 123c446395 fix #5449 2021-08-01 13:03:40 -07:00
Nikolaj Bjorner a4cc9e7895 #5429 #5445 2021-08-01 12:49:36 -07:00
Nikolaj Bjorner 924ea6ab31 #5429 again 2021-08-01 12:00:22 -07:00
Nikolaj Bjorner 50f5cafb50 fix #5446 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-01 05:09:58 -07:00
Nikolaj Bjorner 490dc66ec2 remove sine filter #5446 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-01 05:05:45 -07:00
Nikolaj Bjorner 5b32c3778f remove out 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-31 18:00:37 -07:00
Nikolaj Bjorner f5a08cc54e add wip 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-31 17:57:36 -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 ed27ce5526 fix regression in goal2sat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-31 11:41:55 -07:00
Nikolaj Bjorner 7de8c72246 cleanups 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-31 11:32:47 -07:00
Nikolaj Bjorner 6a9241ff0f #5429 2021-07-31 11:00:12 -07:00
Nikolaj Bjorner e5401a4303 use quantifier 2021-07-31 00:32:43 -07:00
Nikolaj Bjorner 77cd82a5ca flatten if-then-else 2021-07-30 23:28:30 -07:00
Nikolaj Bjorner bcf0f671b8 disable drat inside of quantifier elaboration 2021-07-30 23:27:37 -07:00
Nikolaj Bjorner 1e8009bbfc build/labels 2021-07-30 22:29:00 -07:00
Nikolaj Bjorner 53ab931626 #5429 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-30 21:35:09 -07:00
Nikolaj Bjorner 1488bf81ae #5429 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-30 15:34:12 -07:00
Nikolaj Bjorner 31267e6ab8 #5429 2021-07-30 14:55:59 -07:00
Nikolaj Bjorner f3f83d0445 #5429 2021-07-30 13:43:02 -07:00
Nikolaj Bjorner 5ca8628e0d na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-30 13:42:54 -07:00