mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity
19537 commits 49 branches 53 tags 182 MiB
Commit graph

19537 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
ea6827505e add missing callback to m_created_eh 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-25 10:13:09 +01:00
Nikolaj Bjorner
f639a7e1bc add marker for top-level expression in rule. 2022-01-24 15:20:44 +01:00
Nikolaj Bjorner
61ab72b6a3 fix #4869 2022-01-24 15:14:47 +01:00
Nikolaj Bjorner
3b8c0b7ae6 fix #5791 2022-01-24 15:11:24 +01:00
Nikolaj Bjorner
20f9814939 fix #5789 
fix incorrect constant folding
 2022-01-24 09:42:14 +01:00
Nikolaj Bjorner
d02235fe08 #5778 
not really specific to euf.true, but about rem(x,0) semantics that should align with mod semantics. It also reproduces without sat.euf=true.
 2022-01-22 16:16:48 +01:00
Hennadii Chernyshchyk
85f6456655
Add missing constness (#5787) 2022-01-21 15:32:25 +01:00
Nikolaj Bjorner
9969809745 #5778 2022-01-21 09:40:06 +01:00
Nikolaj Bjorner
a1f7676c81 remove assertion - literals could be assigned but propagation incomplete 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-21 03:10:41 +01:00
Nikolaj Bjorner
007af9cb8a fix #5784 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-21 03:08:03 +01:00
Nikolaj Bjorner
17280846f8 added comments to explain #5781 2022-01-21 01:40:31 +01:00
Nikolaj Bjorner
b1ff4bc24a no normalize 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-20 19:21:19 +01:00
Nikolaj Bjorner
75a81af426 fix #5786 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-20 19:18:23 +01:00
Nikolaj Bjorner
af9ae35984 term 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-20 14:43:16 +01:00
Nikolaj Bjorner
c527fda0b6 term 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-20 14:41:27 +01:00
Nikolaj Bjorner
f1a302bba7 term 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-20 14:38:34 +01:00
Nikolaj Bjorner
7a8c969033 ensure b_internalized 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-20 13:27:23 +01:00
Nikolaj Bjorner
a3d4e9a4e8 adding created to sat/smt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-20 11:48:27 +01:00
Nikolaj Bjorner
c00591daaf finish is-fixed 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-19 16:28:34 +01:00
Nikolaj Bjorner
e5767bf2b8 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-19 15:19:07 +01:00
Nikolaj Bjorner
0f03ef4ab0 for Clemens: ensure fixed values are propagated after registration 
Also allow to register expressions that the rewriter changes to ensure they get picked up.
 2022-01-19 14:38:11 +01:00
Nikolaj Bjorner
5b0389615b #5780 2022-01-19 10:10:36 +01:00
Nikolaj Bjorner
06feb71eb1 fix bug in root setting exposed by incremental mode pb_solver 2022-01-18 10:55:27 +01:00
Nikolaj Bjorner
36cfb88f5f add preliminary stub to handle closure types 2022-01-17 22:01:31 -08:00
Nikolaj Bjorner
d777306bb6 #5778 2022-01-17 10:43:15 -08:00
Nikolaj Bjorner
fcc9f379e7 #5778 2022-01-16 19:36:00 -08:00
Nikolaj Bjorner
a15da8f9ba #5778 2022-01-16 19:11:55 -08:00
Nikolaj Bjorner
637ddf9397 fix #5777 
latest issue
 2022-01-16 18:09:38 -08:00
Nikolaj Bjorner
0dd5a5e576 #5777 2022-01-16 17:46:08 -08:00
Nikolaj Bjorner
a48d3fdbb1 #5777 2022-01-16 14:01:49 -08:00
Nikolaj Bjorner
ea93345b75 #5777 2022-01-16 10:52:25 -08:00
Nikolaj Bjorner
cd56d55e34 #5753 2022-01-16 09:31:16 -08:00
Nikolaj Bjorner
bc9c6ad93d #5753 2022-01-15 18:01:31 -08:00
Nikolaj Bjorner
1b5f7cd9e5 na 2022-01-15 10:05:26 -08:00
Nikolaj Bjorner
17cfc1d034 #5753 2022-01-15 10:03:03 -08:00
Nikolaj Bjorner
74824ac901 #5753 
get_antecedent has to be well-founded. It got broken when using eval during propagation and egraph explain during conflict resolution.
 2022-01-15 09:35:25 -08:00
Nikolaj Bjorner
d09abdf58e fix #5771 
Missing congruence closure enforcement on auxiliary guard predicates.
It diverges but is sound.
 2022-01-14 15:46:40 -08:00
Nikolaj Bjorner
d5cc162fa7 bug in bounds 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-13 15:42:23 -08:00
Nikolaj Bjorner
2363bfc132 internalize arithmetic sub-terms #5753 2022-01-13 15:34:04 -08:00
Nikolaj Bjorner
e816946ddc handling unsimplified input 2022-01-13 14:40:46 -08:00
Nikolaj Bjorner
b259f46f85 dependencies 2022-01-13 12:34:58 -08:00
Nikolaj Bjorner
4b6679e8e0 #5753 2022-01-13 12:19:54 -08:00
Nikolaj Bjorner
366cd9b16d missing pb cases 2022-01-12 14:50:40 -08:00
Nikolaj Bjorner
dfe2b27f9a #5773 2022-01-12 13:28:15 -08:00
Nikolaj Bjorner
0720998bac #5753 2022-01-12 13:12:10 -08:00
Nikolaj Bjorner
10dc8d7313 #5753 2022-01-12 12:49:06 -08:00
Nikolaj Bjorner
56d3718cde add simplification with qe-lite as an option #5767 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-01-12 03:41:21 -08:00
Nikolaj Bjorner
08294d62e5 separate dependencies for qe_lite 2022-01-12 03:26:22 -08:00
Nikolaj Bjorner
2bcc814031 add macro to track closures declared in z3_api 
This is to ease integration with external API wrappers that rely on accessing
information about type names that are used.
#5762
 2022-01-12 02:47:39 -08:00
Nikolaj Bjorner
e5eaea46aa ensure m_true is assigned #5753 2022-01-11 10:42:05 -08:00