mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity
873 commits 23 branches 48 tags 156 MiB
Commit graph

873 commits

This branch
This branch
All branches
Author SHA1 Message Date
Leonardo de Moura 349c21d4de Add configure script that is just a wrapper for python 'src/mk_make.py'. It makes the build more user friendly for users familiar with ./configure + make idiom 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-01-13 11:34:05 -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 93f37bdf9f Merge branch 'realclosure' into unstable 2013-01-12 22:03:40 -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 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
Christoph M. Wintersteiger 61b686f86f FPA: fixes for sbits < ebits 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-01-11 11:15:18 +00: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
Christoph M. Wintersteiger dd127c2f71 Java API: bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-01-10 18:16:29 +00:00
Christoph M. Wintersteiger 3482b8f4f1 .NET API: bugfix 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
 2013-01-10 18:08:56 +00: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