mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-28 18:29:23 +00:00
Code Activity
18887 commits 46 branches 52 tags 178 MiB
Commit graph

1117 commits

Author SHA1 Message Date
Nikolaj Bjorner
fa3886136b adding Boolean propagation, watch; and factoring 2021-09-18 22:18:15 -04:00
Nikolaj Bjorner
f01da40e49 adding watches on Booleans 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-16 22:01:34 +01:00
Nikolaj Bjorner
c25fd71bf4 fixes 2021-09-16 10:10:50 +01:00
Nikolaj Bjorner
689c5b4e12 generalize level 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-15 16:46:30 +01:00
Nikolaj Bjorner
7e7f88ae3d fix backtracking from fi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-15 09:28:59 +01:00
Nikolaj Bjorner
3c8c8f5d40 update var dependency tracking 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-15 09:10:36 +01:00
Jakob Rath
34631d972d fix compiler warning 2021-09-14 15:10:17 +02:00
Jakob Rath
b90b888d0f add nicer way of adding inequalities with constants 2021-09-14 15:03:45 +02:00
Jakob Rath
c4e098b5d4 add hack for testing conflict resolution (but commented out) 2021-09-14 14:49:56 +02:00
Jakob Rath
a8e68ebf86 verify_sat should perform a semantic check 2021-09-14 14:49:20 +02:00
Jakob Rath
66a41383e8 remove remove_var 2021-09-14 14:45:03 +02:00
Jakob Rath
8103627e47 fix test_l4 2021-09-14 14:45:03 +02:00
Nikolaj Bjorner
f9b1b4e65d add mode to display to get constraints without wild-card notation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-14 14:13:31 +02:00
Jakob Rath
15ebbbda2c fix assertion 2021-09-14 14:04:35 +02:00
Jakob Rath
f04345724c Ensure core is conflicting also after set(v) 2021-09-14 11:24:09 +02:00
Jakob Rath
d9eca1f40f reset/set on successful superposition 2021-09-14 11:08:57 +02:00
Jakob Rath
640acd2ebc notes for later 2021-09-14 11:01:35 +02:00
Jakob Rath
d935714874 Track FI lemma in core; remove bailout_lemma 2021-09-14 11:01:06 +02:00
Jakob Rath
d36a658139 forbidden intervals fixes 2021-09-14 10:15:10 +02:00
Jakob Rath
43fef8e8ba External constraints need to remember their sign 2021-09-14 09:50:07 +02:00
Jakob Rath
50a5e24c69 Handle boolean conflict from input 2021-09-14 09:09:50 +02:00
Jakob Rath
18710a86d7 print clauses 2021-09-13 17:44:19 +02:00
Nikolaj Bjorner
c082ea4357 update dep 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-13 17:35:36 +02:00
Nikolaj Bjorner
9e6fd7cb70 Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat 2021-09-13 16:49:45 +02:00
Nikolaj Bjorner
705fd0d01d bailout quick 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-13 16:49:43 +02:00
Jakob Rath
067902bf31 Simplify revert_decision; disable resolving over new items for now 2021-09-13 16:21:14 +02:00
Jakob Rath
a4c3a8c640 more fixes 2021-09-13 16:01:22 +02:00
Jakob Rath
b6c478c2ca fix iterator 2021-09-13 15:34:06 +02:00
Jakob Rath
e5289f84a0 some fixes 2021-09-13 15:09:50 +02:00
Jakob Rath
cf80225fee lemma 2021-09-13 14:46:35 +02:00
Jakob Rath
8edcb9e268 deal with literals in conflict_core 2021-09-13 14:41:13 +02:00
Jakob Rath
1a810cc696 update saturation 2021-09-13 13:49:29 +02:00
Jakob Rath
412b6ffd4a fix build 2021-09-13 13:37:17 +02:00
Nikolaj Bjorner
6ffcea0bde Merge branch 'polysat' of https://github.com/z3prover/z3 into polysat 2021-09-13 13:14:29 +02:00
Nikolaj Bjorner
73b4e7f2a8 update set/unset mark for propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-13 13:14:07 +02:00
Jakob Rath
0ff87a9943 stats, comment 2021-09-13 11:51:19 +02:00
Jakob Rath
f1ce0e233a Handle bailouts in conflict_core 2021-09-13 11:48:28 +02:00
Jakob Rath
79d7ae5417 Remove fallback lemma 2021-09-13 11:43:04 +02:00
Jakob Rath
bb227c0d6e Track existing constraints with indexed_uint_set 2021-09-13 11:00:08 +02:00
Jakob Rath
6c8e8dada6 comments 2021-09-13 04:48:22 +02:00
Jakob Rath
71e97a4098 don't need marks in bool_var_manager anymore 2021-09-13 04:35:37 +02:00
Nikolaj Bjorner
7b9726a95c simpler 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-12 18:35:39 +02:00
Nikolaj Bjorner
8bc4932092 nits 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-12 18:30:55 +02:00
Nikolaj Bjorner
e365ad0e9e merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-12 18:14:25 +02:00
Nikolaj Bjorner
f5fd295e01 reorganize variable tracking for lemmas 
this is going to break a bunch
 2021-09-12 18:05:29 +02:00
Jakob Rath
6db8672f75 Update search_iterator 2021-09-12 16:23:54 +02:00
Jakob Rath
4933505cba remove from header 2021-09-12 16:11:47 +02:00
Jakob Rath
00cc81d1a4 remove another cm 2021-09-12 16:09:13 +02:00
Jakob Rath
a8c132f769 merge 'keep' and 'handle_saturation_premises' 2021-09-12 16:05:34 +02:00
Nikolaj Bjorner
deeb6c7784 remove cm 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2021-09-11 20:18:12 +02:00