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

1431 commits

Author SHA1 Message Date
Nuno Lopes
7ce88d4da9 fix a few compilation warnings 
- remove unused variables and class fields
 - add support for gcc 4.5 & clang's __builtin_unreachable
 - fix 2 bugs related to strict aliasing
 - remove a few unused function parameters

Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
 2013-04-21 14:36:39 -07:00
Leonardo de Moura
f6f59ad6bc Fix memory allocation problems in RCF module 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-04-10 19:03:25 -07:00
Leonardo de Moura
3ae01cf619 Fix cygwin (with python 2.6) compilation problems. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-28 17:29:55 -08:00
Leonardo de Moura
4624919786 Improve html pretty printer for RCF package 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-27 11:24:23 -08:00
Leonardo de Moura
77f58269ed Add html pretty printing mode for RCF package 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-27 10:19:54 -08:00
Leonardo de Moura
5d938a5fe2 Fix bug 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-20 18:41:24 -08:00
Leonardo de Moura
3344151aca Replace # with x in the definition of algebraic elements 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-20 18:21:09 -08:00
Leonardo de Moura
bb386c0f18 Fix problem in inv_rf 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-16 11:19:11 -08:00
Leonardo de Moura
eea3384106 Add lazy normalization for algebraic extension values. Increase default max_precision to 128. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-15 16:35:36 -08:00
Leonardo de Moura
217c8375ce Add new rational function normalization procedure. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-15 14:34:34 -08:00
Leonardo de Moura
f0737bdf7f Replace expensive_eval_sign_at with version that does not generate rational numbers 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-14 18:30:36 -08:00
Leonardo de Moura
799fe073db Add API for extracting numerator/denominator of RCF numerals. Add field to store the original isolating interval before refinement. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-14 18:29:08 -08:00
Leonardo de Moura
991a1528cd Cache isolating interval for better pretty printing 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-14 12:17:15 -08:00
Leonardo de Moura
025cb2a2a8 Avoid wasteful memory allocation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-14 12:03:22 -08:00
Leonardo de Moura
38e0b4a20a Fix bug. Add is_denominator_one macro. 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-14 11:55:52 -08:00
Leonardo de Moura
742f2b07dd Add support for compact string representation in the RCF API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-14 11:08:32 -08:00
Leonardo de Moura
6c35e08e43 Make sure we do not use denominators != 1 when encoding values of algebraic extensions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-14 10:43:18 -08:00
Leonardo de Moura
7312f49f88 Fix Visual Studio warnings 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-13 09:06:07 -08:00
Leonardo de Moura
f747bde548 Add restore_interval for extensions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-12 21:59:41 -08:00
Leonardo de Moura
be2bf861c7 Use clean_denominators before root isolation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-12 20:43:17 -08:00
Leonardo de Moura
2b5883454c Add support for prem_gcd in square_free 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-12 19:49:50 -08:00
Leonardo de Moura
551d0b7de0 Fix bug in sprem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-12 19:44:05 -08:00
Leonardo de Moura
7711146d23 Add prem_gcd based on pseudo-remainder 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-12 19:36:07 -08:00
Leonardo de Moura
13d5c3e07a Add normalize_int_coeffs to control the coefficient growth in Sturm sequences 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-12 18:01:29 -08:00
Leonardo de Moura
e6102a8260 Move clean_denominators code to the top 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-12 17:11:42 -08:00
Leonardo de Moura
1e362e6fec Add comments to mark sections 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-12 17:08:58 -08:00
Leonardo de Moura
a9fa232f11 Fix bug in compare 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-12 16:45:24 -08:00
Leonardo de Moura
ea9421bb38 Expose rcf module parameters 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-12 16:40:45 -08:00
Leonardo de Moura
e6a35c6241 Add prem to avoid rational function values 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-12 16:27:56 -08:00
Leonardo de Moura
09d3686d58 Fix memory leak in realclosure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-12 15:54:07 -08:00
Leonardo de Moura
1d761ea9a5 Add clean_denominators procedure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-12 15:45:43 -08:00
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
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
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
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
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
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