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

18822 commits

This branch
This branch
All branches
Author SHA1 Message Date
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 323003aed9 Add .env to gitignore to prevent environment files from being tracked 2024-08-29 15:28:54 -07:00
Nikolaj Bjorner e31881ba30 peli 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-29 15:25:35 -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 ace3472a96 add smt params to path 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-25 18:49:57 -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
Nikolaj Bjorner a2b8b724b2 fixes to semantics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-23 09:20:11 -07:00
Nikolaj Bjorner 3884fc7b11 add factoring 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-23 05:05:10 -07:00
Nikolaj Bjorner cfc4448be4 update sls_test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-21 22:32:58 -07:00