mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 03:02:29 +00:00
Code Activity
19813 commits 49 branches 53 tags 180 MiB
Commit graph

3430 commits

Author SHA1 Message Date
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
Nikolaj Bjorner
b143a954c5 add notes and additional functions to sls-seq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-11-25 13:46:16 -08:00
Nikolaj Bjorner
aed3279d7d add missing new_value_eh when repaired up 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-11-24 19:57:40 -08:00
Nikolaj Bjorner
1e839e5ac2 add missing new_value_eh when repaired up 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-11-24 19:42:13 -08:00
Nikolaj Bjorner
7ed185aa9e add comments 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-11-24 19:09:50 -08:00
Nikolaj Bjorner
4559b23caf add local search functionality to sls_seq_plugin 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-11-24 11:24:17 -08:00
Nikolaj Bjorner
b4e768cfb0 adding plugin for local search strings 2024-11-22 13:56:03 -08:00
Nikolaj Bjorner
4b72e517b7 SLS: log clause , allow more frequent export of SLS state to SMT 2024-11-17 20:13:02 -08:00
Nikolaj Bjorner
84447b7031 remove incremental mode from EUF, include statistics about restart vs propagation calls to sls 2024-11-17 16:58:18 -08:00
Nikolaj Bjorner
c7ea4964f2 bug fixes to sls 2024-11-17 13:07:38 -08:00
Nikolaj Bjorner
2310514e02 fix #7454 2024-11-16 18:20:06 -08:00
Nikolaj Bjorner
5fd1231ec0 incorporate ls during propagation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-11-16 15:28:28 -08:00
Nikolaj Bjorner
f64d077d2a fix re-entrancy bug during flip in arith_base 2024-11-16 12:29:03 -08:00
Nikolaj Bjorner
197951cad4 fixes to sls 2024-11-16 08:28:24 -08:00