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

20010 commits

This branch
This branch
All branches
Author SHA1 Message Date
Jakob Rath
cbb280d2b7 Use bv.solver parameter 2023-12-22 11:52:35 +01:00
Jakob Rath
e1a2c2fe47 wrap value 2023-12-22 11:08:41 +01:00
Jakob Rath
0e8de50d61 display 2023-12-22 11:08:41 +01:00
Jakob Rath
4dc77036a6 interval conflict fixes 2023-12-22 11:08:41 +01:00
Jakob Rath
c6ee5b76ad viable_slicing_interface 2023-12-21 15:31:18 +01:00
Jakob Rath
bb49c71ba9 viable propagation reason part 2 (explain equivalent pvars) 2023-12-21 14:58:10 +01:00
Jakob Rath
2ae91beb83 Add another case of interval reduction 2023-12-21 14:54:14 +01:00
Jakob Rath
8605dea8be fix alloc_entry 2023-12-21 14:42:46 +01:00
Jakob Rath
df0cd30754 fix viable propagation reason (part 1) 2023-12-21 14:37:13 +01:00
Jakob Rath
93dd0b6054 interval 2023-12-21 14:35:21 +01:00
Jakob Rath
8e84aac36c solver::eval 2023-12-21 14:34:12 +01:00
Jakob Rath
5b9ae557ed fix 2023-12-21 12:15:55 +01:00
Jakob Rath
dfd812884d vector: fix missing destructor call 2023-12-18 12:16:00 +01:00
Jakob Rath
48fd2bcfe8 restore commment 2023-12-18 12:02:41 +01:00
Jakob Rath
b279df7f85 fix merge failure 2023-12-18 11:39:21 +01:00
Jakob Rath
734c44b004 Merge remote-tracking branch 'origin/master' into polysat 2023-12-18 10:18:05 +01:00
Nikolaj Bjorner
2f2bf749b9 fixes to intblast encoding and more arithmetic rewriters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-17 18:15:51 -08:00
Nikolaj Bjorner
bb99f44214 fix bugs in elim-unconstr2 and fix bugs in intblast_solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-17 17:42:55 -08:00
Nikolaj Bjorner
4867073290 remove windowsArm64 from nightly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-17 10:04:49 -08:00
Nikolaj Bjorner
d0a59f3740 intblast with lazy expansion of shl, ashr, lshr 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-16 15:12:57 -08:00
Bruce Mitchener
50e0fd3ba6
Use noexcept more. (#7058) 2023-12-16 12:14:53 +00:00
Nikolaj Bjorner
b44ab2f620 add rewriters for and 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-15 14:55:02 -08:00
Nikolaj Bjorner
4778f27b46 revert to standard solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-15 14:33:23 -08:00
Nikolaj Bjorner
9293923b8a Add intblast solver 2023-12-15 13:50:38 -08:00
Nikolaj Bjorner
0520558fc0 port updated pdd from polysat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-15 08:54:03 -08:00
Christoph M. Wintersteiger
2e83352d42
Fix bug in fp.round_to_integral (#7060) 2023-12-15 08:34:27 -08:00
Bruce Mitchener
e90a844508
Use override more. (#7059) 2023-12-15 08:44:57 +00:00
Lev Nachmanson
f6e69d43a3 Merge branch 'master' of https://github.com/z3prover/z3 2023-12-14 08:21:21 -10:00
Christoph M. Wintersteiger
a2b490baa6
Disable Python compilation cache during build (#7057) 
* Disable Python compilation cache during build

* More pythonic check for none
 2023-12-14 07:26:52 -08:00
Jakob Rath
c45eb2a870 Fix assertion 2023-12-14 16:19:35 +01:00
Jakob Rath
d59b6e4efa polynomial superposition needs a different constraint query 2023-12-14 15:43:43 +01:00
Jakob Rath
6bde7e2c8c Unify the two recursive calls in find_on_layer 2023-12-14 15:01:49 +01:00
Jakob Rath
14fe69048a Fix recursive case of find_on_layer 
Even if the hole is bigger than lower layer domain size, we need to
start the search at the current value.
 2023-12-14 14:51:10 +01:00
Jakob Rath
b8f59d15c6 Fix propagation 2023-12-14 14:29:46 +01:00
Jakob Rath
18d966dc02 Rework handling of propagation reasons in viable 2023-12-14 12:20:45 +01:00
Nikolaj Bjorner
7c2e4f2f9c fiddle with what gets added to win-arm64 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-13 20:43:17 -08:00
Nikolaj Bjorner
f7d9a5ba93
Revert "Disable Python compilation cache during build (#7052)" (#7054) 
This reverts commit 8293be859f.
 2023-12-13 19:32:00 -08:00
Nikolaj Bjorner
b40e3015ef fix #7053 2023-12-13 19:25:18 -08:00
Nikolaj Bjorner
c20b8cb978 nightly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-13 18:46:20 -08:00
Nikolaj Bjorner
995b40865b remove readme reference, add arm64 build to nightly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-13 18:44:11 -08:00
Christoph M. Wintersteiger
8293be859f
Disable Python compilation cache during build (#7052) 
* Disable Python compilation cache during build

* Fix var name
 2023-12-13 18:05:33 -08:00
Bruce Mitchener
3ebec56880
tptr.h: Include <cstdint> once rather than twice. (#7051) 2023-12-13 09:36:41 -08:00
Lev Nachmanson
536f4f84bb Merge branch 'master' of https://github.com/z3prover/z3 2023-12-12 15:23:43 -10:00
Nikolaj Bjorner
0f4e96ac5d fix character 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-10 20:50:32 -08:00
Nikolaj Bjorner
5fc039d6ea nuget spec: does this work? 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-10 12:33:29 -08:00
Nikolaj Bjorner
5732c3c980 add readme under content 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-10 11:11:37 -08:00
Nikolaj Bjorner
91837c3aee try adding readme again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-10 10:22:41 -08:00
Nikolaj Bjorner
70d4f32ffd port updates from poly/polysat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-09 13:00:43 -08:00
Nikolaj Bjorner
e580c384b8 import updates to rational from polysat 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-09 12:46:06 -08:00
Nikolaj Bjorner
575538d325 follow error message to put dependencies in setup args 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-08 18:38:29 -08:00