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

3039 commits

Author SHA1 Message Date
Nikolaj Bjorner
dc83c5b28d fix #7049 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-13 20:04:47 -08:00
Nikolaj Bjorner
06ebf9a02a n/a 2023-12-12 14:41:31 -08:00
Nikolaj Bjorner
b72575148f axioms for b-and 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-11 15:45:54 -08:00
Nikolaj Bjorner
17c480f837 adding band 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-12-11 14:51:21 -08:00
Nikolaj Bjorner
9373e1b7f5 intblast debugging 2023-12-11 10:00:11 -08:00
Nikolaj Bjorner
f89de2b455 more internalize cases 2023-12-10 23:49:23 -08:00
Nikolaj Bjorner
83c71b4943 fix internalization for quot/rem 2023-12-10 22:21:14 -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
Nikolaj Bjorner
7b490543ca add missing simplification; handle nit #6952 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-10-25 10:00:15 -07:00
Nikolaj Bjorner
0859be5649 #6953 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-10-25 09:07:04 -07:00
Nikolaj Bjorner
8fac89cdcc enable more simplification in case inequality triggers a change. 2023-10-21 19:58:39 -07:00
Nikolaj Bjorner
5942dc24bd #6523 2023-10-15 11:41:25 -07:00
Nikolaj Bjorner
61319ffd85 cache is_shared information in the enode 
observed perf overhead for QF_NIA is that assume_eqs in theory_lra incurs significant overhead when calling is_relevant_and_shared. The call to context::is_shared and the loop checking for beta redexes is a main bottleneck. The bottleneck is avoided by caching the result if is_shared inside the enode. It is invalidated for every merge/unmerge.
 2023-09-23 17:19:06 -07:00
Nikolaj Bjorner
643512613a simplify last_index function 2023-09-18 12:52:59 -07:00
Nuno Lopes
b1c52c0b16 don't crash when a function doesn't have a model when converting a solver to string 2023-09-18 10:16:19 +01:00
Nikolaj Bjorner
b87a91379c fix #6894 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-14 17:14:14 -07:00
Nikolaj Bjorner
50d76a2fe3 fix #6894 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-14 17:14:14 -07:00
Nikolaj Bjorner
4d9af7848d add parameter to disable pattern inference #6884 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-03 15:27:37 -07:00
Nikolaj Bjorner
99239068ba some template instantiations #6869 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-09-03 15:21:49 -07:00
Nuno Lopes
00593609c5 minor code simplification 2023-08-30 12:50:29 +01:00
Nikolaj Bjorner
63467f9dfa fix #6876 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-25 17:14:35 -07:00
Nikolaj Bjorner
1d9e0feb84 Merge branch 'master' of https://github.com/z3prover/z3 2023-08-21 09:19:16 -07:00
Nikolaj Bjorner
79aa317af4 remove if-def inside cpp file that should not be there #6869 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-21 09:19:06 -07:00
Nuno Lopes
57c667e355 remove unused code 2023-08-20 15:16:47 +01:00
Nuno Lopes
8210aafb69 ast compare_nodes: fail faster when comparing quantifier expressions 2023-08-20 14:09:04 +01:00
Nikolaj Bjorner
5e3df9ee77
Arith min max (#6864) 
* prepare for dependencies

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* snapshot

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* more refactoring

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* more refactoring

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* build

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* pass in u_dependency_manager

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* address NYIs

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* more refactoring names

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* eq_explanation update

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* add outline of bounds improvement functionality

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fix unit tests

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove unused structs

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* more bounds

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* more bounds

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* convert more internals to use u_dependency instead of constraint_index

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* convert more internals to use u_dependency instead of constraint_index

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remember to push/pop scopes

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* use the main function for updating bounds

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* remove reset of shared dep manager

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* disable improve-bounds, add statistics

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

---------

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-19 17:44:09 -07:00
Nikolaj Bjorner
63ea8efcfb remove output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-17 15:20:12 -07:00
Nikolaj Bjorner
51df7b75ce fix 6800 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-17 15:18:22 -07:00
Nikolaj Bjorner
6366f8f6b2 na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2023-08-13 14:05:07 -07:00