mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-26 15:53:41 +00:00
Code Activity
19676 commits 29 branches 51 tags 167 MiB
Commit graph

19676 commits

This branch
This branch
All branches
Author SHA1 Message Date
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
Nikolaj Bjorner
d73d104ded remove overwriting x,y,rval 2025-04-23 09:17:22 -07:00
Nikolaj Bjorner
ff920ba51b handle root expressions, and checking exponentiation with nlsat 
this one is for you @matthai
 2025-04-22 13:47:47 -07:00
Carson Radtke
2fe2735b5e
Replace _DEBUG with Z3DEBUG (#7628) 
Fixes https://github.com/Z3Prover/z3/issues/7627
 2025-04-22 13:39:01 -07:00