mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity
16137 commits 49 branches 53 tags 182 MiB
Commit graph

16137 commits

This branch
This branch
All branches
Author SHA1 Message Date
Zachary Wimer
77dea18f54
Added missing fp conversion methods to C++ API (#5234) 2021-04-30 18:45:28 -07:00
Nikolaj Bjorner
c50e6bdbb1 fix #5229 2021-04-30 02:32:16 -07:00
Nikolaj Bjorner
381e502d30 fix #5224 2021-04-29 20:12:20 -07:00
Zachary Wimer
e4b660321f
Cpp api string const (#5228) 
* string_const added

* typo fixed
 2021-04-29 16:16:48 -07:00
Nikolaj Bjorner
decbf4be11 fix undo record for lblset 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-29 14:06:18 -07:00
Nikolaj Bjorner
a8ccbd7103 fix #5226 2021-04-29 13:36:25 -07:00
Nikolaj Bjorner
30e904bfa4 disable threads for extensions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-27 21:46:56 -07:00
Nikolaj Bjorner
007b792e0f #5215 2021-04-27 21:05:02 -07:00
Nikolaj Bjorner
5ecc32e731 #5215 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-27 20:46:25 -07:00
Nikolaj Bjorner
308f399224 #5215 converting NYI 2021-04-27 16:19:54 -07:00
Nikolaj Bjorner
89373d5bf9 #5215 2021-04-27 16:02:08 -07:00
Nikolaj Bjorner
4da4591fe7 #5215 2021-04-27 15:40:17 -07:00
Nikolaj Bjorner
e5892e5e97 #5215 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-27 15:26:56 -07:00
Nikolaj Bjorner
a71b4fab23 na 2021-04-27 09:31:04 -07:00
Nikolaj Bjorner
78571b9a51 fix #5219 2021-04-27 09:30:10 -07:00
Nikolaj Bjorner
d731ec7cba
Revert "Cpp api fp to bv (#5218)" (#5221) 
This reverts commit fa2d593739.
 2021-04-27 08:44:15 -07:00
Zachary Wimer
fa2d593739
Cpp api fp to bv (#5218) 
* fpa_to_ubv and fpa_to_sbv added to C++ API

* Bug fix

* fpa_fp method added to API

* Adjust types to prefer sort over expr and bug fix
 2021-04-26 17:00:05 -07:00
Nikolaj Bjorner
ecfbc1cc06 trace 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-26 15:15:27 -07:00
Nikolaj Bjorner
22a76e4985 fix typos in comments 2021-04-26 15:15:27 -07:00
Nikolaj Bjorner
a1b036a4fa
Update README.md 2021-04-25 17:02:34 -07:00
Nikolaj Bjorner
3ff5d4226a
Update README.md 2021-04-25 16:59:53 -07:00
Nikolaj Bjorner
0422b59123 build 2021-04-24 16:37:03 -07:00
Nikolaj Bjorner
c03fac8390 Investigating std::vector and #5178 2021-04-24 14:50:59 -07:00
Nikolaj Bjorner
385109d484 regarding #5206 2021-04-24 14:25:26 -07:00
Nikolaj Bjorner
a19e469cc2 fix #5212 2021-04-24 13:27:41 -07:00
Nikolaj Bjorner
af5e7a1c48 #5211 2021-04-24 10:28:22 -07:00
Nikolaj Bjorner
b1e8303257 #5211 2021-04-24 10:23:09 -07:00
Nikolaj Bjorner
07e2ca100d fix #5213 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-04-23 10:05:08 -07:00
Nikolaj Bjorner
e0393f85fa #5211 2021-04-22 23:46:05 -07:00
Nikolaj Bjorner
b5496d823d #5211 2021-04-22 23:14:28 -07:00
Nikolaj Bjorner
d2f15d1b1a #5211 2021-04-22 23:04:54 -07:00
Nikolaj Bjorner
67ec86fc66 #5211 2021-04-22 22:53:18 -07:00
Nikolaj Bjorner
5d49cb5519 #5211 2021-04-22 22:42:05 -07:00
Nikolaj Bjorner
5cfe273460 #5211 
```
 (declare-fun v5 () Bool)
 (declare-fun i1 () Int)
 (declare-fun i2 () Int)
 (declare-fun i4 () Int)
 (declare-fun i5 () Int)
 (declare-fun i6 () Int)
 (declare-fun i9 () Int)
 (declare-fun i10 () Int)
 (assert (or (not (=> (= 23 i6 i4 i2 85) v5)) (<= i1 8 i9 i9 (+ (+ i1 349 i10 i6) i5)) (>= i4 782)))
 (check-sat)
```
 2021-04-22 22:10:39 -07:00
Nikolaj Bjorner
bcb33a5b3a remove unused functions 2021-04-22 21:46:31 -07:00
Nikolaj Bjorner
4c4810c611 fix #5207 2021-04-22 13:10:11 -07:00
Nikolaj Bjorner
d67919373e add bailout option for code review #5208 
@levnach
Could you review and maybe make this much more streamlined?
The patch is to simply bail out the iterator if it fails to find canonical monics.
If m_ff could produce the existing canonical monics up front this kind of bail-out could maybe avoided.
 2021-04-22 11:30:11 -07:00
Tias Guns
a52b485d9c
marco: immediately shrink to core if not subset (#5203) 
Small improvement, found while translating it in another system
 2021-04-20 12:29:52 -07:00
Nikolaj Bjorner
8263d20e0d add code review comment 2021-04-20 11:30:25 -07:00
Nikolaj Bjorner
b658934bd8 fix #5197 fix #5193 2021-04-20 10:16:44 -07:00
Nikolaj Bjorner
44d77a978a cw review comments #5200 2021-04-20 09:27:59 -07:00
Nikolaj Bjorner
770c79a939 prepare for std::vector 2021-04-20 09:24:24 -07:00
Zachary Wimer
831afa8124
Cpp api add missing fp methods (return type correction) (#5200) 
* added is_nan and is_inf to API

* added support to to_ieee_bv

* bug fix
 2021-04-19 17:55:23 -07:00
Zachary Wimer
10e9345cd7
C++ API add missing FP methods (#5199) 
* added is_nan and is_inf to API

* added support to to_ieee_bv
 2021-04-19 15:24:09 -07:00
Zachary Wimer
542878dea3
Add sge and sgt to API; now has sge,sgt,sle,slt, and unsigned counterparts (#5194) 2021-04-19 08:53:43 -07:00
Zachary Wimer
f8228ff50e
[c++ api] add const (#5195) 2021-04-19 10:24:12 +01:00
Nuno Lopes
e67b9ebcf7 try to fix ARM32 build (#2776) 2021-04-17 16:14:05 +01:00
Zachary Wimer
a1741e0e16
z3 c++ api: delete implicit constructor (#5191) 2021-04-16 10:46:03 +01:00
Zachary Wimer
239ace4353
expr move semantics supported via ast (#5190) 2021-04-15 13:37:31 -07:00
Nuno Lopes
21e59f7c6e
change model evaluator to respect resource limits (#5184) 2021-04-14 11:48:39 -07:00