mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity
20014 commits 23 branches 48 tags 156 MiB
Commit graph

20014 commits

This branch
This branch
All branches
Author SHA1 Message Date
Jakob Rath 134f677ec3 skip empty layers 2023-12-22 13:25:45 +01:00
Jakob Rath 6f93ec26ba no recursive polysat calls 2023-12-22 13:23:45 +01:00
Jakob Rath f111bd4de3 remove outdated assertions 2023-12-22 12:10:15 +01:00
Jakob Rath 5ad4d1017e reset tmp vectors 2023-12-22 11:57:31 +01:00
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