mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity
18653 commits 49 branches 53 tags 182 MiB
Commit graph

15838 commits

Author SHA1 Message Date
Jakob Rath
80184c6ee2 fix ashr axioms 2024-01-11 18:09:17 +01:00
Nikolaj Bjorner
9fb9e659b0 full interval case 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-11 08:44:16 -08:00
Nikolaj Bjorner
86de8bd5b1 add case for exclude 0 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-10 17:19:10 -08:00
Nikolaj Bjorner
17f4e8033f add associativity up front in internalize 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-10 17:01:53 -08:00
Nikolaj Bjorner
33c37cfdf0 bugbash bit-wise operations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-10 16:05:55 -08:00
Nikolaj Bjorner
33f17215f7 bugfixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-10 11:00:16 -08:00
Nikolaj Bjorner
e7c9c5f7a2 add built-in support for bvor: the rewriter converts bitwise and to bit-wise or so using bvor as a basis makes better sense 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-10 10:16:31 -08:00
Nikolaj Bjorner
e2c5d7d358 bugbash 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-09 15:30:33 -08:00
Nikolaj Bjorner
3e23ff9bad bugbash 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-09 14:16:16 -08:00
Nikolaj Bjorner
21711a14f5 bugbash 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-09 14:15:25 -08:00
Nikolaj Bjorner
f34e55e86e bugfix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-08 20:44:30 -08:00
Nikolaj Bjorner
cc4ed602e5 inline propagation when adding new viable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-08 20:31:14 -08:00
Nikolaj Bjorner
e26d597917 working on unit propagation explanation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-07 15:29:18 -08:00
Nikolaj Bjorner
11c529162d add facility to support propagation 2024-01-06 16:26:03 -08:00
Nikolaj Bjorner
30c0771d24 redo fixed bits, add simplifications to intblast solver 2024-01-06 16:12:01 -08:00
Nikolaj Bjorner
c4b7061590 bugbash 
fix missing justification in explain_slice
tune intblast solver with some simplifications
bypass conflicts if the state is already conflicting
 2024-01-04 20:14:22 -08:00
Nikolaj Bjorner
cb672c7992 overflow example works 
- introduce weak/strong eval to temper unit propagation to use only weak evaluation.
- harness the amount of interval propagation provided on overflow constraints
- weak evaluation on overflow constraints is now trivialized
- viable insertion also does conflict detection
 2024-01-04 15:55:24 -08:00
Nikolaj Bjorner
5fc208cefc improve diagnostics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-04 11:07:09 -08:00
Nikolaj Bjorner
7b0c04a3e8 bugbash 2024-01-04 10:54:02 -08:00
Nikolaj Bjorner
f71219a9d0 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-03 20:28:57 -08:00
Nikolaj Bjorner
f805130c0b chain viables 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-03 20:22:01 -08:00
Nikolaj Bjorner
1cdefa81b7 degree reduction simplification to help int-blasting 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-03 13:46:27 -08:00
Nikolaj Bjorner
698c627359 bugbash 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-03 13:13:58 -08:00
Nikolaj Bjorner
3e13fe1fb2 bugbash 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-03 13:13:43 -08:00
Nikolaj Bjorner
f5aec6ecdf bugbash 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-03 13:12:42 -08:00
Nikolaj Bjorner
5730cad4e0 working on viable/explain 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-03 10:56:56 -08:00
Nikolaj Bjorner
e670194a2d filling in viable conflict analysis 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-03 10:10:57 -08:00
Nikolaj Bjorner
83b5352db6 fixing viable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-03 08:27:23 -08:00
Nikolaj Bjorner
21236dc80a working on viable explanations 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-02 16:20:13 -08:00
Nikolaj Bjorner
b706434282 bugfixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-02 14:30:09 -08:00
Nikolaj Bjorner
1a742ff784 bugfixes 2024-01-02 09:45:13 -08:00
Nikolaj Bjorner
c467f093d0 bugfixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-02 08:23:28 -08:00
Nikolaj Bjorner
f70f1bb85c bugfixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-01 19:43:38 -08:00
Nikolaj Bjorner
7fd1c171ce na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-01 19:11:29 -08:00
Nikolaj Bjorner
adebd2fd94 debugging 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-01 19:10:11 -08:00
Nikolaj Bjorner
141ba7661f monotone overflow 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-01 16:55:02 -08:00
Nikolaj Bjorner
d91820fe51 bug fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-01 16:24:15 -08:00
Nikolaj Bjorner
7dea0b855b fixup overflow rules 2024-01-01 13:40:48 -08:00
Nikolaj Bjorner
fb5f81cf75 add bit blast optio 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-01 11:08:30 -08:00
Nikolaj Bjorner
09b3d99db1 tidy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-31 17:09:49 -08:00
Nikolaj Bjorner
30b5b3bd15 cleanup op-defs 2023-12-31 16:47:15 -08:00
Nikolaj Bjorner
ff7854f4ea build fixes 2023-12-31 15:51:15 -08:00
Nikolaj Bjorner
7dd37a748d import equality superposition 2023-12-31 15:40:04 -08:00
Nikolaj Bjorner
b25451bd87 cleanup 2023-12-31 15:22:21 -08:00
Nikolaj Bjorner
57cb999061 display monomials 2023-12-31 15:05:57 -08:00
Nikolaj Bjorner
483508d257 move all saturation functionality into saturation.cpp, differentiate basic multiplication by -1, 1 from other powers of 2. 2023-12-31 14:42:10 -08:00
Nikolaj Bjorner
7bd7faa722 add proof checker plugin 
fixes to monomials
 2023-12-31 05:30:21 -08:00
Nikolaj Bjorner
32825a26cb Update hints to carry premises 2023-12-30 17:29:36 -08:00
Nikolaj Bjorner
f328ddf88e Add monomials container to keep track of non-linear multipliers 
Refine constraints to include an unfolded version of them where multiplier definitions are expanded.
 2023-12-30 14:14:12 -08:00
Nikolaj Bjorner
78f32401ac bugfixes 2023-12-29 18:11:40 -08:00