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

15399 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
7a1a2b2525 make unit types generic 2021-05-20 15:28:26 -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
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
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
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
Nikolaj Bjorner
e3e2860198 move to interval arithmetic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-07 15:32:56 -07:00
Nikolaj Bjorner
5f48cffbb6 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-06 19:23:28 -07:00
Nikolaj Bjorner
d33b9f2698 a test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-06 19:09:31 -07:00
Nikolaj Bjorner
b5d1b0336a na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-06 19:00:51 -07:00
Nikolaj Bjorner
a1ded7f1ec na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-06 18:53:05 -07:00
Nikolaj Bjorner
1d724de915 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-06 18:46:47 -07:00
Nikolaj Bjorner
5931e0d902 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-06 18:43:47 -07:00
Nikolaj Bjorner
59221f1d63 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-06 16:32:56 -07:00
Nikolaj Bjorner
cfd204e5fe na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-06 13:08:45 -07:00
Nikolaj Bjorner
253c954094 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-06 10:51:42 -07:00
Nikolaj Bjorner
bd5aa2ac21 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-06 09:26:08 -07:00
Nikolaj Bjorner
5ca8295dcc na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-04 12:05:44 -07:00
Nikolaj Bjorner
8cd1ddf445 add accounting for integrality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-04 11:57:25 -07:00
Jakob Rath
fd1758ffab
Polysat: check test results, forbidden intervals for coefficient -1 (#5241) 
* Use scoped_ptr for condition

* Check solver result in unit tests

* Add test for unusual cjust

* Add solver::get_value

* Broken assertion

* Support forbidden interval for coefficient -1
 2021-05-04 09:33:55 -07:00
Nikolaj Bjorner
5791b41133 more testing of fixplex 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-03 16:31:00 -07:00
Nikolaj Bjorner
dc879dc3fb merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-03 12:41:14 -07:00
Nikolaj Bjorner
0c6722f48b na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-03 11:47:00 -07:00
Nikolaj Bjorner
60cf482cea fix #5239 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-03 11:44:44 -07:00
Jakob Rath
f7e476a4a0
Polysat: fixes in solver, forbidden intervals for eq_constraint (#5240) 
* Rename to neg_cond

* Add some logging utilities

* Implement case of forbidden interval covering the whole domain

* Implement diseq_narrow

* Do not activate constraint if we are in a conflict state

* comments

* Assert that lemma isn't undefined

* Update revert_decision to work in the case where narrowing causes propagation

* Fix case of non-disjunctive lemma from forbidden intervals

* Conflict should not leak outside user scope

* Add guard to decide(), some notes

* Add test case

* Add constraints to watchlist of unassigned variable during propagation

* Move common propagation functionality into base class

* Combine eq/diseq narrow

* Compute forbidden interval for equality constraints by considering them as p <=u 0 (or p >u 0 for disequalities)
 2021-05-03 09:30:17 -07:00
Nikolaj Bjorner
2c97799564 #5237 
be stingier on stack instead of punting and saying users can set ulimit
 2021-05-02 16:18:55 -07:00
Nikolaj Bjorner
ff480d1183 fix #5238 2021-05-02 16:09:01 -07:00
Nikolaj Bjorner
04876ba8b7 n 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-02 10:51:33 -07:00
Nikolaj Bjorner
51a4db862a #5223 2021-05-02 10:40:22 -07:00
Nikolaj Bjorner
0810720267 #5223 2021-05-02 10:30:35 -07:00
Nikolaj Bjorner
323e0e6270 #5223 2021-05-01 16:43:54 -07:00
Nikolaj Bjorner
7835388361 #5223 2021-05-01 15:31:05 -07:00
Nikolaj Bjorner
6de0615779 #5223 2021-05-01 15:18:59 -07:00
Nikolaj Bjorner
6520f43f9d na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-01 14:43:58 -07:00
Nikolaj Bjorner
501dbd9475 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-01 14:26:22 -07:00
Nikolaj Bjorner
57a7bef96b na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-05-01 13:58:34 -07:00