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

18804 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Nikolaj Bjorner
80e7f6d355 disable tabu when using reset moves 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-21 22:28:50 -07:00
Nikolaj Bjorner
42289c2f44 disable fail restart 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-21 19:51:09 -07:00
Nikolaj Bjorner
988a46dbc4 fix division by 0 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-21 17:32:58 -07:00
Nikolaj Bjorner
f6dd6a38cd update 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-20 11:51:52 -07:00
Nikolaj Bjorner
8b281b625e updates 2024-08-19 16:04:28 -07:00
Nikolaj Bjorner
de8faa231f fixes to ite and other 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-16 16:48:12 -07:00
Nikolaj Bjorner
98f4b5103e refactor basic plugin and clause generation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-15 14:04:03 -07:00
Nikolaj Bjorner
438389771d fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-14 16:20:24 -07:00
Nikolaj Bjorner
7d765ddb6b fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-14 15:55:30 -07:00
Nikolaj Bjorner
4978f5a9ac fixes 2024-08-13 21:38:38 -07:00
Nikolaj Bjorner
74c6eafde4 Update sls_test.cpp 2024-08-13 15:20:44 -07:00
Nikolaj Bjorner
afef727b88 bug fixes 2024-08-13 14:50:17 -07:00
Nikolaj Bjorner
920c207a27 fix typo 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-12 19:23:11 -07:00
Nikolaj Bjorner
849385c6a1 bugfixes in sls-arith 2024-08-12 17:42:52 -07:00
Nikolaj Bjorner
8dac67d713 evolve sls arith 2024-08-06 15:07:29 -07:00
Nikolaj Bjorner
fce21981c6 fixes to sls 2024-07-27 03:29:54 +02:00
Nikolaj Bjorner
5e62984178 updates to repair logic, mainly arithmetic 2024-07-21 21:03:14 -07:00
Nikolaj Bjorner
5b0d49cd76 testing / debugging arithmetic 2024-07-19 11:31:43 -07:00