mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 22:59:02 +00:00
Code Activity
19095 commits 23 branches 48 tags 157 MiB
Commit graph

3243 commits

Author SHA1 Message Date
Nikolaj Bjorner 81678923a1 take into account for empty vars 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-12-30 12:15:27 -08:00
Clemens Eisenhofer 27cb81e7e6
Several changes to make sls terminate more often with length/extract operations (#7498) 
* Fixed range regex

* Fix sls for str.at

* Added case for str.at

* Pad/Truncate string in sls extract/length to fit length constraints

* Guarded index check

* Added missing progressing cases in extraction

* Add padding if required

* Commented out debug output
 2024-12-30 10:53:27 -08:00
Nikolaj Bjorner 4773bec975 check for null before debug assertions 2024-12-30 09:44:23 -08:00
Nikolaj Bjorner d8741b4aec have apply-update check can_set instead of caller 2024-12-30 08:56:09 -08:00
Nikolaj Bjorner bcf66f214f code cleanup, add comments 2024-12-30 08:51:49 -08:00
Clemens Eisenhofer 19c95f8561
Add new string repair heuristic (#7496) 
* Fixed spurious counterexamples in seq-sls. Updates might not be identity mapping

* Removed debug code

* One check was missing

* Trying different update generation function

* Renamed function

* Added parameter to select string update function
 2024-12-30 08:49:07 -08:00
Clemens Eisenhofer e002c57aa2
Fixed range regex (#7497) 2024-12-30 08:48:09 -08:00
Nikolaj Bjorner d81de1a67e align updated version of lookahead with legacy heuristics 2024-12-29 21:22:32 -08:00
Nikolaj Bjorner 6ea68310c9 fix stack overflow regression in bool_rewriter 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-12-28 18:21:59 -08:00
Nikolaj Bjorner 3526d03cca remove VERIFY output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-12-28 18:01:32 -08:00
Nikolaj Bjorner f41134d1b6 h 
- avoid more platform specific behavior when using m_mk_extract,
- rename mk_eq in bool_rewriter to mk_eq_plain to distinguish it from mk_eq_rw
- rework bv_lookahead to be more closely based on sls_engine, which has much better heuristic behavior than attempt 1.
 2024-12-28 17:40:25 -08:00
Nikolaj Bjorner a5bc5ed813 try uneven lookahead skew 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-12-28 17:40:25 -08:00
Nikolaj Bjorner 0b9ed925d6 try dual phase lookahead 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-12-27 13:34:48 -08:00
Nikolaj Bjorner 1f55ec5cef fix random update to a legal one 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-12-27 13:01:47 -08:00
Nikolaj Bjorner c82518ca36 include cmath to define std::pow 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-12-27 12:29:44 -08:00
Nikolaj Bjorner b0eee16109 fix double override bug in bv_lookahead, integrate with bv_eval 2024-12-27 12:26:18 -08:00
Clemens Eisenhofer 8de0005ab3
Bugfix seq-eq sls (#7495) 
* Fixed spurious counterexamples in seq-sls. Updates might not be identity mapping

* Removed debug code

* One check was missing
 2024-12-27 08:40:34 -08:00
Nikolaj Bjorner 5eb71c3be6 integrate lookahead v1 into repair loop 
this ports some functionality from lookahead solver for qfbv-sls into sls-smt.
 2024-12-26 17:49:30 -08:00
Nikolaj Bjorner c58171478f remove dead code 2024-12-26 13:48:55 -08:00
Nikolaj Bjorner d3a6521185 rely on is_sat fallback for failed repair-up, add separate file for WIP on lookahead. 2024-12-26 13:06:28 -08:00
Nikolaj Bjorner 13dcfd26dd remove debug out 2024-12-25 15:23:47 -08:00
Nikolaj Bjorner c9cae77304 update regex membership to be slightly better tuned 2024-12-25 10:56:16 -08:00
Nikolaj Bjorner f4ed432244 try a basic heuristic that finds some string that belongs to re. 2024-12-25 10:10:59 -08:00
Nikolaj Bjorner e332904fb2 cosmetic updates 2024-12-23 18:49:38 -08:00
Nikolaj Bjorner 85d3041a80 avoid platform non-reproducibility due to argument evaluation ordering 2024-12-23 17:13:51 -08:00
Nikolaj Bjorner 23c4728d68 remove some platform specific behavior 2024-12-23 16:28:10 -08:00
Nikolaj Bjorner 4f4cafbc98 start update with expr-inverter to handle PB 2024-12-22 18:17:42 -08:00
Nikolaj Bjorner b592ce4707 reserve space in heap to avoid debug check in elim_unconstrained 2024-12-22 18:17:40 -08:00
Nikolaj Bjorner a214dc32e8 add some comments, fix nyis 2024-12-22 13:52:19 +01:00
Nikolaj Bjorner 3b2315d771 remove verbose output 2024-12-21 15:52:57 +01:00
Nikolaj Bjorner 578804acf4 fix #7460 2024-12-21 14:42:23 +01:00
Nuno Lopes e4ab2944fe
Optimize expr_safe_replace for quantifiers when all source patterns are vars (#7481) 
* Update expr_safe_replace.cpp

* Update expr_safe_replace.cpp

* Update expr_safe_replace.cpp
 2024-12-19 23:05:13 +01:00
Nuno Lopes c33bc2c8be expr_abstract: save 1 hashtable lookup per app argument 
when we already know that the app is missing one arg to rewrite
 2024-12-18 09:50:50 +00:00
Nuno Lopes 2f5c0a6985 remove 2 unneeded lambda captures 2024-12-17 16:02:24 +00:00
Nuno Lopes 6f24123f0c reduce hash table lookups in expr_abstract in half 2024-12-16 11:00:55 +00:00
Nikolaj Bjorner b529a58b91 add unit test for incremental equation edit distance with repair 2024-12-15 05:53:28 -08:00
Nikolaj Bjorner 31ee56c1ca wip - incremental edit distance algorithm 2024-12-13 09:30:49 -08:00
Nikolaj Bjorner 538f74d64c extract stats with finalize for parallel mode 2024-12-13 09:30:49 -08:00
Nikolaj Bjorner 1e5c59a06f add repair step for str.replace 2024-12-12 09:15:36 -08:00
Nikolaj Bjorner e8c2360043 fix #7461 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-12-09 16:57:17 -08:00
Nikolaj Bjorner 8f5658b77d add another baseline heuristic for string equalities, add cases for array axioms. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-12-09 15:55:19 -08:00
Nikolaj Bjorner 4fbf54afd0 fixes to regex membership and edit updates 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-12-06 09:50:30 -08:00
Nikolaj Bjorner bcb61ee12c v0 of edit distance repair 2024-12-05 14:14:27 -08:00
Nikolaj Bjorner a17d4e68eb bugfix to elim_uncnstr to ensure nodes are created. Prepare smt_internalizer to replay unit literals 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-12-04 15:32:15 -08:00
Nikolaj Bjorner aec867586a updates to equality solving search 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-12-02 13:41:18 -08:00
Nikolaj Bjorner e6feb8423a sls: fix bug where unsat remains empty after a literal is flipped. The new satisfiable subset should be checked 
refined interface between solvers to expose fixed variables for tabu objectives
 2024-12-01 18:35:56 -08:00
Nikolaj Bjorner 24c3cd38d1 add v0 of equality solver 2024-11-30 17:25:49 -08:00
Nikolaj Bjorner b7b611d84b inherit from std::exception 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-11-27 10:26:34 -08:00
Nikolaj Bjorner 1e62029413 use ztring 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-11-25 17:36:42 -08:00
Nikolaj Bjorner fce377e1d7 add basic regex functions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-11-25 17:34:49 -08:00