mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity
19211 commits 49 branches 53 tags 182 MiB
Commit graph

187 commits

Author SHA1 Message Date
Nikolaj Bjorner
ecc302bdc8 fix trace build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-25 11:38:58 -08:00
Nikolaj Bjorner
d805322dfb create separate file for expression based lookahead solver 2025-01-25 11:19:40 -08:00
Nikolaj Bjorner
f6e7dcff47 Fix crash exposed in QF_UFNIA 2025-01-24 15:31:10 -08:00
Nikolaj Bjorner
9e8dd68ee6 disable lookahead on compound values (fixes bug reported by Clemens), bail to rationals when there are reals. 2025-01-24 11:01:18 -08:00
Nikolaj Bjorner
053349cd36 remove incorrect calls to VERIFY in array solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-24 09:54:21 -08:00
Nikolaj Bjorner
0e8969ce60 deal with compiler warnings and include value exchange prior to final check. 2025-01-24 09:40:33 -08:00
Nikolaj Bjorner
ce615ee116 avoid repeated clauses during scoring function 2025-01-23 10:51:12 -08:00
Nikolaj Bjorner
b149d1f803 count every lookahead as activity 2025-01-22 22:57:43 -08:00
Nikolaj Bjorner
4d33f442b9 enable value import in parallel mode 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-22 22:45:01 -08:00
Nikolaj Bjorner
e32f685f14 disable backoff on smt->sls value export 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-22 22:15:10 -08:00
Nikolaj Bjorner
beb9d2e553 update restart next 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-22 21:40:35 -08:00
Nikolaj Bjorner
ec3915218d modify backoff mechanisms and theory exchange 2025-01-22 20:32:30 -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
decaee83f3 move from justified_expr to dependent_expr by aligning datatypes 2025-01-22 11:46:10 -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
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
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
f422e26b3c add case for ite 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-15 18:53:26 -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
11909cfdff allow a plateau mode 2025-01-14 16:38:12 -08:00
Nikolaj Bjorner
8515cebd19 add plateau option 2025-01-14 13:54:20 -08:00
Nikolaj Bjorner
a08a3ee32b align reslimit with ddfw 2025-01-13 18:19:35 -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
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
Nikolaj Bjorner
b780b54574 optimization of sls-arith and fix build warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-12 09:49:48 -08:00
Nikolaj Bjorner
49dba337f7 fix ubuntu clang build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-11 20:02:31 -08:00
Nikolaj Bjorner
c6f58c8bf7 updates to some_string_in_re per code review comments 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-11 17:47:27 -08:00
Clemens Eisenhofer
c572fc2e4f
Regex membership (#7506) 
* Make finding a word in the regex iterative

* Fixed gc problem
 2025-01-11 17:41:37 -08:00
Nikolaj Bjorner
9a237d55ca fix misc build warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-11 17:41:24 -08:00
Nikolaj Bjorner
d97bd48669 adding lookahead mode to arithmetic sls solver 2025-01-11 15:47:17 -08:00
Nikolaj Bjorner
847278fba8 adding global lookahead variant to sls arith solver 2025-01-09 16:47:33 -08:00
Clemens Eisenhofer
5c60c6662c
Small seq-sls fixes (#7503) 
* Calculation based on wrong update list

* Fixed regex problem
 2025-01-07 09:26:00 -08:00
Nikolaj Bjorner
e133a297ba change score for comparisons to use hamming distance 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-07 03:58:44 -08:00
Nikolaj Bjorner
f77f259542 fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-06 18:12:12 -08:00
Nikolaj Bjorner
b6f45bcd9f limit lookahead count to 20 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-06 18:06:00 -08:00
Nikolaj Bjorner
aed0ad3505 limit lookahead count to 10 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-06 17:40:17 -08:00
Nikolaj Bjorner
59fad2b10a shave off bv test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-06 17:25:30 -08:00
Nikolaj Bjorner
e3e650a249 optimzie 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-06 15:36:20 -08:00
Nikolaj Bjorner
6787d87623 hoist update stack creation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-06 13:16:07 -08:00
Nikolaj Bjorner
5a5570ef4e remove type check in insert_update 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-06 11:12:08 -08:00
Nikolaj Bjorner
67827bfe56 restore nyi trace 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-01-06 08:37:14 -08:00