mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity
18625 commits 24 branches 48 tags 158 MiB
Commit graph

3060 commits

Author SHA1 Message Date
Nikolaj Bjorner
aed48e9f9b fix type of get-id 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-13 17:17:02 -08:00
Nikolaj Bjorner
d422f7b067 reorder fields 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-13 17:14:41 -08:00
Nikolaj Bjorner
01c5a09575 put ensure concat on a list 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-13 13:44:59 -08:00
Nikolaj Bjorner
0ca94b9c2f get-theory-id 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-13 12:22:11 -08:00
Nikolaj Bjorner
1f23ffb23c add placeholder for tracking theory justifications in EUF 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-13 11:59:01 -08:00
Nikolaj Bjorner
73b032ae4e propagate values in euf_bv_plugin over extract 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-13 11:46:53 -08:00
Nikolaj Bjorner
abc0cf3775 fix offset bug in explain 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-01-12 10:04:52 -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
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
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
03e012c1d8 bugfixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-29 15:13:11 -08:00
Nikolaj Bjorner
91b9d78cd3 bugfixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-28 17:36:42 -08:00
Nikolaj Bjorner
20afc55b41 misc bugfixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-28 14:24:52 -08:00
Nikolaj Bjorner
737913b67e bugfixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-27 14:00:28 -08:00
Nikolaj Bjorner
6103c9d718 bug fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-27 11:29:42 -08:00
Nikolaj Bjorner
fbbad72c29 use lazy explanation function for slices, use euf-bv-plugin to extract slices 2023-12-23 11:10:18 -08:00
Nikolaj Bjorner
0353177fe0 import master branch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-16 16:56:09 -08:00
Nikolaj Bjorner
c03a05eb75 axioms for b-and 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-16 16:29:11 -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
9293923b8a Add intblast solver 2023-12-15 13:50:38 -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
Nikolaj Bjorner
8e26c2af17 fix #7049 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-08 13:05:21 -08:00
Christoph M. Wintersteiger
6910a4e18c
Fix to_fp_signed (#7034) 2023-12-03 16:38:06 -08:00
Nikolaj Bjorner
ea3628e50b remove hoist functionality 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-03 16:28:43 -08:00
Nikolaj Bjorner
1de25ed09c pending files 2023-12-02 19:43:51 -08:00
Nikolaj Bjorner
ba8d8f0af7 Disable hoist entirely, it is bad on QF_LIA and does not help on other observed cases 2023-12-02 15:40:47 -08:00
Nikolaj Bjorner
5c1e7f7112 fix #7029 2023-12-02 10:48:40 -08:00
Nikolaj Bjorner
a15a7cee7b touch 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-01 14:13:05 -08:00
Nikolaj Bjorner
faf14012ba Regressions reported by Guido 2023-12-01 13:32:13 -08:00
Nikolaj Bjorner
b52fd8d954 add EUF plugin framework. 
plugin setting allows adding equality saturation within the E-graph propagation without involving externalizing theory solver dispatch. It makes equality saturation independent of SAT integration.
Add a special relation operator to support ad-hoc AC symbols.
 2023-11-30 13:58:30 -08:00
Nikolaj Bjorner
26440ed3d8 deal with ubuntu/clang warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-11-29 15:45:19 -08:00
Nikolaj Bjorner
e9abdbb7a4 fix #7011 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-11-29 15:08:08 -08:00
Nikolaj Bjorner
2f01b5b567 re-enable delayed literal propagation 2023-11-29 14:00:17 -08:00
Nikolaj Bjorner
4289cfac8d revert some fixes to euf 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-11-29 13:47:59 -08:00
Nikolaj Bjorner
d469c1054e remove separate to_add_literal queue 2023-11-29 12:45:43 -08:00
Nikolaj Bjorner
e972eb33b2 #6523 - contains_ptr bug regarding etable reinserts 2023-11-29 10:44:36 -08:00
Nikolaj Bjorner
79bbbf76d0 fix #7006 2023-11-28 15:06:27 -08:00
Bruce Mitchener
9d1ceab1f2
cmake: Use FindPython3. (#7019) 
`FindPythonInterp` has been deprecated for a long time and is more
verbal about that deprecation now.

The build system no longer uses `PYTHON_EXECUTABLE` but instead uses
`Python3_EXECUTABLE`.
 2023-11-27 11:20:21 +01:00
Nikolaj Bjorner
b9455c3692 #6999 deal with implicit assumptions, more robust pattern matching 
The code is making some assumptions that arrays are 1-dimensional. This is not generally true.
Introducing pattern matching to ensure the assumption is met.
Avoid get_arg(..) especially when there is an approach based on pattern matching recognizers.
 2023-11-17 10:06:20 -08:00
Nikolaj Bjorner
ad2107f079 fix #6978 2023-11-14 08:45:22 -08:00
Nikolaj Bjorner
f97dd34028 tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-10-30 14:54:04 -07:00
Christoph M. Wintersteiger
9d57bdd2ef
Assorted fixes for floats (#6968) 
* Improve 4be26eb543

* Add-on to 0f4f32c5d0

* Fix mk_numeral

* Fix corner-case in fp.div

* Fixes for corner-cases in mk_to_fp_(un)signed

* Fix out-of-range results in mpf_manager::fma

* Further adjustments for fp.to_fp_(un)signed

* fp.to_fp from real can't be NaN

* fp.to_fp from reals: add bounds

* Fix NaN encodings in theory_fpa.

* Fix fp.fma rounding with tiny floats

* Fix literal creation order in theory_fpa
 2023-10-29 17:29:42 -07:00
Nikolaj Bjorner
93427f1175 regression test 2447 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-10-26 08:48:58 -07:00
Nikolaj Bjorner
0b8d7b755d useful string rewrites 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-10-26 03:48:50 -07:00