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

2485 commits

Author SHA1 Message Date
Nikolaj Bjorner 93415740b6 left over bugs #5532 
disabling complete const rewriting (temporarily) as it can loop
 2021-09-07 07:00:41 +02:00
Nikolaj Bjorner be4df46f6f #5532 remove unsound rewrite rule that was recently added 2021-09-07 06:42:24 +02:00
Nikolaj Bjorner 72f6271d82 #5532 
bugs in:
- rewriting of 0-ary expressions was incomplete
- sharing annotations when a node has two theories attached it is shared
- sharing of const of an array

Remove unreadable part of pretty printer for lp solver.
 2021-09-06 19:14:03 +02:00
Nikolaj Bjorner 38b82fa742 const rewriting revisited 2021-09-04 17:59:08 -07:00
Nikolaj Bjorner 9c5ef79701 #5532 2021-09-04 09:05:49 -07:00
Nikolaj Bjorner cf9e55fa96 #5516 
expose ability to expand select/store and select/ite (lambdas are always expanded) during pre-processing for N.P. Lopes.
 2021-09-01 17:44:17 -07:00
Nikolaj Bjorner ab2baa764c #5518 
@wintersteiger
This example exposes a bug in is_unique_value
```
(assert (= (fp.to_real ((_ to_fp 8 24) (_ bv4286579200 32))) (fp.to_real ((_ to_fp 8 24) (_ bv4286578944 32)))))
(check-sat)
```
It returns true for fp representations that map to NaN. It can only return true for fp values that are unique relative to having no other bit-vector representation so not corresponding to an equivalence class of values such as NaN.
I am having it return false. If there is a way to refine the test it will catch some earlier inferences.
 2021-08-31 14:52:45 -07:00
Nikolaj Bjorner 0b063f7903 #5518 2021-08-31 12:50:24 -07:00
Nikolaj Bjorner 535f442655 #5518 
regression from adding lambdas in model
 2021-08-31 12:13:27 -07:00
Nikolaj Bjorner 4f064ee5d6 simplify based on comment from Jamie Sharp #5512 2021-08-28 17:08:34 -07:00
Nikolaj Bjorner e3a83dd0dd Integrate fixes from #5512 
Pull request #5512 identifies a in line 1139 where the const-case-multiplier constructor returns false and does useless work.
In this update we also remove mk_const_multiplier because code path is subsumed by mk_const_case_multiplier.
 2021-08-28 10:46:45 -07:00
Nikolaj Bjorner e9a30385cf remove wtm and booth 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-08-27 15:32:06 -07:00
Nikolaj Bjorner 07c26208fa regressions from previous push 2021-08-25 18:30:50 -07:00
Nikolaj Bjorner 2daf569da6 update Bool rewriter to pull negations up 2021-08-25 17:50:49 -07:00
Nikolaj Bjorner e6264a80ff extend macro detection to negated equivalences #5496 2021-08-25 17:47:30 -07:00
Nikolaj Bjorner f03d756e08 missing rewrite exposed by #5498 2021-08-25 06:34:27 -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 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 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 c8a83749dd #5484 2021-08-16 11:19:22 -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 fde8808a40 #5454 2021-08-11 16:59:46 -07:00
Nikolaj Bjorner 178262fc12 #5454 2021-08-11 09:30:03 -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
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 1173c93150 #5140 2021-08-02 17:13:47 -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 6a9241ff0f #5429 2021-07-31 11:00:12 -07:00
Nikolaj Bjorner 31267e6ab8 #5429 2021-07-30 14:55:59 -07:00
Nikolaj Bjorner b8a437bd8a #5429 
relevancy propagation applies to quantifier unfolding.
 2021-07-29 15:05:06 -07:00
Nikolaj Bjorner 703659a3a8 fix #5439 2021-07-28 17:16:17 -07:00
Nikolaj Bjorner 5652d2a157 #5429 #5431 2021-07-25 11:59:42 -07:00
Nikolaj Bjorner b638405e42 simplify #5431 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-07-25 09:57:38 -07:00
Margus Veanes 4fd1e6d32c
added derivative support for (str.to_re (str.from_int ...)) (#5431) 2021-07-25 09:51:48 -07:00
Nikolaj Bjorner 32beb91efa sat.euf add missing function 2021-07-22 19:17:17 -07:00
Nikolaj Bjorner 39c3f34a30 remove unused dependency 2021-07-21 09:25:08 -07:00
Nikolaj Bjorner 644bd82ac7 #5422 2021-07-21 09:08:55 -07:00