mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity
842 commits 23 branches 48 tags 157 MiB
Commit graph

842 commits

This branch
This branch
All branches
Author SHA1 Message Date
Leonardo de Moura d60f2db116 Remove select method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-12 09:46:00 -08:00
Leonardo de Moura a03a6e9bf6 Add more tracing 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-11 21:12:51 -08:00
Leonardo de Moura ef11ef61b5 Clean m_val field when switching to GMP bignum 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-11 17:55:52 -08:00
Leonardo de Moura 5ce70eb521 Fix bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-11 17:55:03 -08:00
Leonardo de Moura 3cc072f3a7 Add bisect_isolate_roots 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-11 16:28:39 -08:00
Leonardo de Moura f70de8dd47 Fix support for gmp 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-11 16:28:19 -08:00
Leonardo de Moura 5a9040a247 Replace is_real with depends_on_infinitesimals to avoid misunderstandings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-11 10:35:38 -08:00
Leonardo de Moura 0de6b4cc92 Complete the implementation of expensive_algebraic_poly_interval 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-11 10:11:03 -08:00
Leonardo de Moura 714167a378 Add more tracing 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-10 18:36:47 -08:00
Leonardo de Moura 2f5c7c9ba9 Add determine_algebraic_sign 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-10 17:07:32 -08:00
Leonardo de Moura 619e597174 Add normalize_algebraic 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-10 13:38:51 -08:00
Leonardo de Moura 4cd2998743 Add power operator to C and Python RCF APIs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-10 13:05:47 -08:00
Leonardo de Moura 191e503418 Fix bug. Improve nl_nz_sqf_isolate_roots 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-10 12:51:54 -08:00
Leonardo de Moura 71ab7759d1 Add root method (syntax sugar for isolate_roots) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-10 12:23:37 -08:00
Leonardo de Moura 1a7d39f9a0 Add refine_algebraic_interval 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-10 12:09:07 -08:00
Leonardo de Moura 4a0b431cf4 Add mk_algebraic method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-10 11:13:21 -08:00
Leonardo de Moura 872165fa55 Add more tracing to sign_det_isolate_roots 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-10 09:17:22 -08:00
Leonardo de Moura eca78aa9c6 Fix incorrect assertions and bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-10 08:52:25 -08:00
Leonardo de Moura 191de6f7b5 Fix test program 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-10 08:01:42 -08:00
Leonardo de Moura d644b37ac1 Add non naive sign determination algorithm 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-09 22:35:39 -08:00
Leonardo de Moura 1712f0a33b Add goodies 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-09 18:43:32 -08:00
Leonardo de Moura 81807c7001 Add procedure for computing TaQ(Q, P; a, b) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-09 13:37:10 -08:00
Leonardo de Moura b662bc8dc7 Add lower and upper bounds for negative and positive roots 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-09 11:16:04 -08:00
Leonardo de Moura 9c8b428ffb Add matrix operations needed for implementing non-naive sign determination 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-08 17:58:34 -08:00
Leonardo de Moura ff809db16d Add get_int and get_uint to mpz_manager 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-08 15:40:19 -08:00
Leonardo de Moura e01a7b6268 Fix memory management bugs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-07 17:31:53 -08:00
Leonardo de Moura 5873a59769 Add root upper bounds estimation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-07 16:23:30 -08:00
Leonardo de Moura 4ea06b8040 Fix Z3_enable_trace API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-07 16:22:47 -08:00
Leonardo de Moura 56db84a0e5 Fix RCF API logging bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-07 15:10:16 -08:00
Leonardo de Moura 09b5724d82 Simplify RCF C API. Add Z3_rcf_mk_roots (C API) and MkRoots (Python API). Implement basic root isolation support. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-07 12:25:28 -08:00
Leonardo de Moura 3c1f1a3b65 Fix bug in realclosure::compare function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-06 21:50:36 -08:00
Leonardo de Moura 3e19df0441 Fix API logging bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-06 21:25:46 -08:00
Leonardo de Moura 4d578b418f Fix bug in approx_div 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-06 21:15:37 -08:00
Leonardo de Moura 1c8101419b Add Python API for RCF module 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-06 20:59:00 -08:00
Leonardo de Moura 9fbbdb56e4 Implement RCF external C API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-06 20:06:27 -08:00
Leonardo de Moura f1d47f35b2 Add refine interval infrastructure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-06 18:30:41 -08:00
Leonardo de Moura c01f27fe13 Add small interval caching infrastructure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-06 10:46:38 -08:00
Leonardo de Moura 47c6a73e19 Add RCF external API skeletons 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-05 22:24:56 -08:00
Leonardo de Moura ecb58091f7 Add support for transcendental values such as pi and e, and the power operator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-05 21:26:12 -08:00
Leonardo de Moura ae1da72cb7 Implement compare 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-05 20:21:49 -08:00
Leonardo de Moura 3ffda25350 Implement add, sub, mul, div, inv, neg 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-05 18:43:57 -08:00
Leonardo de Moura 322d355290 Simplify data-structures 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-05 11:51:58 -08:00
Leonardo de Moura 14827e94f0 Fix typos and bugs. Add tests. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-04 15:01:27 -08:00
Leonardo de Moura ff62948d90 Add div and inv for binary rational intervals 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-04 12:31:28 -08:00
Leonardo de Moura 0203fa56d2 Add tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-04 08:11:33 -08:00
Leonardo de Moura 9ede98a029 Fix bugs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-04 08:09:20 -08:00
Leonardo de Moura 15ed819fbd Implement mk_transcendental. Replace extension_ref with extension *. Remove m_to_delete 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-03 22:09:43 -08:00
Leonardo de Moura 1ed275b801 Fix typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-03 22:08:32 -08:00
Leonardo de Moura 6160b2891b Change representation for values in the module for encoding infinitesimals, algebraic extensions and transcendal extensions. Implement basic polynomial operations for polynomials in this field 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-03 17:47:23 -08:00
Leonardo de Moura ed5b106574 Add support for ref_buffers with different initial sizes. Add shrink and operator= methods. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-03 17:45:28 -08:00