mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-10 15:20:30 +00:00
Code Activity
19120 commits 48 branches 58 tags 223 MiB
Commit graph

2480 commits

Author SHA1 Message Date
Jakob Rath
a4f14fa29f fix prefix constraint 2024-05-14 19:33:32 +02:00
Jakob Rath
1f686126a3 guard against stale explain_kind 2024-05-14 19:16:31 +02:00
Jakob Rath
962edfd03c set proper explain_kind in case of full interval 2024-05-14 19:13:34 +02:00
Jakob Rath
47d93037f7 fix prefix 2024-05-14 18:54:29 +02:00
Jakob Rath
705d94d883 reduce output 2024-05-14 16:44:44 +02:00
Jakob Rath
ec0224912b enable 2024-05-14 16:37:40 +02:00
Jakob Rath
5b8c6a98c2 fix? 2024-05-14 16:34:31 +02:00
Jakob Rath
38745512c0 first attempt at new explain_overlap 2024-05-14 16:22:57 +02:00
Jakob Rath
764ccebcbf Add constraints::fixed 2024-05-14 15:03:30 +02:00
Jakob Rath
cc799bbfc1 fix sign_extend 2024-05-14 10:57:25 +02:00
Jakob Rath
b640ea775a begin updated viable-conflict 
copy explain_overlap
 2024-05-14 10:40:26 +02:00
Jakob Rath
1292fb2adb extra px < qx axioms 2024-05-13 22:46:49 +02:00
Jakob Rath
d28441bd8f Add additional ashr axiom 2024-05-13 15:21:17 +02:00
Jakob Rath
fb5a40a6fd fix sle 2024-05-13 15:14:49 +02:00
Jakob Rath
94955e3fae Merge remote-tracking branch 'origin/master' into poly 2024-05-11 23:30:53 +02:00
Jakob Rath
a3c85d3a60 subsumption hotfix 2024-05-11 17:54:59 +02:00
Jakob Rath
2494ffacaf print validation num_check 2024-05-11 14:23:54 +02:00
Jakob Rath
c3ffbf05db fix bv type error in projection check 2024-05-11 14:16:18 +02:00
Jakob Rath
d335b6b035 add missing include 2024-05-11 12:44:57 +02:00
Jakob Rath
f904c08116 enable the saturation rules 2024-05-10 14:59:19 +02:00
Jakob Rath
7925ef731f relax eq_resolve conditions 
fixes Example 1
 2024-05-06 15:24:00 +02:00
Jakob Rath
0a8879b505 also normalize or_op 2024-05-06 13:26:17 +02:00
Jakob Rath
c7a80eaf5d port additional simplification from polysat branch 2024-05-06 13:16:10 +02:00
Jakob Rath
7a3349eeae disable assertions for now 2024-05-03 10:03:03 +02:00
Jakob Rath
f8c593edf9 remove unused ckind_t::smul_fl_t 2024-04-23 14:38:33 +02:00
Nikolaj Bjorner
cbef183ae5 type check equality injectivity axiom 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-04-20 14:57:04 -04:00
Nikolaj Bjorner
e184a9a711 fix translation of bvudiv 2024-04-20 07:32:52 -04:00
Nikolaj Bjorner
0368b52716 add missing expr 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-04-17 15:16:11 +02:00
Jakob Rath
69ea52407f refactor, update comment 2024-04-15 11:18:42 +02:00
Nikolaj Bjorner
2682c2ef2b sls updates 
- add SINGLE_THREAD mode
- add interface to retrieve "best" model so far
 2024-04-13 16:42:26 +02:00
Jakob Rath
06e5595e87 revert for now 2024-04-12 14:35:12 +02:00
Nikolaj Bjorner
43dd6a5436 include mutex 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-04-11 18:19:58 +02:00
Jakob Rath
183f96b481 explain_hole_overlap wip 2024-04-11 11:26:07 +02:00
Jakob Rath
138c90d52b explain_overlap, notes on case ebw < abw 2024-04-11 11:19:49 +02:00
Jakob Rath
adea39b92e dbg output 2024-04-11 11:12:49 +02:00
Jakob Rath
020a4d5d04 r_interval::contains 2024-04-11 11:11:02 +02:00
Nikolaj Bjorner
c0bdc7cdd6 enable concurrent sls with new solver core 
allow using sls engine (for bit-vectors) with the new core.

Examples

z3 sat.smt=true tactic.default_tactic=smt /v:1 smt.sls.enable=true smt.bv.solver=0 /st C:\QF_BV_SAT\bench_10.smt2
z3 sat.smt=true tactic.default_tactic=smt /v:1 smt.sls.enable=true smt.bv.solver=2 /st C:\QF_BV_SAT\bench_10.smt2
z3 C:\QF_BV_SAT\bench_11100.smt2 sat.smt=true tactic.default_tactic=smt /v:1 smt.sls.enable=true smt.bv.solver=2 /st
 2024-04-11 10:49:30 +02:00
Jakob Rath
3f3b052933 move modification to the front 2024-04-04 10:28:08 +02:00
Jakob Rath
2b89767d1f ensure smaller layers are visited first 2024-04-03 18:25:18 +02:00
Jakob Rath
18eeb48b34 invalidated reference 2024-04-03 17:58:35 +02:00
Jakob Rath
b808dece15 always restart find_overlap at smallest size 2024-04-03 17:38:43 +02:00
Jakob Rath
583c40de1f check 2024-04-03 16:42:17 +02:00
Jakob Rath
4a51139bc8 fix marking for redundancy 2024-04-03 16:41:21 +02:00
Jakob Rath
017ae78c81 enable removal of redundant explanations 2024-04-03 15:38:33 +02:00
Jakob Rath
c5b02f8360 simplify side conditions on reduced intervals 2024-04-03 15:38:33 +02:00
Jakob Rath
d19de4b1d3 fixed_bits notes 2024-04-03 15:38:33 +02:00
Jakob Rath
60422d2071 separate terminology (suffix vs. overlap) 2024-04-02 16:34:49 +02:00
Jakob Rath
17131983fe use loop instead of goto 2024-04-02 16:31:51 +02:00
Jakob Rath
88be5e6611 check hole_len 2024-04-02 16:28:45 +02:00
Jakob Rath
47f28c6857 find_overlap should stay on lower bit-width to find conflicts 2024-04-02 16:27:29 +02:00