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

15837 commits

This branch
This branch
All branches
Author SHA1 Message Date
Matt Thornton
9cc1549dbe
Use osx-x64 for mac rid rather than macos. (#5288) 2021-05-20 15:19:31 -07:00
Nikolaj Bjorner
03d2c5f3d0 consolidate literals 2021-05-20 12:58:27 -07:00
alexandernutz
8a5addd891
make the two monotonicity tests into one using push/pop; fix division modelling (#5220) 
* make the two monotonicity tests into one using push/pop

* whitespace...

* proper division modelling for monotonicity test -- overflow checks still missing, though

* double bitwidth for overflow checking in monotonicity example
 2021-05-20 10:00:13 -07:00
Nikolaj Bjorner
c959e28d4a remove prints, remove ability to toggle eager_eq_axioms option 
NB. Spacer sets eager_eq_axioms option to false, but relevancy of this option is not clear at all as all other default paths don't use this option and theory_lra is incorrect when it is set to false.
 2021-05-20 04:26:45 -07:00
Nikolaj Bjorner
cc12e3ed38 fix #5280 2021-05-19 16:52:24 -07:00
Nikolaj Bjorner
e0860ea173 fix #5279 2021-05-19 13:31:31 -07:00
Nikolaj Bjorner
ec034679ce #5215 
memory leaks
 2021-05-19 12:42:38 -07:00
Nikolaj Bjorner
abe3ef2382 #5215 2021-05-19 10:33:23 -07:00
Nikolaj Bjorner
d450fd4227 #5215 2021-05-19 10:03:49 -07:00
Nikolaj Bjorner
7b3a587505 fix #5225 2021-05-18 18:04:03 -07:00
Nikolaj Bjorner
9031b5b949 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-18 11:46:46 -07:00
Nikolaj Bjorner
0490056e7a na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-17 19:19:28 -07:00
Nikolaj Bjorner
30974968af fix #5256 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-17 17:41:34 -07:00
Nikolaj Bjorner
4f9ad28a05 fix #5252 2021-05-17 16:16:12 -07:00
Nikolaj Bjorner
55f8ad068f fix #5262 2021-05-17 15:51:03 -07:00
Nikolaj Bjorner
8384f38eb5 fix #5254 2021-05-17 15:42:01 -07:00
Nikolaj Bjorner
1a432529dd fix #5272 2021-05-17 11:10:05 -07:00
Nikolaj Bjorner
d2bd92eab9 fix #5271 2021-05-17 10:42:34 -07:00
Nikolaj Bjorner
93a9847815 BUILD_LIBZ3_SHARED 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-16 15:44:44 -07:00
Margus Veanes
8ca6f567d3
fixing issue #5140 (#5268) 2021-05-16 13:53:08 -07:00
Nikolaj Bjorner
973a32a015 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-16 13:50:41 -07:00
Nikolaj Bjorner
eaca24ac01 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-15 17:00:49 -07:00
Nikolaj Bjorner
88bbe9d54e na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-15 10:12:11 -07:00
Nikolaj Bjorner
683ce27c8f linear solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-14 17:10:01 -07:00
Nikolaj Bjorner
17fcf79c04 interleave linear solver calls 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-14 11:31:35 -07:00
Nikolaj Bjorner
118dc0f3b4 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-14 10:25:42 -07:00
Nikolaj Bjorner
587750b9a3 outline layer between polysat solver and fixplex 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-13 18:04:44 -07:00
Nikolaj Bjorner
334bde7623 Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat 2021-05-13 17:24:00 -07:00
Nikolaj Bjorner
49a903c875 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-13 17:23:55 -07:00
Nikolaj Bjorner
d833483ca0 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-13 17:18:09 -07:00
Nikolaj Bjorner
cf8b3a0788 add copy constructor to handle reference count miss-match 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-12 17:56:09 -07:00
Nikolaj Bjorner
0d776ecf88 eliminate basic variables from new rows 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-12 15:58:35 -07:00
Zachary Wimer
f942c3df91
operator= checks this equality before moving (#5265) 2021-05-12 13:10:14 -07:00
Nikolaj Bjorner
7869cdbbc8 #5259 - the Ranjit 2s shave 
shave a couple of seconds from the Ranjit regression
 2021-05-12 10:43:16 -07:00
Nikolaj Bjorner
62b7719d5a separate into self-contained mod interval 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-11 11:22:55 -07:00
Nikolaj Bjorner
04c0db75bf test eqs1 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-10 21:21:50 -07:00
Nikolaj Bjorner
be7b964206 fix row pivot/del 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-10 19:53:34 -07:00
Nikolaj Bjorner
cd82205b06 nit 2021-05-10 19:14:18 -07:00
Nikolaj Bjorner
d27d09f87a #5261 2021-05-10 13:35:25 -07:00
Nikolaj Bjorner
897a2d6470 #5261 2021-05-10 13:33:37 -07:00
Nikolaj Bjorner
f02fbb49bb fix #5253 2021-05-10 13:00:52 -07:00
Nikolaj Bjorner
2ea4b0f4e0 #5260 2021-05-10 11:42:11 -07:00
Nikolaj Bjorner
e2a52ed6ee #5259 again 2021-05-10 11:15:19 -07:00
Nikolaj Bjorner
987099c765 Hoist creation of m_rep for #5259 2021-05-10 10:54:21 -07:00
Nikolaj Bjorner
a61e9d6b49 #5260 2021-05-10 10:33:43 -07:00
Nikolaj Bjorner
28328e63fd fix #5255 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-09 20:48:11 -07:00
Nikolaj Bjorner
31a5bd7fd7 regression from July 4 2020 tweeted by Dr. RJ and crowd profiled - let's submit this somwhere? 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-09 20:33:43 -07:00
Nikolaj Bjorner
0b6c7cd7b4 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-09 20:13:33 -07:00
Nikolaj Bjorner
43cc0e6575 fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-07 18:03:34 -07:00
Nikolaj Bjorner
654892fec1 inverse approx 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-07 17:33:07 -07:00