mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity
19979 commits 49 branches 53 tags 182 MiB
Commit graph

19979 commits

This branch
This branch
All branches
Author SHA1 Message Date
Lev Nachmanson
15a3818fce cleanup in dioph_eq.cpp 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-13 14:57:21 -07:00
Nikolaj Bjorner
1109139359 move to readme-cmake 2025-05-13 14:36:20 -07:00
Nikolaj Bjorner
ce1535119d include some build cheat sheet 2025-05-13 14:34:47 -07:00
Nikolaj Bjorner
a5a2a13d34 update version number 2025-05-13 14:32:35 -07:00
Nikolaj Bjorner
0d3c29a250 handle larger buffers 2025-05-13 14:11:59 -07:00
Lev Nachmanson
6b32aaed10 remove slack heuristic 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-12 14:02:17 -07:00
Lev Nachmanson
a5e5d4dbd3 testing 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-12 14:02:17 -07:00
Lev Nachmanson
bbaec0bf95 trying randomly shuffle the indices in the slack utilization 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-12 14:02:17 -07:00
Lev Nachmanson
52241b6474 some refactoring of lar_solver.h 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-12 14:02:17 -07:00
Lev Nachmanson
fef954c028 shring lar_solver.h 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-12 14:02:17 -07:00
Lev Nachmanson
4abd9843a0 fix the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-12 14:02:17 -07:00
Lev Nachmanson
e3f5e8c8a6 restore lar_solver::add_named_var 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-12 14:02:17 -07:00
Lev Nachmanson
b375faa77c continue PIMPL refactor in lar_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-12 14:02:17 -07:00
Lev Nachmanson
b7ffcb7e61 implement imp of lar_solver as lar_solver::imp 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-12 14:02:17 -07:00
Lev Nachmanson
39955f1d04 remove a function from lar_solver 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-12 14:02:17 -07:00
Lev Nachmanson
4e56834b76 test 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-12 14:02:17 -07:00
Lev Nachmanson
a527667fc0 shuffle more functionality from lar_solver.h to lar_solver::imp 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-12 14:02:17 -07:00
Lev Nachmanson
c81eb74c93 apply the slack idea in a loop 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-12 14:02:17 -07:00
Lev Nachmanson
e041fe95bc slack 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-05-12 14:02:17 -07:00
Nikolaj Bjorner
7ca94e8fef add E-matching to EUF completion 2025-05-10 16:15:04 -07:00
Nikolaj Bjorner
9232ef579c remove copy of LICENSE.txt - pypi doesn't take it 2025-05-09 16:53:45 -07:00
Nikolaj Bjorner
49dffaed39 enable pypi 2025-05-09 15:37:19 -07:00
Nikolaj Bjorner
b54ed38cea enable pypi 2025-05-09 13:15:42 -07:00
Nikolaj Bjorner
59a7e007a4 disable pypi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-05-09 08:26:38 -07:00
Nikolaj Bjorner
d4b622e239 update version number 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-05-09 08:25:40 -07:00
Nikolaj Bjorner
a51239c641 update namespace, hoist exported functions outside of embedded namespace 2025-05-07 15:57:47 -07:00
Nikolaj Bjorner
644118660f list euf dependency in api cmakefile 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-05-07 15:47:03 -07:00
Nikolaj Bjorner
eca5cd1841 mark virtual methods as override 2025-05-07 15:24:20 -07:00
Nikolaj Bjorner
9a299eb9ff move mam to euf 2025-05-07 14:38:59 -07:00
Nikolaj Bjorner
0e4c033e30 fix #7639 2025-05-03 11:06:25 -07:00
Nikolaj Bjorner
4bedb5f8fc fix #7638 2025-05-03 11:04:41 -07:00
Nikolaj Bjorner
dd211bade9 filter out terms that are not solved 2025-04-30 09:40:45 -07:00
Lev Nachmanson
f89e133d52
revert the behavior of add_zero_assumption (#7631) 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2025-04-28 16:07:46 -07:00
Nikolaj Bjorner
6af61fa0f4 remove experiment 2025-04-28 10:00:02 -07:00
Nikolaj Bjorner
b502126ebc fix #7634 2025-04-27 23:57:57 -07:00
Nikolaj Bjorner
24090fc48c move flush smc to first use 2025-04-27 11:44:45 -07:00
Nikolaj Bjorner
a626cd0fed flush smc before use in model construction 2025-04-27 11:18:18 -07:00
Nikolaj Bjorner
71b5e44058 #7596 - flush smc before copy 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-04-27 10:36:27 -07:00
Nikolaj Bjorner
7a302239c2 fix #7630 2025-04-26 11:40:48 -07:00
Nikolaj Bjorner
d581dc1db4 #7630 propagate parameters on lazy tactics 2025-04-26 11:22:16 -07:00
Nuno Lopes
322e4441b3 Fix conversion of signed 1-bit BV to FP 
Fixes https://github.com/AliveToolkit/alive2/issues/1193
 2025-04-25 12:38:00 +01:00
Nikolaj Bjorner
792ffeeda7 fix latent sign bug 2025-04-23 17:22:57 -07:00
Nikolaj Bjorner
fe1fff3b7e add scaffolding for experiments with slack 2025-04-23 17:07:50 -07:00
Nikolaj Bjorner
12ccf59ab9 rename fields to compile on c++ platforms 2025-04-23 17:06:15 -07:00
Nikolaj Bjorner
e41acd7b50 convert m_r_upper and m_r_lower bounds to plain vectors 
manage backtracking state together with backtracking of column data.
 2025-04-23 16:33:38 -07:00
Nikolaj Bjorner
fae60946bf consolidate some bounds references 2025-04-23 15:45:44 -07:00
Nikolaj Bjorner
f6fbeda9d7 fix #7629 2025-04-23 15:22:44 -07:00
Nikolaj Bjorner
7641393f8a use inlined functions 2025-04-23 14:28:31 -07:00
Nikolaj Bjorner
5cc57b8958 coalesce updates to bounds 2025-04-23 14:05:17 -07:00
Nikolaj Bjorner
579ba8bd70 add power axioms to arith_solver 2025-04-23 10:48:29 -07:00