mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-28 18:29:23 +00:00
Code Activity
19999 commits 46 branches 52 tags 178 MiB
Commit graph

19999 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
3a3e176dce fix build for tests 2025-01-22 13:30:12 -08:00
Nikolaj Bjorner
6893e782ed add cases for new parameters for ts build 2025-01-22 11:59:36 -08:00
Nikolaj Bjorner
bd566f16b1 Expose PARAMETER_INTERNAL and PARAMETER_ZSTRING in case API users access these #7522 2025-01-22 11:46:11 -08:00
Nikolaj Bjorner
ef275ab1a0 fix #7523 2025-01-22 11:46:11 -08:00
Nikolaj Bjorner
4fce314bf2 improve diagnostics for flips 2025-01-22 11:46:10 -08:00
Nikolaj Bjorner
72c7a9cf6a fix re-entrancy bug between ddfw and theory solvers. 
Flips triggered from external sources should not trigger callbacks.
 2025-01-22 11:46:10 -08:00
Nikolaj Bjorner
071c9abd69 Update macro_finder.cpp 
move to justified_expr
 2025-01-22 11:46:10 -08:00
Nikolaj Bjorner
decaee83f3 move from justified_expr to dependent_expr by aligning datatypes 2025-01-22 11:46:10 -08:00
Michał Górny
fc9ff946b7
use cmake from PyPI only when system executable is not available (#7514) 
Rather than pulling `cmake` from PyPI unconditionally, add it to build
dependencies only if the system `cmake` executable cannot be found.
This eliminates an unnecessary dependency on systems featuring CMake,
and ensures that whenever possible, a downstream patched CMake version
is used that is more compatible with the system in question.
 2025-01-21 14:39:19 -08:00
dependabot[bot]
45ff1f4df3
Bump docker/build-push-action from 6.10.0 to 6.12.0 (#7516) 
Bumps [docker/build-push-action](https://github.com/docker/build-push-action) from 6.10.0 to 6.12.0.
- [Release notes](https://github.com/docker/build-push-action/releases)
- [Commits](https://github.com/docker/build-push-action/compare/v6.10.0...v6.12.0)

---
updated-dependencies:
- dependency-name: docker/build-push-action
  dependency-type: direct:production
  update-type: version-update:semver-minor
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2025-01-21 14:38:40 -08:00
Nikolaj Bjorner
d944779e18 move away from sets and into vectors for data associated with Boolean variables 2025-01-21 14:30:11 -08:00
Nikolaj Bjorner
92ad285951 use vector instead of indexed uint set for Boolean var occurrences 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-21 13:35:48 -08:00
Nikolaj Bjorner
eebff13f8b don't store full use list of clauses to avoid space overhead 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-21 13:23:13 -08:00
Nikolaj Bjorner
fb0eb029a8 use lifted bool 2025-01-21 09:13:38 -08:00
Clemens Eisenhofer
1553bae20c
Performance improvements for seq-sls (#7519) 
* Improve length repair

* Fixed arguments

* Special case regex membership with constant string

* Trying hybrid eq-repair strategy

* Different heuristic

* Fixed stoi
 2025-01-21 08:01:59 -08:00
Nikolaj Bjorner
3cdcd831b1 fix build breaks 2025-01-20 20:36:26 -08:00
Nikolaj Bjorner
a3f7541719 fix #7517 2025-01-20 19:04:36 -08:00
Nikolaj Bjorner
fb5834268e fix unit tests, add subsampling mode for false literals 2025-01-20 17:34:59 -08:00
Nikolaj Bjorner
22e4054674 add clausal lookahead to arithmetic solver as part of portfolio 
have legacy qfbv-sls solver use nnf pre-processing. It relies on it for correctness of the score updates.
 2025-01-20 16:16:46 -08:00
Nikolaj Bjorner
a941f5ae84 reset m_conflict indicator on sls model 2025-01-15 20:56:44 -08:00
Nikolaj Bjorner
557c01a0e5 fix #7499 - add another way to avoid adding user-defined functions to models if user don't want it 
- you can already do model.user_functions=false
- now you can also specify smtlib2_compliant (globally) and get smtlib2 behavior
 2025-01-15 19:52:04 -08:00
Nikolaj Bjorner
a5e1e7f5d2 set lookahead mode to default 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-15 19:10:25 -08:00
Nikolaj Bjorner
158dea575b add case for ite 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-15 19:07:18 -08:00
Nikolaj Bjorner
eed3fa6d49 add case for ite 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-15 18:54:50 -08:00
Nikolaj Bjorner
f422e26b3c add case for ite 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-15 18:53:26 -08:00
Nikolaj Bjorner
5365952796 fix #7510 2025-01-15 13:12:20 -08:00
Nikolaj Bjorner
a84130e844 prepare update stack for Boolean lookaheads 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-15 12:33:31 -08:00
Nikolaj Bjorner
498c9a686b throw exceptions where sls lacks support 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-15 11:20:03 -08:00
Nikolaj Bjorner
5fec07a57e fix unit test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-15 08:38:14 -08:00
Nikolaj Bjorner
878fd48819 fix compiler warning 2025-01-14 16:38:22 -08:00
Nikolaj Bjorner
11909cfdff allow a plateau mode 2025-01-14 16:38:12 -08:00
Nikolaj Bjorner
076d3dbf13 fix assertion violation in the code path where the simplifier throws a memout exception 2025-01-14 16:37:53 -08:00
Nikolaj Bjorner
31d4ba0009 re-introduce option to dump arithmetic lemmas to std-out 2025-01-14 13:54:56 -08:00
Nikolaj Bjorner
8515cebd19 add plateau option 2025-01-14 13:54:20 -08:00
Nikolaj Bjorner
648cf9602e fix uninitialized variable warnings 2025-01-14 13:54:05 -08:00
Lev Nachmanson
27cc928631 try m_fixed_var_eh 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-01-14 07:11:53 -10:00
Nikolaj Bjorner
8c5abdf818 Can's fix to relevancy propagation 2025-01-14 08:14:53 -08:00
Nikolaj Bjorner
89ed4d6c8b use monomial variable, not the fixed variable 2025-01-14 07:27:59 -08:00
Nikolaj Bjorner
a08a3ee32b align reslimit with ddfw 2025-01-13 18:19:35 -08:00
Nikolaj Bjorner
3c5b8bd03d Update parray.h 
deal with compiler warnings by initializing m_elem
 2025-01-13 18:19:12 -08:00
Nikolaj Bjorner
c01336553e move fixed variable propagation to nla_core/monomial_bounds 2025-01-13 18:18:53 -08:00
Nikolaj Bjorner
f3e7c8c9df include QF_SNIA 2025-01-13 08:13:39 -08:00
Nikolaj Bjorner
943d881340 fixes to hybrid mode 2025-01-12 16:59:27 -08:00
Nikolaj Bjorner
9770c00592 adjust heuristic in random-inc-dec for finite domains 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-12 14:23:18 -08:00
Nikolaj Bjorner
97acf71d2d fixup registration with new terms during internalization 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-12 14:12:02 -08:00
Nikolaj Bjorner
d3183fafc7 remove binspr experiment 2025-01-12 13:39:26 -08:00
Nikolaj Bjorner
8d2b9b41fd fix compiler warnings 2025-01-12 13:39:13 -08:00
Nikolaj Bjorner
85356c5548 enable propagation when there are changed columns 
- to fix bug reported by Nikhil Swamy/F*
- deal with some compiler warnings by adding annotations
 2025-01-12 13:30:31 -08:00
Nikolaj Bjorner
558758fcf1 another stab at fixing substring interval extraction combinatorics 
- i is the offset into val_other. The valid offsets are 0... |val_other|-1.
- j is the length of the substring. It only makes sense to extract strings of length 1,... |val_other|-i
 2025-01-12 11:14:17 -08:00
Nikolaj Bjorner
fa22b646aa address some build warnings. 2025-01-12 10:18:11 -08:00