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

18113 commits

This branch
This branch
All branches
Author SHA1 Message Date
Jakob Rath
2bc1b3a6dd Better exception recording 2022-11-30 11:50:23 +01:00
Jakob Rath
ceddb97bfd Disable asserts 2022-11-30 11:48:39 +01:00
Jakob Rath
032e7e0337 Remove not_op 2022-11-30 11:47:00 +01:00
Jakob Rath
7febcd47ec Forgot univariate shl 2022-11-30 11:38:16 +01:00
Jakob Rath
4026ac9427 For r = p & q: "p = 0 => r = 0" is subsumed by "r <= p" 2022-11-30 11:35:36 +01:00
Jakob Rath
e6eea83b67 Missed some univariate constraints 2022-11-29 15:51:34 +01:00
Jakob Rath
5b6e383c88 Pretty-print powers of two 2022-11-29 15:49:58 +01:00
Clemens Eisenhofer
2b7fd152c4 Merge branch 'polysat' of https://github.com/Z3Prover/z3 into polysat 2022-11-29 14:54:49 +01:00
Jakob Rath
630276dbad Re-enable saturation 2022-11-29 10:00:25 +01:00
Jakob Rath
4aa04fa475 Lemma names 2022-11-28 19:13:38 +01:00
Jakob Rath
0c44391b9e Don't call assign_eh for internal constraints 2022-11-28 18:43:19 +01:00
Jakob Rath
c1f9a26f09 disable assertion for now 2022-11-28 18:15:24 +01:00
Jakob Rath
a3767b177c comment 2022-11-28 18:11:51 +01:00
Jakob Rath
c488a766b5 Unit testing fixes 2022-11-28 18:05:25 +01:00
Jakob Rath
3d79cddf33 Update saturation inferences 2022-11-28 18:02:18 +01:00
Jakob Rath
7468b2326c inequality 2022-11-28 18:00:17 +01:00
Jakob Rath
e6c9e13848 Disable copy/move of pdd_manager 2022-11-28 17:41:04 +01:00
Jakob Rath
77b4303b66 Don't jump over base level 2022-11-28 16:14:06 +01:00
Jakob Rath
1b1e310919 fix release build 2022-11-24 14:02:47 +01:00
Jakob Rath
3a92641ca0 Unit test: catch exceptions during instance setup 2022-11-23 17:02:15 +01:00
Jakob Rath
3713f51c15 Print unit test numbers 2022-11-23 17:01:11 +01:00
Jakob Rath
5c63a67634 disable for now 2022-11-23 16:59:26 +01:00
Jakob Rath
558fd718c0 Current base level may be too high to deallocate clause 2022-11-23 16:54:58 +01:00
Jakob Rath
0e32077321 Use insert_eval for potentially new constraints 2022-11-23 16:54:35 +01:00
Jakob Rath
76c106476c superposition hotfix 2022-11-23 16:53:26 +01:00
Jakob Rath
bef1b9b429 Simplify 2022-11-23 15:11:27 +01:00
Jakob Rath
f51d5c2fe9 Add note on potential replay problem 2022-11-23 15:00:31 +01:00
Jakob Rath
0313f91dc2 fix 2022-11-23 14:55:41 +01:00
Jakob Rath
a39cce18cb Fix another assertion 2022-11-23 13:46:44 +01:00
Jakob Rath
4224a14bdc Need to re-check whether lemma was asserting 2022-11-23 13:22:43 +01:00
Jakob Rath
58c299dc33 fix assertion failure 2022-11-23 13:21:58 +01:00
Jakob Rath
2787a22007 Backtrack/backjump based on accumulated lemmas 2022-11-23 12:49:36 +01:00
Jakob Rath
fdc186b204 Simplify constraint evaluation 2022-11-23 12:19:03 +01:00
Clemens Eisenhofer
e083f5fde8 Added missing mk_var calls 2022-11-23 10:01:20 +01:00
Jakob Rath
e4999b07aa Remove active flag from constraint 
Superseded by boolean assignment and pwatch
 2022-11-22 14:45:51 +01:00
Jakob Rath
da762700d6 quot_rem 2022-11-22 14:19:35 +01:00
Jakob Rath
85a633a3e0 Update resolve_value 2022-11-22 13:47:31 +01:00
Jakob Rath
a144a09ede Propagation must be justified by a prefix of Gamma 2022-11-22 13:42:31 +01:00
Jakob Rath
33ea8d6e57 viable conflict also depends on vars 2022-11-22 13:40:29 +01:00
Clemens Eisenhofer
2882b92d3b Fixed logging in Release-mode 2022-11-21 17:47:47 +01:00
Jakob Rath
6e72a97727 Refactor assignment and search state 2022-11-21 17:25:15 +01:00
Clemens Eisenhofer
b116d5ac9e Fixed assignment bug for shifts/band 2022-11-21 16:40:28 +01:00
Clemens Eisenhofer
0341851958 Deal with special case that coefficients are multiples directly (Without calculating the symbolic inverse) 2022-11-21 14:36:01 +01:00
Clemens Eisenhofer
7cb87df00c Bug fix; may not rewrite inequality 2022-11-21 11:34:23 +01:00
Clemens Eisenhofer
133f3d0a02 Evaluate bitwise operations on values 2022-11-21 09:38:53 +01:00
Clemens Eisenhofer
5c3180562d Some more ways of calculating the inverse 2022-11-21 09:19:17 +01:00
Clemens Eisenhofer
5240a8382a Make it compile again 2022-11-20 17:34:37 +01:00
Clemens Eisenhofer
4f4d56eb91 Added alternative way of calculating number of trailing zeros + hamming distance 2022-11-20 17:25:04 +01:00
Clemens Eisenhofer
98d572b48b First try to generalize variable elimination 2022-11-20 11:35:12 +01:00
Jakob Rath
022c06f75d pdd::subst_get 2022-11-18 15:14:38 +01:00