mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity
18828 commits 49 branches 53 tags 182 MiB
Commit graph

3220 commits

Author SHA1 Message Date
Nikolaj Bjorner
a8486d6019 Refactor alignment of member variables in bv_plugin of sls namespace 2024-09-02 16:36:58 -07:00
Nikolaj Bjorner
8319832d20 Remove bv_sls_eval.cpp as part of code cleanup and refactoring 2024-09-01 16:54:28 -07:00
Nikolaj Bjorner
027dd9cfd8 Add initial implementation of bit-vector SLS evaluation module in bv_sls_eval.cpp 2024-09-01 16:53:44 -07:00
Nikolaj Bjorner
27e3d28cfc fixing conca 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-09-01 16:34:35 -07:00
Nikolaj Bjorner
39eaf62040 Remove typename from member declarations in bv_fixed class 2024-08-31 17:40:49 -07:00
Nikolaj Bjorner
6b66e81897 Refactor bv_sls files to sls_bv with namespace and class name adjustments 2024-08-30 17:41:50 -07:00
Nikolaj Bjorner
27702ba09c Rename source files for consistency in src/ast/sls directory 2024-08-30 17:35:39 -07:00
Nikolaj Bjorner
d0da02695c Remove verbose logging in register_term function of sls_basic_plugin and fix formatting in sls_context 2024-08-30 11:58:50 -07:00
Nikolaj Bjorner
7be2c3ae1e Enhance bv_sls_eval with improved repair and logging, refine is_bv_predicate in sls_bv_plugin 2024-08-30 11:50:12 -07:00
Nikolaj Bjorner
dba9670411 Remove m_num_pelis member from stats struct in sls_context 2024-08-29 17:15:28 -07:00
Nikolaj Bjorner
6312ab2184 Add m_num_pelis counter to stats in sls_context 2024-08-29 15:29:42 -07:00
Nikolaj Bjorner
5f9eb8917b gcm 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-29 15:10:35 -07:00
Nikolaj Bjorner
43a5b3dde0 logging and fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-28 15:45:29 -07:00
Nikolaj Bjorner
677b5b4196 fixes to handling signed operators 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-27 14:00:26 -07:00
Nikolaj Bjorner
b1f7965697 fix mul inverse 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-27 13:40:09 -07:00
Nikolaj Bjorner
ed0ffc1b49 fixes to mul 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-27 11:58:18 -07:00
Nikolaj Bjorner
4146e938e8 na 2024-08-27 11:45:27 -07:00
Nikolaj Bjorner
3bcd98b653 include bounds checks in set random 2024-08-27 10:59:27 -07:00
Nikolaj Bjorner
7699ce56db fixing repair 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-27 10:39:15 -07:00
Nikolaj Bjorner
6b0a10637c reserve for multiplication 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-27 10:06:10 -07:00
Nikolaj Bjorner
a0ae5c8d5e fixup repairs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-27 04:30:18 -07:00
Nikolaj Bjorner
6488e33915 fixes to fixed 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-26 18:42:32 -07:00
Nikolaj Bjorner
9fcddc5774 fixes to bv 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-26 17:51:14 -07:00
Nikolaj Bjorner
eb555ee0a7 use std::pow 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-26 10:32:42 -07:00
Nikolaj Bjorner
e3b92fec82 use exponential decay with breaks 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-26 10:21:46 -07:00
Nikolaj Bjorner
62a8512401 use reward as proxy for score 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-26 09:49:53 -07:00
Nikolaj Bjorner
2549a2cf07 use reward as proxy for score 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-26 09:30:38 -07:00
Nikolaj Bjorner
cd92b38697 avoid negative reward 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-26 09:21:38 -07:00
Nikolaj Bjorner
8a49002f60 reorg monomials 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-25 18:33:01 -07:00
Nikolaj Bjorner
fa6091dc16 remove coefficient from multiplication definition 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-25 15:23:59 -07:00
Nikolaj Bjorner
2bcb56fb13 disable non-tabu version of find_nl_moves 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-25 13:00:08 -07:00
Nikolaj Bjorner
df980acd67 use unit coefficients for muls 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-25 12:59:22 -07:00
Nikolaj Bjorner
0df6fe65f7 enable multiplier expansion, enable linear move 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 18:31:59 -07:00
Nikolaj Bjorner
803fd2a10f remove linear opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 18:31:02 -07:00
Nikolaj Bjorner
7f02ee4263 separate linear update remove 20% threshold 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 18:14:31 -07:00
Nikolaj Bjorner
ab66239c11 separate linear update 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 18:13:16 -07:00
Nikolaj Bjorner
ebbcfafd81 include 5% reset probability 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 17:58:49 -07:00
Nikolaj Bjorner
32c3a5af67 include linear moves 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 17:56:34 -07:00
Nikolaj Bjorner
d6b89ba2d5 make reset updates recursive 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 14:16:34 -07:00
Nikolaj Bjorner
47b793a5e0 disable nested mul, use non-lookahead 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 13:55:43 -07:00
Nikolaj Bjorner
059ccd67bb disable nested mul 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 13:27:09 -07:00
Nikolaj Bjorner
c643672e9f perform lookahead update + nested mul 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 13:25:48 -07:00
Nikolaj Bjorner
29aca5b1d6 flatten products 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 13:00:50 -07:00
Nikolaj Bjorner
87d556d37d delay factoring 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 10:57:35 -07:00
Nikolaj Bjorner
67d3f3b110 localize impact of factoring 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 10:14:59 -07:00
Nikolaj Bjorner
3c92119b1a disable tabu in fallback modes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 09:55:43 -07:00
Nikolaj Bjorner
11ed99089b remove restart 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 09:32:04 -07:00
Nikolaj Bjorner
b2bc51e9ac fix bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-23 16:44:44 -07:00
Nikolaj Bjorner
0b8177c7d6 generalize factoring 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-23 16:23:37 -07:00
Nikolaj Bjorner
69dd247cfc re-add tabu override 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-23 09:25:34 -07:00